Updated logic that creates a numeric problem using matches

2 files changed, 67 insertions, 97 deletions

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<PVariable, Variable> 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<XExpression, BoolExpr> templates;

         private Map<XExpression, Map<Object, Expr>> bindings;

-        private BoolExpr test;

 

         public NumericProblemSolver() {

                 HashMap<String, String> cfg = new HashMap<String, String>();

                 cfg.put("model", "true");

                 ctx = new Context(cfg); 

                 s = ctx.mkSolver();

-                templates = new HashMap<XExpression, BoolExpr>();

                 bindings = new HashMap<XExpression, Map<Object, Expr>>();

         }

 

         public Context getNumericProblemContext() {

                 return ctx;

         }

+        

+        // TODO: Remove this after integration

+        public void test(XExpression expression) throws Exception {

+                Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>();

+                matches.put(expression, null);

+                isSatisfiable(matches);

+        }

+        

+        public boolean isSatisfiable(Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> 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<Object,Integer> getOneSolution(List<Object> objs, Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {

+                Map<Object,Integer> sol = new HashMap<Object, Integer>();

+                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<JvmIdentifiableElement, PrimitiveElement> aMatch, Map<Object, Expr> 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<XExpression, Set<List<Object>>> matches = new HashMap<XExpression, Set<List<Object>>>();

-                Object o1 = new Object();

-                Object o2 = new Object();

-                List<Object> list = new ArrayList<Object>();

-                list.add(o1);

-                list.add(o2);

-                Set<List<Object>> set = new HashSet<List<Object>>();

-                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<JvmIdentifiableElement, PrimitiveElement> aMatch, Map<Object, Expr> 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<XExpression, Set<List<Object>>> 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<Object,Integer> getOneSolution(List<Object>, Map<XExpression, Set<List<Object>>> matches) {

-//              Map<Object,Integer> sol = new HashMap<Object, Integer>();

-//              BoolExpr problemInstance = formNumericProblemInstance(matches);

-//              s.add(problemInstance);

-//              if (s.check() == Status.SATISFIABLE) {

-//                      //TODO:  Form the map here

-//              }

-//              return sol;

-//      }

-        

-        private BoolExpr formNumericProblemInstance(Map<XExpression, Set<List<Object>>> matches) throws Exception {

+        private BoolExpr formNumericProblemInstance(Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {

                 BoolExpr constraintInstances = ctx.mkTrue();

                 for (XExpression e: matches.keySet()) {

-                        BoolExpr template = templates.get(e);

-                        Set<List<Object>> matchSets = matches.get(e);

+                        Set<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e);

                         Map<Object, Expr> varMap = bindings.get(e);

 

                         if (varMap == null) {

@@ -184,49 +188,11 @@ public class NumericProblemSolver {
                                 bindings.put(e, varMap);

                         }

 

-                        for (List<Object> aMatch: matchSets) {

-                                Expr[] expressions = template.getArgs().clone();

-                                formNumericProblemInstance(expressions, aMatch, varMap, 0);

-                                constraintInstances = ctx.mkAnd(constraintInstances, formConstraintInstance(template, expressions));

+                        for (Map<JvmIdentifiableElement, PrimitiveElement> 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<Object> match, Map<Object, Expr> 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);

-                        }

-                }

-        }

 }