aboutsummaryrefslogtreecommitdiffstats
path: root/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic
diff options
context:
space:
mode:
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic')
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF2
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java169
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java28
-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.java22
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend21
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java60
7 files changed, 117 insertions, 209 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF
index 23fba304..d8e9608d 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF
@@ -21,7 +21,7 @@ Require-Bundle: com.google.guava,
21 org.eclipse.xtext, 21 org.eclipse.xtext,
22 org.eclipse.xtext.xbase;bundle-version="2.18.0", 22 org.eclipse.xtext.xbase;bundle-version="2.18.0",
23 hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", 23 hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0",
24 com.microsoft.z3 24 com.microsoft.z3;bundle-version="4.8.8"
25Bundle-ActivationPolicy: lazy 25Bundle-ActivationPolicy: lazy
26Export-Package: 26Export-Package:
27 hu.bme.mit.inf.dslreasoner.viatra2logic, 27 hu.bme.mit.inf.dslreasoner.viatra2logic,
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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2
3import java.lang.reflect.InvocationTargetException;
4
5import org.eclipse.emf.common.notify.Adapter;
6import org.eclipse.emf.common.notify.Notification;
7import org.eclipse.emf.common.util.EList;
8import org.eclipse.emf.common.util.TreeIterator;
9import org.eclipse.emf.ecore.EClass;
10import org.eclipse.emf.ecore.EObject;
11import org.eclipse.emf.ecore.EOperation;
12import org.eclipse.emf.ecore.EReference;
13import org.eclipse.emf.ecore.EStructuralFeature;
14import org.eclipse.emf.ecore.resource.Resource;
15
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
18
19public 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
10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; 10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
11 11
12public class NumericDynamicProblemSolver extends NumericProblemSolver{ 12public 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;
generated by cgit v1.2.3-54-g00ecf (git 2.45.1) at 2024-06-01 02:25:15 +0000