From bc403272d867f82edd623179d82c080e57154c1a Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 16 Feb 2021 09:01:25 +0100 Subject: CrossingScenario case study is ready for server --- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 2 +- .../viatra2logic/NumericDrealProblemSolver.java | 3 ++- .../viatra2logic/NumericDynamicProblemSolver.java | 4 +++- .../inf/dslreasoner/viatra2logic/NumericTranslator.xtend | 6 ++++-- .../dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | 15 ++++++++++++--- 5 files changed, 22 insertions(+), 8 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src') 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 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 arrayToMap(Object[] tuple, ArrayList 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 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(); } @@ -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; -- cgit v1.2.3-54-g00ecf