From 40303748df2676f23b9617335a401678bdf21ed7 Mon Sep 17 00:00:00 2001 From: anqili426 Date: Tue, 31 Mar 2020 10:13:34 -0400 Subject: Added call to form numeric problem templates --- .../inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src') 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 f474ded4..a1e18250 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 @@ -16,12 +16,17 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class ExpressionEvaluation2Logic { val extension LogicProblemBuilder builder = new LogicProblemBuilder + val NumericProblemSolver numericSolver = new NumericProblemSolver def Term transformCheck(XExpression expression, Map variable2Variable) { return expression.transform(variable2Variable) } + def Term transformEval(PVariable target, XExpression expression, Map variable2Variable) { - return target.lookup(variable2Variable) == expression.transform(variable2Variable) + val test = expression.transform(variable2Variable) + numericSolver.formNumericProblemTemplate(expression) + + return test } static val N_Base = "org.eclipse.xtext.xbase.lib." -- cgit v1.2.3-54-g00ecf From 7b3ec6bfed2581cd3bb5bbb497bfc518d19f21c3 Mon Sep 17 00:00:00 2001 From: anqili426 Date: Tue, 31 Mar 2020 10:15:44 -0400 Subject: Added logic to form numeric problem templates --- .../viatra2logic/NumericProblemSolver.java | 160 +++++++++++++++++++++ 1 file changed, 160 insertions(+) create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src') 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 new file mode 100644 index 00000000..a58bd855 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java @@ -0,0 +1,160 @@ +package hu.bme.mit.inf.dslreasoner.viatra2logic; + +import java.util.ArrayList; +import java.util.HashMap; + +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 com.microsoft.z3.ArithExpr; +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import com.microsoft.z3.IntExpr; +import com.microsoft.z3.Solver; +import com.microsoft.z3.Status; + + +public class 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 static int counter = 0; + + private Context ctx; + private ArithExpr[] vars = new ArithExpr[2]; + + public NumericProblemSolver() { + HashMap cfg = new HashMap(); + cfg.put("model", "true"); + ctx = new Context(cfg); + } + + public Context getNumericProblemContext() { + return ctx; + } + + public BoolExpr 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)) { + 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); + } + + // 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; + + } + + 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++; + } + // 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)) { + 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); + } + +} -- cgit v1.2.3-54-g00ecf 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(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src') 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 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/hu.bme.mit.inf.dslreasoner.viatra2logic/src') 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 From d8f9e9d3863255f367caa3098a4fd7c87f81b841 Mon Sep 17 00:00:00 2001 From: anqili426 Date: Wed, 15 Apr 2020 01:24:14 -0400 Subject: Added logic to get a solution --- .../viatra2logic/NumericProblemSolver.java | 23 ++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src') 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 834cc2f0..b9532c46 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 @@ -16,8 +16,10 @@ import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; import com.microsoft.z3.IntExpr; +import com.microsoft.z3.Model; import com.microsoft.z3.Solver; import com.microsoft.z3.Status; +import com.microsoft.z3.enumerations.Z3_ast_print_mode; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; @@ -42,14 +44,15 @@ public class NumericProblemSolver { private Context ctx; private Solver s; - private Map> bindings; + private Map varMap; public NumericProblemSolver() { HashMap cfg = new HashMap(); cfg.put("model", "true"); ctx = new Context(cfg); + ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); s = ctx.mkSolver(); - bindings = new HashMap>(); + varMap = new HashMap(); } public Context getNumericProblemContext() { @@ -80,7 +83,13 @@ public class NumericProblemSolver { BoolExpr problemInstance = formNumericProblemInstance(matches); s.add(problemInstance); if (s.check() == Status.SATISFIABLE) { - //TODO: Form the solution here + Model m = s.getModel(); + Set allObj = varMap.keySet(); + for (Object o: allObj) { + IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); + Integer oSol = Integer.parseInt(val.toString()); + sol.put(o, oSol); + } } return sol; } @@ -117,6 +126,7 @@ public class NumericProblemSolver { throw new Exception ("Unsupported binary operation " + name); } + System.out.println(constraint.toString()); return constraint; } @@ -181,13 +191,6 @@ public class NumericProblemSolver { BoolExpr constraintInstances = ctx.mkTrue(); for (XExpression e: matches.keySet()) { Set> matchSets = matches.get(e); - Map varMap = bindings.get(e); - - if (varMap == null) { - varMap = new HashMap(); - bindings.put(e, varMap); - } - for (Map aMatch: matchSets) { BoolExpr constraintInstance = formNumericConstraint(e, aMatch, varMap); constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); -- cgit v1.2.3-54-g00ecf From 931cc6de2ab952e63490fcbfc8fe481958261123 Mon Sep 17 00:00:00 2001 From: anqili426 Date: Wed, 15 Apr 2020 02:59:15 -0400 Subject: Added test methods with running time measurement --- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 12 +- .../viatra2logic/NumericProblemSolver.java | 201 ++++++++++++++++++--- 2 files changed, 185 insertions(+), 28 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src') 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 adecf1d4..569414f0 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,11 +13,6 @@ 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 @@ -28,8 +23,11 @@ class ExpressionEvaluation2Logic { } def Term transformEval(PVariable target, XExpression expression, Map variable2Variable) { - numericSolver.test(expression); -// numericSolver.isSatisfiable(null) +// numericSolver.testIsNotSat(expression, expression.transform(variable2Variable)); +// numericSolver.testGetOneSol(expression, expression.transform(variable2Variable)); + numericSolver.testGetOneSol2(expression, expression.transform(variable2Variable)); +// numericSolver.testIsSat(expression, expression.transform(variable2Variable)); + return expression.transform(variable2Variable) } 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 b9532c46..28fa2c64 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,6 +1,8 @@ package hu.bme.mit.inf.dslreasoner.viatra2logic; +import java.util.ArrayList; import java.util.HashMap; +import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Set; @@ -21,6 +23,7 @@ import com.microsoft.z3.Solver; import com.microsoft.z3.Status; import com.microsoft.z3.enumerations.Z3_ast_print_mode; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; @@ -59,23 +62,181 @@ public class NumericProblemSolver { return ctx; } - // TODO: Remove this after integration - public void test(XExpression expression) throws Exception { + public void testIsSat(XExpression expression, Term t) throws Exception { + int count = 10000; Map>> matches = new HashMap>>(); - matches.put(expression, null); - isSatisfiable(matches); + Set> matchSet = new HashSet>(); + ArrayList allElem = getJvmIdentifiableElements(expression); + + for (int i = 0; i < count; i++) { + Map match = new HashMap(); + for (JvmIdentifiableElement e: allElem) { + FakeIntegerElement intE = new FakeIntegerElement(); + match.put(e, intE); + } + matchSet.add(match); + } + + matches.put(expression, matchSet); + long start = System.currentTimeMillis(); + boolean sat = isSatisfiable(matches); + long end = System.currentTimeMillis(); + System.out.println(sat); + System.out.println("Number of matches: " + count); + System.out.println("Running time:" + (end - start)); + } + + + public void testIsNotSat(XExpression expression, Term t) throws Exception { + Map>> matches = new HashMap>>(); + Set> matchSet = new HashSet>(); + Map match = new HashMap(); + ArrayList allElem = getJvmIdentifiableElements(expression); + FakeIntegerElement int1 = null; + FakeIntegerElement int2 = null; + boolean first = true; + for (JvmIdentifiableElement e: allElem) { + FakeIntegerElement intE = new FakeIntegerElement(); + if (first) { + int1 = intE; + first = false; + } else { + int2 = intE; + } + + match.put(e, intE); + } + matchSet.add(match); + + Map match2 = new HashMap(); + boolean first2 = true; + for (JvmIdentifiableElement e: allElem) { + if (first2) { + match2.put(e, int2); + first2 = false; + } else { + match2.put(e, int1); + } + } + matchSet.add(match2); + + matches.put(expression, matchSet); + long start = System.currentTimeMillis(); + boolean sat = isSatisfiable(matches); + long end = System.currentTimeMillis(); + System.out.println(sat); + System.out.println("Number of matches: "); + System.out.println("Running time:" + (end - start)); + } + + + public void testGetOneSol(XExpression expression, Term t) throws Exception { + int count = 10; + Map>> matches = new HashMap>>(); + Set> matchSet = new HashSet>(); + + ArrayList allElem = getJvmIdentifiableElements(expression); + List obj = new ArrayList(); + + for (int i = 0; i < count; i++) { + Map match = new HashMap(); + for (JvmIdentifiableElement e: allElem) { + FakeIntegerElement intE = new FakeIntegerElement(); + obj.add(intE); + match.put(e, intE); + } + matchSet.add(match); + matches.put(expression, matchSet); + } + + long start = System.currentTimeMillis(); + Map sol = getOneSolution(obj, matches); + long end = System.currentTimeMillis(); + + + // Print sol + for (Object o: sol.keySet()) { + System.out.println(o + " :" + sol.get(o)); + } + + + System.out.println("Number of matches: " + count); + System.out.println("Running time:" + (end - start)); + } + + + public void testGetOneSol2(XExpression expression, Term t) throws Exception { + int count = 50; + Map>> matches = new HashMap>>(); + Set> matchSet = new HashSet>(); + ArrayList allElem = getJvmIdentifiableElements(expression); + List obj = new ArrayList(); + for (int i = 0; i < count; i++) { + Map match = new HashMap(); + FakeIntegerElement int2 = null; + boolean first = false; + for (JvmIdentifiableElement e: allElem) { + FakeIntegerElement intE = new FakeIntegerElement(); + if (first) { + first = false; + } else { + int2 = intE; + } + obj.add(intE); + match.put(e, intE); + } + + Map match2 = new HashMap(); + boolean first2 = true; + for (JvmIdentifiableElement e: allElem) { + FakeIntegerElement intE = null; + if (first2) { + intE = int2; + first2 = false; + } else { + intE = new FakeIntegerElement(); + } + obj.add(intE); + match2.put(e, intE); + } + + + matchSet.add(match); + matchSet.add(match2); + } + matches.put(expression, matchSet); + + long start = System.currentTimeMillis(); + Map sol = getOneSolution(obj, matches); + long end = System.currentTimeMillis(); + + System.out.println("Number of matches: " + matchSet.size()); + System.out.println("Running time:" + (end - start)); + } + + 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); + } } 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; + return s.check() == Status.SATISFIABLE; } public Map getOneSolution(List objs, Map>> matches) throws Exception { @@ -84,8 +245,7 @@ public class NumericProblemSolver { s.add(problemInstance); if (s.check() == Status.SATISFIABLE) { Model m = s.getModel(); - Set allObj = varMap.keySet(); - for (Object o: allObj) { + for (Object o: objs) { IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); Integer oSol = Integer.parseInt(val.toString()); sol.put(o, oSol); @@ -94,7 +254,7 @@ public class NumericProblemSolver { return sol; } - private BoolExpr formNumericConstraint(XExpression e, Map aMatch, Map varMap) throws Exception { + private BoolExpr formNumericConstraint(XExpression e, Map aMatch) throws Exception { if (!(e instanceof XBinaryOperation)) { throw new Exception ("error in check expression!!!"); } @@ -103,8 +263,8 @@ public class NumericProblemSolver { BoolExpr constraint = null; - ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch, varMap); - ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch, varMap); + 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); @@ -126,12 +286,11 @@ public class NumericProblemSolver { throw new Exception ("Unsupported binary operation " + name); } - System.out.println(constraint.toString()); return constraint; } // TODO: add variable: state of the solver - private ArithExpr formNumericConstraintHelper(XExpression e, Map aMatch, Map varMap) throws Exception { + private ArithExpr formNumericConstraintHelper(XExpression e, Map aMatch) throws Exception { ArithExpr expr = null; // Variables if (e instanceof XFeatureCall) { @@ -158,8 +317,8 @@ public class NumericProblemSolver { // Expressions with operators else if (e instanceof XBinaryOperation) { String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); - ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch, varMap); - ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch, varMap); + 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); @@ -192,7 +351,7 @@ public class NumericProblemSolver { for (XExpression e: matches.keySet()) { Set> matchSets = matches.get(e); for (Map aMatch: matchSets) { - BoolExpr constraintInstance = formNumericConstraint(e, aMatch, varMap); + BoolExpr constraintInstance = formNumericConstraint(e, aMatch); constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); } } -- cgit v1.2.3-54-g00ecf From 3ba19eb2cd323b9cc6e1abfae3255d51aac0fc19 Mon Sep 17 00:00:00 2001 From: anqili426 Date: Wed, 15 Apr 2020 12:57:29 -0400 Subject: Added measurements --- .../viatra2logic/NumericProblemSolver.java | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src') 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 28fa2c64..7845c528 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 @@ -164,9 +164,8 @@ public class NumericProblemSolver { System.out.println("Running time:" + (end - start)); } - public void testGetOneSol2(XExpression expression, Term t) throws Exception { - int count = 50; + int count = 100; Map>> matches = new HashMap>>(); Set> matchSet = new HashSet>(); ArrayList allElem = getJvmIdentifiableElements(expression); @@ -206,12 +205,11 @@ public class NumericProblemSolver { } matches.put(expression, matchSet); - long start = System.currentTimeMillis(); - Map sol = getOneSolution(obj, matches); - long end = System.currentTimeMillis(); - System.out.println("Number of matches: " + matchSet.size()); - System.out.println("Running time:" + (end - start)); + for (int i = 0; i < 10; i++) { + Map sol = getOneSolution(obj, matches); + Thread.sleep(3000); + } } private ArrayList getJvmIdentifiableElements(XExpression expression) { @@ -241,16 +239,26 @@ public class NumericProblemSolver { public Map getOneSolution(List objs, Map>> matches) throws Exception { Map sol = new HashMap(); + long startformingProblem = System.currentTimeMillis(); BoolExpr problemInstance = formNumericProblemInstance(matches); + long endformingProblem = System.currentTimeMillis(); + System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); s.add(problemInstance); + long startSolvingProblem = System.currentTimeMillis(); if (s.check() == Status.SATISFIABLE) { Model m = s.getModel(); + long endSolvingProblem = System.currentTimeMillis(); + System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); + long startFormingSolution = System.currentTimeMillis(); for (Object o: objs) { IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); Integer oSol = Integer.parseInt(val.toString()); sol.put(o, oSol); } + long endFormingSolution = System.currentTimeMillis(); + System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); } + return sol; } -- cgit v1.2.3-54-g00ecf From 2cf27da1e2d10d358f7438e702e075ef1360fcbe Mon Sep 17 00:00:00 2001 From: anqili426 Date: Wed, 22 Apr 2020 13:14:23 -0400 Subject: Added new test --- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 3 +- .../viatra2logic/NumericProblemSolver.java | 48 +++++++++++++++++++++- 2 files changed, 49 insertions(+), 2 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src') 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 569414f0..a27e8904 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 @@ -25,7 +25,8 @@ class ExpressionEvaluation2Logic { def Term transformEval(PVariable target, XExpression expression, Map variable2Variable) { // numericSolver.testIsNotSat(expression, expression.transform(variable2Variable)); // numericSolver.testGetOneSol(expression, expression.transform(variable2Variable)); - numericSolver.testGetOneSol2(expression, expression.transform(variable2Variable)); +// numericSolver.testGetOneSol2(expression, expression.transform(variable2Variable)); + numericSolver.testGetOneSol3(expression, expression.transform(variable2Variable)); // numericSolver.testIsSat(expression, expression.transform(variable2Variable)); return expression.transform(variable2Variable) 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 7845c528..ff3a85eb 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 @@ -5,6 +5,7 @@ import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.Random; import java.util.Set; import org.eclipse.xtext.common.types.JvmIdentifiableElement; @@ -165,7 +166,7 @@ public class NumericProblemSolver { } public void testGetOneSol2(XExpression expression, Term t) throws Exception { - int count = 100; + int count = 250; Map>> matches = new HashMap>>(); Set> matchSet = new HashSet>(); ArrayList allElem = getJvmIdentifiableElements(expression); @@ -208,6 +209,49 @@ public class NumericProblemSolver { System.out.println("Number of matches: " + matchSet.size()); for (int i = 0; i < 10; i++) { Map sol = getOneSolution(obj, matches); + System.out.println("**********************"); + Thread.sleep(3000); + } + } + + public void testGetOneSol3(XExpression expression, Term t) throws Exception { + int count = 15000; + Random rand = new Random(); + Map>> matches = new HashMap>>(); + Set> matchSet = new HashSet>(); + ArrayList allElem = getJvmIdentifiableElements(expression); + List obj = new ArrayList(); + for (int i = 0; i < count; i++) { + Map match = new HashMap(); + if (obj.size() > 1) { + for (JvmIdentifiableElement e: allElem) { + FakeIntegerElement intE = null; + int useOld = rand.nextInt(10); + if (useOld == 1) { + System.out.println("here "); + int index = rand.nextInt(obj.size()); + intE = (FakeIntegerElement) obj.get(index); + } else { + intE = new FakeIntegerElement(); + } + obj.add(intE); + match.put(e, intE); + } + } else { + for (JvmIdentifiableElement e: allElem) { + FakeIntegerElement intE = new FakeIntegerElement(); + obj.add(intE); + match.put(e, intE); + } + } + matchSet.add(match); + } + matches.put(expression, matchSet); + + System.out.println("Number of matches: " + matchSet.size()); + for (int i = 0; i < 10; i++) { + Map sol = getOneSolution(obj, matches); + System.out.println("**********************"); Thread.sleep(3000); } } @@ -257,6 +301,8 @@ public class NumericProblemSolver { } long endFormingSolution = System.currentTimeMillis(); System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); + } else { + System.out.println("Unsatisfiable"); } return sol; -- cgit v1.2.3-54-g00ecf