diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java | 169 | ||||
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | 28 | ||||
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java (renamed from Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java) | 24 | ||||
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 22 | ||||
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend | 21 | ||||
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | 60 |
6 files changed, 116 insertions, 208 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java deleted file mode 100644 index 7b8634c4..00000000 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java +++ /dev/null | |||
@@ -1,169 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.lang.reflect.InvocationTargetException; | ||
4 | |||
5 | import org.eclipse.emf.common.notify.Adapter; | ||
6 | import org.eclipse.emf.common.notify.Notification; | ||
7 | import org.eclipse.emf.common.util.EList; | ||
8 | import org.eclipse.emf.common.util.TreeIterator; | ||
9 | import org.eclipse.emf.ecore.EClass; | ||
10 | import org.eclipse.emf.ecore.EObject; | ||
11 | import org.eclipse.emf.ecore.EOperation; | ||
12 | import org.eclipse.emf.ecore.EReference; | ||
13 | import org.eclipse.emf.ecore.EStructuralFeature; | ||
14 | import org.eclipse.emf.ecore.resource.Resource; | ||
15 | |||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | ||
18 | |||
19 | public class FakeIntegerElement implements PrimitiveElement{ | ||
20 | |||
21 | public FakeIntegerElement() { | ||
22 | |||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public EList<TypeDefinition> getDefinedInType() { | ||
27 | // TODO Auto-generated method stub | ||
28 | return null; | ||
29 | } | ||
30 | |||
31 | @Override | ||
32 | public String getName() { | ||
33 | // TODO Auto-generated method stub | ||
34 | return null; | ||
35 | } | ||
36 | |||
37 | @Override | ||
38 | public void setName(String value) { | ||
39 | // TODO Auto-generated method stub | ||
40 | |||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public EClass eClass() { | ||
45 | // TODO Auto-generated method stub | ||
46 | return null; | ||
47 | } | ||
48 | |||
49 | @Override | ||
50 | public Resource eResource() { | ||
51 | // TODO Auto-generated method stub | ||
52 | return null; | ||
53 | } | ||
54 | |||
55 | @Override | ||
56 | public EObject eContainer() { | ||
57 | // TODO Auto-generated method stub | ||
58 | return null; | ||
59 | } | ||
60 | |||
61 | @Override | ||
62 | public EStructuralFeature eContainingFeature() { | ||
63 | // TODO Auto-generated method stub | ||
64 | return null; | ||
65 | } | ||
66 | |||
67 | @Override | ||
68 | public EReference eContainmentFeature() { | ||
69 | // TODO Auto-generated method stub | ||
70 | return null; | ||
71 | } | ||
72 | |||
73 | @Override | ||
74 | public EList<EObject> eContents() { | ||
75 | // TODO Auto-generated method stub | ||
76 | return null; | ||
77 | } | ||
78 | |||
79 | @Override | ||
80 | public TreeIterator<EObject> eAllContents() { | ||
81 | // TODO Auto-generated method stub | ||
82 | return null; | ||
83 | } | ||
84 | |||
85 | @Override | ||
86 | public boolean eIsProxy() { | ||
87 | // TODO Auto-generated method stub | ||
88 | return false; | ||
89 | } | ||
90 | |||
91 | @Override | ||
92 | public EList<EObject> eCrossReferences() { | ||
93 | // TODO Auto-generated method stub | ||
94 | return null; | ||
95 | } | ||
96 | |||
97 | @Override | ||
98 | public Object eGet(EStructuralFeature feature) { | ||
99 | // TODO Auto-generated method stub | ||
100 | return null; | ||
101 | } | ||
102 | |||
103 | @Override | ||
104 | public Object eGet(EStructuralFeature feature, boolean resolve) { | ||
105 | // TODO Auto-generated method stub | ||
106 | return null; | ||
107 | } | ||
108 | |||
109 | @Override | ||
110 | public void eSet(EStructuralFeature feature, Object newValue) { | ||
111 | // TODO Auto-generated method stub | ||
112 | |||
113 | } | ||
114 | |||
115 | @Override | ||
116 | public boolean eIsSet(EStructuralFeature feature) { | ||
117 | // TODO Auto-generated method stub | ||
118 | return false; | ||
119 | } | ||
120 | |||
121 | @Override | ||
122 | public void eUnset(EStructuralFeature feature) { | ||
123 | // TODO Auto-generated method stub | ||
124 | |||
125 | } | ||
126 | |||
127 | @Override | ||
128 | public Object eInvoke(EOperation operation, EList<?> arguments) throws InvocationTargetException { | ||
129 | // TODO Auto-generated method stub | ||
130 | return null; | ||
131 | } | ||
132 | |||
133 | @Override | ||
134 | public EList<Adapter> eAdapters() { | ||
135 | // TODO Auto-generated method stub | ||
136 | return null; | ||
137 | } | ||
138 | |||
139 | @Override | ||
140 | public boolean eDeliver() { | ||
141 | // TODO Auto-generated method stub | ||
142 | return false; | ||
143 | } | ||
144 | |||
145 | @Override | ||
146 | public void eSetDeliver(boolean deliver) { | ||
147 | // TODO Auto-generated method stub | ||
148 | |||
149 | } | ||
150 | |||
151 | @Override | ||
152 | public void eNotify(Notification notification) { | ||
153 | // TODO Auto-generated method stub | ||
154 | |||
155 | } | ||
156 | |||
157 | @Override | ||
158 | public boolean isValueSet() { | ||
159 | // TODO Auto-generated method stub | ||
160 | return false; | ||
161 | } | ||
162 | |||
163 | @Override | ||
164 | public void setValueSet(boolean value) { | ||
165 | // TODO Auto-generated method stub | ||
166 | |||
167 | } | ||
168 | |||
169 | } | ||
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 cecd3623..f30e390b 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 | |||
@@ -365,8 +365,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
365 | Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); | 365 | Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); |
366 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { | 366 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { |
367 | String constraint = formNumericConstraint(e, aMatch); | 367 | String constraint = formNumericConstraint(e, aMatch); |
368 | if (constraint != null) { | 368 | if (constraint != null) { |
369 | String negAssert = "(assert " + constraint + ")"; | 369 | String negAssert = "(assert " + constraint + ")"; |
370 | curConstraints.add(negAssert); | 370 | curConstraints.add(negAssert); |
371 | } | 371 | } |
372 | } | 372 | } |
@@ -426,8 +426,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
426 | 426 | ||
427 | boolean result = false; | 427 | boolean result = false; |
428 | List<List<String>> outputs = null; | 428 | List<List<String>> outputs = null; |
429 | if (outputProcess != null) { | 429 | if (outputProcess != null) { |
430 | outputs = getProcessOutput(outputProcess); | 430 | outputs = getProcessOutput(outputProcess); |
431 | result = getDrealResult(outputProcess.exitValue(), outputs); | 431 | result = getDrealResult(outputProcess.exitValue(), outputs); |
432 | // } else { | 432 | // } else { |
433 | // System.err.print("Timeout, RETRYING..."); | 433 | // System.err.print("Timeout, RETRYING..."); |
@@ -575,4 +575,24 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
575 | //TODO Check if above went well? | 575 | //TODO Check if above went well? |
576 | } | 576 | } |
577 | 577 | ||
578 | @Override | ||
579 | protected void initialize() { | ||
580 | // TODO Auto-generated method stub | ||
581 | |||
582 | } | ||
583 | |||
584 | @Override | ||
585 | protected boolean internalIsSatisfiable( | ||
586 | Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { | ||
587 | // TODO Auto-generated method stub | ||
588 | return false; | ||
589 | } | ||
590 | |||
591 | @Override | ||
592 | protected Map<PrimitiveElement, Number> internalGetOneSolution(List<PrimitiveElement> objs, | ||
593 | Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { | ||
594 | // TODO Auto-generated method stub | ||
595 | return null; | ||
596 | } | ||
597 | |||
578 | } | 598 | } |
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/NumericDynamicProblemSolverXXX.java index e8c20138..199c089b 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/NumericDynamicProblemSolverXXX.java | |||
@@ -9,13 +9,13 @@ import org.eclipse.xtext.xbase.XExpression; | |||
9 | 9 | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
11 | 11 | ||
12 | public class NumericDynamicProblemSolver extends NumericProblemSolver{ | 12 | public class NumericDynamicProblemSolverXXX 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 | private int timeout; |
17 | 17 | ||
18 | public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { | 18 | public NumericDynamicProblemSolverXXX(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { |
19 | // this.z3Solver = new NumericZ3ProblemSolver(); | 19 | // this.z3Solver = new NumericZ3ProblemSolver(); |
20 | this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout); | 20 | this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout); |
21 | this.timeout = drealTimeout; | 21 | this.timeout = drealTimeout; |
@@ -40,4 +40,24 @@ public class NumericDynamicProblemSolver extends NumericProblemSolver{ | |||
40 | public Map<PrimitiveElement, Number> getOneSolution(List<PrimitiveElement> objs, | 40 | public Map<PrimitiveElement, Number> getOneSolution(List<PrimitiveElement> objs, |
41 | Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { | 41 | Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { |
42 | throw new Exception("Should not reach here - getOneSolution"); | 42 | throw new Exception("Should not reach here - getOneSolution"); |
43 | } | ||
44 | |||
45 | @Override | ||
46 | protected void initialize() { | ||
47 | // TODO Auto-generated method stub | ||
48 | |||
49 | } | ||
50 | |||
51 | @Override | ||
52 | protected boolean internalIsSatisfiable( | ||
53 | Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { | ||
54 | // TODO Auto-generated method stub | ||
55 | return false; | ||
56 | } | ||
57 | |||
58 | @Override | ||
59 | protected Map<PrimitiveElement, Number> internalGetOneSolution(List<PrimitiveElement> objs, | ||
60 | Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { | ||
61 | // TODO Auto-generated method stub | ||
62 | return null; | ||
43 | }} | 63 | }} |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java index 5e823d9d..8f57e40c 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | |||
@@ -35,6 +35,24 @@ public abstract class NumericProblemSolver { | |||
35 | public long getEndSolvingProblem() {return endSolvingProblem;} | 35 | public long getEndSolvingProblem() {return endSolvingProblem;} |
36 | public long getEndFormingSolution() {return endFormingSolution;} | 36 | public long getEndFormingSolution() {return endFormingSolution;} |
37 | 37 | ||
38 | public abstract boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception; | 38 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
39 | public abstract Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception; | 39 | if(!initialized) { |
40 | this.initialize(); | ||
41 | this.initialized=true; | ||
42 | } | ||
43 | return this.internalIsSatisfiable(matches); | ||
44 | } | ||
45 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception{ | ||
46 | if(!initialized) { | ||
47 | this.initialize(); | ||
48 | this.initialized=true; | ||
49 | } | ||
50 | return this.internalGetOneSolution(objs, matches); | ||
51 | } | ||
52 | |||
53 | boolean initialized = false; | ||
54 | protected abstract void initialize(); | ||
55 | |||
56 | protected abstract boolean internalIsSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception; | ||
57 | protected abstract Map<PrimitiveElement,Number> internalGetOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception; | ||
40 | } | 58 | } |
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 a11ae8a8..9ae36a6d 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 | |||
@@ -58,31 +58,18 @@ class NumericTranslator { | |||
58 | return res | 58 | return res |
59 | } | 59 | } |
60 | 60 | ||
61 | def NumericProblemSolver selectProblemSolver(String selection) { | ||
62 | // return new NumericProblemSolver | ||
63 | // add numeric solver decision procedure here | ||
64 | if (numericSolver instanceof NumericDynamicProblemSolver) { | ||
65 | val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver | ||
66 | return dynamicSolver.selectSolver(selection); | ||
67 | } else{ | ||
68 | if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver(this.timeout) | ||
69 | return numericSolver; | ||
70 | } | ||
71 | } | ||
72 | 61 | ||
73 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches, String select) { | 62 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches, String select) { |
74 | val input = formNumericProblemInstance(matches) | 63 | val input = formNumericProblemInstance(matches) |
75 | val solver = selectProblemSolver(select) | 64 | val satisfiability = numericSolver.isSatisfiable(input) |
76 | val satisfiability = solver.isSatisfiable(input) | 65 | numericSolver.updateTimes |
77 | solver.updateTimes | ||
78 | return satisfiability | 66 | return satisfiability |
79 | } | 67 | } |
80 | 68 | ||
81 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches, String select) { | 69 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches, String select) { |
82 | val input = formNumericProblemInstance(matches) | 70 | val input = formNumericProblemInstance(matches) |
83 | val solver = selectProblemSolver(select) | 71 | val solution = numericSolver.getOneSolution(primitiveElements,input) |
84 | val solution = solver.getOneSolution(primitiveElements,input) | 72 | numericSolver.updateTimes |
85 | solver.updateTimes | ||
86 | return solution | 73 | return solution |
87 | } | 74 | } |
88 | 75 | ||
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; |