aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2020-12-14 03:27:43 -0500
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-01-06 00:02:49 +0100
commit8fd50f7d4a979117a1e643f5384b76f4a3e36801 (patch)
treea5bb21af9c982f18bd216b1f9c98f9548169a2e2
parentadd numericProblemSolver supertype (diff)
downloadVIATRA-Generator-8fd50f7d4a979117a1e643f5384b76f4a3e36801.tar.gz
VIATRA-Generator-8fd50f7d4a979117a1e643f5384b76f4a3e36801.tar.zst
VIATRA-Generator-8fd50f7d4a979117a1e643f5384b76f4a3e36801.zip
implement isSatisfiable with Dreal integration
Diffstat
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java420
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java23
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend4
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java16
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend3
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend1
6 files changed, 256 insertions, 211 deletions
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 1e5742b7..9b9136c7 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
@@ -1,7 +1,10 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic; 1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2 2
3import java.io.BufferedInputStream;
3import java.io.BufferedReader; 4import java.io.BufferedReader;
4import java.io.File; 5import java.io.File;
6import java.io.FileInputStream;
7import java.io.FileNotFoundException;
5import java.io.IOException; 8import java.io.IOException;
6import java.io.InputStream; 9import java.io.InputStream;
7import java.io.InputStreamReader; 10import java.io.InputStreamReader;
@@ -12,55 +15,37 @@ import java.util.HashMap;
12import java.util.List; 15import java.util.List;
13import java.util.Map; 16import java.util.Map;
14import java.util.UUID; 17import java.util.UUID;
18import java.util.concurrent.TimeUnit;
15 19
16import org.eclipse.xtext.common.types.JvmIdentifiableElement; 20import org.eclipse.xtext.common.types.JvmIdentifiableElement;
21import org.eclipse.xtext.xbase.XBinaryOperation;
17import org.eclipse.xtext.xbase.XExpression; 22import org.eclipse.xtext.xbase.XExpression;
23import org.eclipse.xtext.xbase.XFeatureCall;
24import org.eclipse.xtext.xbase.XNumberLiteral;
18 25
26import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement;
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; 27import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
28import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement;
20 29
21public class NumericDrealProblemSolver extends NumericProblemSolver{ 30public class NumericDrealProblemSolver extends NumericProblemSolver{
22 private static final String N_Base = "org.eclipse.xtext.xbase.lib.";
23 private static final String N_PLUS = "operator_plus";
24 private static final String N_MINUS = "operator_minus";
25 private static final String N_POWER = "operator_power";
26 private static final String N_MULTIPLY = "operator_multiply";
27 private static final String N_DIVIDE = "operator_divide";
28 private static final String N_MODULO = "operator_modulo";
29 private static final String N_LESSTHAN = "operator_lessThan";
30 private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan";
31 private static final String N_GREATERTHAN = "operator_greaterThan";
32 private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan";
33 private static final String N_EQUALS = "operator_equals";
34 private static final String N_NOTEQUALS = "operator_notEquals";
35 private static final String N_EQUALS3 = "operator_tripleEquals";
36 private static final String N_NOTEQUALS3 = "operator_tripleNotEquals";
37 31
38 private File tempFile; 32 private final String containerName;
39 private PrintWriter printer;
40 private String containerName;
41 private Map<Object, String> varMap; 33 private Map<Object, String> varMap;
34 private List<String> curVars;
42 35
43 public NumericDrealProblemSolver() throws IOException, InterruptedException { 36 public NumericDrealProblemSolver() throws IOException, InterruptedException {
44 //setup smt2 input file
45 tempFile = File.createTempFile("smt", ".smt2");
46 printer = new PrintWriter(tempFile);
47 printer.println(";Header comment");
48 printer.println("(set-logic QF_NRA)");
49
50 //setup docker 37 //setup docker
51 File parentPath = tempFile.getParentFile(); 38 //TODO ENSURE that container name is not already in use????
52 System.out.println(parentPath); 39 File tempDir = new File(System.getProperty("java.io.tmpdir"));
53 System.out.println(tempFile);
54 //TODO ENSURE that container name is not already in use
55 containerName = UUID.randomUUID().toString().replace("-", ""); 40 containerName = UUID.randomUUID().toString().replace("-", "");
56 List<String> startDocker = new ArrayList<String>( 41 List<String> startDocker = new ArrayList<String>(
57 Arrays.asList("docker", "run", 42 Arrays.asList("docker", "run",
58 "-id", "--rm", 43 "-id", "--rm",
59 "--name", containerName, 44 "--name", containerName,
60 "-p", "8080:80", 45// "-p", "8080:80",
61 "-v", parentPath + ":/mnt", 46 "-v", tempDir + ":/mnt",
62 "dreal/dreal4")); 47 "dreal/dreal4"));
63 Process p = runProcess(startDocker); 48 Process p = runProcess(startDocker);
64 49
65 //setup varmap 50 //setup varmap
66 varMap = new HashMap<Object, String>(); 51 varMap = new HashMap<Object, String>();
@@ -69,70 +54,235 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
69 private Process runProcess(List<String> cmd) throws IOException, InterruptedException { 54 private Process runProcess(List<String> cmd) throws IOException, InterruptedException {
70// println(cmd) 55// println(cmd)
71 ProcessBuilder pb = new ProcessBuilder(cmd); 56 ProcessBuilder pb = new ProcessBuilder(cmd);
72 pb.redirectOutput();
73 pb.redirectError();
74 Process p = pb.start(); 57 Process p = pb.start();
75 p.waitFor(); 58// p.waitFor();
76 //TODO timeout if needed 59 //TODO timeout if needed
77// if (!p.waitFor(TIMEOUT, TimeUnit.SECONDS)) { 60 if (!p.waitFor(5, TimeUnit.SECONDS)) {
78// p.destroy(); 61 p.destroy();
79// } 62 }
80 return p; 63 return p;
81 } 64 }
82
83//
84// private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) {
85// ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>();
86// XExpression left = ((XBinaryOperation) expression).getLeftOperand();
87// XExpression right = ((XBinaryOperation) expression).getRightOperand();
88//
89// getJvmIdentifiableElementsHelper(left, allElem);
90// getJvmIdentifiableElementsHelper(right, allElem);
91// return allElem;
92// }
93//
94// private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) {
95// if (e instanceof XFeatureCall) {
96// allElem.add(((XFeatureCall) e).getFeature());
97// } else if (e instanceof XBinaryOperation) {
98// getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem);
99// getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem);
100// }
101// }
102 65
103 private Process callDreal() throws IOException, InterruptedException { 66 private Process callDreal(String tempFileName) throws IOException, InterruptedException {
104 List<String> drealCmd = new ArrayList<String>( 67 List<String> drealCmd = new ArrayList<String>(
105 Arrays.asList("docker", "exec", 68 Arrays.asList("docker", "exec",
106 containerName, 69 containerName,
107 "dreal", 70 "dreal",
108 "--model", 71 "--model",
109 "mnt/" + tempFile.getName())); 72 "mnt/" + tempFileName));
110 return runProcess(drealCmd); 73 return runProcess(drealCmd);
111 } 74 }
112 75
113 private boolean getDrealResult(Process p) throws IOException { 76 private List<String> getDrealStream(InputStream stream) throws IOException {
114 if (p.exitValue() == 1) {return false;} 77 List<String> output = new ArrayList<String>();
78 BufferedReader r = new BufferedReader(new InputStreamReader(stream));
115 79
116 BufferedReader output = new BufferedReader(new InputStreamReader(p.getInputStream())); 80 String rl = "";
81 while ((rl = r.readLine()) != null) {output.add(rl);}
82 return output;
83 }
84
85 private List<List<String>> getProcessOutput(Process p) throws IOException {
86 List<List<String>> outputs = new ArrayList<List<String>>();
87 outputs.add(getDrealStream(p.getInputStream()));
88 outputs.add(getDrealStream(p.getErrorStream()));
89 return outputs;
90 }
91
92 private boolean getDrealResult(int exitVal, List<List<String>> outputs) throws IOException {
93 //error at process-level
94 if (exitVal == 1) {printError(outputs.get(1)); return false;}
95
96 //error at dreal-level
97 if (! outputs.get(1).isEmpty()) {printError(outputs.get(1)); return false;}
117 98
118 String resultRaw = output.readLine(); 99 //print output
100// printOutput(outputs.get(0));
101
102 String resultRaw = outputs.get(0).get(0);
119 if (resultRaw.startsWith("unsat")) {return false;} 103 if (resultRaw.startsWith("unsat")) {return false;}
120 if (resultRaw.startsWith("delta-sat")) {return true;} 104 if (resultRaw.startsWith("delta-sat")) {return true;}
121 throw new IOException("Unknown dreal output first line"); 105 throw new IOException("Unknown dreal output first line");
122 //TODO make the above better 106 //TODO make the above better
107 }
108
109 private String formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception {
110 //The check equation MUST be a binary operation
111 if (!(e instanceof XBinaryOperation)) {
112 throw new Exception ("error in check expression!!!");
113 }
114
115 String name = ((XBinaryOperation) e).getFeature().getQualifiedName();
116
117 String operator = "";
118
119 String left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch);
120 String right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch);
121
122 if (nameEndsWith(name, N_LESSTHAN)) {
123 operator = "<";
124 } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) {
125 operator = "<=";
126 } else if (nameEndsWith(name, N_GREATERTHAN)) {
127 operator = ">";
128 } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) {
129 operator = ">=";
130 } else if (nameEndsWith(name, N_EQUALS)) {
131 operator = "<";
132 } else if (nameEndsWith(name, N_NOTEQUALS)) {
133 //Exceptional case
134 return "(not (=" + " " + left_operand + " " + right_operand + "))";
135// } else if (nameEndsWith(name, N_EQUALS3)) {
136// operator = "<";
137// } else if (nameEndsWith(name, N_NOTEQUALS3)) {
138// operator = "<";
139 } else {
140 throw new Exception ("Unsupported binary operation " + name);
141 }
142
143 return "(" + operator + " " + left_operand + " " + right_operand + ")";
144 }
145
146 private String formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception {
147 String expr = "";
148 // Variables
149 if (e instanceof XFeatureCall) {
150 PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature());
151 boolean isInt = matchedObj instanceof IntegerElement;
152 if (!matchedObj.isValueSet()) {
153 if (varMap.get(matchedObj) == null) {
154 expr = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.hashCode(); //TODO ISSUE
155 varMap.put(matchedObj, expr);
156 } else {
157 expr = varMap.get(matchedObj);
158 }
159 } else {
160 //TODO unsure what it means if something gets in here
161 if (isInt) {
162 expr = Integer.toString(((IntegerElement) matchedObj).getValue());
163 } else {
164 expr = Double.toString(((RealElement) matchedObj).getValue().doubleValue());
165 }
166 varMap.put(matchedObj, expr);
167 }
168 //Add variable declarations
169 if(! curVars.contains(expr)) {
170 String varDecl = "(declare-fun " + expr + " () ";
171 if (isInt) {varDecl += "Int)";}
172 else {varDecl += "Real)";}
173 curVars.add(varDecl);
174 }
175 }
176 // Constants
177 else if (e instanceof XNumberLiteral) {
178 //we do not care if it is an int or a real.
179 //We actually do not even check f the value parses into a number
180 expr = ((XNumberLiteral) e).getValue();
181 //TODO ensure that the value is a valid number
182 // expr = Integer.parseInt(value)
183 }
184 // Expressions with operators
185 else if (e instanceof XBinaryOperation) {
186 String name = ((XBinaryOperation) e).getFeature().getQualifiedName();
187 String left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch);
188 String right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch);
189
190 String operator = "";
191 if (nameEndsWith(name, N_PLUS)) {
192 operator = "+";
193 } else if (nameEndsWith(name, N_MINUS)) {
194 operator = "-";
195 } else if (nameEndsWith(name, N_POWER)) {
196 operator = "^";
197 } else if (nameEndsWith(name, N_MULTIPLY)) {
198 operator = "*";
199 } else if (nameEndsWith(name, N_DIVIDE)) {
200 operator = "/";
201// } else if (nameEndsWith(name, N_MODULO)) {
202// expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand);
203 } else {
204 throw new Exception ("Unsupported binary operation " + name);
205 }
206
207 expr = "(" + operator + " " + left_operand + " " + right_operand + ")";
208 } else {
209 throw new Exception ("Unsupported expression " + e.getClass().getSimpleName());
210 }
211 return expr;
212
213 }
214
215 private boolean nameEndsWith(String name, String end) {
216 return name.startsWith(N_Base) && name.endsWith(end);
217 }
218
219 private String formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
220 //CREATE SMT2 TEMP FILE
221 File tempFile = File.createTempFile("smt", ".smt2");
222 String tempFileName = tempFile.getName();
223
224 //STM2 FILE CONTENT CREATION
225 curVars = new ArrayList<String>();
226 List<String> curConstraints = new ArrayList<String>();
227
228 PrintWriter printer = new PrintWriter(tempFile);
229 printer.println(";Header comment");
230 printer.println("(set-logic QF_NRA)");
231 for (XExpression e: matches.keySet()) {
232 Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e);
233 for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) {
234 String constraint = formNumericConstraint(e, aMatch);
235 String negAssert = "(assert (not " + constraint + "))";
236 curConstraints.add(negAssert);
237 }
238 }
239 //Add Content to SMT2 file
240 for (String varDecl : curVars) {printer.println(varDecl);}
241 for (String negAssert : curConstraints) {printer.println(negAssert);}
242 printer.println("(check-sat)");
243 printer.close();
244 return tempFileName;
245 }
246
247 private void printFileContent(String path) throws IOException {
248 InputStream input = new BufferedInputStream(new FileInputStream(path));
249 byte[] buffer = new byte[8192];
250
251 try {
252 for (int length = 0; (length = input.read(buffer)) != -1;) {
253 System.out.write(buffer, 0, length);
254 }
255 } finally {
256 input.close();
257 }
258 }
259
260 private void printOutput(List<String> list) {
261 for (String line : list) {
262 System.out.println(line);
263 }
264 }
265
266 private void printError(List<String> list) {
267 for (String line : list) {
268 System.err.println(line);
269 }
123 } 270 }
124 271
125 public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { 272 public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
273 //CREATE DREAL STM2 FILE at this.tempfile location
126 long startformingProblem = System.nanoTime(); 274 long startformingProblem = System.nanoTime();
127 //CREATE DREAL STM2 FILE 275 String tempFileName = formNumericProblemInstance(matches);
128 //TODO
129
130 printer.close();
131 endformingProblem = System.nanoTime()-startformingProblem; 276 endformingProblem = System.nanoTime()-startformingProblem;
277
278// printFileContent(System.getProperty("java.io.tmpdir") + tempFileName);
279
280 //CALL DREAL
132 long startSolvingProblem = System.nanoTime(); 281 long startSolvingProblem = System.nanoTime();
133 //CALL DREAL 282 Process outputProcess = callDreal(tempFileName);
134 Process outputProcess = callDreal(); 283 List<List<String>> outputs = getProcessOutput(outputProcess);
135 boolean result = getDrealResult(outputProcess); 284 boolean result = getDrealResult(outputProcess.exitValue(), outputs);
285 System.out.println(result);
136 endSolvingProblem = System.nanoTime()-startSolvingProblem; 286 endSolvingProblem = System.nanoTime()-startSolvingProblem;
137 //CLOSE 287 //CLOSE
138 return result; 288 return result;
@@ -177,124 +327,12 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
177// return sol; 327// return sol;
178 return null; 328 return null;
179 } 329 }
180// 330
181// private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { 331 public void teardown() throws IOException, InterruptedException {
182// if (!(e instanceof XBinaryOperation)) { 332 List<String> stopDocker = new ArrayList<String>(
183// throw new Exception ("error in check expression!!!"); 333 Arrays.asList("docker", "stop", containerName));
184// } 334 runProcess(stopDocker);
185// 335 //TODO Check if above went well?
186// String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); 336 }
187// 337
188// BoolExpr constraint = null;
189//
190// ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch);
191// ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch);
192//
193// if (nameEndsWith(name, N_LESSTHAN)) {
194// constraint = ctx.mkLt(left_operand, right_operand);
195// } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) {
196// constraint = ctx.mkLe(left_operand, right_operand);
197// } else if (nameEndsWith(name, N_GREATERTHAN)) {
198// constraint = ctx.mkGt(left_operand, right_operand);
199// } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) {
200// constraint = ctx.mkGe(left_operand, right_operand);
201// } else if (nameEndsWith(name, N_EQUALS)) {
202// constraint = ctx.mkEq(left_operand, right_operand);
203// } else if (nameEndsWith(name, N_NOTEQUALS)) {
204// constraint = ctx.mkDistinct(left_operand, right_operand);
205// } else if (nameEndsWith(name, N_EQUALS3)) {
206// constraint = ctx.mkGe(left_operand, right_operand); // ???
207// } else if (nameEndsWith(name, N_NOTEQUALS3)) {
208// constraint = ctx.mkGe(left_operand, right_operand); // ???
209// } else {
210// throw new Exception ("Unsupported binary operation " + name);
211// }
212//
213// return constraint;
214// }
215//
216// private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception {
217// ArithExpr expr = null;
218// // Variables
219// if (e instanceof XFeatureCall) {
220// PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature());
221// boolean isInt = matchedObj instanceof IntegerElement;
222// if (!matchedObj.isValueSet()) {
223// if (varMap.get(matchedObj) == null) {
224// String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString();
225// if (isInt) {
226// expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort());
227// } else {
228// expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getRealSort());
229// }
230// varMap.put(matchedObj, expr);
231// } else {
232// expr = (ArithExpr) varMap.get(matchedObj);
233// }
234// } else {
235// if (isInt) {
236// int value = ((IntegerElement) matchedObj).getValue();
237// expr = (ArithExpr) ctx.mkInt(value);
238// } else {
239// double value = ((RealElement) matchedObj).getValue().doubleValue();
240// expr = (ArithExpr) ctx.mkReal(String.valueOf(value));
241// }
242// varMap.put(matchedObj, expr);
243// }
244// }
245// // Constants
246// else if (e instanceof XNumberLiteral) {
247// String value = ((XNumberLiteral) e).getValue();
248// try{
249// int val = Integer.parseInt(value);
250// expr = (ArithExpr) ctx.mkInt(val);
251// } catch(NumberFormatException err){
252// try{
253// expr = (ArithExpr) ctx.mkReal(value);
254// } catch(NumberFormatException err2){}
255// }
256// }
257// // Expressions with operators
258// else if (e instanceof XBinaryOperation) {
259// String name = ((XBinaryOperation) e).getFeature().getQualifiedName();
260// ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch);
261// ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch);
262//
263// if (nameEndsWith(name, N_PLUS)) {
264// expr = ctx.mkAdd(left_operand, right_operand);
265// } else if (nameEndsWith(name, N_MINUS)) {
266// expr = ctx.mkAdd(left_operand, ctx.mkUnaryMinus(right_operand));
267// } else if (nameEndsWith(name, N_POWER)) {
268// expr = ctx.mkPower(left_operand, right_operand);
269// } else if (nameEndsWith(name, N_MULTIPLY)) {
270// expr = ctx.mkMul(left_operand, right_operand);
271// } else if (nameEndsWith(name, N_DIVIDE)) {
272// expr = ctx.mkDiv(left_operand, right_operand);
273// } else if (nameEndsWith(name, N_MODULO)) {
274// expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand);
275// } else {
276// throw new Exception ("Unsupported binary operation " + name);
277// }
278// } else {
279// throw new Exception ("Unsupported expression " + e.getClass().getSimpleName());
280// }
281// return expr;
282//
283// }
284//
285// private boolean nameEndsWith(String name, String end) {
286// return name.startsWith(N_Base) && name.endsWith(end);
287// }
288//
289// private BoolExpr formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
290// BoolExpr constraintInstances = ctx.mkTrue();
291// for (XExpression e: matches.keySet()) {
292// Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e);
293// for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) {
294// BoolExpr constraintInstance = ctx.mkNot(formNumericConstraint(e, aMatch));
295// constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance);
296// }
297// }
298// return constraintInstances;
299// }
300} 338}
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 d818ec91..5e823d9d 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
@@ -6,13 +6,30 @@ import java.util.Map;
6import org.eclipse.xtext.common.types.JvmIdentifiableElement; 6import org.eclipse.xtext.common.types.JvmIdentifiableElement;
7import org.eclipse.xtext.xbase.XExpression; 7import org.eclipse.xtext.xbase.XExpression;
8 8
9import com.microsoft.z3.Expr;
10
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; 11import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
10 12
11public abstract class NumericProblemSolver { 13public abstract class NumericProblemSolver {
14 protected static final String N_Base = "org.eclipse.xtext.xbase.lib.";
15 protected static final String N_PLUS = "operator_plus";
16 protected static final String N_MINUS = "operator_minus";
17 protected static final String N_POWER = "operator_power";
18 protected static final String N_MULTIPLY = "operator_multiply";
19 protected static final String N_DIVIDE = "operator_divide";
20 protected static final String N_MODULO = "operator_modulo";
21 protected static final String N_LESSTHAN = "operator_lessThan";
22 protected static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan";
23 protected static final String N_GREATERTHAN = "operator_greaterThan";
24 protected static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan";
25 protected static final String N_EQUALS = "operator_equals";
26 protected static final String N_NOTEQUALS = "operator_notEquals";
27 protected static final String N_EQUALS3 = "operator_tripleEquals";
28 protected static final String N_NOTEQUALS3 = "operator_tripleNotEquals";
12 29
13 long endformingProblem=0; 30 protected long endformingProblem=0;
14 long endSolvingProblem=0; 31 protected long endSolvingProblem=0;
15 long endFormingSolution=0; 32 protected long endFormingSolution=0;
16 33
17 public long getEndformingProblem() {return endformingProblem;} 34 public long getEndformingProblem() {return endformingProblem;}
18 public long getEndSolvingProblem() {return endSolvingProblem;} 35 public long getEndSolvingProblem() {return endSolvingProblem;}
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 d63604b0..22ea41bf 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
@@ -16,6 +16,7 @@ import org.eclipse.xtext.xbase.XFeatureCall
16class NumericTranslator { 16class NumericTranslator {
17 17
18 private XExpressionExtractor extractor = new XExpressionExtractor(); 18 private XExpressionExtractor extractor = new XExpressionExtractor();
19 private NumericDrealProblemSolver drealSolver = new NumericDrealProblemSolver();
19 20
20 long formingProblemTime=0; 21 long formingProblemTime=0;
21 long solvingProblemTime=0; 22 long solvingProblemTime=0;
@@ -52,7 +53,7 @@ class NumericTranslator {
52 53
53 def NumericProblemSolver selectProblemSolver() { 54 def NumericProblemSolver selectProblemSolver() {
54// return new NumericProblemSolver 55// return new NumericProblemSolver
55 return new NumericDrealProblemSolver 56 return drealSolver;
56 } 57 }
57 58
58 def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { 59 def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) {
@@ -80,4 +81,5 @@ class NumericTranslator {
80 def getFormingProblemTime() {formingProblemTime} 81 def getFormingProblemTime() {formingProblemTime}
81 def getSolvingProblemTime() {solvingProblemTime} 82 def getSolvingProblemTime() {solvingProblemTime}
82 def getFormingSolutionTime() {formingSolutionTime} 83 def getFormingSolutionTime() {formingSolutionTime}
84 def getDrealSolver(){return drealSolver}
83} \ No newline at end of file 85} \ No newline at end of file
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 a594eb60..ab7f6ddc 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
@@ -28,22 +28,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
28 28
29 29
30public class NumericZ3ProblemSolver extends NumericProblemSolver{ 30public class NumericZ3ProblemSolver extends NumericProblemSolver{
31 private static final String N_Base = "org.eclipse.xtext.xbase.lib.";
32 private static final String N_PLUS = "operator_plus";
33 private static final String N_MINUS = "operator_minus";
34 private static final String N_POWER = "operator_power";
35 private static final String N_MULTIPLY = "operator_multiply";
36 private static final String N_DIVIDE = "operator_divide";
37 private static final String N_MODULO = "operator_modulo";
38 private static final String N_LESSTHAN = "operator_lessThan";
39 private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan";
40 private static final String N_GREATERTHAN = "operator_greaterThan";
41 private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan";
42 private static final String N_EQUALS = "operator_equals";
43 private static final String N_NOTEQUALS = "operator_notEquals";
44 private static final String N_EQUALS3 = "operator_tripleEquals";
45 private static final String N_NOTEQUALS3 = "operator_tripleNotEquals";
46
47 31
48 private Context ctx; 32 private Context ctx;
49 private Solver s; 33 private Solver s;
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index 8e992741..1f902b90 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -163,6 +163,9 @@ class ViatraReasoner extends LogicReasoner {
163 } 163 }
164 val solverTime = System.nanoTime - solverStartTime 164 val solverTime = System.nanoTime - solverStartTime
165 viatraConfig.progressMonitor.workedSearchFinished 165 viatraConfig.progressMonitor.workedSearchFinished
166
167 //dreal teardown
168 numericSolver.numericDrealSolver.teardown()
166 169
167 // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches 170 // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches
168 val statistics = createStatistics => [ 171 val statistics = createStatistics => [
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
index 70e8e9c2..0e789671 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -68,6 +68,7 @@ class NumericSolver {
68 def getSolverFormingProblem(){this.t.formingProblemTime} 68 def getSolverFormingProblem(){this.t.formingProblemTime}
69 def getSolverSolvingProblem(){this.t.solvingProblemTime} 69 def getSolverSolvingProblem(){this.t.solvingProblemTime}
70 def getSolverSolution(){this.t.formingSolutionTime} 70 def getSolverSolution(){this.t.formingSolutionTime}
71 def getNumericDrealSolver(){this.t.drealSolver}
71 72
72 def boolean maySatisfiable() { 73 def boolean maySatisfiable() {
73 if(intermediateConsistencyCheck) { 74 if(intermediateConsistencyCheck) {
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-06 05:01:40 +0000