diff options
Diffstat (limited to 'Framework/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 | 80 |
1 files changed, 42 insertions, 38 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 7dedfaeb..55d52031 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 | |||
@@ -35,6 +35,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
35 | public class NumericDrealProblemSolver extends NumericProblemSolver{ | 35 | public class NumericDrealProblemSolver extends NumericProblemSolver{ |
36 | 36 | ||
37 | private final String containerName; | 37 | private final String containerName; |
38 | private final String smtFileName = "tmp/smt.smt2"; | ||
38 | private Map<Object, String> varMap; | 39 | private Map<Object, String> varMap; |
39 | private Map<String, String> curVar2Decl; | 40 | private Map<String, String> curVar2Decl; |
40 | 41 | ||
@@ -48,8 +49,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
48 | Arrays.asList("docker", "run", | 49 | Arrays.asList("docker", "run", |
49 | "-id", "--rm", | 50 | "-id", "--rm", |
50 | "--name", containerName, | 51 | "--name", containerName, |
51 | // "-p", "8080:80", | 52 | // "-p", "8080:80", |
52 | "-v", tempDir + ":/mnt", | ||
53 | "dreal/dreal4")); | 53 | "dreal/dreal4")); |
54 | runProcess(startDocker); | 54 | runProcess(startDocker); |
55 | 55 | ||
@@ -58,28 +58,31 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
58 | } | 58 | } |
59 | 59 | ||
60 | private Process runProcess(List<String> cmd) throws IOException, InterruptedException { | 60 | private Process runProcess(List<String> cmd) throws IOException, InterruptedException { |
61 | // println(cmd) | 61 | String s = String.join(" ", cmd); |
62 | ProcessBuilder pb = new ProcessBuilder(cmd); | 62 | Process p = Runtime.getRuntime().exec(s); |
63 | Process p = pb.start(); | ||
64 | // p.waitFor(); | 63 | // p.waitFor(); |
65 | //TODO timeout if needed | 64 | //TODO timeout if needed |
66 | if (!p.waitFor(5, TimeUnit.SECONDS)) { | 65 | if (!p.waitFor(5, TimeUnit.SECONDS)) { |
67 | p.destroy(); | 66 | p.destroy(); |
68 | System.err.println("TIMEOUT"); | 67 | System.err.println("TIMEOUT"); //DEBUG |
69 | } | 68 | } |
70 | return p; | 69 | return p; |
71 | } | 70 | } |
72 | 71 | ||
73 | private Process callDreal(String tempFileName, boolean getModel) throws IOException, InterruptedException { | 72 | private Process callDreal(List<String> numProbContents, boolean getModel) throws IOException, InterruptedException { |
74 | List<String> drealCmd = new ArrayList<String>( | 73 | String numProbContentStr = String.join("\\n", numProbContents); |
75 | Arrays.asList("docker", "exec", | 74 | List<String> drealCmd = new ArrayList<String>(Arrays.asList( |
76 | containerName, | 75 | "docker", "exec", containerName, |
76 | "bash", "-c", | ||
77 | "\""+ "printf", | ||
78 | "\'" + numProbContentStr + "\'", | ||
79 | ">", | ||
80 | smtFileName, | ||
81 | "&&", | ||
77 | "dreal")); | 82 | "dreal")); |
78 | if (getModel) {drealCmd.add("--model");} | 83 | if (getModel) {drealCmd.add("--model");} |
79 | String tmpFileLoc = "mnt/" + tempFileName; | 84 | drealCmd.add(smtFileName + "\""); |
80 | //REMOVE LINE BELOW IF USING WINDOWS | 85 | |
81 | tmpFileLoc = "../" + tmpFileLoc;//ONLY IF USING LINUX | ||
82 | drealCmd.add(tmpFileLoc); | ||
83 | return runProcess(drealCmd); | 86 | return runProcess(drealCmd); |
84 | } | 87 | } |
85 | 88 | ||
@@ -223,18 +226,16 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
223 | return name.startsWith(N_Base) && name.endsWith(end); | 226 | return name.startsWith(N_Base) && name.endsWith(end); |
224 | } | 227 | } |
225 | 228 | ||
226 | private String formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 229 | private List<String> formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
227 | //CREATE SMT2 TEMP FILE | ||
228 | File tempFile = File.createTempFile("smt", ".smt2"); | ||
229 | String tempFileName = tempFile.getName(); | ||
230 | 230 | ||
231 | //STM2 FILE CONTENT CREATION | 231 | //STM2 FILE CONTENT CREATION |
232 | curVar2Decl = new HashMap<String, String>(); | 232 | curVar2Decl = new HashMap<String, String>(); |
233 | List<String> curConstraints = new ArrayList<String>(); | 233 | List<String> curConstraints = new ArrayList<String>(); |
234 | 234 | ||
235 | PrintWriter printer = new PrintWriter(tempFile); | 235 | List<String> contents = new ArrayList<String>(); |
236 | printer.println(";Header comment"); | 236 | contents.add(";Header comment"); |
237 | printer.println("(set-logic QF_NRA)"); | 237 | contents.add("(set-logic QF_NRA)"); |
238 | //For loop below also populates carVar2Decl | ||
238 | for (XExpression e: matches.keySet()) { | 239 | for (XExpression e: matches.keySet()) { |
239 | Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); | 240 | Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e); |
240 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { | 241 | for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) { |
@@ -243,12 +244,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
243 | curConstraints.add(negAssert); | 244 | curConstraints.add(negAssert); |
244 | } | 245 | } |
245 | } | 246 | } |
246 | //Add Content to SMT2 file | 247 | //Add content to file |
247 | for (String varDecl : curVar2Decl.values()) {printer.println(varDecl);} | 248 | contents.addAll(curVar2Decl.values()); |
248 | for (String negAssert : curConstraints) {printer.println(negAssert);} | 249 | contents.addAll(curConstraints); |
249 | printer.println("(check-sat)"); | 250 | contents.add("(check-sat)"); |
250 | printer.close(); | 251 | return contents; |
251 | return tempFileName; | ||
252 | } | 252 | } |
253 | 253 | ||
254 | @SuppressWarnings("unused") | 254 | @SuppressWarnings("unused") |
@@ -278,20 +278,20 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
278 | } | 278 | } |
279 | 279 | ||
280 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 280 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
281 | //CREATE DREAL STM2 FILE at this.tempfile location | 281 | //CREATE DREAL STM2 FILE CONTENTS |
282 | long startformingProblem = System.nanoTime(); | 282 | long startformingProblem = System.nanoTime(); |
283 | String tempFileName = formNumericProblemInstance(matches); | 283 | List<String> numProbContent = formNumericProblemInstance(matches); |
284 | endformingProblem = System.nanoTime()-startformingProblem; | 284 | endformingProblem = System.nanoTime()-startformingProblem; |
285 | 285 | ||
286 | //CALL DREAL | 286 | //CALL DREAL |
287 | long startSolvingProblem = System.nanoTime(); | 287 | long startSolvingProblem = System.nanoTime(); |
288 | Process outputProcess = callDreal(tempFileName, false); | 288 | Process outputProcess = callDreal(numProbContent, false); |
289 | List<List<String>> outputs = getProcessOutput(outputProcess); | 289 | List<List<String>> outputs = getProcessOutput(outputProcess); |
290 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); | 290 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); |
291 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 291 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
292 | 292 | ||
293 | //DEBUG - Print things | 293 | //DEBUG - Print things |
294 | // printFileContent(System.getProperty("java.io.tmpdir") + tempFileName); | 294 | // printOutput(numProbContent); |
295 | // printOutput(outputs.get(0)); | 295 | // printOutput(outputs.get(0)); |
296 | // System.out.println(result); | 296 | // System.out.println(result); |
297 | //END DEBUG | 297 | //END DEBUG |
@@ -318,22 +318,26 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
318 | 318 | ||
319 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 319 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
320 | 320 | ||
321 | |||
322 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); | 321 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); |
323 | //CREATE DREAL STM2 FILE at this.tempfile location | 322 | //CREATE DREAL STM2 FILE at this.tempfile location |
324 | long startformingProblem = System.nanoTime(); | 323 | long startformingProblem = System.nanoTime(); |
325 | String tempFileName = formNumericProblemInstance(matches); | 324 | List<String> numProbContent = formNumericProblemInstance(matches); |
326 | endformingProblem = System.nanoTime()-startformingProblem; | 325 | endformingProblem = System.nanoTime()-startformingProblem; |
327 | 326 | ||
328 | //CALL DREAL | 327 | //CALL DREAL |
329 | long startSolvingProblem = System.nanoTime(); | 328 | long startSolvingProblem = System.nanoTime(); |
330 | Process outputProcess = callDreal(tempFileName, true); | 329 | Process outputProcess = callDreal(numProbContent, true); |
331 | List<List<String>> outputs = getProcessOutput(outputProcess); | 330 | List<List<String>> outputs = getProcessOutput(outputProcess); |
332 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); | 331 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); |
333 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 332 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
334 | |||
335 | //GET SOLUTION | ||
336 | 333 | ||
334 | //DEBUG - Print things | ||
335 | // printOutput(numProbContent); | ||
336 | // printOutput(outputs.get(0)); | ||
337 | // System.out.println(result); | ||
338 | //END DEBUG | ||
339 | |||
340 | //GET SOLUTION | ||
337 | if (result) { | 341 | if (result) { |
338 | long startFormingSolution = System.nanoTime(); | 342 | long startFormingSolution = System.nanoTime(); |
339 | Map<String, String> solMap = parseDrealOutput(outputs.get(0)); | 343 | Map<String, String> solMap = parseDrealOutput(outputs.get(0)); |