5 files changed, 22 insertions, 8 deletions

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
index ae94c327..f8d3e3bd 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
@@ -21,7 +21,7 @@ class ExpressionEvaluation2Logic {
         def getNumericSolver() {

                 if(_numericSolver === null) {

                         // it seems like this getter has no use

-                        _numericSolver = (new NumericTranslator(null)).selectProblemSolver("z3")

+                        _numericSolver = (new NumericTranslator(null, 0)).selectProblemSolver("z3")

                 }

                 return _numericSolver

         }

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
index eb63d96a..cecd3623 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
@@ -44,7 +44,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
         

         private final int TIMEOUT_DOCKER = 5000;

         private int TIMEOUT_LOCAL = -1;

-        private final int DEBUG_PRINT = 2;

+        private final int DEBUG_PRINT = 0;

 

         public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath, int drealTimeout) throws IOException, InterruptedException {

                 this.useDocker = useDocker;

@@ -72,6 +72,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
         private Process runProcess(List<String> cmd, int timeout) throws IOException, InterruptedException {

 //              String s = String.join(" ", cmd);

 //              Process p = Runtime.getRuntime().exec(s);

+                Runtime.getRuntime().exec("killall -9 dreal").waitFor();

                 Process p = (new ProcessBuilder(cmd)).start();

 //              p.waitFor();

                 //TODO timeout if needed

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
index 1e5c1f29..e8c20138 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
@@ -13,16 +13,18 @@ public class NumericDynamicProblemSolver extends NumericProblemSolver{
         
 //      private NumericZ3ProblemSolver z3Solver;
         private NumericDrealProblemSolver drealSolver;
+        private int timeout;
         
         public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException {
 //              this.z3Solver = new NumericZ3ProblemSolver();
                 this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout);
+                this.timeout = drealTimeout;
         }
         
         public NumericProblemSolver selectSolver(String selection) {
                 switch (selection) {
                 case "z3":
-                        return new NumericZ3ProblemSolver();
+                        return new NumericZ3ProblemSolver(timeout);
                 case "dreal":
                         return this.drealSolver;
                 default:
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
index 791dd644..a11ae8a8 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend
@@ -17,6 +17,7 @@ class NumericTranslator {
         

         private XExpressionExtractor extractor = new XExpressionExtractor();

         private NumericProblemSolver numericSolver;

+        private int timeout;

         

         long formingProblemTime=0;

         long solvingProblemTime=0;

@@ -29,8 +30,9 @@ class NumericTranslator {
                         }

                 }

                 

-        new(NumericProblemSolver numericProblemSolver){

+        new(NumericProblemSolver numericProblemSolver, int timeout){

                 this.numericSolver = numericProblemSolver

+                this.timeout = timeout;

         }

         

         def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) {

@@ -63,7 +65,7 @@ class NumericTranslator {
                         val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver

                         return dynamicSolver.selectSolver(selection);

                 } else{

-                        if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver
+                        if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver(this.timeout)
                         return numericSolver;

                 }
         }

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
index 612e93a6..0799953f 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
@@ -1,6 +1,5 @@
 package hu.bme.mit.inf.dslreasoner.viatra2logic;

 

-import java.io.File;

 import java.util.ArrayList;

 import java.util.HashMap;

 import java.util.List;

@@ -20,6 +19,7 @@ import com.microsoft.z3.Context;
 import com.microsoft.z3.Expr;

 import com.microsoft.z3.IntExpr;

 import com.microsoft.z3.Model;

+import com.microsoft.z3.Params;

 import com.microsoft.z3.RealExpr;

 import com.microsoft.z3.Solver;

 import com.microsoft.z3.Status;

@@ -36,7 +36,7 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
         private Solver s;

         private Map<Object, Expr> varMap;

 

-        public NumericZ3ProblemSolver() {

+        public NumericZ3ProblemSolver(int timeout) {

                 //FOR LINUX VM

                 //Not Elegant, but this is working for now

 //              String root = "/home/models/VIATRA-Generator";

@@ -50,6 +50,11 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
                 ctx = new Context(cfg); 

                 ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL);

                 s = ctx.mkSolver();

+                if (timeout != -1) {

+                        Params p = ctx.mkParams();
+                    p.add("timeout", timeout);
+                    s.setParameters(p);

+                }

                 varMap = new HashMap<Object, Expr>();

         }

 

@@ -82,7 +87,11 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
                 s.add(problemInstance);

                 endformingProblem = System.nanoTime()-startformingProblem;

                 long startSolvingProblem = System.nanoTime();

-                boolean result = (s.check() == Status.SATISFIABLE);

+//              System.out.print("start - ");

+                Status soln = s.check();

+                boolean result = (soln == Status.SATISFIABLE);

+                if (soln == Status.UNKNOWN) System.err.println("TIMEOUT");

+//              System.out.println("end");

                 endSolvingProblem = System.nanoTime()-startSolvingProblem;

                 this.ctx.close();

                 return result;