From d0d465672d8745d091999e9d5036260dbc47c8dd Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Mon, 11 Feb 2019 14:25:27 -0800
Subject: [PATCH] Adding timeout for Alloy interpreter

---
 src/AlloyEnc/alloyenc.cc | 8 +++++++-
 src/AlloyEnc/alloyenc.h  | 1 +
 src/csolver.h            | 1 +
 3 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
index 6a8dcdf..cad0529 100644
--- a/src/AlloyEnc/alloyenc.cc
+++ b/src/AlloyEnc/alloyenc.cc
@@ -9,6 +9,7 @@
 #include "signature.h"
 #include "set.h"
 #include "function.h"
+#include "inc_solver.h"
 #include <fstream>
 #include <vector>
 
@@ -98,6 +99,11 @@ void AlloyEnc::dumpAlloyFooter(){
 	output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
 }
 
+uint AlloyEnc::getTimeout(){
+	uint timeout =csolver->getSatSolverTimeout(); 
+	return timeout == (uint)NOTIMEOUT? 1000: timeout;
+}
+
 void AlloyEnc::dumpAlloyHeader(){
 	output << "open util/integer" << endl;
 }
@@ -109,7 +115,7 @@ int AlloyEnc::solve(){
 	if( output.is_open()){
 		output.close();
 	}
-	snprintf(buffer, sizeof(buffer), "./run.sh java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", alloyFileName, solutionFile);
+	snprintf(buffer, sizeof(buffer), "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), alloyFileName, solutionFile);
 	int status = system(buffer);
 	if (status == 0) {
 		//Read data in from results file
diff --git a/src/AlloyEnc/alloyenc.h b/src/AlloyEnc/alloyenc.h
index 97049e2..3edfdbf 100644
--- a/src/AlloyEnc/alloyenc.h
+++ b/src/AlloyEnc/alloyenc.h
@@ -19,6 +19,7 @@ public:
 private:
 	void dumpAlloyFooter();
 	void dumpAlloyHeader();
+	inline uint getTimeout();
 	string encodeConstraint(BooleanEdge constraint);
 	int getResult();
 	string encodeBooleanLogic( BooleanLogic *bl);
diff --git a/src/csolver.h b/src/csolver.h
index 74d0bf6..6fea9ee 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -171,6 +171,7 @@ public:
 	long long getElapsedTime() { return elapsedTime; }
 	long long getEncodeTime();
 	long long getSolveTime();
+	long getSatSolverTimeout() { return satsolverTimeout;}
 
 	CMEMALLOC;
 
-- 
2.34.1