Adding timeout for Alloy interpreter

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
index 6a8dcdfe1a122af005f6abd8e99f87521299ddf6..cad0529553b8eea22bc009f7d5ccfc60c8ee13ea 100644 (file)
--- 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 97049e2fefdbb60e733287d5eca0a3a4f80fde32..3edfdbf926d6546f27dac6a63210233c123b2e6e 100644 (file)
--- 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 74d0bf6e2c64b9e237f7ab0e9381b6b40a3f7c63..6fea9ee7bfb888a9e564d9492efd8d7777d6d16a 100644 (file)
--- 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;