diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-19 12:46:58 +0100 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-19 12:46:58 +0100 |
commit | 953227f62ece22f06bc54a47eeec8bf79b25dc27 (patch) | |
tree | 72bf39c26b2e58bd5ac4ba0506cf78608e80c309 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner | |
parent | add vsconfig flag to allow running dreal locally (diff) | |
download | VIATRA-Generator-953227f62ece22f06bc54a47eeec8bf79b25dc27.tar.gz VIATRA-Generator-953227f62ece22f06bc54a47eeec8bf79b25dc27.tar.zst VIATRA-Generator-953227f62ece22f06bc54a47eeec8bf79b25dc27.zip |
add Actor+CollisionExists constrs & adjust dreal parser & measurements
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | 52 |
1 files changed, 36 insertions, 16 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 1ce3af06..30e68260 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 | |||
@@ -23,6 +23,7 @@ import org.eclipse.xtext.xbase.XBinaryOperation; | |||
23 | import org.eclipse.xtext.xbase.XExpression; | 23 | import org.eclipse.xtext.xbase.XExpression; |
24 | import org.eclipse.xtext.xbase.XFeatureCall; | 24 | import org.eclipse.xtext.xbase.XFeatureCall; |
25 | import org.eclipse.xtext.xbase.XNumberLiteral; | 25 | import org.eclipse.xtext.xbase.XNumberLiteral; |
26 | import org.eclipse.xtext.xbase.XUnaryOperation; | ||
26 | 27 | ||
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | 28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; |
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
@@ -35,6 +36,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
35 | private String containerName = "<container-name-here>"; | 36 | private String containerName = "<container-name-here>"; |
36 | private String drealLocalPath = "<path-to-dreal-here>"; | 37 | private String drealLocalPath = "<path-to-dreal-here>"; |
37 | private final String smtFileName = "tmp/smt.smt2"; | 38 | private final String smtFileName = "tmp/smt.smt2"; |
39 | private final File localTempFile = File.createTempFile("smt", ".smt2"); | ||
38 | private Map<Object, String> varMap; | 40 | private Map<Object, String> varMap; |
39 | private Map<String, String> curVar2Decl; | 41 | private Map<String, String> curVar2Decl; |
40 | 42 | ||
@@ -76,11 +78,12 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
76 | } | 78 | } |
77 | 79 | ||
78 | private Process callDrealDocker(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { | 80 | private Process callDrealDocker(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { |
81 | //TODO currently not working for Linux | ||
79 | String numProbContentStr = String.join("\\n", numProbContents); | 82 | String numProbContentStr = String.join("\\n", numProbContents); |
80 | List<String> drealCmd = new ArrayList<String>(Arrays.asList( | 83 | List<String> drealCmd = new ArrayList<String>(Arrays.asList( |
81 | "docker", "exec", containerName, | 84 | "docker", "exec", containerName, |
82 | "bash", "-c", | 85 | "bash", "-c", |
83 | "\""+ "printf", | 86 | "\"printf " + |
84 | "\'" + numProbContentStr + "\'", | 87 | "\'" + numProbContentStr + "\'", |
85 | ">", | 88 | ">", |
86 | smtFileName, | 89 | smtFileName, |
@@ -89,14 +92,14 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
89 | if (getModel) {drealCmd.add("--model");} | 92 | if (getModel) {drealCmd.add("--model");} |
90 | drealCmd.add(smtFileName + "\""); | 93 | drealCmd.add(smtFileName + "\""); |
91 | 94 | ||
95 | // System.out.println(drealCmd); | ||
96 | // | ||
92 | return runProcess(drealCmd, TIMEOUT_DOCKER); | 97 | return runProcess(drealCmd, TIMEOUT_DOCKER); |
93 | } | 98 | } |
94 | 99 | ||
95 | private Process callDrealLocal(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { | 100 | private Process callDrealLocal(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { |
96 | //print numProbConents to temp file | 101 | //print numProbConents to temp file |
97 | File tempFile = File.createTempFile("smt", ".smt2"); | 102 | PrintWriter printer = new PrintWriter(localTempFile); |
98 | |||
99 | PrintWriter printer = new PrintWriter(tempFile); | ||
100 | for (String s : numProbContents) { | 103 | for (String s : numProbContents) { |
101 | printer.println(s); | 104 | printer.println(s); |
102 | } | 105 | } |
@@ -106,9 +109,9 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
106 | List<String> drealCmd = new ArrayList<String>(); | 109 | List<String> drealCmd = new ArrayList<String>(); |
107 | drealCmd.add(drealLocalPath); | 110 | drealCmd.add(drealLocalPath); |
108 | if (getModel) {drealCmd.add("--model");} | 111 | if (getModel) {drealCmd.add("--model");} |
109 | drealCmd.add(tempFile.getAbsolutePath()); | 112 | drealCmd.add(localTempFile.getAbsolutePath()); |
110 | 113 | ||
111 | System.out.println(drealCmd); | 114 | // System.out.println(drealCmd); |
112 | 115 | ||
113 | return runProcess(drealCmd, TIMEOUT_LOCAL); | 116 | return runProcess(drealCmd, TIMEOUT_LOCAL); |
114 | } | 117 | } |
@@ -244,6 +247,13 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
244 | } | 247 | } |
245 | 248 | ||
246 | expr = "(" + operator + " " + left_operand + " " + right_operand + ")"; | 249 | expr = "(" + operator + " " + left_operand + " " + right_operand + ")"; |
250 | } | ||
251 | else if (e instanceof XUnaryOperation){ | ||
252 | String name = ((XUnaryOperation) e).getFeature().getQualifiedName(); | ||
253 | System.out.println(name); | ||
254 | String op = ((XUnaryOperation) e).getOperand().toString(); | ||
255 | System.out.println(op); | ||
256 | throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); | ||
247 | } else { | 257 | } else { |
248 | throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); | 258 | throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); |
249 | } | 259 | } |
@@ -327,7 +337,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
327 | //DEBUG - Print things | 337 | //DEBUG - Print things |
328 | // printOutput(numProbContent); | 338 | // printOutput(numProbContent); |
329 | // printOutput(outputs.get(0)); | 339 | // printOutput(outputs.get(0)); |
330 | // System.out.println(result); | 340 | System.out.println(result); |
331 | //END DEBUG | 341 | //END DEBUG |
332 | 342 | ||
333 | return result; | 343 | return result; |
@@ -335,15 +345,25 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
335 | 345 | ||
336 | private Map<String, String> parseDrealOutput(List<String> output) { | 346 | private Map<String, String> parseDrealOutput(List<String> output) { |
337 | Map<String, String> res = new HashMap<String, String>(); | 347 | Map<String, String> res = new HashMap<String, String>(); |
338 | String re = "(\\w+) : \\[([0-9\\-+.e]+), ([0-9\\-+.e]+)\\]"; | 348 | String re1 = "(\\w+) : \\[([0-9\\-+.e]+), ([0-9\\-+.e]+)\\]"; |
339 | Pattern p = Pattern.compile(re); | 349 | Pattern p1 = Pattern.compile(re1); |
350 | String re2 = "(\\w+) : <([0-9\\-+.e]+), ([0-9\\-+.e]+)>"; | ||
351 | Pattern p2 = Pattern.compile(re2); | ||
340 | for (String varVal : output) { | 352 | for (String varVal : output) { |
341 | Matcher m = p.matcher(varVal); | 353 | Matcher m1 = p1.matcher(varVal); |
342 | if (m.matches()) { | 354 | Matcher m2 = p2.matcher(varVal); |
343 | String name = m.group(1); | 355 | if (m1.matches()) { |
344 | String lowerB = m.group(2); | 356 | String name = m1.group(1); |
345 | String upperB = m.group(2); | 357 | String lowerB = m1.group(2); |
358 | String upperB = m1.group(3); | ||
346 | res.put(name, lowerB); | 359 | res.put(name, lowerB); |
360 | } else { | ||
361 | if (m2.matches()) { | ||
362 | String name = m2.group(1); | ||
363 | String lowerB = m2.group(2); | ||
364 | String upperB = m2.group(3); | ||
365 | res.put(name, lowerB); | ||
366 | } | ||
347 | } | 367 | } |
348 | } | 368 | } |
349 | return res; | 369 | return res; |
@@ -363,8 +383,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
363 | long startSolvingProblem = System.nanoTime(); | 383 | long startSolvingProblem = System.nanoTime(); |
364 | 384 | ||
365 | Process outputProcess; | 385 | Process outputProcess; |
366 | if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); | 386 | if (this.useDocker) outputProcess = callDrealDocker(numProbContent, true); |
367 | else outputProcess = callDrealLocal(numProbContent, false); | 387 | else outputProcess = callDrealLocal(numProbContent, true); |
368 | 388 | ||
369 | List<List<String>> outputs = getProcessOutput(outputProcess); | 389 | List<List<String>> outputs = getProcessOutput(outputProcess); |
370 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); | 390 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); |