From 6d4bfc394b0a8995fdb2ff7ad1eb97a3e7374289 Mon Sep 17 00:00:00 2001 From: anqili426 Date: Tue, 7 Apr 2020 21:20:37 -0400 Subject: Added logic to create a numeric problem instance with pattern matches --- .../viatra2logic/NumericProblemSolver.java | 162 +++++++++++++++------ 1 file changed, 117 insertions(+), 45 deletions(-) diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java index a58bd855..2372177a 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java @@ -1,7 +1,13 @@ package hu.bme.mit.inf.dslreasoner.viatra2logic; import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collections; import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; import org.eclipse.xtext.xbase.XBinaryOperation; import org.eclipse.xtext.xbase.XExpression; @@ -11,6 +17,7 @@ import org.eclipse.xtext.xbase.XNumberLiteral; import com.microsoft.z3.ArithExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; import com.microsoft.z3.IntExpr; import com.microsoft.z3.Solver; import com.microsoft.z3.Status; @@ -32,34 +39,38 @@ public class NumericProblemSolver { 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 static int counter = 0; - + private Context ctx; - private ArithExpr[] vars = new ArithExpr[2]; + private Solver s; + private Map templates; + private Map> bindings; + private BoolExpr test; public NumericProblemSolver() { HashMap cfg = new HashMap(); cfg.put("model", "true"); - ctx = new Context(cfg); + ctx = new Context(cfg); + s = ctx.mkSolver(); + templates = new HashMap(); + bindings = new HashMap>(); } - + public Context getNumericProblemContext() { return ctx; } - public BoolExpr formNumericProblemTemplate(XExpression e) throws Exception { + public void formNumericProblemTemplate(XExpression e) 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 = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); - + if (nameEndsWith(name, N_LESSTHAN)) { constraint = ctx.mkLt(left_operand, right_operand); } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { @@ -80,57 +91,39 @@ public class NumericProblemSolver { throw new Exception ("Unsupported binary operation " + name); } - // To check the constraint - System.out.println(constraint.toString()); - - int mage = 5; - int page = 25; - - BoolExpr inst = ctx.mkTrue(); - for (ArithExpr var: vars) { - inst = ctx.mkAnd(inst, ctx.mkEq(var, ctx.mkInt(mage))); - } - System.out.println(inst.toString()); - - Solver s = ctx.mkSolver(); - s.add(constraint); - s.add(inst); - - if (s.check() == Status.SATISFIABLE) { - System.out.println("satisfiable"); - } else { - System.out.println("not satisfiable"); - } - - - return constraint; - + templates.put(e, constraint); + HashMap>> matches = new HashMap>>(); + Object o1 = new Object(); + Object o2 = new Object(); + List list = new ArrayList(); + list.add(o1); + list.add(o2); + Set> set = new HashSet>(); + set.add(list); + matches.put(e, set); + System.out.println("************************"); + System.out.println(this.isSatisfiable(matches)); } + // TODO: add variable: state of the solver private ArithExpr formNumericProblemTemplateHelper(XExpression e) throws Exception { ArithExpr expr = null; // Variables - // how to know the data type of this variable????? if (e instanceof XFeatureCall) { String var_name = ((XFeatureCall) e).getFeature().getQualifiedName(); - vars[counter] = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); - expr = vars[counter]; - counter++; + expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); } // 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){} - // What to do with short / float / double??? - // e.g. For floats, need to use FPAdd instead of normal Add!! } // Expressions with operators else if (e instanceof XBinaryOperation) { String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); - ArithExpr left_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); - + if (nameEndsWith(name, N_PLUS)) { expr = ctx.mkAdd(left_operand, right_operand); } else if (nameEndsWith(name, N_MINUS)) { @@ -152,9 +145,88 @@ public class NumericProblemSolver { return expr; } - + private boolean nameEndsWith(String name, String end) { return name.startsWith(N_Base) && name.endsWith(end); } + public boolean isSatisfiable(Map>> matches) throws Exception { + boolean sat = false; + BoolExpr problemInstance = formNumericProblemInstance(matches); + s.add(problemInstance); + if (s.check() == Status.SATISFIABLE) { + sat = true; + } else { + sat = false; + } + return sat; + } + +// public Map getOneSolution(List, Map>> matches) { +// Map sol = new HashMap(); +// BoolExpr problemInstance = formNumericProblemInstance(matches); +// s.add(problemInstance); +// if (s.check() == Status.SATISFIABLE) { +// //TODO: Form the map here +// } +// return sol; +// } + + private BoolExpr formNumericProblemInstance(Map>> matches) throws Exception { + BoolExpr constraintInstances = ctx.mkTrue(); + for (XExpression e: matches.keySet()) { + BoolExpr template = templates.get(e); + Set> matchSets = matches.get(e); + Map varMap = bindings.get(e); + + if (varMap == null) { + varMap = new HashMap(); + bindings.put(e, varMap); + } + + for (List aMatch: matchSets) { + Expr[] expressions = template.getArgs().clone(); + formNumericProblemInstance(expressions, aMatch, varMap, 0); + constraintInstances = ctx.mkAnd(constraintInstances, formConstraintInstance(template, expressions)); + } + } + return constraintInstances; + } + + // TODO: Create a new exception class?? + private BoolExpr formConstraintInstance(BoolExpr template, Expr[] expressions) throws Exception { + if (expressions.length != 2) { + throw new Exception("Wrong format"); + } + BoolExpr inst = ctx.mkTrue(); + ArithExpr leftOperand = (ArithExpr) expressions[0]; + ArithExpr rightOperand = (ArithExpr) expressions[1]; + if (template.isLE()) { + inst = ctx.mkLe(leftOperand, rightOperand); + } else if (template.isLT()) { + inst = ctx.mkLt(leftOperand, rightOperand); + } else if (template.isGE()) { + inst = ctx.mkGe(leftOperand, rightOperand); + } else if (template.isGT()) { + inst = ctx.mkGt(leftOperand, rightOperand); + } else if (template.isEq()) { + inst = ctx.mkEq(leftOperand, rightOperand); + } else if (template.isDistinct()) { + inst = ctx.mkDistinct(leftOperand, rightOperand); + } else { + throw new Exception("Something went wrong"); + } + return inst; + } + + // TODO: This is not gonna work....How to plug in matched objects to the template??? + private void formNumericProblemInstance(Expr[] expr, List match, Map varMap, int ind) { + for (int i = 0; i < expr.length; i++) { + if (expr[i].isConst()) { + expr[i] = ctx.mkConst(expr[i].toString(), ctx.getIntSort()); + } else if (expr[i].getArgs().length > 0) { + formNumericProblemInstance(expr[i].getArgs(), match, varMap, ind); + } + } + } } -- cgit v1.2.3-54-g00ecf