aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-01-09 23:11:54 -0500
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-01-09 23:11:54 -0500
commitf67986e33257ef1cc6df95f04ca93a372654cb30 (patch)
tree12fcdcab045972198db4c728e7b2802a1e5672f0
parentfix dup decl bug + adjust famTree case study (diff)
downloadVIATRA-Generator-f67986e33257ef1cc6df95f04ca93a372654cb30.tar.gz
VIATRA-Generator-f67986e33257ef1cc6df95f04ca93a372654cb30.tar.zst
VIATRA-Generator-f67986e33257ef1cc6df95f04ca93a372654cb30.zip
remove local-docker file transfer
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java80
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
35public class NumericDrealProblemSolver extends NumericProblemSolver{ 35public 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));