diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-02-15 07:42:02 +0100 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-02-15 07:42:02 +0100 |
commit | 0c56d765b120654bfd3534aa5b6d12476070515b (patch) | |
tree | 10a01c11769364116061e33fda4167db68a4c8be /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf | |
parent | finished first impl that works sometimes (issue w/ SAT in Dreal rerun) (diff) | |
download | VIATRA-Generator-0c56d765b120654bfd3534aa5b6d12476070515b.tar.gz VIATRA-Generator-0c56d765b120654bfd3534aa5b6d12476070515b.tar.zst VIATRA-Generator-0c56d765b120654bfd3534aa5b6d12476070515b.zip |
fix dreal call on solved problem imprecision issue
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/NumericDrealProblemSolver.java | 58 |
1 files changed, 49 insertions, 9 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 d7e0b20c..70aa933a 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 | |||
@@ -8,7 +8,6 @@ import java.io.IOException; | |||
8 | import java.io.InputStream; | 8 | import java.io.InputStream; |
9 | import java.io.InputStreamReader; | 9 | import java.io.InputStreamReader; |
10 | import java.io.PrintWriter; | 10 | import java.io.PrintWriter; |
11 | import java.text.DecimalFormat; | ||
12 | import java.util.ArrayList; | 11 | import java.util.ArrayList; |
13 | import java.util.Arrays; | 12 | import java.util.Arrays; |
14 | import java.util.HashMap; | 13 | import java.util.HashMap; |
@@ -96,7 +95,6 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
96 | } | 95 | } |
97 | 96 | ||
98 | private Process callDrealDocker(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { | 97 | private Process callDrealDocker(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { |
99 | //TODO currently not working for Linux | ||
100 | String numProbContentStr = String.join("\\n", numProbContents); | 98 | String numProbContentStr = String.join("\\n", numProbContents); |
101 | List<String> drealCmd = new ArrayList<String>(Arrays.asList( | 99 | List<String> drealCmd = new ArrayList<String>(Arrays.asList( |
102 | "docker", "exec", containerName, | 100 | "docker", "exec", containerName, |
@@ -169,6 +167,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
169 | if (!(e instanceof XBinaryOperation)) { | 167 | if (!(e instanceof XBinaryOperation)) { |
170 | throw new Exception ("error in check expression!!!"); | 168 | throw new Exception ("error in check expression!!!"); |
171 | } | 169 | } |
170 | |||
171 | //should only make a difference if we are filling in variables during generation | ||
172 | //basically, if we are using a strategy | ||
173 | //TODO do this for z3 | ||
174 | if (! hasUnfilledVariable(e, aMatch)) return null; | ||
172 | 175 | ||
173 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | 176 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); |
174 | 177 | ||
@@ -201,6 +204,33 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
201 | 204 | ||
202 | return "(" + operator + " " + left_operand + " " + right_operand + ")"; | 205 | return "(" + operator + " " + left_operand + " " + right_operand + ")"; |
203 | } | 206 | } |
207 | |||
208 | private boolean hasUnfilledVariable(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> m) throws Exception { | ||
209 | |||
210 | if (e instanceof XFeatureCall) { | ||
211 | PrimitiveElement obj = m.get(((XFeatureCall) e).getFeature()); | ||
212 | return !obj.isValueSet(); | ||
213 | } | ||
214 | if (e instanceof XNumberLiteral) return false; | ||
215 | if (e instanceof XBinaryOperation) { | ||
216 | XBinaryOperation ebo = (XBinaryOperation) e; | ||
217 | boolean l = hasUnfilledVariable(ebo.getLeftOperand(), m); | ||
218 | boolean r = hasUnfilledVariable(ebo.getRightOperand(), m); | ||
219 | return (l || r); | ||
220 | } | ||
221 | if (e instanceof XIfExpression) { | ||
222 | XIfExpression ebo = (XIfExpression) e; | ||
223 | boolean i = hasUnfilledVariable(ebo.getIf(), m); | ||
224 | boolean t = hasUnfilledVariable(ebo.getThen(), m); | ||
225 | boolean el = hasUnfilledVariable(ebo.getElse(), m); | ||
226 | return (i || t || el); | ||
227 | } | ||
228 | if (e instanceof XBlockExpression) { | ||
229 | XExpression expr = ((XBlockExpression) e).getExpressions().get(0); | ||
230 | return hasUnfilledVariable(expr, m); | ||
231 | } | ||
232 | throw new Exception(); | ||
233 | } | ||
204 | 234 | ||
205 | private String formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | 235 | private String formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { |
206 | String expr = ""; | 236 | String expr = ""; |
@@ -331,10 +361,13 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
331 | Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); | 361 | Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); |
332 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { | 362 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { |
333 | String constraint = formNumericConstraint(e, aMatch); | 363 | String constraint = formNumericConstraint(e, aMatch); |
334 | String negAssert = "(assert " + constraint + ")"; | 364 | if (constraint != null) { |
335 | curConstraints.add(negAssert); | 365 | String negAssert = "(assert " + constraint + ")"; |
366 | curConstraints.add(negAssert); | ||
367 | } | ||
336 | } | 368 | } |
337 | } | 369 | } |
370 | if (curConstraints.isEmpty()) return null; | ||
338 | //Add content to file | 371 | //Add content to file |
339 | contents.addAll(curVar2Decl.values()); | 372 | contents.addAll(curVar2Decl.values()); |
340 | contents.addAll(curConstraints); | 373 | contents.addAll(curConstraints); |
@@ -374,7 +407,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
374 | long startformingProblem = System.nanoTime(); | 407 | long startformingProblem = System.nanoTime(); |
375 | List<String> numProbContent = formNumericProblemInstance(matches); | 408 | List<String> numProbContent = formNumericProblemInstance(matches); |
376 | endformingProblem = System.nanoTime()-startformingProblem; | 409 | endformingProblem = System.nanoTime()-startformingProblem; |
377 | 410 | ||
411 | if (numProbContent == null) { | ||
412 | endSolvingProblem = 0; | ||
413 | return true; | ||
414 | } | ||
378 | //CALL DREAL | 415 | //CALL DREAL |
379 | long startSolvingProblem = System.nanoTime(); | 416 | long startSolvingProblem = System.nanoTime(); |
380 | 417 | ||
@@ -451,7 +488,10 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
451 | List<String> numProbContent = formNumericProblemInstance(matches); | 488 | List<String> numProbContent = formNumericProblemInstance(matches); |
452 | endformingProblem = System.nanoTime()-startformingProblem; | 489 | endformingProblem = System.nanoTime()-startformingProblem; |
453 | 490 | ||
454 | 491 | if (numProbContent == null) { | |
492 | endSolvingProblem = 0; | ||
493 | return new HashMap<PrimitiveElement, Number>(); | ||
494 | } | ||
455 | //CALL DREAL | 495 | //CALL DREAL |
456 | long startSolvingProblem = System.nanoTime(); | 496 | long startSolvingProblem = System.nanoTime(); |
457 | 497 | ||
@@ -505,9 +545,9 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
505 | if (obj instanceof IntegerElement) { | 545 | if (obj instanceof IntegerElement) { |
506 | sol.put(obj, Integer.parseInt(value)); | 546 | sol.put(obj, Integer.parseInt(value)); |
507 | } else { | 547 | } else { |
508 | double fullVal = Double.parseDouble(value); | 548 | // double fullVal = Double.parseDouble(value) + 0.0005; |
509 | double trimmed = Math.round(fullVal * 1000.0) / 1000.0; | 549 | // double trimmed = Math.round(fullVal * 10000.0) / 10000.0; |
510 | sol.put(obj, trimmed); | 550 | sol.put(obj, Double.parseDouble(value)); |
511 | } | 551 | } |
512 | } | 552 | } |
513 | } else { | 553 | } else { |