From 97924852b86bd49236cc6214345bf8d2b2d93d66 Mon Sep 17 00:00:00 2001 From: anqili426 Date: Wed, 13 May 2020 15:34:54 -0400 Subject: Use String to create RealExpr --- .../viatra2logic/NumericProblemSolver.java | 81 +++++++++++----------- 1 file changed, 40 insertions(+), 41 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit') 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 5bef061a..0b249962 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 @@ -52,11 +52,11 @@ 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; - + long endformingProblem=0; long endSolvingProblem=0; long endFormingSolution=0; @@ -73,7 +73,7 @@ public class NumericProblemSolver { public Context getNumericProblemContext() { return ctx; } - + public long getEndformingProblem() { return endformingProblem; } @@ -90,12 +90,12 @@ public class NumericProblemSolver { 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()); @@ -104,7 +104,7 @@ public class NumericProblemSolver { getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); } } - + public boolean isSatisfiable(Map>> matches) throws Exception { long startformingProblem = System.nanoTime(); BoolExpr problemInstance = formNumericProblemInstance(matches); @@ -116,7 +116,7 @@ public class NumericProblemSolver { this.ctx.close(); return result; } - + public Map getOneSolution(List objs, Map>> matches) throws Exception { Map sol = new HashMap(); long startformingProblem = System.nanoTime(); @@ -138,11 +138,11 @@ public class NumericProblemSolver { sol.put(o, oSol); } else { RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); - Long oSol = Long.parseLong(val.toString()); + Double oSol = Double.parseDouble(val.toString()); sol.put(o, oSol); } //System.out.println("Solution:" + o + "->" + oSol); - + } else { //System.out.println("not used var:" + o); } @@ -164,7 +164,7 @@ public class NumericProblemSolver { 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); @@ -187,7 +187,7 @@ public class NumericProblemSolver { } else { throw new Exception ("Unsupported binary operation " + name); } - + return constraint; } @@ -214,8 +214,8 @@ public class NumericProblemSolver { int value = ((IntegerElement) matchedObj).getValue(); expr = (ArithExpr) ctx.mkInt(value); } else { - long value = (long) ((RealElement) matchedObj).getValue().doubleValue(); - expr = (ArithExpr) ctx.mkReal(value); + double value = ((RealElement) matchedObj).getValue().doubleValue(); + expr = (ArithExpr) ctx.mkReal(String.valueOf(value)); } varMap.put(matchedObj, expr); } @@ -228,8 +228,7 @@ public class NumericProblemSolver { expr = (ArithExpr) ctx.mkInt(val); } catch(NumberFormatException err){ try{ - long val = Long.parseLong(value); - expr = (ArithExpr) ctx.mkReal(val); + expr = (ArithExpr) ctx.mkReal(value); } catch(NumberFormatException err2){} } } @@ -264,7 +263,7 @@ public class NumericProblemSolver { 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()) { @@ -276,15 +275,15 @@ public class NumericProblemSolver { } return constraintInstances; } - - + + /* public void testIsSat(XExpression expression, Term t) throws Exception { int count = 10000; Map>> matches = new HashMap>>(); Set> matchSet = new HashSet>(); ArrayList allElem = getJvmIdentifiableElements(expression); - + for (int i = 0; i < count; i++) { Map match = new HashMap(); for (JvmIdentifiableElement e: allElem) { @@ -293,7 +292,7 @@ public class NumericProblemSolver { } matchSet.add(match); } - + matches.put(expression, matchSet); long start = System.currentTimeMillis(); boolean sat = isSatisfiable(matches); @@ -302,7 +301,7 @@ public class NumericProblemSolver { 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>(); @@ -319,11 +318,11 @@ public class NumericProblemSolver { } else { int2 = intE; } - + match.put(e, intE); } matchSet.add(match); - + Map match2 = new HashMap(); boolean first2 = true; for (JvmIdentifiableElement e: allElem) { @@ -335,7 +334,7 @@ public class NumericProblemSolver { } } matchSet.add(match2); - + matches.put(expression, matchSet); long start = System.currentTimeMillis(); boolean sat = isSatisfiable(matches); @@ -344,16 +343,16 @@ 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>>(); Iterable> matchSet = new ArrayList>(); - + ArrayList allElem = getJvmIdentifiableElements(expression); List obj = new ArrayList(); - + for (int i = 0; i < count; i++) { Map match = new HashMap(); for (JvmIdentifiableElement e: allElem) { @@ -364,18 +363,18 @@ public class NumericProblemSolver { ((ArrayList) 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)); }*/ @@ -400,7 +399,7 @@ public class NumericProblemSolver { obj.add(intE); match.put(e, intE); } - + Map match2 = new HashMap(); boolean first2 = true; for (JvmIdentifiableElement e: allElem) { @@ -414,13 +413,13 @@ public class NumericProblemSolver { obj.add(intE); match2.put(e, intE); } - - + + matchSet.add(match); matchSet.add(match2); } matches.put(expression, matchSet); - + System.out.println("Number of matches: " + matchSet.size()); for (int i = 0; i < 10; i++) { Map sol = getOneSolution(obj, matches); @@ -428,7 +427,7 @@ public class NumericProblemSolver { Thread.sleep(3000); } } - + public void testGetOneSol3(XExpression expression, Term t) throws Exception { int count = 15000; Random rand = new Random(); @@ -462,7 +461,7 @@ public class NumericProblemSolver { 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); @@ -470,5 +469,5 @@ public class NumericProblemSolver { Thread.sleep(3000); } } - */ + */ } -- cgit v1.2.3-70-g09d2