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 | |
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')
2 files changed, 101 insertions, 20 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend index 1b68fed2..9e11d2cf 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend | |||
@@ -1,6 +1,7 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic | 1 | package hu.bme.mit.inf.dslreasoner.viatra2logic |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable |
6 | import java.util.Map | 7 | import java.util.Map |
@@ -8,9 +9,11 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | |||
8 | import org.eclipse.xtext.xbase.XBinaryOperation | 9 | import org.eclipse.xtext.xbase.XBinaryOperation |
9 | import org.eclipse.xtext.xbase.XExpression | 10 | import org.eclipse.xtext.xbase.XExpression |
10 | import org.eclipse.xtext.xbase.XFeatureCall | 11 | import org.eclipse.xtext.xbase.XFeatureCall |
12 | import org.eclipse.xtext.xbase.XIfExpression | ||
11 | import org.eclipse.xtext.xbase.XMemberFeatureCall | 13 | import org.eclipse.xtext.xbase.XMemberFeatureCall |
12 | import org.eclipse.xtext.xbase.XNumberLiteral | 14 | import org.eclipse.xtext.xbase.XNumberLiteral |
13 | import org.eclipse.xtext.xbase.XUnaryOperation | 15 | import org.eclipse.xtext.xbase.XUnaryOperation |
16 | import org.eclipse.xtext.xbase.XBlockExpression | ||
14 | 17 | ||
15 | class ExpressionEvaluation2Logic { | 18 | class ExpressionEvaluation2Logic { |
16 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | 19 | val extension LogicProblemBuilder builder = new LogicProblemBuilder |
@@ -139,6 +142,41 @@ class ExpressionEvaluation2Logic { | |||
139 | throw new UnsupportedOperationException('''Unsupported numeric type: "«s»"''') | 142 | throw new UnsupportedOperationException('''Unsupported numeric type: "«s»"''') |
140 | } | 143 | } |
141 | 144 | ||
145 | def protected dispatch Term transform(XIfExpression i, Map<PVariable, Variable> variable2Variable) { | ||
146 | |||
147 | val cond_op = i.^if.transform(variable2Variable) | ||
148 | val then_op = i.then.transform(variable2Variable) | ||
149 | val else_op = i.^else.transform(variable2Variable) | ||
150 | |||
151 | if (cond_op === null) { | ||
152 | println("-> " + i.^if) | ||
153 | println("-> " + i.then) | ||
154 | println("-> " + i.^else) | ||
155 | throw new UnsupportedOperationException('''Your ITE statement has a null condition.''') | ||
156 | } | ||
157 | if (then_op === null) { | ||
158 | println("-> " + i.^if) | ||
159 | println("-> " + i.then) | ||
160 | println("-> " + i.^else) | ||
161 | throw new UnsupportedOperationException('''Your ITE statement has a null "then" statement"".''') | ||
162 | } | ||
163 | return ITE(cond_op, then_op, else_op) | ||
164 | } | ||
165 | |||
166 | def protected dispatch Term transform(XBlockExpression b, Map<PVariable, Variable> variable2Variable) { | ||
167 | val exprs = newArrayList | ||
168 | for(e:b.expressions){ exprs.add(transform(e, variable2Variable)) } | ||
169 | |||
170 | if (exprs.size > 1) | ||
171 | throw new UnsupportedOperationException('''blocks with more than 1 statement are not currently supportes: "«exprs»"''') | ||
172 | if (exprs.isEmpty) | ||
173 | throw new UnsupportedOperationException('''blocks is empty: "«exprs»"''') | ||
174 | |||
175 | return exprs.get(0) | ||
176 | } | ||
177 | |||
178 | |||
179 | |||
142 | def protected dispatch Term transform(XExpression e, Map<PVariable, Variable> variable2Variable) { | 180 | def protected dispatch Term transform(XExpression e, Map<PVariable, Variable> variable2Variable) { |
143 | throw new UnsupportedOperationException('''Unsupported expression: "«e.class.simpleName»" - «e»''') | 181 | throw new UnsupportedOperationException('''Unsupported expression: "«e.class.simpleName»" - «e»''') |
144 | } | 182 | } |
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); |