From db7f0ebb8efc522990835d8a042db8141856cf5c Mon Sep 17 00:00:00 2001 From: anqili426 Date: Wed, 8 Apr 2020 14:15:22 -0400 Subject: Updated logic that creates a numeric problem using matches --- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 12 +- .../viatra2logic/NumericProblemSolver.java | 152 ++++++++------------- 2 files changed, 67 insertions(+), 97 deletions(-) (limited to 'Framework') 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 a1e18250..adecf1d4 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 @@ -13,6 +13,11 @@ import org.eclipse.xtext.xbase.XNumberLiteral import org.eclipse.xtext.xbase.XUnaryOperation import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import com.microsoft.z3.BoolExpr +import java.util.Set +import java.util.List +import org.eclipse.xtext.common.types.JvmIdentifiableElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement class ExpressionEvaluation2Logic { val extension LogicProblemBuilder builder = new LogicProblemBuilder @@ -23,10 +28,9 @@ class ExpressionEvaluation2Logic { } def Term transformEval(PVariable target, XExpression expression, Map variable2Variable) { - val test = expression.transform(variable2Variable) - numericSolver.formNumericProblemTemplate(expression) - - return test + numericSolver.test(expression); +// numericSolver.isSatisfiable(null) + return expression.transform(variable2Variable) } static val N_Base = "org.eclipse.xtext.xbase.lib." 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 2372177a..834cc2f0 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,14 +1,11 @@ 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.common.types.JvmIdentifiableElement; import org.eclipse.xtext.xbase.XBinaryOperation; import org.eclipse.xtext.xbase.XExpression; import org.eclipse.xtext.xbase.XFeatureCall; @@ -22,6 +19,9 @@ import com.microsoft.z3.IntExpr; import com.microsoft.z3.Solver; import com.microsoft.z3.Status; +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; + public class NumericProblemSolver { private static final String N_Base = "org.eclipse.xtext.xbase.lib."; @@ -42,24 +42,50 @@ public class NumericProblemSolver { private Context ctx; 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); s = ctx.mkSolver(); - templates = new HashMap(); bindings = new HashMap>(); } public Context getNumericProblemContext() { return ctx; } + + // TODO: Remove this after integration + public void test(XExpression expression) throws Exception { + Map>> matches = new HashMap>>(); + matches.put(expression, null); + isSatisfiable(matches); + } + + 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 objs, Map>> matches) throws Exception { + Map sol = new HashMap(); + BoolExpr problemInstance = formNumericProblemInstance(matches); + s.add(problemInstance); + if (s.check() == Status.SATISFIABLE) { + //TODO: Form the solution here + } + return sol; + } - public void formNumericProblemTemplate(XExpression e) throws Exception { + private BoolExpr formNumericConstraint(XExpression e, Map aMatch, Map varMap) throws Exception { if (!(e instanceof XBinaryOperation)) { throw new Exception ("error in check expression!!!"); } @@ -68,8 +94,8 @@ public class NumericProblemSolver { BoolExpr constraint = null; - ArithExpr left_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getLeftOperand()); - ArithExpr right_operand = formNumericProblemTemplateHelper(((XBinaryOperation) e).getRightOperand()); + ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch, varMap); + ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch, varMap); if (nameEndsWith(name, N_LESSTHAN)) { constraint = ctx.mkLt(left_operand, right_operand); @@ -91,27 +117,28 @@ public class NumericProblemSolver { throw new Exception ("Unsupported binary operation " + name); } - 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)); + return constraint; } // TODO: add variable: state of the solver - private ArithExpr formNumericProblemTemplateHelper(XExpression e) throws Exception { + private ArithExpr formNumericConstraintHelper(XExpression e, Map aMatch, Map varMap) throws Exception { ArithExpr expr = null; // Variables if (e instanceof XFeatureCall) { - String var_name = ((XFeatureCall) e).getFeature().getQualifiedName(); - expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); + PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); + if (!matchedObj.isValueSet()) { + if (varMap.get(matchedObj) == null) { + String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString(); + expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); + varMap.put(matchedObj, expr); + } else { + expr = (ArithExpr) varMap.get(matchedObj); + } + } else { + int value = ((IntegerElement) matchedObj).getValue(); + expr = (ArithExpr) ctx.mkInt(value); + varMap.put(matchedObj, expr); + } } // Constants else if (e instanceof XNumberLiteral) { @@ -121,8 +148,8 @@ public class NumericProblemSolver { // 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()); + ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch, varMap); + ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch, varMap); if (nameEndsWith(name, N_PLUS)) { expr = ctx.mkAdd(left_operand, right_operand); @@ -149,34 +176,11 @@ public class NumericProblemSolver { 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 { + 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); + Set> matchSets = matches.get(e); Map varMap = bindings.get(e); if (varMap == null) { @@ -184,49 +188,11 @@ public class NumericProblemSolver { 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)); + for (Map aMatch: matchSets) { + BoolExpr constraintInstance = formNumericConstraint(e, aMatch, varMap); + constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); } } 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