From 69283b38059f5ccede4b4a52ecffa0e64d8f49c9 Mon Sep 17 00:00:00 2001 From: anqili426 Date: Sun, 10 May 2020 22:54:24 -0400 Subject: Added support for real numbers --- .../viatra2logic/NumericProblemSolver.java | 50 +++++++++++++++------- 1 file changed, 35 insertions(+), 15 deletions(-) (limited to 'Framework') 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 8749a5a8..7240f612 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,5 +1,6 @@ package hu.bme.mit.inf.dslreasoner.viatra2logic; +import java.math.BigDecimal; import java.util.ArrayList; import java.util.HashMap; import java.util.HashSet; @@ -23,12 +24,14 @@ import com.microsoft.z3.Context; import com.microsoft.z3.Expr; import com.microsoft.z3.IntExpr; import com.microsoft.z3.Model; +import com.microsoft.z3.RealExpr; 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.RealElement; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; @@ -95,8 +98,8 @@ public class NumericProblemSolver { return result; } - public Map getOneSolution(List objs, Map>> matches) throws Exception { - Map sol = new HashMap(); + 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(); @@ -110,10 +113,17 @@ public class NumericProblemSolver { 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()); + if (o instanceof IntegerElement) { + IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); + Integer oSol = Integer.parseInt(val.toString()); + sol.put(o, oSol); + } else { + RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); + Long oSol = Long.parseLong(val.toString()); + sol.put(o, oSol); + } //System.out.println("Solution:" + o + "->" + oSol); - sol.put(o, oSol); + } else { //System.out.println("not used var:" + o); } @@ -162,23 +172,32 @@ public class NumericProblemSolver { 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()); + boolean isInt = matchedObj instanceof IntegerElement; 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()); + if (isInt) { + expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); + } else { + expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getRealSort()); + } varMap.put(matchedObj, expr); } else { expr = (ArithExpr) varMap.get(matchedObj); } } else { - int value = ((IntegerElement) matchedObj).getValue(); - expr = (ArithExpr) ctx.mkInt(value); + if (isInt) { + int value = ((IntegerElement) matchedObj).getValue(); + expr = (ArithExpr) ctx.mkInt(value); + } else { + long value = (long) ((RealElement) matchedObj).getValue().doubleValue(); + expr = (ArithExpr) ctx.mkReal(value); + } varMap.put(matchedObj, expr); } } @@ -186,6 +205,7 @@ public class NumericProblemSolver { else if (e instanceof XNumberLiteral) { String value = ((XNumberLiteral) e).getValue(); try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){} + try{ long val = Long.parseLong(value); expr = (ArithExpr) ctx.mkReal(val);} catch(NumberFormatException err){} } // Expressions with operators else if (e instanceof XBinaryOperation) { @@ -300,13 +320,13 @@ public class NumericProblemSolver { } */ - /*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>(); + Map>> matches = new HashMap>>(); + Iterable> matchSet = new ArrayList>(); ArrayList allElem = getJvmIdentifiableElements(expression); - List obj = new ArrayList(); + List obj = new ArrayList(); for (int i = 0; i < count; i++) { Map match = new HashMap(); @@ -315,12 +335,12 @@ public class NumericProblemSolver { obj.add(intE); match.put(e, intE); } - matchSet.add(match); + ((ArrayList) matchSet).add(match); matches.put(expression, matchSet); } long start = System.currentTimeMillis(); - Map sol = getOneSolution(obj, matches); + Map sol = getOneSolution(obj, matches); long end = System.currentTimeMillis(); -- cgit v1.2.3-70-g09d2 From d24451ed79bf1080ed8be195eac5047ef91e587f Mon Sep 17 00:00:00 2001 From: anqili426 Date: Mon, 11 May 2020 14:12:17 -0400 Subject: Fixed bug in setting constant types --- .../inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'Framework') 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 7240f612..070b71ad 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 @@ -204,8 +204,15 @@ public class NumericProblemSolver { // 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){} - try{ long val = Long.parseLong(value); expr = (ArithExpr) ctx.mkReal(val);} catch(NumberFormatException err){} + try{ + int val = Integer.parseInt(value); + expr = (ArithExpr) ctx.mkInt(val); + } catch(NumberFormatException err){ + try{ + long val = Long.parseLong(value); + expr = (ArithExpr) ctx.mkReal(val); + } catch(NumberFormatException err2){} + } } // Expressions with operators else if (e instanceof XBinaryOperation) { -- cgit v1.2.3-70-g09d2 From 09c0f7bd18e6cec7f8e37bd2bcac9849636d33d1 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Mon, 11 May 2020 22:03:54 +0200 Subject: Bigliteral serialization in xmi transformation fixed --- .../bme/mit/inf/dslreasoner/logic2ecore/Logic2Ecore.xtend | 14 +++++++++++++- .../visualisation/PartialInterpretation2Gml.xtend | 2 +- 2 files changed, 14 insertions(+), 2 deletions(-) (limited to 'Framework') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic2ecore/src/hu/bme/mit/inf/dslreasoner/logic2ecore/Logic2Ecore.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic2ecore/src/hu/bme/mit/inf/dslreasoner/logic2ecore/Logic2Ecore.xtend index 92deeae6..08c6b7b7 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.logic2ecore/src/hu/bme/mit/inf/dslreasoner/logic2ecore/Logic2Ecore.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic2ecore/src/hu/bme/mit/inf/dslreasoner/logic2ecore/Logic2Ecore.xtend @@ -20,6 +20,8 @@ import org.eclipse.emf.ecore.EcorePackage import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder import java.util.Map +import org.eclipse.emf.ecore.EAttribute +import java.math.BigDecimal class Logic2Ecore { val extension LogicStructureBuilder structureBuilder = new LogicStructureBuilder @@ -92,7 +94,7 @@ class Logic2Ecore { list += l.key } else { try { - sourceObject.eSet(attributeType,l.key) + sourceObject.eSet(attributeType,translateType(attributeType.EAttributeType,l.key)) } catch(Exception e) { e.printStackTrace } @@ -107,6 +109,16 @@ class Logic2Ecore { return element2Object.values.root } + def translateType(EDataType type, Object value) { + if(type == EcorePackage.eINSTANCE.EFloat) { + val bd = value as BigDecimal + return bd.floatValue + } else if( type == EcorePackage.eINSTANCE.EDouble ) { + val bd = value as BigDecimal + return bd.doubleValue + } else return value + } + // if(attributeType.EAttributeType.isSuperTypeOf(targetObject.eClass)) { // val expression = ecore2Logic.IsAttributeValue(forwardTrace,sourceElement,targetElement,attributeType) diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend index 2b42a8b1..190b5c94 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend @@ -107,7 +107,7 @@ class PartialInterpretation2Gml { } def protected transormTitle(DefinedElement object) { - if(object.name!= null)object.name + if(object.name!= null)object.name.replace("\"", "") else "null" } -- cgit v1.2.3-70-g09d2 From dcb8024268969d00ead59209b7866d29cba7fb33 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 12 May 2020 03:02:00 +0200 Subject: precise time measurements for the numeric solver --- .../viatra2logic/NumericProblemSolver.java | 39 ++++++++++++++++------ 1 file changed, 29 insertions(+), 10 deletions(-) (limited to 'Framework') 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 070b71ad..a5b9fc66 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 @@ -56,6 +56,10 @@ public class NumericProblemSolver { private Context ctx; private Solver s; private Map varMap; + + long endformingProblem=0; + long endSolvingProblem=0; + long endFormingSolution=0; public NumericProblemSolver() { HashMap cfg = new HashMap(); @@ -70,7 +74,18 @@ public class NumericProblemSolver { return ctx; } - + public long getEndformingProblem() { + return endformingProblem; + } + + public long getEndSolvingProblem() { + return endSolvingProblem; + } + + public long getEndFormingSolution() { + return endFormingSolution; + } + private ArrayList getJvmIdentifiableElements(XExpression expression) { ArrayList allElem = new ArrayList(); XExpression left = ((XBinaryOperation) expression).getLeftOperand(); @@ -91,26 +106,30 @@ public class NumericProblemSolver { } public boolean isSatisfiable(Map>> matches) throws Exception { + long startformingProblem = System.nanoTime(); BoolExpr problemInstance = formNumericProblemInstance(matches); s.add(problemInstance); + endformingProblem = System.nanoTime()-startformingProblem; + long startSolvingProblem = System.nanoTime(); boolean result = (s.check() == Status.SATISFIABLE); + endSolvingProblem = System.nanoTime()-startSolvingProblem; this.ctx.close(); return result; } public Map getOneSolution(List objs, Map>> matches) throws Exception { Map sol = new HashMap(); - long startformingProblem = System.currentTimeMillis(); + long startformingProblem = System.nanoTime(); BoolExpr problemInstance = formNumericProblemInstance(matches); - long endformingProblem = System.currentTimeMillis(); - System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); + endformingProblem = System.nanoTime()-startformingProblem; + //System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); s.add(problemInstance); - long startSolvingProblem = System.currentTimeMillis(); + long startSolvingProblem = System.nanoTime(); if (s.check() == Status.SATISFIABLE) { Model m = s.getModel(); - long endSolvingProblem = System.currentTimeMillis(); + endSolvingProblem = System.nanoTime()-startSolvingProblem; System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); - long startFormingSolution = System.currentTimeMillis(); + long startFormingSolution = System.nanoTime(); for (PrimitiveElement o: objs) { if(varMap.containsKey(o)) { if (o instanceof IntegerElement) { @@ -128,10 +147,10 @@ public class NumericProblemSolver { //System.out.println("not used var:" + o); } } - long endFormingSolution = System.currentTimeMillis(); - System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); + endFormingSolution = System.nanoTime()-startFormingSolution; + //System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); } else { - System.out.println("Unsatisfiable"); + System.out.println("Unsatisfiable numerical problem"); } this.ctx.close(); return sol; -- cgit v1.2.3-70-g09d2 From 0ca3b7409e1b98bb2ebeb65df9dbe316500302e9 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 12 May 2020 03:19:32 +0200 Subject: logging detailed measurement data for the numerical solver --- .../inf/dslreasoner/viatra2logic/NumericTranslator.xtend | 16 ++++++++++++++++ .../viatrasolver/reasoner/ViatraReasoner.xtend | 11 ++++++++++- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 3 +++ 3 files changed, 29 insertions(+), 1 deletion(-) (limited to 'Framework') 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 index 89719b91..81bc1796 100644 --- 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 @@ -19,6 +19,10 @@ class NumericTranslator { private XExpressionExtractor extractor = new XExpressionExtractor(); + long formingProblemTime=0; + long solvingProblemTime=0; + long formingSolutionTime=0; + val comparator = new Comparator(){ override compare(JvmIdentifiableElement o1, JvmIdentifiableElement o2) { //println('''«o1.simpleName» - «o2.simpleName»''') @@ -52,6 +56,7 @@ class NumericTranslator { val input = formNumericProblemInstance(matches) val solver = new NumericProblemSolver val satisfiability = solver.isSatisfiable(input) + solver.updateTimes return satisfiability } @@ -59,6 +64,17 @@ class NumericTranslator { val input = formNumericProblemInstance(matches) val solver = new NumericProblemSolver val solution = solver.getOneSolution(primitiveElements,input) + solver.updateTimes return solution } + + private def updateTimes(NumericProblemSolver s) { + this.formingProblemTime += s.getEndformingProblem + this.solvingProblemTime += s.getEndSolvingProblem + this.formingSolutionTime += s.getEndFormingSolution + } + + def getFormingProblemTime() {formingProblemTime} + def getSolvingProblemTime() {solvingProblemTime} + def getFormingSolutionTime() {formingSolutionTime} } \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index bafe78f6..293df935 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend @@ -159,7 +159,16 @@ class ViatraReasoner extends LogicReasoner{ it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "NumericalSolverTime" it.value = (strategy.numericSolver.runtime/1000000) as int + it.name = "NumericalSolverSumTime" it.value = (strategy.numericSolver.runtime/1000000) as int + ] + it.entries += createIntStatisticEntry => [ + it.name = "NumericalSolverProblemFormingTime" it.value = (strategy.numericSolver.solverFormingProblem/1000000) as int + ] + it.entries += createIntStatisticEntry => [ + it.name = "NumericalSolverSolvingTime" it.value = (strategy.numericSolver.solverSolvingProblem/1000000) as int + ] + it.entries += createIntStatisticEntry => [ + it.name = "NumericalSolverInterpretingSolution" it.value = (strategy.numericSolver.solverSolution/1000000) as int ] it.entries += createIntStatisticEntry => [ it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index 9da97d30..0fb5d702 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend @@ -56,6 +56,9 @@ class NumericSolver { def getCachingTime(){cachingTime} def getNumberOfSolverCalls(){numberOfSolverCalls} def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} + def getSolverFormingProblem(){this.t.formingProblemTime} + def getSolverSolvingProblem(){this.t.solvingProblemTime} + def getSolverSolution(){this.t.formingSolutionTime} def boolean maySatisfiable() { isSatisfiable(this.constraint2MustUnitPropagationPrecondition) -- cgit v1.2.3-70-g09d2 From cdf6729249f723865ca7a6636d49bee50a1f5f80 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 12 May 2020 03:19:49 +0200 Subject: removed unnecesary printing --- .../hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Framework') 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 a5b9fc66..5bef061a 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 @@ -128,7 +128,7 @@ public class NumericProblemSolver { if (s.check() == Status.SATISFIABLE) { Model m = s.getModel(); endSolvingProblem = System.nanoTime()-startSolvingProblem; - System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); + //System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); long startFormingSolution = System.nanoTime(); for (PrimitiveElement o: objs) { if(varMap.containsKey(o)) { -- cgit v1.2.3-70-g09d2 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') 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 From 28b8a136335733343360d2e6ff0bbdb959334386 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Thu, 14 May 2020 23:06:40 +0200 Subject: separtor ; -> \t --- .../inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Framework') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend index d673cb17..d6dc1c5e 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend @@ -17,7 +17,7 @@ class StatisticsData { } class StatisticSections2CSV { - static val separator = ';' + static val separator = '\t' static val empty = "" private def getValue(Map map,String key) { -- cgit v1.2.3-70-g09d2 From 73738a94151363ae96557d749ff4ab93d941f983 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Sun, 17 May 2020 01:34:05 +0200 Subject: Setting delimier in every printing mode to ',' --- .../inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend | 2 +- .../dslreasoner/logic/model/statistics/StatisticSections2Print.xtend | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'Framework') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend index d6dc1c5e..a78ceb19 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend @@ -17,7 +17,7 @@ class StatisticsData { } class StatisticSections2CSV { - static val separator = '\t' + static val separator = ',' static val empty = "" private def getValue(Map map,String key) { diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend index 39370d75..c5e81f94 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend @@ -12,7 +12,7 @@ class StatisticSections2Print { { var result = ""; for(statistic : statistics) { - result+= '''«statistic.readValue»;''' + result+= '''«statistic.readValue»,''' } return result } -- cgit v1.2.3-70-g09d2