From f67986e33257ef1cc6df95f04ca93a372654cb30 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Sat, 9 Jan 2021 23:11:54 -0500 Subject: remove local-docker file transfer --- .../viatra2logic/NumericDrealProblemSolver.java | 80 ++++++++++++---------- 1 file 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 public class NumericDrealProblemSolver extends NumericProblemSolver{ private final String containerName; + private final String smtFileName = "tmp/smt.smt2"; private Map varMap; private Map curVar2Decl; @@ -48,8 +49,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ Arrays.asList("docker", "run", "-id", "--rm", "--name", containerName, -// "-p", "8080:80", - "-v", tempDir + ":/mnt", +// "-p", "8080:80", "dreal/dreal4")); runProcess(startDocker); @@ -58,28 +58,31 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } private Process runProcess(List cmd) throws IOException, InterruptedException { -// println(cmd) - ProcessBuilder pb = new ProcessBuilder(cmd); - Process p = pb.start(); + String s = String.join(" ", cmd); + Process p = Runtime.getRuntime().exec(s); // p.waitFor(); //TODO timeout if needed if (!p.waitFor(5, TimeUnit.SECONDS)) { p.destroy(); - System.err.println("TIMEOUT"); + System.err.println("TIMEOUT"); //DEBUG } return p; } - private Process callDreal(String tempFileName, boolean getModel) throws IOException, InterruptedException { - List drealCmd = new ArrayList( - Arrays.asList("docker", "exec", - containerName, + private Process callDreal(List numProbContents, boolean getModel) throws IOException, InterruptedException { + String numProbContentStr = String.join("\\n", numProbContents); + List drealCmd = new ArrayList(Arrays.asList( + "docker", "exec", containerName, + "bash", "-c", + "\""+ "printf", + "\'" + numProbContentStr + "\'", + ">", + smtFileName, + "&&", "dreal")); if (getModel) {drealCmd.add("--model");} - String tmpFileLoc = "mnt/" + tempFileName; - //REMOVE LINE BELOW IF USING WINDOWS - tmpFileLoc = "../" + tmpFileLoc;//ONLY IF USING LINUX - drealCmd.add(tmpFileLoc); + drealCmd.add(smtFileName + "\""); + return runProcess(drealCmd); } @@ -223,18 +226,16 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ return name.startsWith(N_Base) && name.endsWith(end); } - private String formNumericProblemInstance(Map>> matches) throws Exception { - //CREATE SMT2 TEMP FILE - File tempFile = File.createTempFile("smt", ".smt2"); - String tempFileName = tempFile.getName(); + private List formNumericProblemInstance(Map>> matches) throws Exception { //STM2 FILE CONTENT CREATION curVar2Decl = new HashMap(); List curConstraints = new ArrayList(); - PrintWriter printer = new PrintWriter(tempFile); - printer.println(";Header comment"); - printer.println("(set-logic QF_NRA)"); + List contents = new ArrayList(); + contents.add(";Header comment"); + contents.add("(set-logic QF_NRA)"); + //For loop below also populates carVar2Decl for (XExpression e: matches.keySet()) { Iterable> matchSets = matches.get(e); for (Map aMatch: matchSets) { @@ -243,12 +244,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ curConstraints.add(negAssert); } } - //Add Content to SMT2 file - for (String varDecl : curVar2Decl.values()) {printer.println(varDecl);} - for (String negAssert : curConstraints) {printer.println(negAssert);} - printer.println("(check-sat)"); - printer.close(); - return tempFileName; + //Add content to file + contents.addAll(curVar2Decl.values()); + contents.addAll(curConstraints); + contents.add("(check-sat)"); + return contents; } @SuppressWarnings("unused") @@ -278,20 +278,20 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } public boolean isSatisfiable(Map>> matches) throws Exception { - //CREATE DREAL STM2 FILE at this.tempfile location + //CREATE DREAL STM2 FILE CONTENTS long startformingProblem = System.nanoTime(); - String tempFileName = formNumericProblemInstance(matches); + List numProbContent = formNumericProblemInstance(matches); endformingProblem = System.nanoTime()-startformingProblem; - //CALL DREAL + //CALL DREAL long startSolvingProblem = System.nanoTime(); - Process outputProcess = callDreal(tempFileName, false); + Process outputProcess = callDreal(numProbContent, false); List> outputs = getProcessOutput(outputProcess); boolean result = getDrealResult(outputProcess.exitValue(), outputs); endSolvingProblem = System.nanoTime()-startSolvingProblem; //DEBUG - Print things -// printFileContent(System.getProperty("java.io.tmpdir") + tempFileName); +// printOutput(numProbContent); // printOutput(outputs.get(0)); // System.out.println(result); //END DEBUG @@ -318,22 +318,26 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ public Map getOneSolution(List objs, Map>> matches) throws Exception { - Map sol = new HashMap(); //CREATE DREAL STM2 FILE at this.tempfile location long startformingProblem = System.nanoTime(); - String tempFileName = formNumericProblemInstance(matches); + List numProbContent = formNumericProblemInstance(matches); endformingProblem = System.nanoTime()-startformingProblem; - //CALL DREAL + //CALL DREAL long startSolvingProblem = System.nanoTime(); - Process outputProcess = callDreal(tempFileName, true); + Process outputProcess = callDreal(numProbContent, true); List> outputs = getProcessOutput(outputProcess); boolean result = getDrealResult(outputProcess.exitValue(), outputs); endSolvingProblem = System.nanoTime()-startSolvingProblem; - - //GET SOLUTION + //DEBUG - Print things +// printOutput(numProbContent); +// printOutput(outputs.get(0)); +// System.out.println(result); + //END DEBUG + + //GET SOLUTION if (result) { long startFormingSolution = System.nanoTime(); Map solMap = parseDrealOutput(outputs.get(0)); -- cgit v1.2.3