From 41a48543aea119acae321aae61b85d711610b652 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Wed, 20 Jan 2021 08:44:27 +0100 Subject: almost finish crossscen VQL + implement ITE handling + prelim results --- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 38 ++++++++++ .../viatra2logic/NumericDrealProblemSolver.java | 83 ++++++++++++++++------ 2 files changed, 101 insertions(+), 20 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend index 1b68fed2..9e11d2cf 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend @@ -1,6 +1,7 @@ package hu.bme.mit.inf.dslreasoner.viatra2logic import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable import java.util.Map @@ -8,9 +9,11 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable import org.eclipse.xtext.xbase.XBinaryOperation import org.eclipse.xtext.xbase.XExpression import org.eclipse.xtext.xbase.XFeatureCall +import org.eclipse.xtext.xbase.XIfExpression import org.eclipse.xtext.xbase.XMemberFeatureCall import org.eclipse.xtext.xbase.XNumberLiteral import org.eclipse.xtext.xbase.XUnaryOperation +import org.eclipse.xtext.xbase.XBlockExpression class ExpressionEvaluation2Logic { val extension LogicProblemBuilder builder = new LogicProblemBuilder @@ -139,6 +142,41 @@ class ExpressionEvaluation2Logic { throw new UnsupportedOperationException('''Unsupported numeric type: "«s»"''') } + def protected dispatch Term transform(XIfExpression i, Map variable2Variable) { + + val cond_op = i.^if.transform(variable2Variable) + val then_op = i.then.transform(variable2Variable) + val else_op = i.^else.transform(variable2Variable) + + if (cond_op === null) { + println("-> " + i.^if) + println("-> " + i.then) + println("-> " + i.^else) + throw new UnsupportedOperationException('''Your ITE statement has a null condition.''') + } + if (then_op === null) { + println("-> " + i.^if) + println("-> " + i.then) + println("-> " + i.^else) + throw new UnsupportedOperationException('''Your ITE statement has a null "then" statement"".''') + } + return ITE(cond_op, then_op, else_op) + } + + def protected dispatch Term transform(XBlockExpression b, Map variable2Variable) { + val exprs = newArrayList + for(e:b.expressions){ exprs.add(transform(e, variable2Variable)) } + + if (exprs.size > 1) + throw new UnsupportedOperationException('''blocks with more than 1 statement are not currently supportes: "«exprs»"''') + if (exprs.isEmpty) + throw new UnsupportedOperationException('''blocks is empty: "«exprs»"''') + + return exprs.get(0) + } + + + def protected dispatch Term transform(XExpression e, Map variable2Variable) { throw new UnsupportedOperationException('''Unsupported expression: "«e.class.simpleName»" - «e»''') } 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 30e68260..575a9224 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 @@ -20,8 +20,10 @@ import java.util.regex.Pattern; import org.eclipse.xtext.common.types.JvmIdentifiableElement; import org.eclipse.xtext.xbase.XBinaryOperation; +import org.eclipse.xtext.xbase.XBlockExpression; import org.eclipse.xtext.xbase.XExpression; import org.eclipse.xtext.xbase.XFeatureCall; +import org.eclipse.xtext.xbase.XIfExpression; import org.eclipse.xtext.xbase.XNumberLiteral; import org.eclipse.xtext.xbase.XUnaryOperation; @@ -72,7 +74,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ //TODO timeout if needed if (!p.waitFor(timeout, TimeUnit.SECONDS)) { p.destroy(); - System.err.println("TIMEOUT"); //DEBUG + return null; } return p; } @@ -147,7 +149,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } private String formNumericConstraint(XExpression e, Map aMatch) throws Exception { - //The check equation MUST be a binary operation + //The check equation MUST be a binary operation of the listed types (comparisons) if (!(e instanceof XBinaryOperation)) { throw new Exception ("error in check expression!!!"); } @@ -159,19 +161,20 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ String left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); String right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); + //NOTE that everything is inverted, due to how the MG handles vql constraints if (nameEndsWith(name, N_LESSTHAN)) { - operator = "<"; + operator = ">"; } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { - operator = "<="; + operator = ">="; } else if (nameEndsWith(name, N_GREATERTHAN)) { - operator = ">"; + operator = "<"; } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { - operator = ">="; + 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_NOTEQUALS)) { + operator = "="; // } else if (nameEndsWith(name, N_EQUALS3)) { // operator = "<"; // } else if (nameEndsWith(name, N_NOTEQUALS3)) { @@ -240,6 +243,19 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ operator = "*"; } else if (nameEndsWith(name, N_DIVIDE)) { operator = "/"; + } else 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_MODULO)) { // expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); } else { @@ -249,12 +265,30 @@ 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); + //TODO + //This is, for example, "-1000" throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); - } else { + } + else if (e instanceof XIfExpression) { + + String if_operand = formNumericConstraintHelper(((XIfExpression) e).getIf(), aMatch); + String then_operand = formNumericConstraintHelper(((XIfExpression) e).getThen(), aMatch); + String else_operand = formNumericConstraintHelper(((XIfExpression) e).getElse(), aMatch); + + expr = "(ite " + if_operand + " " + then_operand + " " + else_operand + ")"; + } + else if (e instanceof XBlockExpression) { + XBlockExpression ebl = (XBlockExpression) e; + + if (ebl.getExpressions().size() > 1) + throw new Exception("Unsupported: blocks with more than 1 statement are not currently supportes: " + ebl); + if (ebl.getExpressions().isEmpty()) + throw new Exception("Unsupported: blocks is empty:" + ebl); + + //TODO make this more general + expr = formNumericConstraintHelper(ebl.getExpressions().get(0), aMatch); + } + else { throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); } return expr; @@ -279,7 +313,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ Iterable> matchSets = matches.get(e); for (Map aMatch: matchSets) { String constraint = formNumericConstraint(e, aMatch); - String negAssert = "(assert (not " + constraint + "))"; + String negAssert = "(assert " + constraint + ")"; curConstraints.add(negAssert); } } @@ -329,16 +363,24 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ Process outputProcess; if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); else outputProcess = callDrealLocal(numProbContent, false); - - List> outputs = getProcessOutput(outputProcess); - boolean result = getDrealResult(outputProcess.exitValue(), outputs); + + boolean result = false; + List> outputs = null; + if (outputProcess != null) { + outputs = getProcessOutput(outputProcess); + result = getDrealResult(outputProcess.exitValue(), outputs); + } endSolvingProblem = System.nanoTime()-startSolvingProblem; //DEBUG - Print things + if (outputProcess == null) { + System.err.println("TIMEOUT"); +// printOutput(numProbContent); + } // printOutput(numProbContent); -// printOutput(outputs.get(0)); - System.out.println(result); - //END DEBUG +// if (outputs != null) printOutput(outputs.get(0)); +// System.out.println(result); +// END DEBUG return result; } @@ -391,6 +433,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ endSolvingProblem = System.nanoTime()-startSolvingProblem; //DEBUG - Print things + System.out.println("Getting Solution!"); // printOutput(numProbContent); // printOutput(outputs.get(0)); // System.out.println(result); -- cgit v1.2.3-70-g09d2