From 6dfdda9b3a6764cf5e4b5fc4303a49bb80193c5a Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Mon, 14 Dec 2020 03:27:43 -0500 Subject: implement isSatisfiable with Dreal integration --- .../viatra2logic/NumericDrealProblemSolver.java | 420 +++++++++++---------- 1 file changed, 229 insertions(+), 191 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java') 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 1e5742b7..9b9136c7 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 @@ -1,7 +1,10 @@ package hu.bme.mit.inf.dslreasoner.viatra2logic; +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; @@ -12,55 +15,37 @@ import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.UUID; +import java.util.concurrent.TimeUnit; import org.eclipse.xtext.common.types.JvmIdentifiableElement; +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 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; public class NumericDrealProblemSolver extends NumericProblemSolver{ - private static final String N_Base = "org.eclipse.xtext.xbase.lib."; - private static final String N_PLUS = "operator_plus"; - private static final String N_MINUS = "operator_minus"; - private static final String N_POWER = "operator_power"; - private static final String N_MULTIPLY = "operator_multiply"; - private static final String N_DIVIDE = "operator_divide"; - private static final String N_MODULO = "operator_modulo"; - private static final String N_LESSTHAN = "operator_lessThan"; - private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan"; - private static final String N_GREATERTHAN = "operator_greaterThan"; - private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan"; - private static final String N_EQUALS = "operator_equals"; - private static final String N_NOTEQUALS = "operator_notEquals"; - private static final String N_EQUALS3 = "operator_tripleEquals"; - private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; - private File tempFile; - private PrintWriter printer; - private String containerName; + private final String containerName; private Map varMap; + private List curVars; - public NumericDrealProblemSolver() throws IOException, InterruptedException { - //setup smt2 input file - tempFile = File.createTempFile("smt", ".smt2"); - printer = new PrintWriter(tempFile); - printer.println(";Header comment"); - printer.println("(set-logic QF_NRA)"); - + public NumericDrealProblemSolver() throws IOException, InterruptedException { //setup docker - File parentPath = tempFile.getParentFile(); - System.out.println(parentPath); - System.out.println(tempFile); - //TODO ENSURE that container name is not already in use + //TODO ENSURE that container name is not already in use???? + File tempDir = new File(System.getProperty("java.io.tmpdir")); containerName = UUID.randomUUID().toString().replace("-", ""); List startDocker = new ArrayList( Arrays.asList("docker", "run", "-id", "--rm", "--name", containerName, - "-p", "8080:80", - "-v", parentPath + ":/mnt", +// "-p", "8080:80", + "-v", tempDir + ":/mnt", "dreal/dreal4")); - Process p = runProcess(startDocker); + Process p = runProcess(startDocker); //setup varmap varMap = new HashMap(); @@ -69,70 +54,235 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ private Process runProcess(List cmd) throws IOException, InterruptedException { // println(cmd) ProcessBuilder pb = new ProcessBuilder(cmd); - pb.redirectOutput(); - pb.redirectError(); Process p = pb.start(); - p.waitFor(); +// p.waitFor(); //TODO timeout if needed -// if (!p.waitFor(TIMEOUT, TimeUnit.SECONDS)) { -// p.destroy(); -// } + if (!p.waitFor(5, TimeUnit.SECONDS)) { + p.destroy(); + } return p; } - -// -// private ArrayList getJvmIdentifiableElements(XExpression expression) { -// ArrayList allElem = new ArrayList(); -// XExpression left = ((XBinaryOperation) expression).getLeftOperand(); -// XExpression right = ((XBinaryOperation) expression).getRightOperand(); -// -// getJvmIdentifiableElementsHelper(left, allElem); -// getJvmIdentifiableElementsHelper(right, allElem); -// return allElem; -// } -// -// private void getJvmIdentifiableElementsHelper(XExpression e, List allElem) { -// if (e instanceof XFeatureCall) { -// allElem.add(((XFeatureCall) e).getFeature()); -// } else if (e instanceof XBinaryOperation) { -// getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem); -// getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); -// } -// } - private Process callDreal() throws IOException, InterruptedException { + private Process callDreal(String tempFileName) throws IOException, InterruptedException { List drealCmd = new ArrayList( Arrays.asList("docker", "exec", containerName, "dreal", "--model", - "mnt/" + tempFile.getName())); + "mnt/" + tempFileName)); return runProcess(drealCmd); } - private boolean getDrealResult(Process p) throws IOException { - if (p.exitValue() == 1) {return false;} + private List getDrealStream(InputStream stream) throws IOException { + List output = new ArrayList(); + BufferedReader r = new BufferedReader(new InputStreamReader(stream)); - BufferedReader output = new BufferedReader(new InputStreamReader(p.getInputStream())); + String rl = ""; + while ((rl = r.readLine()) != null) {output.add(rl);} + return output; + } + + private List> getProcessOutput(Process p) throws IOException { + List> outputs = new ArrayList>(); + outputs.add(getDrealStream(p.getInputStream())); + outputs.add(getDrealStream(p.getErrorStream())); + return outputs; + } + + private boolean getDrealResult(int exitVal, List> outputs) throws IOException { + //error at process-level + if (exitVal == 1) {printError(outputs.get(1)); return false;} + + //error at dreal-level + if (! outputs.get(1).isEmpty()) {printError(outputs.get(1)); return false;} - String resultRaw = output.readLine(); + //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;} throw new IOException("Unknown dreal output first line"); //TODO make the above better + } + + private String formNumericConstraint(XExpression e, Map aMatch) throws Exception { + //The check equation MUST be a binary operation + if (!(e instanceof XBinaryOperation)) { + throw new Exception ("error in check expression!!!"); + } + + String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); + + String operator = ""; + + String left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); + String right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); + + if (nameEndsWith(name, N_LESSTHAN)) { + operator = "<"; + } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { + operator = "<="; + } else if (nameEndsWith(name, N_GREATERTHAN)) { + operator = ">"; + } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { + operator = ">="; + } else if (nameEndsWith(name, N_EQUALS)) { + operator = "<"; + } else if (nameEndsWith(name, N_NOTEQUALS)) { + //Exceptional case + return "(not (=" + " " + left_operand + " " + right_operand + "))"; +// } else if (nameEndsWith(name, N_EQUALS3)) { +// operator = "<"; +// } else if (nameEndsWith(name, N_NOTEQUALS3)) { +// operator = "<"; + } else { + throw new Exception ("Unsupported binary operation " + name); + } + + return "(" + operator + " " + left_operand + " " + right_operand + ")"; + } + + private String formNumericConstraintHelper(XExpression e, Map aMatch) throws Exception { + String expr = ""; + // Variables + if (e instanceof XFeatureCall) { + PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); + boolean isInt = matchedObj instanceof IntegerElement; + if (!matchedObj.isValueSet()) { + if (varMap.get(matchedObj) == null) { + expr = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.hashCode(); //TODO ISSUE + varMap.put(matchedObj, expr); + } else { + expr = varMap.get(matchedObj); + } + } else { + //TODO unsure what it means if something gets in here + if (isInt) { + expr = Integer.toString(((IntegerElement) matchedObj).getValue()); + } else { + expr = Double.toString(((RealElement) matchedObj).getValue().doubleValue()); + } + varMap.put(matchedObj, expr); + } + //Add variable declarations + if(! curVars.contains(expr)) { + String varDecl = "(declare-fun " + expr + " () "; + if (isInt) {varDecl += "Int)";} + else {varDecl += "Real)";} + curVars.add(varDecl); + } + } + // Constants + else if (e instanceof XNumberLiteral) { + //we do not care if it is an int or a real. + //We actually do not even check f the value parses into a number + expr = ((XNumberLiteral) e).getValue(); + //TODO ensure that the value is a valid number + // expr = Integer.parseInt(value) + } + // Expressions with operators + else if (e instanceof XBinaryOperation) { + String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); + String left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); + String right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); + + String operator = ""; + if (nameEndsWith(name, N_PLUS)) { + operator = "+"; + } else if (nameEndsWith(name, N_MINUS)) { + operator = "-"; + } else if (nameEndsWith(name, N_POWER)) { + operator = "^"; + } else if (nameEndsWith(name, N_MULTIPLY)) { + operator = "*"; + } else if (nameEndsWith(name, N_DIVIDE)) { + operator = "/"; +// } else if (nameEndsWith(name, N_MODULO)) { +// expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); + } else { + throw new Exception ("Unsupported binary operation " + name); + } + + expr = "(" + operator + " " + left_operand + " " + right_operand + ")"; + } else { + throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); + } + return expr; + + } + + private boolean nameEndsWith(String name, String end) { + 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(); + + //STM2 FILE CONTENT CREATION + curVars = new ArrayList(); + List curConstraints = new ArrayList(); + + PrintWriter printer = new PrintWriter(tempFile); + printer.println(";Header comment"); + printer.println("(set-logic QF_NRA)"); + for (XExpression e: matches.keySet()) { + Iterable> matchSets = matches.get(e); + for (Map aMatch: matchSets) { + String constraint = formNumericConstraint(e, aMatch); + String negAssert = "(assert (not " + constraint + "))"; + curConstraints.add(negAssert); + } + } + //Add Content to SMT2 file + for (String varDecl : curVars) {printer.println(varDecl);} + for (String negAssert : curConstraints) {printer.println(negAssert);} + printer.println("(check-sat)"); + printer.close(); + return tempFileName; + } + + private void printFileContent(String path) throws IOException { + InputStream input = new BufferedInputStream(new FileInputStream(path)); + byte[] buffer = new byte[8192]; + + try { + for (int length = 0; (length = input.read(buffer)) != -1;) { + System.out.write(buffer, 0, length); + } + } finally { + input.close(); + } + } + + private void printOutput(List list) { + for (String line : list) { + System.out.println(line); + } + } + + private void printError(List list) { + for (String line : list) { + System.err.println(line); + } } public boolean isSatisfiable(Map>> matches) throws Exception { + //CREATE DREAL STM2 FILE at this.tempfile location long startformingProblem = System.nanoTime(); - //CREATE DREAL STM2 FILE - //TODO - - printer.close(); + String tempFileName = formNumericProblemInstance(matches); endformingProblem = System.nanoTime()-startformingProblem; + +// printFileContent(System.getProperty("java.io.tmpdir") + tempFileName); + + //CALL DREAL long startSolvingProblem = System.nanoTime(); - //CALL DREAL - Process outputProcess = callDreal(); - boolean result = getDrealResult(outputProcess); + Process outputProcess = callDreal(tempFileName); + List> outputs = getProcessOutput(outputProcess); + boolean result = getDrealResult(outputProcess.exitValue(), outputs); + System.out.println(result); endSolvingProblem = System.nanoTime()-startSolvingProblem; //CLOSE return result; @@ -177,124 +327,12 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ // return sol; return null; } -// -// private BoolExpr formNumericConstraint(XExpression e, Map aMatch) throws Exception { -// if (!(e instanceof XBinaryOperation)) { -// throw new Exception ("error in check expression!!!"); -// } -// -// String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); -// -// BoolExpr constraint = null; -// -// ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); -// ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); -// -// if (nameEndsWith(name, N_LESSTHAN)) { -// constraint = ctx.mkLt(left_operand, right_operand); -// } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { -// constraint = ctx.mkLe(left_operand, right_operand); -// } else if (nameEndsWith(name, N_GREATERTHAN)) { -// constraint = ctx.mkGt(left_operand, right_operand); -// } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { -// constraint = ctx.mkGe(left_operand, right_operand); -// } else if (nameEndsWith(name, N_EQUALS)) { -// constraint = ctx.mkEq(left_operand, right_operand); -// } else if (nameEndsWith(name, N_NOTEQUALS)) { -// constraint = ctx.mkDistinct(left_operand, right_operand); -// } else if (nameEndsWith(name, N_EQUALS3)) { -// constraint = ctx.mkGe(left_operand, right_operand); // ??? -// } else if (nameEndsWith(name, N_NOTEQUALS3)) { -// constraint = ctx.mkGe(left_operand, right_operand); // ??? -// } else { -// throw new Exception ("Unsupported binary operation " + name); -// } -// -// return constraint; -// } -// -// private ArithExpr formNumericConstraintHelper(XExpression e, Map aMatch) throws Exception { -// ArithExpr expr = null; -// // Variables -// if (e instanceof XFeatureCall) { -// PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); -// boolean isInt = matchedObj instanceof IntegerElement; -// if (!matchedObj.isValueSet()) { -// if (varMap.get(matchedObj) == null) { -// String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString(); -// if (isInt) { -// expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); -// } else { -// expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getRealSort()); -// } -// varMap.put(matchedObj, expr); -// } else { -// expr = (ArithExpr) varMap.get(matchedObj); -// } -// } else { -// if (isInt) { -// int value = ((IntegerElement) matchedObj).getValue(); -// expr = (ArithExpr) ctx.mkInt(value); -// } else { -// double value = ((RealElement) matchedObj).getValue().doubleValue(); -// expr = (ArithExpr) ctx.mkReal(String.valueOf(value)); -// } -// varMap.put(matchedObj, expr); -// } -// } -// // Constants -// else if (e instanceof XNumberLiteral) { -// String value = ((XNumberLiteral) e).getValue(); -// try{ -// int val = Integer.parseInt(value); -// expr = (ArithExpr) ctx.mkInt(val); -// } catch(NumberFormatException err){ -// try{ -// expr = (ArithExpr) ctx.mkReal(value); -// } catch(NumberFormatException err2){} -// } -// } -// // Expressions with operators -// else if (e instanceof XBinaryOperation) { -// String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); -// ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); -// ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); -// -// if (nameEndsWith(name, N_PLUS)) { -// expr = ctx.mkAdd(left_operand, right_operand); -// } else if (nameEndsWith(name, N_MINUS)) { -// expr = ctx.mkAdd(left_operand, ctx.mkUnaryMinus(right_operand)); -// } else if (nameEndsWith(name, N_POWER)) { -// expr = ctx.mkPower(left_operand, right_operand); -// } else if (nameEndsWith(name, N_MULTIPLY)) { -// expr = ctx.mkMul(left_operand, right_operand); -// } else if (nameEndsWith(name, N_DIVIDE)) { -// expr = ctx.mkDiv(left_operand, right_operand); -// } else if (nameEndsWith(name, N_MODULO)) { -// expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); -// } else { -// throw new Exception ("Unsupported binary operation " + name); -// } -// } else { -// throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); -// } -// return expr; -// -// } -// -// private boolean nameEndsWith(String name, String end) { -// return name.startsWith(N_Base) && name.endsWith(end); -// } -// -// private BoolExpr formNumericProblemInstance(Map>> matches) throws Exception { -// BoolExpr constraintInstances = ctx.mkTrue(); -// for (XExpression e: matches.keySet()) { -// Iterable> matchSets = matches.get(e); -// for (Map aMatch: matchSets) { -// BoolExpr constraintInstance = ctx.mkNot(formNumericConstraint(e, aMatch)); -// constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); -// } -// } -// return constraintInstances; -// } + + public void teardown() throws IOException, InterruptedException { + List stopDocker = new ArrayList( + Arrays.asList("docker", "stop", containerName)); + runProcess(stopDocker); + //TODO Check if above went well? + } + } -- cgit v1.2.3-54-g00ecf