From 953227f62ece22f06bc54a47eeec8bf79b25dc27 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 19 Jan 2021 12:46:58 +0100 Subject: add Actor+CollisionExists constrs & adjust dreal parser & measurements --- .../viatra2logic/NumericDrealProblemSolver.java | 52 +++++++++++++++------- 1 file changed, 36 insertions(+), 16 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src') 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 1ce3af06..30e68260 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 @@ -23,6 +23,7 @@ import org.eclipse.xtext.xbase.XBinaryOperation; import org.eclipse.xtext.xbase.XExpression; import org.eclipse.xtext.xbase.XFeatureCall; import org.eclipse.xtext.xbase.XNumberLiteral; +import org.eclipse.xtext.xbase.XUnaryOperation; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; @@ -35,6 +36,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ private String containerName = ""; private String drealLocalPath = ""; private final String smtFileName = "tmp/smt.smt2"; + private final File localTempFile = File.createTempFile("smt", ".smt2"); private Map varMap; private Map curVar2Decl; @@ -76,11 +78,12 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } private Process callDrealDocker(List numProbContents, boolean getModel) throws IOException, InterruptedException { + //TODO currently not working for Linux String numProbContentStr = String.join("\\n", numProbContents); List drealCmd = new ArrayList(Arrays.asList( "docker", "exec", containerName, "bash", "-c", - "\""+ "printf", + "\"printf " + "\'" + numProbContentStr + "\'", ">", smtFileName, @@ -89,14 +92,14 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ if (getModel) {drealCmd.add("--model");} drealCmd.add(smtFileName + "\""); +// System.out.println(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); + PrintWriter printer = new PrintWriter(localTempFile); for (String s : numProbContents) { printer.println(s); } @@ -106,9 +109,9 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ List drealCmd = new ArrayList(); drealCmd.add(drealLocalPath); if (getModel) {drealCmd.add("--model");} - drealCmd.add(tempFile.getAbsolutePath()); + drealCmd.add(localTempFile.getAbsolutePath()); - System.out.println(drealCmd); +// System.out.println(drealCmd); return runProcess(drealCmd, TIMEOUT_LOCAL); } @@ -244,6 +247,13 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } expr = "(" + operator + " " + left_operand + " " + right_operand + ")"; + } + else if (e instanceof XUnaryOperation){ + String name = ((XUnaryOperation) e).getFeature().getQualifiedName(); + System.out.println(name); + String op = ((XUnaryOperation) e).getOperand().toString(); + System.out.println(op); + throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); } else { throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); } @@ -327,7 +337,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ //DEBUG - Print things // printOutput(numProbContent); // printOutput(outputs.get(0)); -// System.out.println(result); + System.out.println(result); //END DEBUG return result; @@ -335,15 +345,25 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ private Map parseDrealOutput(List output) { Map res = new HashMap(); - String re = "(\\w+) : \\[([0-9\\-+.e]+), ([0-9\\-+.e]+)\\]"; - Pattern p = Pattern.compile(re); + String re1 = "(\\w+) : \\[([0-9\\-+.e]+), ([0-9\\-+.e]+)\\]"; + Pattern p1 = Pattern.compile(re1); + String re2 = "(\\w+) : <([0-9\\-+.e]+), ([0-9\\-+.e]+)>"; + Pattern p2 = Pattern.compile(re2); 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); + Matcher m1 = p1.matcher(varVal); + Matcher m2 = p2.matcher(varVal); + if (m1.matches()) { + String name = m1.group(1); + String lowerB = m1.group(2); + String upperB = m1.group(3); res.put(name, lowerB); + } else { + if (m2.matches()) { + String name = m2.group(1); + String lowerB = m2.group(2); + String upperB = m2.group(3); + res.put(name, lowerB); + } } } return res; @@ -363,8 +383,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ long startSolvingProblem = System.nanoTime(); Process outputProcess; - if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); - else outputProcess = callDrealLocal(numProbContent, false); + if (this.useDocker) outputProcess = callDrealDocker(numProbContent, true); + else outputProcess = callDrealLocal(numProbContent, true); List> outputs = getProcessOutput(outputProcess); boolean result = getDrealResult(outputProcess.exitValue(), outputs); -- cgit v1.2.3-54-g00ecf