diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | 74 |
1 files changed, 58 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 f6c0bc71..1ce3af06 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 | |||
@@ -7,6 +7,7 @@ import java.io.FileInputStream; | |||
7 | import java.io.IOException; | 7 | 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.util.ArrayList; | 11 | import java.util.ArrayList; |
11 | import java.util.Arrays; | 12 | import java.util.Arrays; |
12 | import java.util.HashMap; | 13 | import java.util.HashMap; |
@@ -28,43 +29,53 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; | 29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; |
29 | 30 | ||
30 | public class NumericDrealProblemSolver extends NumericProblemSolver{ | 31 | public class NumericDrealProblemSolver extends NumericProblemSolver{ |
32 | |||
33 | private final boolean useDocker; | ||
31 | 34 | ||
32 | private final String containerName; | 35 | private String containerName = "<container-name-here>"; |
36 | private String drealLocalPath = "<path-to-dreal-here>"; | ||
33 | private final String smtFileName = "tmp/smt.smt2"; | 37 | private final String smtFileName = "tmp/smt.smt2"; |
34 | private Map<Object, String> varMap; | 38 | private Map<Object, String> varMap; |
35 | private Map<String, String> curVar2Decl; | 39 | private Map<String, String> curVar2Decl; |
40 | |||
41 | private final int TIMEOUT_DOCKER = 5; | ||
42 | private final int TIMEOUT_LOCAL = 2; | ||
36 | 43 | ||
37 | public NumericDrealProblemSolver() throws IOException, InterruptedException { | 44 | public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { |
45 | this.useDocker = useDocker; | ||
46 | this.varMap = new HashMap<Object, String>(); | ||
47 | this.drealLocalPath = drealLocalPath; | ||
48 | |||
49 | if (useDocker) setupDocker(); | ||
50 | } | ||
51 | |||
52 | private void setupDocker() throws IOException, InterruptedException { | ||
38 | //setup docker | 53 | //setup docker |
39 | //TODO ENSURE that container name is not already in use???? | 54 | //TODO ENSURE that container name is not already in use???? |
40 | //TODO if dreal/dreal4 image is not downloaded, download it. | 55 | //TODO if dreal/dreal4 image is not downloaded, download it. |
41 | File tempDir = new File(System.getProperty("java.io.tmpdir")); | 56 | this.containerName = UUID.randomUUID().toString().replace("-", ""); |
42 | containerName = UUID.randomUUID().toString().replace("-", ""); | ||
43 | List<String> startDocker = new ArrayList<String>( | 57 | List<String> startDocker = new ArrayList<String>( |
44 | Arrays.asList("docker", "run", | 58 | Arrays.asList("docker", "run", |
45 | "-id", "--rm", | 59 | "-id", "--rm", |
46 | "--name", containerName, | 60 | "--name", containerName, |
47 | // "-p", "8080:80", | 61 | // "-p", "8080:80", |
48 | "dreal/dreal4")); | 62 | "dreal/dreal4")); |
49 | runProcess(startDocker); | 63 | runProcess(startDocker, TIMEOUT_DOCKER); |
50 | |||
51 | //setup varmap | ||
52 | varMap = new HashMap<Object, String>(); | ||
53 | } | 64 | } |
54 | 65 | ||
55 | private Process runProcess(List<String> cmd) throws IOException, InterruptedException { | 66 | private Process runProcess(List<String> cmd, int timeout) throws IOException, InterruptedException { |
56 | String s = String.join(" ", cmd); | 67 | String s = String.join(" ", cmd); |
57 | Process p = Runtime.getRuntime().exec(s); | 68 | Process p = Runtime.getRuntime().exec(s); |
58 | // p.waitFor(); | 69 | // p.waitFor(); |
59 | //TODO timeout if needed | 70 | //TODO timeout if needed |
60 | if (!p.waitFor(5, TimeUnit.SECONDS)) { | 71 | if (!p.waitFor(timeout, TimeUnit.SECONDS)) { |
61 | p.destroy(); | 72 | p.destroy(); |
62 | System.err.println("TIMEOUT"); //DEBUG | 73 | System.err.println("TIMEOUT"); //DEBUG |
63 | } | 74 | } |
64 | return p; | 75 | return p; |
65 | } | 76 | } |
66 | 77 | ||
67 | private Process callDreal(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { | 78 | private Process callDrealDocker(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { |
68 | String numProbContentStr = String.join("\\n", numProbContents); | 79 | String numProbContentStr = String.join("\\n", numProbContents); |
69 | List<String> drealCmd = new ArrayList<String>(Arrays.asList( | 80 | List<String> drealCmd = new ArrayList<String>(Arrays.asList( |
70 | "docker", "exec", containerName, | 81 | "docker", "exec", containerName, |
@@ -78,7 +89,28 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
78 | if (getModel) {drealCmd.add("--model");} | 89 | if (getModel) {drealCmd.add("--model");} |
79 | drealCmd.add(smtFileName + "\""); | 90 | drealCmd.add(smtFileName + "\""); |
80 | 91 | ||
81 | return runProcess(drealCmd); | 92 | return runProcess(drealCmd, TIMEOUT_DOCKER); |
93 | } | ||
94 | |||
95 | private Process callDrealLocal(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { | ||
96 | //print numProbConents to temp file | ||
97 | File tempFile = File.createTempFile("smt", ".smt2"); | ||
98 | |||
99 | PrintWriter printer = new PrintWriter(tempFile); | ||
100 | for (String s : numProbContents) { | ||
101 | printer.println(s); | ||
102 | } | ||
103 | printer.close(); | ||
104 | |||
105 | //call local dreal with path to temp file | ||
106 | List<String> drealCmd = new ArrayList<String>(); | ||
107 | drealCmd.add(drealLocalPath); | ||
108 | if (getModel) {drealCmd.add("--model");} | ||
109 | drealCmd.add(tempFile.getAbsolutePath()); | ||
110 | |||
111 | System.out.println(drealCmd); | ||
112 | |||
113 | return runProcess(drealCmd, TIMEOUT_LOCAL); | ||
82 | } | 114 | } |
83 | 115 | ||
84 | private List<String> getDrealStream(InputStream stream) throws IOException { | 116 | private List<String> getDrealStream(InputStream stream) throws IOException { |
@@ -262,6 +294,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
262 | } | 294 | } |
263 | } | 295 | } |
264 | 296 | ||
297 | @SuppressWarnings("unused") | ||
265 | private void printOutput(List<String> list) { | 298 | private void printOutput(List<String> list) { |
266 | for (String line : list) { | 299 | for (String line : list) { |
267 | System.out.println(line); | 300 | System.out.println(line); |
@@ -282,7 +315,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
282 | 315 | ||
283 | //CALL DREAL | 316 | //CALL DREAL |
284 | long startSolvingProblem = System.nanoTime(); | 317 | long startSolvingProblem = System.nanoTime(); |
285 | Process outputProcess = callDreal(numProbContent, false); | 318 | |
319 | Process outputProcess; | ||
320 | if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); | ||
321 | else outputProcess = callDrealLocal(numProbContent, false); | ||
322 | |||
286 | List<List<String>> outputs = getProcessOutput(outputProcess); | 323 | List<List<String>> outputs = getProcessOutput(outputProcess); |
287 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); | 324 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); |
288 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 325 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
@@ -320,10 +357,15 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
320 | long startformingProblem = System.nanoTime(); | 357 | long startformingProblem = System.nanoTime(); |
321 | List<String> numProbContent = formNumericProblemInstance(matches); | 358 | List<String> numProbContent = formNumericProblemInstance(matches); |
322 | endformingProblem = System.nanoTime()-startformingProblem; | 359 | endformingProblem = System.nanoTime()-startformingProblem; |
323 | 360 | ||
361 | |||
324 | //CALL DREAL | 362 | //CALL DREAL |
325 | long startSolvingProblem = System.nanoTime(); | 363 | long startSolvingProblem = System.nanoTime(); |
326 | Process outputProcess = callDreal(numProbContent, true); | 364 | |
365 | Process outputProcess; | ||
366 | if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); | ||
367 | else outputProcess = callDrealLocal(numProbContent, false); | ||
368 | |||
327 | List<List<String>> outputs = getProcessOutput(outputProcess); | 369 | List<List<String>> outputs = getProcessOutput(outputProcess); |
328 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); | 370 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); |
329 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 371 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
@@ -373,7 +415,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
373 | public void teardown() throws IOException, InterruptedException { | 415 | public void teardown() throws IOException, InterruptedException { |
374 | List<String> stopDocker = new ArrayList<String>( | 416 | List<String> stopDocker = new ArrayList<String>( |
375 | Arrays.asList("docker", "stop", containerName)); | 417 | Arrays.asList("docker", "stop", containerName)); |
376 | runProcess(stopDocker); | 418 | runProcess(stopDocker, TIMEOUT_DOCKER); |
377 | //TODO Check if above went well? | 419 | //TODO Check if above went well? |
378 | } | 420 | } |
379 | 421 | ||