From 598fa1dae639ac110b2f549e8c2978ae3974c53a Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 19 Jan 2021 01:15:32 +0100 Subject: add vsconfig flag to allow running dreal locally --- .../viatra2logic/NumericDrealProblemSolver.java | 74 +++++++++++++++++----- 1 file changed, 58 insertions(+), 16 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme') 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; import java.io.IOException; import java.io.InputStream; import java.io.InputStreamReader; +import java.io.PrintWriter; import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; @@ -28,43 +29,53 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; public class NumericDrealProblemSolver extends NumericProblemSolver{ + + private final boolean useDocker; - private final String containerName; + private String containerName = ""; + private String drealLocalPath = ""; private final String smtFileName = "tmp/smt.smt2"; private Map varMap; private Map curVar2Decl; + + private final int TIMEOUT_DOCKER = 5; + private final int TIMEOUT_LOCAL = 2; - public NumericDrealProblemSolver() throws IOException, InterruptedException { + public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { + this.useDocker = useDocker; + this.varMap = new HashMap(); + this.drealLocalPath = drealLocalPath; + + if (useDocker) setupDocker(); + } + + private void setupDocker() throws IOException, InterruptedException { //setup docker //TODO ENSURE that container name is not already in use???? //TODO if dreal/dreal4 image is not downloaded, download it. - File tempDir = new File(System.getProperty("java.io.tmpdir")); - containerName = UUID.randomUUID().toString().replace("-", ""); + this.containerName = UUID.randomUUID().toString().replace("-", ""); List startDocker = new ArrayList( Arrays.asList("docker", "run", "-id", "--rm", "--name", containerName, // "-p", "8080:80", "dreal/dreal4")); - runProcess(startDocker); - - //setup varmap - varMap = new HashMap(); + runProcess(startDocker, TIMEOUT_DOCKER); } - private Process runProcess(List cmd) throws IOException, InterruptedException { + private Process runProcess(List cmd, int timeout) throws IOException, InterruptedException { String s = String.join(" ", cmd); Process p = Runtime.getRuntime().exec(s); // p.waitFor(); //TODO timeout if needed - if (!p.waitFor(5, TimeUnit.SECONDS)) { + if (!p.waitFor(timeout, TimeUnit.SECONDS)) { p.destroy(); System.err.println("TIMEOUT"); //DEBUG } return p; } - private Process callDreal(List numProbContents, boolean getModel) throws IOException, InterruptedException { + private Process callDrealDocker(List numProbContents, boolean getModel) throws IOException, InterruptedException { String numProbContentStr = String.join("\\n", numProbContents); List drealCmd = new ArrayList(Arrays.asList( "docker", "exec", containerName, @@ -78,7 +89,28 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ if (getModel) {drealCmd.add("--model");} drealCmd.add(smtFileName + "\""); - return runProcess(drealCmd); + return runProcess(drealCmd, TIMEOUT_DOCKER); + } + + private Process callDrealLocal(List numProbContents, boolean getModel) throws IOException, InterruptedException { + //print numProbConents to temp file + File tempFile = File.createTempFile("smt", ".smt2"); + + PrintWriter printer = new PrintWriter(tempFile); + for (String s : numProbContents) { + printer.println(s); + } + printer.close(); + + //call local dreal with path to temp file + List drealCmd = new ArrayList(); + drealCmd.add(drealLocalPath); + if (getModel) {drealCmd.add("--model");} + drealCmd.add(tempFile.getAbsolutePath()); + + System.out.println(drealCmd); + + return runProcess(drealCmd, TIMEOUT_LOCAL); } private List getDrealStream(InputStream stream) throws IOException { @@ -262,6 +294,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } } + @SuppressWarnings("unused") private void printOutput(List list) { for (String line : list) { System.out.println(line); @@ -282,7 +315,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ //CALL DREAL long startSolvingProblem = System.nanoTime(); - Process outputProcess = callDreal(numProbContent, false); + + Process outputProcess; + if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); + else outputProcess = callDrealLocal(numProbContent, false); + List> outputs = getProcessOutput(outputProcess); boolean result = getDrealResult(outputProcess.exitValue(), outputs); endSolvingProblem = System.nanoTime()-startSolvingProblem; @@ -320,10 +357,15 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ long startformingProblem = System.nanoTime(); List numProbContent = formNumericProblemInstance(matches); endformingProblem = System.nanoTime()-startformingProblem; - + + //CALL DREAL long startSolvingProblem = System.nanoTime(); - Process outputProcess = callDreal(numProbContent, true); + + Process outputProcess; + if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); + else outputProcess = callDrealLocal(numProbContent, false); + List> outputs = getProcessOutput(outputProcess); boolean result = getDrealResult(outputProcess.exitValue(), outputs); endSolvingProblem = System.nanoTime()-startSolvingProblem; @@ -373,7 +415,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ public void teardown() throws IOException, InterruptedException { List stopDocker = new ArrayList( Arrays.asList("docker", "stop", containerName)); - runProcess(stopDocker); + runProcess(stopDocker, TIMEOUT_DOCKER); //TODO Check if above went well? } -- cgit v1.2.3-54-g00ecf