diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf')
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 { | |||
21 | def getNumericSolver() { | 21 | def getNumericSolver() { |
22 | if(_numericSolver === null) { | 22 | if(_numericSolver === null) { |
23 | // it seems like this getter has no use | 23 | // it seems like this getter has no use |
24 | _numericSolver = (new NumericTranslator(null)).selectProblemSolver("z3") | 24 | _numericSolver = (new NumericTranslator(null, 0)).selectProblemSolver("z3") |
25 | } | 25 | } |
26 | return _numericSolver | 26 | return _numericSolver |
27 | } | 27 | } |
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{ | |||
44 | 44 | ||
45 | private final int TIMEOUT_DOCKER = 5000; | 45 | private final int TIMEOUT_DOCKER = 5000; |
46 | private int TIMEOUT_LOCAL = -1; | 46 | private int TIMEOUT_LOCAL = -1; |
47 | private final int DEBUG_PRINT = 2; | 47 | private final int DEBUG_PRINT = 0; |
48 | 48 | ||
49 | public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { | 49 | public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { |
50 | this.useDocker = useDocker; | 50 | this.useDocker = useDocker; |
@@ -72,6 +72,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
72 | private Process runProcess(List<String> cmd, int timeout) throws IOException, InterruptedException { | 72 | private Process runProcess(List<String> cmd, int timeout) throws IOException, InterruptedException { |
73 | // String s = String.join(" ", cmd); | 73 | // String s = String.join(" ", cmd); |
74 | // Process p = Runtime.getRuntime().exec(s); | 74 | // Process p = Runtime.getRuntime().exec(s); |
75 | Runtime.getRuntime().exec("killall -9 dreal").waitFor(); | ||
75 | Process p = (new ProcessBuilder(cmd)).start(); | 76 | Process p = (new ProcessBuilder(cmd)).start(); |
76 | // p.waitFor(); | 77 | // p.waitFor(); |
77 | //TODO timeout if needed | 78 | //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{ | |||
13 | 13 | ||
14 | // private NumericZ3ProblemSolver z3Solver; | 14 | // private NumericZ3ProblemSolver z3Solver; |
15 | private NumericDrealProblemSolver drealSolver; | 15 | private NumericDrealProblemSolver drealSolver; |
16 | private int timeout; | ||
16 | 17 | ||
17 | public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { | 18 | public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { |
18 | // this.z3Solver = new NumericZ3ProblemSolver(); | 19 | // this.z3Solver = new NumericZ3ProblemSolver(); |
19 | this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout); | 20 | this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout); |
21 | this.timeout = drealTimeout; | ||
20 | } | 22 | } |
21 | 23 | ||
22 | public NumericProblemSolver selectSolver(String selection) { | 24 | public NumericProblemSolver selectSolver(String selection) { |
23 | switch (selection) { | 25 | switch (selection) { |
24 | case "z3": | 26 | case "z3": |
25 | return new NumericZ3ProblemSolver(); | 27 | return new NumericZ3ProblemSolver(timeout); |
26 | case "dreal": | 28 | case "dreal": |
27 | return this.drealSolver; | 29 | return this.drealSolver; |
28 | default: | 30 | 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 { | |||
17 | 17 | ||
18 | private XExpressionExtractor extractor = new XExpressionExtractor(); | 18 | private XExpressionExtractor extractor = new XExpressionExtractor(); |
19 | private NumericProblemSolver numericSolver; | 19 | private NumericProblemSolver numericSolver; |
20 | private int timeout; | ||
20 | 21 | ||
21 | long formingProblemTime=0; | 22 | long formingProblemTime=0; |
22 | long solvingProblemTime=0; | 23 | long solvingProblemTime=0; |
@@ -29,8 +30,9 @@ class NumericTranslator { | |||
29 | } | 30 | } |
30 | } | 31 | } |
31 | 32 | ||
32 | new(NumericProblemSolver numericProblemSolver){ | 33 | new(NumericProblemSolver numericProblemSolver, int timeout){ |
33 | this.numericSolver = numericProblemSolver | 34 | this.numericSolver = numericProblemSolver |
35 | this.timeout = timeout; | ||
34 | } | 36 | } |
35 | 37 | ||
36 | def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) { | 38 | def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) { |
@@ -63,7 +65,7 @@ class NumericTranslator { | |||
63 | val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver | 65 | val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver |
64 | return dynamicSolver.selectSolver(selection); | 66 | return dynamicSolver.selectSolver(selection); |
65 | } else{ | 67 | } else{ |
66 | if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver | 68 | if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver(this.timeout) |
67 | return numericSolver; | 69 | return numericSolver; |
68 | } | 70 | } |
69 | } | 71 | } |
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | 1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; |
2 | 2 | ||
3 | import java.io.File; | ||
4 | import java.util.ArrayList; | 3 | import java.util.ArrayList; |
5 | import java.util.HashMap; | 4 | import java.util.HashMap; |
6 | import java.util.List; | 5 | import java.util.List; |
@@ -20,6 +19,7 @@ import com.microsoft.z3.Context; | |||
20 | import com.microsoft.z3.Expr; | 19 | import com.microsoft.z3.Expr; |
21 | import com.microsoft.z3.IntExpr; | 20 | import com.microsoft.z3.IntExpr; |
22 | import com.microsoft.z3.Model; | 21 | import com.microsoft.z3.Model; |
22 | import com.microsoft.z3.Params; | ||
23 | import com.microsoft.z3.RealExpr; | 23 | import com.microsoft.z3.RealExpr; |
24 | import com.microsoft.z3.Solver; | 24 | import com.microsoft.z3.Solver; |
25 | import com.microsoft.z3.Status; | 25 | import com.microsoft.z3.Status; |
@@ -36,7 +36,7 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
36 | private Solver s; | 36 | private Solver s; |
37 | private Map<Object, Expr> varMap; | 37 | private Map<Object, Expr> varMap; |
38 | 38 | ||
39 | public NumericZ3ProblemSolver() { | 39 | public NumericZ3ProblemSolver(int timeout) { |
40 | //FOR LINUX VM | 40 | //FOR LINUX VM |
41 | //Not Elegant, but this is working for now | 41 | //Not Elegant, but this is working for now |
42 | // String root = "/home/models/VIATRA-Generator"; | 42 | // String root = "/home/models/VIATRA-Generator"; |
@@ -50,6 +50,11 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
50 | ctx = new Context(cfg); | 50 | ctx = new Context(cfg); |
51 | ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); | 51 | ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); |
52 | s = ctx.mkSolver(); | 52 | s = ctx.mkSolver(); |
53 | if (timeout != -1) { | ||
54 | Params p = ctx.mkParams(); | ||
55 | p.add("timeout", timeout); | ||
56 | s.setParameters(p); | ||
57 | } | ||
53 | varMap = new HashMap<Object, Expr>(); | 58 | varMap = new HashMap<Object, Expr>(); |
54 | } | 59 | } |
55 | 60 | ||
@@ -82,7 +87,11 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
82 | s.add(problemInstance); | 87 | s.add(problemInstance); |
83 | endformingProblem = System.nanoTime()-startformingProblem; | 88 | endformingProblem = System.nanoTime()-startformingProblem; |
84 | long startSolvingProblem = System.nanoTime(); | 89 | long startSolvingProblem = System.nanoTime(); |
85 | boolean result = (s.check() == Status.SATISFIABLE); | 90 | // System.out.print("start - "); |
91 | Status soln = s.check(); | ||
92 | boolean result = (soln == Status.SATISFIABLE); | ||
93 | if (soln == Status.UNKNOWN) System.err.println("TIMEOUT"); | ||
94 | // System.out.println("end"); | ||
86 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 95 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
87 | this.ctx.close(); | 96 | this.ctx.close(); |
88 | return result; | 97 | return result; |