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(-) 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