From 3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Sat, 9 May 2020 20:33:19 +0200 Subject: Numeric Solver integration to exploration --- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 2 +- .../viatra2logic/NumericProblemSolver.java | 334 +++++++++++---------- .../viatra2logic/NumericTranslator.xtend | 64 ++++ 3 files changed, 238 insertions(+), 162 deletions(-) create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend (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 a27e8904..b4303739 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 @@ -26,7 +26,7 @@ class ExpressionEvaluation2Logic { // numericSolver.testIsNotSat(expression, expression.transform(variable2Variable)); // numericSolver.testGetOneSol(expression, expression.transform(variable2Variable)); // numericSolver.testGetOneSol2(expression, expression.transform(variable2Variable)); - numericSolver.testGetOneSol3(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 ff3a85eb..0e6e824c 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,9 +5,12 @@ import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.Map.Entry; import java.util.Random; import java.util.Set; +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint; +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation; import org.eclipse.xtext.common.types.JvmIdentifiableElement; import org.eclipse.xtext.xbase.XBinaryOperation; import org.eclipse.xtext.xbase.XExpression; @@ -46,6 +49,7 @@ public class NumericProblemSolver { private static final String N_EQUALS3 = "operator_tripleEquals"; private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; + private Context ctx; private Solver s; private Map varMap; @@ -63,6 +67,170 @@ public class NumericProblemSolver { return ctx; } + + 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 { + BoolExpr problemInstance = formNumericProblemInstance(matches); + s.add(problemInstance); + return s.check() == Status.SATISFIABLE; + } + + 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 (PrimitiveElement o: objs) { + if(varMap.containsKey(o)) { + IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); + Integer oSol = Integer.parseInt(val.toString()); + //System.out.println("Solution:" + o + "->" + oSol); + sol.put(o, oSol); + } else { + //System.out.println("not used var:" + o); + } + } + long endFormingSolution = System.currentTimeMillis(); + System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); + } else { + System.out.println("Unsatisfiable"); + } + + return sol; + } + + private BoolExpr formNumericConstraint(XExpression e, Map aMatch) 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 = 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); + } 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); + } + + return constraint; + } + + // TODO: add variable: state of the solver + private ArithExpr formNumericConstraintHelper(XExpression e, Map aMatch) throws Exception { + ArithExpr expr = null; + // Variables + if (e instanceof XFeatureCall) { + 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) { + String value = ((XNumberLiteral) e).getValue(); + try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){} + } + // Expressions with operators + else if (e instanceof XBinaryOperation) { + String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); + 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); + } 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); + } + + private BoolExpr formNumericProblemInstance(Map>> matches) throws Exception { + BoolExpr constraintInstances = ctx.mkTrue(); + for (XExpression e: matches.keySet()) { + Iterable> matchSets = matches.get(e); + for (Map aMatch: matchSets) { + BoolExpr constraintInstance = ctx.mkNot(formNumericConstraint(e, aMatch)); + constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); + } + } + return constraintInstances; + } + + + /* public void testIsSat(XExpression expression, Term t) throws Exception { int count = 10000; Map>> matches = new HashMap>>(); @@ -87,7 +255,6 @@ public class NumericProblemSolver { System.out.println("Running time:" + (end - start)); } - public void testIsNotSat(XExpression expression, Term t) throws Exception { Map>> matches = new HashMap>>(); Set> matchSet = new HashSet>(); @@ -129,9 +296,9 @@ public class NumericProblemSolver { System.out.println("Number of matches: "); System.out.println("Running time:" + (end - start)); } - + */ - public void testGetOneSol(XExpression expression, Term t) throws Exception { + /*public void testGetOneSol(XExpression expression, Term t) throws Exception { int count = 10; Map>> matches = new HashMap>>(); Set> matchSet = new HashSet>(); @@ -163,8 +330,8 @@ public class NumericProblemSolver { 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 = 250; Map>> matches = new HashMap>>(); @@ -255,160 +422,5 @@ public class NumericProblemSolver { Thread.sleep(3000); } } - - 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 { - BoolExpr problemInstance = formNumericProblemInstance(matches); - s.add(problemInstance); - return s.check() == Status.SATISFIABLE; - } - - 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)); - } else { - System.out.println("Unsatisfiable"); - } - - return sol; - } - - private BoolExpr formNumericConstraint(XExpression e, Map aMatch) 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 = 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); - } 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); - } - - return constraint; - } - - // TODO: add variable: state of the solver - private ArithExpr formNumericConstraintHelper(XExpression e, Map aMatch) throws Exception { - ArithExpr expr = null; - // Variables - if (e instanceof XFeatureCall) { - 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) { - String value = ((XNumberLiteral) e).getValue(); - try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){} - } - // Expressions with operators - else if (e instanceof XBinaryOperation) { - String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); - 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); - } 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); - } - - private BoolExpr formNumericProblemInstance(Map>> matches) throws Exception { - BoolExpr constraintInstances = ctx.mkTrue(); - for (XExpression e: matches.keySet()) { - Set> matchSets = matches.get(e); - for (Map aMatch: matchSets) { - BoolExpr constraintInstance = formNumericConstraint(e, aMatch); - constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); - } - } - return constraintInstances; - } + */ } diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend new file mode 100644 index 00000000..89719b91 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend @@ -0,0 +1,64 @@ +package hu.bme.mit.inf.dslreasoner.viatra2logic + +import org.eclipse.xtext.xbase.XExpression +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation +import org.eclipse.xtext.common.types.JvmIdentifiableElement +import java.util.Set +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement +import java.util.Map +import com.microsoft.z3.BoolExpr +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import java.util.Map.Entry +import org.eclipse.xtext.xbase.XFeatureCall +import java.util.Comparator +import java.util.ArrayList +import java.util.HashMap +import java.util.List + +class NumericTranslator { + + private XExpressionExtractor extractor = new XExpressionExtractor(); + + val comparator = new Comparator(){ + override compare(JvmIdentifiableElement o1, JvmIdentifiableElement o2) { + //println('''«o1.simpleName» - «o2.simpleName»''') + o1.simpleName.compareTo(o2.simpleName) + } + } + def Map arrayToMap(Object[] tuple, ArrayList variablesInOrder) { + val res = new HashMap + for(var i=0; i> matches) throws Exception { + val res = new HashMap + for (Entry> entry: matches.entrySet()) { + val ExpressionEvaluation constraint = entry.getKey() as ExpressionEvaluation; + val XExpression expression = extractor.extractExpression(constraint.getEvaluator()); + val Iterable tuples = entry.getValue(); + val features = expression.eAllContents.filter(XFeatureCall).map[it.feature].toSet + val variablesInOrder = new ArrayList(features) + variablesInOrder.toList.sort(comparator) + //println(variablesInOrder) + val map = tuples.map[it.arrayToMap(variablesInOrder)] + res.put(expression,map) + } + return res + } + + def delegateIsSatisfiable(Map> matches) { + val input = formNumericProblemInstance(matches) + val solver = new NumericProblemSolver + val satisfiability = solver.isSatisfiable(input) + return satisfiability + } + + def delegateGetSolution(List primitiveElements, Map> matches) { + val input = formNumericProblemInstance(matches) + val solver = new NumericProblemSolver + val solution = solver.getOneSolution(primitiveElements,input) + return solution + } +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf