From 0e9b67c9d7ff3a71792c2727d29f9da6c3259215 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Mon, 14 Dec 2020 15:01:48 -0500 Subject: implement getOneSolution with Dreal Integration --- .../viatra2logic/NumericDrealProblemSolver.java | 130 +++++++++++++-------- 1 file changed, 79 insertions(+), 51 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 9b9136c7..c71bb53a 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 @@ -4,7 +4,6 @@ import java.io.BufferedInputStream; import java.io.BufferedReader; import java.io.File; import java.io.FileInputStream; -import java.io.FileNotFoundException; import java.io.IOException; import java.io.InputStream; import java.io.InputStreamReader; @@ -16,6 +15,8 @@ import java.util.List; import java.util.Map; import java.util.UUID; import java.util.concurrent.TimeUnit; +import java.util.regex.Matcher; +import java.util.regex.Pattern; import org.eclipse.xtext.common.types.JvmIdentifiableElement; import org.eclipse.xtext.xbase.XBinaryOperation; @@ -23,6 +24,9 @@ import org.eclipse.xtext.xbase.XExpression; import org.eclipse.xtext.xbase.XFeatureCall; import org.eclipse.xtext.xbase.XNumberLiteral; +import com.microsoft.z3.IntExpr; +import com.microsoft.z3.RealExpr; + import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; @@ -36,6 +40,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ public NumericDrealProblemSolver() 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("-", ""); List startDocker = new ArrayList( @@ -45,7 +50,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ // "-p", "8080:80", "-v", tempDir + ":/mnt", "dreal/dreal4")); - Process p = runProcess(startDocker); + runProcess(startDocker); //setup varmap varMap = new HashMap(); @@ -63,13 +68,13 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ return p; } - private Process callDreal(String tempFileName) throws IOException, InterruptedException { + private Process callDreal(String tempFileName, boolean getModel) throws IOException, InterruptedException { List drealCmd = new ArrayList( Arrays.asList("docker", "exec", containerName, - "dreal", - "--model", - "mnt/" + tempFileName)); + "dreal")); + if (getModel) {drealCmd.add("--model");} + drealCmd.add("mnt/" + tempFileName); return runProcess(drealCmd); } @@ -96,9 +101,6 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ //error at dreal-level if (! outputs.get(1).isEmpty()) {printError(outputs.get(1)); return false;} - //print output -// printOutput(outputs.get(0)); - String resultRaw = outputs.get(0).get(0); if (resultRaw.startsWith("unsat")) {return false;} if (resultRaw.startsWith("delta-sat")) {return true;} @@ -244,6 +246,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ return tempFileName; } + @SuppressWarnings("unused") private void printFileContent(String path) throws IOException { InputStream input = new BufferedInputStream(new FileInputStream(path)); byte[] buffer = new byte[8192]; @@ -274,58 +277,83 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ long startformingProblem = System.nanoTime(); String tempFileName = formNumericProblemInstance(matches); endformingProblem = System.nanoTime()-startformingProblem; - -// printFileContent(System.getProperty("java.io.tmpdir") + tempFileName); //CALL DREAL long startSolvingProblem = System.nanoTime(); - Process outputProcess = callDreal(tempFileName); + Process outputProcess = callDreal(tempFileName, false); List> outputs = getProcessOutput(outputProcess); boolean result = getDrealResult(outputProcess.exitValue(), outputs); - System.out.println(result); endSolvingProblem = System.nanoTime()-startSolvingProblem; - //CLOSE + + //DEBUG - Print things +// printFileContent(System.getProperty("java.io.tmpdir") + tempFileName); +// printOutput(outputs.get(0)); + System.out.println(result); + //END DEBUG + return result; } + + private Map parseDrealOutput(List output) { + Map res = new HashMap(); + String re = "(\\w+) : \\[([0-9\\-.e]+), ([0-9\\-.e]+)\\]"; + Pattern p = Pattern.compile(re); + for (String varVal : output) { + Matcher m = p.matcher(varVal); + if (m.matches()) { + String name = m.group(1); + String lowerB = m.group(2); + String upperB = m.group(2); + res.put(name, lowerB); + } + } + return res; + } + public Map getOneSolution(List objs, Map>> matches) throws Exception { -// Map sol = new HashMap(); -// long startformingProblem = System.nanoTime(); -// BoolExpr problemInstance = formNumericProblemInstance(matches); -// endformingProblem = System.nanoTime()-startformingProblem; -// //System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); -// s.add(problemInstance); -// long startSolvingProblem = System.nanoTime(); -// if (s.check() == Status.SATISFIABLE) { -// Model m = s.getModel(); -// endSolvingProblem = System.nanoTime()-startSolvingProblem; -// //System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); -// long startFormingSolution = System.nanoTime(); -// for (PrimitiveElement o: objs) { -// if(varMap.containsKey(o)) { -// if (o instanceof IntegerElement) { -// IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); -// Integer oSol = Integer.parseInt(val.toString()); -// sol.put(o, oSol); -// } else { -// RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); -// Double oSol = Double.parseDouble(val.toString()); -// sol.put(o, oSol); -// } -// //System.out.println("Solution:" + o + "->" + oSol); -// -// } else { -// //System.out.println("not used var:" + o); -// } -// } -// endFormingSolution = System.nanoTime()-startFormingSolution; -// //System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); -// } else { -// System.out.println("Unsatisfiable numerical problem"); -// } -// this.ctx.close(); -// return sol; - return null; + + + Map sol = new HashMap(); + //CREATE DREAL STM2 FILE at this.tempfile location + long startformingProblem = System.nanoTime(); + String tempFileName = formNumericProblemInstance(matches); + endformingProblem = System.nanoTime()-startformingProblem; + + //CALL DREAL + long startSolvingProblem = System.nanoTime(); + Process outputProcess = callDreal(tempFileName, true); + List> outputs = getProcessOutput(outputProcess); + boolean result = getDrealResult(outputProcess.exitValue(), outputs); + endSolvingProblem = System.nanoTime()-startSolvingProblem; + + //GET SOLUTION + + if (result) { + long startFormingSolution = System.nanoTime(); + Map solMap = parseDrealOutput(outputs.get(0)); + for (PrimitiveElement obj: objs) { + if(varMap.containsKey(obj)) { + if (obj instanceof IntegerElement) { + String varName = varMap.get(obj); + String value = solMap.get(varName); + sol.put(obj, Integer.parseInt(value)); + } else { + String varName = varMap.get(obj); + String value = solMap.get(varName); + sol.put(obj, Integer.parseInt(value)); + } + + } else { +// System.out.println(("variable " + obj + " is not used from Dreal"); + } + } + endFormingSolution = System.nanoTime() - startFormingSolution; + } + else { + System.out.println("Unsatisfiable numerical problem"); + } + return sol; } public void teardown() throws IOException, InterruptedException { -- cgit v1.2.3-54-g00ecf