aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-15 07:42:02 +0100
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-15 07:42:02 +0100
commit0c56d765b120654bfd3534aa5b6d12476070515b (patch)
tree10a01c11769364116061e33fda4167db68a4c8be
parentfinished first impl that works sometimes (issue w/ SAT in Dreal rerun) (diff)
downloadVIATRA-Generator-0c56d765b120654bfd3534aa5b6d12476070515b.tar.gz
VIATRA-Generator-0c56d765b120654bfd3534aa5b6d12476070515b.tar.zst
VIATRA-Generator-0c56d765b120654bfd3534aa5b6d12476070515b.zip
fix dreal call on solved problem imprecision issue
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java58
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend7
2 files changed, 54 insertions, 11 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;
8import java.io.InputStream; 8import java.io.InputStream;
9import java.io.InputStreamReader; 9import java.io.InputStreamReader;
10import java.io.PrintWriter; 10import java.io.PrintWriter;
11import java.text.DecimalFormat;
12import java.util.ArrayList; 11import java.util.ArrayList;
13import java.util.Arrays; 12import java.util.Arrays;
14import java.util.HashMap; 13import 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 {
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 bb2c7dbf..44964079 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
@@ -131,7 +131,6 @@ class NumericSolver {
131 } 131 }
132 def boolean currentSatisfiable() { 132 def boolean currentSatisfiable() {
133 val int phase = determinePhase() 133 val int phase = determinePhase()
134 //TODO generalize this
135 isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) 134 isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase)
136 } 135 }
137 136
@@ -223,7 +222,11 @@ class NumericSolver {
223 } 222 }
224 } 223 }
225 this.runtime+=System.nanoTime-start 224 this.runtime+=System.nanoTime-start
226 if (phase == 2) finalResult = isSatisfiable(matches, 3) 225 //STRATEGY
226 if (phase == 2) {
227 if (!finalResult) return finalResult
228 else finalResult = isSatisfiable(matches, 3)
229 }
227 return finalResult 230 return finalResult
228 } 231 }
229 232