diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2020-12-14 15:01:48 -0500 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2020-12-14 15:01:48 -0500 |
commit | 0e9b67c9d7ff3a71792c2727d29f9da6c3259215 (patch) | |
tree | 7b0a9bd39f67731a55c9e9af87a291dc8803d6d6 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic | |
parent | implement isSatisfiable with Dreal integration (diff) | |
download | VIATRA-Generator-0e9b67c9d7ff3a71792c2727d29f9da6c3259215.tar.gz VIATRA-Generator-0e9b67c9d7ff3a71792c2727d29f9da6c3259215.tar.zst VIATRA-Generator-0e9b67c9d7ff3a71792c2727d29f9da6c3259215.zip |
implement getOneSolution with Dreal Integration
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | 130 |
1 files changed, 79 insertions, 51 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 9b9136c7..c71bb53a 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 | |||
@@ -4,7 +4,6 @@ import java.io.BufferedInputStream; | |||
4 | import java.io.BufferedReader; | 4 | import java.io.BufferedReader; |
5 | import java.io.File; | 5 | import java.io.File; |
6 | import java.io.FileInputStream; | 6 | import java.io.FileInputStream; |
7 | import java.io.FileNotFoundException; | ||
8 | import java.io.IOException; | 7 | import java.io.IOException; |
9 | import java.io.InputStream; | 8 | import java.io.InputStream; |
10 | import java.io.InputStreamReader; | 9 | import java.io.InputStreamReader; |
@@ -16,6 +15,8 @@ import java.util.List; | |||
16 | import java.util.Map; | 15 | import java.util.Map; |
17 | import java.util.UUID; | 16 | import java.util.UUID; |
18 | import java.util.concurrent.TimeUnit; | 17 | import java.util.concurrent.TimeUnit; |
18 | import java.util.regex.Matcher; | ||
19 | import java.util.regex.Pattern; | ||
19 | 20 | ||
20 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | 21 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; |
21 | import org.eclipse.xtext.xbase.XBinaryOperation; | 22 | import org.eclipse.xtext.xbase.XBinaryOperation; |
@@ -23,6 +24,9 @@ import org.eclipse.xtext.xbase.XExpression; | |||
23 | import org.eclipse.xtext.xbase.XFeatureCall; | 24 | import org.eclipse.xtext.xbase.XFeatureCall; |
24 | import org.eclipse.xtext.xbase.XNumberLiteral; | 25 | import org.eclipse.xtext.xbase.XNumberLiteral; |
25 | 26 | ||
27 | import com.microsoft.z3.IntExpr; | ||
28 | import com.microsoft.z3.RealExpr; | ||
29 | |||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | 30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; |
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; | 32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; |
@@ -36,6 +40,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
36 | public NumericDrealProblemSolver() throws IOException, InterruptedException { | 40 | public NumericDrealProblemSolver() throws IOException, InterruptedException { |
37 | //setup docker | 41 | //setup docker |
38 | //TODO ENSURE that container name is not already in use???? | 42 | //TODO ENSURE that container name is not already in use???? |
43 | //TODO if dreal/dreal4 image is not downloaded, download it. | ||
39 | File tempDir = new File(System.getProperty("java.io.tmpdir")); | 44 | File tempDir = new File(System.getProperty("java.io.tmpdir")); |
40 | containerName = UUID.randomUUID().toString().replace("-", ""); | 45 | containerName = UUID.randomUUID().toString().replace("-", ""); |
41 | List<String> startDocker = new ArrayList<String>( | 46 | List<String> startDocker = new ArrayList<String>( |
@@ -45,7 +50,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
45 | // "-p", "8080:80", | 50 | // "-p", "8080:80", |
46 | "-v", tempDir + ":/mnt", | 51 | "-v", tempDir + ":/mnt", |
47 | "dreal/dreal4")); | 52 | "dreal/dreal4")); |
48 | Process p = runProcess(startDocker); | 53 | runProcess(startDocker); |
49 | 54 | ||
50 | //setup varmap | 55 | //setup varmap |
51 | varMap = new HashMap<Object, String>(); | 56 | varMap = new HashMap<Object, String>(); |
@@ -63,13 +68,13 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
63 | return p; | 68 | return p; |
64 | } | 69 | } |
65 | 70 | ||
66 | private Process callDreal(String tempFileName) throws IOException, InterruptedException { | 71 | private Process callDreal(String tempFileName, boolean getModel) throws IOException, InterruptedException { |
67 | List<String> drealCmd = new ArrayList<String>( | 72 | List<String> drealCmd = new ArrayList<String>( |
68 | Arrays.asList("docker", "exec", | 73 | Arrays.asList("docker", "exec", |
69 | containerName, | 74 | containerName, |
70 | "dreal", | 75 | "dreal")); |
71 | "--model", | 76 | if (getModel) {drealCmd.add("--model");} |
72 | "mnt/" + tempFileName)); | 77 | drealCmd.add("mnt/" + tempFileName); |
73 | return runProcess(drealCmd); | 78 | return runProcess(drealCmd); |
74 | } | 79 | } |
75 | 80 | ||
@@ -96,9 +101,6 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
96 | //error at dreal-level | 101 | //error at dreal-level |
97 | if (! outputs.get(1).isEmpty()) {printError(outputs.get(1)); return false;} | 102 | if (! outputs.get(1).isEmpty()) {printError(outputs.get(1)); return false;} |
98 | 103 | ||
99 | //print output | ||
100 | // printOutput(outputs.get(0)); | ||
101 | |||
102 | String resultRaw = outputs.get(0).get(0); | 104 | String resultRaw = outputs.get(0).get(0); |
103 | if (resultRaw.startsWith("unsat")) {return false;} | 105 | if (resultRaw.startsWith("unsat")) {return false;} |
104 | if (resultRaw.startsWith("delta-sat")) {return true;} | 106 | if (resultRaw.startsWith("delta-sat")) {return true;} |
@@ -244,6 +246,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
244 | return tempFileName; | 246 | return tempFileName; |
245 | } | 247 | } |
246 | 248 | ||
249 | @SuppressWarnings("unused") | ||
247 | private void printFileContent(String path) throws IOException { | 250 | private void printFileContent(String path) throws IOException { |
248 | InputStream input = new BufferedInputStream(new FileInputStream(path)); | 251 | InputStream input = new BufferedInputStream(new FileInputStream(path)); |
249 | byte[] buffer = new byte[8192]; | 252 | byte[] buffer = new byte[8192]; |
@@ -274,58 +277,83 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
274 | long startformingProblem = System.nanoTime(); | 277 | long startformingProblem = System.nanoTime(); |
275 | String tempFileName = formNumericProblemInstance(matches); | 278 | String tempFileName = formNumericProblemInstance(matches); |
276 | endformingProblem = System.nanoTime()-startformingProblem; | 279 | endformingProblem = System.nanoTime()-startformingProblem; |
277 | |||
278 | // printFileContent(System.getProperty("java.io.tmpdir") + tempFileName); | ||
279 | 280 | ||
280 | //CALL DREAL | 281 | //CALL DREAL |
281 | long startSolvingProblem = System.nanoTime(); | 282 | long startSolvingProblem = System.nanoTime(); |
282 | Process outputProcess = callDreal(tempFileName); | 283 | Process outputProcess = callDreal(tempFileName, false); |
283 | List<List<String>> outputs = getProcessOutput(outputProcess); | 284 | List<List<String>> outputs = getProcessOutput(outputProcess); |
284 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); | 285 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); |
285 | System.out.println(result); | ||
286 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 286 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
287 | //CLOSE | 287 | |
288 | //DEBUG - Print things | ||
289 | // printFileContent(System.getProperty("java.io.tmpdir") + tempFileName); | ||
290 | // printOutput(outputs.get(0)); | ||
291 | System.out.println(result); | ||
292 | //END DEBUG | ||
293 | |||
288 | return result; | 294 | return result; |
289 | } | 295 | } |
296 | |||
297 | private Map<String, String> parseDrealOutput(List<String> output) { | ||
298 | Map<String, String> res = new HashMap<String, String>(); | ||
299 | String re = "(\\w+) : \\[([0-9\\-.e]+), ([0-9\\-.e]+)\\]"; | ||
300 | Pattern p = Pattern.compile(re); | ||
301 | for (String varVal : output) { | ||
302 | Matcher m = p.matcher(varVal); | ||
303 | if (m.matches()) { | ||
304 | String name = m.group(1); | ||
305 | String lowerB = m.group(2); | ||
306 | String upperB = m.group(2); | ||
307 | res.put(name, lowerB); | ||
308 | } | ||
309 | } | ||
310 | return res; | ||
311 | } | ||
312 | |||
290 | 313 | ||
291 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 314 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
292 | // Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); | 315 | |
293 | // long startformingProblem = System.nanoTime(); | 316 | |
294 | // BoolExpr problemInstance = formNumericProblemInstance(matches); | 317 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); |
295 | // endformingProblem = System.nanoTime()-startformingProblem; | 318 | //CREATE DREAL STM2 FILE at this.tempfile location |
296 | // //System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); | 319 | long startformingProblem = System.nanoTime(); |
297 | // s.add(problemInstance); | 320 | String tempFileName = formNumericProblemInstance(matches); |
298 | // long startSolvingProblem = System.nanoTime(); | 321 | endformingProblem = System.nanoTime()-startformingProblem; |
299 | // if (s.check() == Status.SATISFIABLE) { | 322 | |
300 | // Model m = s.getModel(); | 323 | //CALL DREAL |
301 | // endSolvingProblem = System.nanoTime()-startSolvingProblem; | 324 | long startSolvingProblem = System.nanoTime(); |
302 | // //System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); | 325 | Process outputProcess = callDreal(tempFileName, true); |
303 | // long startFormingSolution = System.nanoTime(); | 326 | List<List<String>> outputs = getProcessOutput(outputProcess); |
304 | // for (PrimitiveElement o: objs) { | 327 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); |
305 | // if(varMap.containsKey(o)) { | 328 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
306 | // if (o instanceof IntegerElement) { | 329 | |
307 | // IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); | 330 | //GET SOLUTION |
308 | // Integer oSol = Integer.parseInt(val.toString()); | 331 | |
309 | // sol.put(o, oSol); | 332 | if (result) { |
310 | // } else { | 333 | long startFormingSolution = System.nanoTime(); |
311 | // RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); | 334 | Map<String, String> solMap = parseDrealOutput(outputs.get(0)); |
312 | // Double oSol = Double.parseDouble(val.toString()); | 335 | for (PrimitiveElement obj: objs) { |
313 | // sol.put(o, oSol); | 336 | if(varMap.containsKey(obj)) { |
314 | // } | 337 | if (obj instanceof IntegerElement) { |
315 | // //System.out.println("Solution:" + o + "->" + oSol); | 338 | String varName = varMap.get(obj); |
316 | // | 339 | String value = solMap.get(varName); |
317 | // } else { | 340 | sol.put(obj, Integer.parseInt(value)); |
318 | // //System.out.println("not used var:" + o); | 341 | } else { |
319 | // } | 342 | String varName = varMap.get(obj); |
320 | // } | 343 | String value = solMap.get(varName); |
321 | // endFormingSolution = System.nanoTime()-startFormingSolution; | 344 | sol.put(obj, Integer.parseInt(value)); |
322 | // //System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); | 345 | } |
323 | // } else { | 346 | |
324 | // System.out.println("Unsatisfiable numerical problem"); | 347 | } else { |
325 | // } | 348 | // System.out.println(("variable " + obj + " is not used from Dreal"); |
326 | // this.ctx.close(); | 349 | } |
327 | // return sol; | 350 | } |
328 | return null; | 351 | endFormingSolution = System.nanoTime() - startFormingSolution; |
352 | } | ||
353 | else { | ||
354 | System.out.println("Unsatisfiable numerical problem"); | ||
355 | } | ||
356 | return sol; | ||
329 | } | 357 | } |
330 | 358 | ||
331 | public void teardown() throws IOException, InterruptedException { | 359 | public void teardown() throws IOException, InterruptedException { |