diff options
author | OszkarSemerath <semerath@mit.bme.hu> | 2021-07-30 10:04:27 +0200 |
---|---|---|
committer | OszkarSemerath <semerath@mit.bme.hu> | 2021-07-30 10:04:27 +0200 |
commit | aaa67b0ef8840d97b062a4f1383bf93410984af3 (patch) | |
tree | 2c07208bb6b5ab27b47bd477dfbcc6e77b50d623 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | |
parent | Config updated and createSharedVersionedMapStores service (diff) | |
download | VIATRA-Generator-aaa67b0ef8840d97b062a4f1383bf93410984af3.tar.gz VIATRA-Generator-aaa67b0ef8840d97b062a4f1383bf93410984af3.tar.zst VIATRA-Generator-aaa67b0ef8840d97b062a4f1383bf93410984af3.zip |
Numeric solver dreal hardcoding -> configV4transformation
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | 60 |
1 files changed, 46 insertions, 14 deletions
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 0799953f..5b4f6de1 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 | |||
@@ -35,24 +35,18 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
35 | private Context ctx; | 35 | private Context ctx; |
36 | private Solver s; | 36 | private Solver s; |
37 | private Map<Object, Expr> varMap; | 37 | private Map<Object, Expr> varMap; |
38 | private int timeout; | ||
38 | 39 | ||
39 | public NumericZ3ProblemSolver(int timeout) { | 40 | public NumericZ3ProblemSolver(int timeout) { |
40 | //FOR LINUX VM | 41 | this.timeout=timeout; |
41 | //Not Elegant, but this is working for now | ||
42 | // String root = "/home/models/VIATRA-Generator"; | ||
43 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | ||
44 | // System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | ||
45 | // System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | ||
46 | //End non-elegance | ||
47 | |||
48 | HashMap<String, String> cfg = new HashMap<String, String>(); | 42 | HashMap<String, String> cfg = new HashMap<String, String>(); |
49 | cfg.put("model", "true"); | 43 | cfg.put("model", "true"); |
50 | ctx = new Context(cfg); | 44 | ctx = new Context(cfg); |
51 | ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); | 45 | ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); |
52 | s = ctx.mkSolver(); | 46 | s = ctx.mkSolver(); |
53 | if (timeout != -1) { | 47 | if (timeout != -1) { |
54 | Params p = ctx.mkParams(); | 48 | Params p = ctx.mkParams(); |
55 | p.add("timeout", timeout); | 49 | p.add("timeout", timeout); |
56 | s.setParameters(p); | 50 | s.setParameters(p); |
57 | } | 51 | } |
58 | varMap = new HashMap<Object, Expr>(); | 52 | varMap = new HashMap<Object, Expr>(); |
@@ -62,7 +56,7 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
62 | return ctx; | 56 | return ctx; |
63 | } | 57 | } |
64 | 58 | ||
65 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { | 59 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(final XExpression expression) { |
66 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | 60 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); |
67 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); | 61 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); |
68 | XExpression right = ((XBinaryOperation) expression).getRightOperand(); | 62 | XExpression right = ((XBinaryOperation) expression).getRightOperand(); |
@@ -80,8 +74,36 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
80 | getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); | 74 | getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); |
81 | } | 75 | } |
82 | } | 76 | } |
83 | 77 | ||
84 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 78 | @Override |
79 | protected void initialize() { | ||
80 | // TODO Auto-generated method stub | ||
81 | |||
82 | } | ||
83 | |||
84 | private void start() { | ||
85 | HashMap<String, String> cfg = new HashMap<String, String>(); | ||
86 | cfg.put("model", "true"); | ||
87 | ctx = new Context(cfg); | ||
88 | ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); | ||
89 | s = ctx.mkSolver(); | ||
90 | if (timeout != -1) { | ||
91 | Params p = ctx.mkParams(); | ||
92 | p.add("timeout", timeout); | ||
93 | s.setParameters(p); | ||
94 | } | ||
95 | varMap = new HashMap<Object, Expr>(); | ||
96 | } | ||
97 | private void stop() { | ||
98 | ctx=null; | ||
99 | s=null; | ||
100 | varMap=null; | ||
101 | } | ||
102 | |||
103 | @Override | ||
104 | protected boolean internalIsSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
105 | start(); | ||
106 | |||
85 | long startformingProblem = System.nanoTime(); | 107 | long startformingProblem = System.nanoTime(); |
86 | BoolExpr problemInstance = formNumericProblemInstance(matches); | 108 | BoolExpr problemInstance = formNumericProblemInstance(matches); |
87 | s.add(problemInstance); | 109 | s.add(problemInstance); |
@@ -94,10 +116,15 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
94 | // System.out.println("end"); | 116 | // System.out.println("end"); |
95 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 117 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
96 | this.ctx.close(); | 118 | this.ctx.close(); |
119 | |||
120 | stop(); | ||
97 | return result; | 121 | return result; |
98 | } | 122 | } |
99 | 123 | ||
100 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 124 | @Override |
125 | protected Map<PrimitiveElement,Number> internalGetOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | ||
126 | start(); | ||
127 | |||
101 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); | 128 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); |
102 | long startformingProblem = System.nanoTime(); | 129 | long startformingProblem = System.nanoTime(); |
103 | BoolExpr problemInstance = formNumericProblemInstance(matches); | 130 | BoolExpr problemInstance = formNumericProblemInstance(matches); |
@@ -147,6 +174,9 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
147 | System.out.println("Unsatisfiable numerical problem"); | 174 | System.out.println("Unsatisfiable numerical problem"); |
148 | } | 175 | } |
149 | this.ctx.close(); | 176 | this.ctx.close(); |
177 | |||
178 | stop(); | ||
179 | |||
150 | return sol; | 180 | return sol; |
151 | } | 181 | } |
152 | 182 | ||
@@ -271,6 +301,8 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ | |||
271 | } | 301 | } |
272 | 302 | ||
273 | 303 | ||
304 | |||
305 | |||
274 | /* | 306 | /* |
275 | public void testIsSat(XExpression expression, Term t) throws Exception { | 307 | public void testIsSat(XExpression expression, Term t) throws Exception { |
276 | int count = 10000; | 308 | int count = 10000; |