diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-20 08:44:27 +0100 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-20 08:44:27 +0100 |
commit | 41a48543aea119acae321aae61b85d711610b652 (patch) | |
tree | da29d1d172eaaa4c9744d77851966b727720ce06 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | |
parent | add Actor+CollisionExists constrs & adjust dreal parser & measurements (diff) | |
download | VIATRA-Generator-41a48543aea119acae321aae61b85d711610b652.tar.gz VIATRA-Generator-41a48543aea119acae321aae61b85d711610b652.tar.zst VIATRA-Generator-41a48543aea119acae321aae61b85d711610b652.zip |
almost finish crossscen VQL + implement ITE handling + prelim results
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | 83 |
1 files changed, 63 insertions, 20 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 30e68260..575a9224 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 | |||
@@ -20,8 +20,10 @@ import java.util.regex.Pattern; | |||
20 | 20 | ||
21 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | 21 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; |
22 | import org.eclipse.xtext.xbase.XBinaryOperation; | 22 | import org.eclipse.xtext.xbase.XBinaryOperation; |
23 | import org.eclipse.xtext.xbase.XBlockExpression; | ||
23 | import org.eclipse.xtext.xbase.XExpression; | 24 | import org.eclipse.xtext.xbase.XExpression; |
24 | import org.eclipse.xtext.xbase.XFeatureCall; | 25 | import org.eclipse.xtext.xbase.XFeatureCall; |
26 | import org.eclipse.xtext.xbase.XIfExpression; | ||
25 | import org.eclipse.xtext.xbase.XNumberLiteral; | 27 | import org.eclipse.xtext.xbase.XNumberLiteral; |
26 | import org.eclipse.xtext.xbase.XUnaryOperation; | 28 | import org.eclipse.xtext.xbase.XUnaryOperation; |
27 | 29 | ||
@@ -72,7 +74,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
72 | //TODO timeout if needed | 74 | //TODO timeout if needed |
73 | if (!p.waitFor(timeout, TimeUnit.SECONDS)) { | 75 | if (!p.waitFor(timeout, TimeUnit.SECONDS)) { |
74 | p.destroy(); | 76 | p.destroy(); |
75 | System.err.println("TIMEOUT"); //DEBUG | 77 | return null; |
76 | } | 78 | } |
77 | return p; | 79 | return p; |
78 | } | 80 | } |
@@ -147,7 +149,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
147 | } | 149 | } |
148 | 150 | ||
149 | private String formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | 151 | private String formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { |
150 | //The check equation MUST be a binary operation | 152 | //The check equation MUST be a binary operation of the listed types (comparisons) |
151 | if (!(e instanceof XBinaryOperation)) { | 153 | if (!(e instanceof XBinaryOperation)) { |
152 | throw new Exception ("error in check expression!!!"); | 154 | throw new Exception ("error in check expression!!!"); |
153 | } | 155 | } |
@@ -159,19 +161,20 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
159 | String left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); | 161 | String left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); |
160 | String right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); | 162 | String right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); |
161 | 163 | ||
164 | //NOTE that everything is inverted, due to how the MG handles vql constraints | ||
162 | if (nameEndsWith(name, N_LESSTHAN)) { | 165 | if (nameEndsWith(name, N_LESSTHAN)) { |
163 | operator = "<"; | 166 | operator = ">"; |
164 | } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { | 167 | } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { |
165 | operator = "<="; | 168 | operator = ">="; |
166 | } else if (nameEndsWith(name, N_GREATERTHAN)) { | 169 | } else if (nameEndsWith(name, N_GREATERTHAN)) { |
167 | operator = ">"; | 170 | operator = "<"; |
168 | } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { | 171 | } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { |
169 | operator = ">="; | 172 | operator = "<="; |
170 | } else if (nameEndsWith(name, N_EQUALS)) { | 173 | } else if (nameEndsWith(name, N_EQUALS)) { |
171 | operator = "<"; | ||
172 | } else if (nameEndsWith(name, N_NOTEQUALS)) { | ||
173 | //Exceptional case | 174 | //Exceptional case |
174 | return "(not (=" + " " + left_operand + " " + right_operand + "))"; | 175 | return "(not (=" + " " + left_operand + " " + right_operand + "))"; |
176 | } else if (nameEndsWith(name, N_NOTEQUALS)) { | ||
177 | operator = "="; | ||
175 | // } else if (nameEndsWith(name, N_EQUALS3)) { | 178 | // } else if (nameEndsWith(name, N_EQUALS3)) { |
176 | // operator = "<"; | 179 | // operator = "<"; |
177 | // } else if (nameEndsWith(name, N_NOTEQUALS3)) { | 180 | // } else if (nameEndsWith(name, N_NOTEQUALS3)) { |
@@ -240,6 +243,19 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
240 | operator = "*"; | 243 | operator = "*"; |
241 | } else if (nameEndsWith(name, N_DIVIDE)) { | 244 | } else if (nameEndsWith(name, N_DIVIDE)) { |
242 | operator = "/"; | 245 | operator = "/"; |
246 | } else if (nameEndsWith(name, N_LESSTHAN)) { | ||
247 | operator = "<"; | ||
248 | } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { | ||
249 | operator = "<="; | ||
250 | } else if (nameEndsWith(name, N_GREATERTHAN)) { | ||
251 | operator = ">"; | ||
252 | } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { | ||
253 | operator = ">="; | ||
254 | } else if (nameEndsWith(name, N_EQUALS)) { | ||
255 | operator = "<"; | ||
256 | } else if (nameEndsWith(name, N_NOTEQUALS)) { | ||
257 | //Exceptional case | ||
258 | return "(not (=" + " " + left_operand + " " + right_operand + "))"; | ||
243 | // } else if (nameEndsWith(name, N_MODULO)) { | 259 | // } else if (nameEndsWith(name, N_MODULO)) { |
244 | // expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); | 260 | // expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); |
245 | } else { | 261 | } else { |
@@ -249,12 +265,30 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
249 | expr = "(" + operator + " " + left_operand + " " + right_operand + ")"; | 265 | expr = "(" + operator + " " + left_operand + " " + right_operand + ")"; |
250 | } | 266 | } |
251 | else if (e instanceof XUnaryOperation){ | 267 | else if (e instanceof XUnaryOperation){ |
252 | String name = ((XUnaryOperation) e).getFeature().getQualifiedName(); | 268 | //TODO |
253 | System.out.println(name); | 269 | //This is, for example, "-1000" |
254 | String op = ((XUnaryOperation) e).getOperand().toString(); | ||
255 | System.out.println(op); | ||
256 | throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); | 270 | throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); |
257 | } else { | 271 | } |
272 | else if (e instanceof XIfExpression) { | ||
273 | |||
274 | String if_operand = formNumericConstraintHelper(((XIfExpression) e).getIf(), aMatch); | ||
275 | String then_operand = formNumericConstraintHelper(((XIfExpression) e).getThen(), aMatch); | ||
276 | String else_operand = formNumericConstraintHelper(((XIfExpression) e).getElse(), aMatch); | ||
277 | |||
278 | expr = "(ite " + if_operand + " " + then_operand + " " + else_operand + ")"; | ||
279 | } | ||
280 | else if (e instanceof XBlockExpression) { | ||
281 | XBlockExpression ebl = (XBlockExpression) e; | ||
282 | |||
283 | if (ebl.getExpressions().size() > 1) | ||
284 | throw new Exception("Unsupported: blocks with more than 1 statement are not currently supportes: " + ebl); | ||
285 | if (ebl.getExpressions().isEmpty()) | ||
286 | throw new Exception("Unsupported: blocks is empty:" + ebl); | ||
287 | |||
288 | //TODO make this more general | ||
289 | expr = formNumericConstraintHelper(ebl.getExpressions().get(0), aMatch); | ||
290 | } | ||
291 | else { | ||
258 | throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); | 292 | throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); |
259 | } | 293 | } |
260 | return expr; | 294 | return expr; |
@@ -279,7 +313,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
279 | Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); | 313 | Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); |
280 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { | 314 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { |
281 | String constraint = formNumericConstraint(e, aMatch); | 315 | String constraint = formNumericConstraint(e, aMatch); |
282 | String negAssert = "(assert (not " + constraint + "))"; | 316 | String negAssert = "(assert " + constraint + ")"; |
283 | curConstraints.add(negAssert); | 317 | curConstraints.add(negAssert); |
284 | } | 318 | } |
285 | } | 319 | } |
@@ -329,16 +363,24 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
329 | Process outputProcess; | 363 | Process outputProcess; |
330 | if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); | 364 | if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); |
331 | else outputProcess = callDrealLocal(numProbContent, false); | 365 | else outputProcess = callDrealLocal(numProbContent, false); |
332 | 366 | ||
333 | List<List<String>> outputs = getProcessOutput(outputProcess); | 367 | boolean result = false; |
334 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); | 368 | List<List<String>> outputs = null; |
369 | if (outputProcess != null) { | ||
370 | outputs = getProcessOutput(outputProcess); | ||
371 | result = getDrealResult(outputProcess.exitValue(), outputs); | ||
372 | } | ||
335 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 373 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
336 | 374 | ||
337 | //DEBUG - Print things | 375 | //DEBUG - Print things |
376 | if (outputProcess == null) { | ||
377 | System.err.println("TIMEOUT"); | ||
378 | // printOutput(numProbContent); | ||
379 | } | ||
338 | // printOutput(numProbContent); | 380 | // printOutput(numProbContent); |
339 | // printOutput(outputs.get(0)); | 381 | // if (outputs != null) printOutput(outputs.get(0)); |
340 | System.out.println(result); | 382 | // System.out.println(result); |
341 | //END DEBUG | 383 | // END DEBUG |
342 | 384 | ||
343 | return result; | 385 | return result; |
344 | } | 386 | } |
@@ -391,6 +433,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
391 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 433 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
392 | 434 | ||
393 | //DEBUG - Print things | 435 | //DEBUG - Print things |
436 | System.out.println("Getting Solution!"); | ||
394 | // printOutput(numProbContent); | 437 | // printOutput(numProbContent); |
395 | // printOutput(outputs.get(0)); | 438 | // printOutput(outputs.get(0)); |
396 | // System.out.println(result); | 439 | // System.out.println(result); |