Adding timeout for Alloy interpreter
authorHamed Gorjiara <hgorjiar@uci.edu>
Mon, 11 Feb 2019 22:25:27 +0000 (14:25 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Mon, 11 Feb 2019 22:25:27 +0000 (14:25 -0800)
src/AlloyEnc/alloyenc.cc
src/AlloyEnc/alloyenc.h
src/csolver.h

index 6a8dcdf..cad0529 100644 (file)
@@ -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
index 97049e2..3edfdbf 100644 (file)
@@ -19,6 +19,7 @@ public:
 private:
        void dumpAlloyFooter();
        void dumpAlloyHeader();
+       inline uint getTimeout();
        string encodeConstraint(BooleanEdge constraint);
        int getResult();
        string encodeBooleanLogic( BooleanLogic *bl);
index 74d0bf6..6fea9ee 100644 (file)
@@ -171,6 +171,7 @@ public:
        long long getElapsedTime() { return elapsedTime; }
        long long getEncodeTime();
        long long getSolveTime();
+       long getSatSolverTimeout() { return satsolverTimeout;}
 
        CMEMALLOC;