diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 50 |
1 files changed, 35 insertions, 15 deletions
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | 1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; |
2 | 2 | ||
3 | import java.math.BigDecimal; | ||
3 | import java.util.ArrayList; | 4 | import java.util.ArrayList; |
4 | import java.util.HashMap; | 5 | import java.util.HashMap; |
5 | import java.util.HashSet; | 6 | import java.util.HashSet; |
@@ -23,12 +24,14 @@ import com.microsoft.z3.Context; | |||
23 | import com.microsoft.z3.Expr; | 24 | import com.microsoft.z3.Expr; |
24 | import com.microsoft.z3.IntExpr; | 25 | import com.microsoft.z3.IntExpr; |
25 | import com.microsoft.z3.Model; | 26 | import com.microsoft.z3.Model; |
27 | import com.microsoft.z3.RealExpr; | ||
26 | import com.microsoft.z3.Solver; | 28 | import com.microsoft.z3.Solver; |
27 | import com.microsoft.z3.Status; | 29 | import com.microsoft.z3.Status; |
28 | import com.microsoft.z3.enumerations.Z3_ast_print_mode; | 30 | import com.microsoft.z3.enumerations.Z3_ast_print_mode; |
29 | 31 | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | 32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; |
31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | 33 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; |
34 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; | ||
32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 35 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
33 | 36 | ||
34 | 37 | ||
@@ -95,8 +98,8 @@ public class NumericProblemSolver { | |||
95 | return result; | 98 | return result; |
96 | } | 99 | } |
97 | 100 | ||
98 | public Map<PrimitiveElement,Integer> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 101 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
99 | Map<PrimitiveElement,Integer> sol = new HashMap<PrimitiveElement, Integer>(); | 102 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); |
100 | long startformingProblem = System.currentTimeMillis(); | 103 | long startformingProblem = System.currentTimeMillis(); |
101 | BoolExpr problemInstance = formNumericProblemInstance(matches); | 104 | BoolExpr problemInstance = formNumericProblemInstance(matches); |
102 | long endformingProblem = System.currentTimeMillis(); | 105 | long endformingProblem = System.currentTimeMillis(); |
@@ -110,10 +113,17 @@ public class NumericProblemSolver { | |||
110 | long startFormingSolution = System.currentTimeMillis(); | 113 | long startFormingSolution = System.currentTimeMillis(); |
111 | for (PrimitiveElement o: objs) { | 114 | for (PrimitiveElement o: objs) { |
112 | if(varMap.containsKey(o)) { | 115 | if(varMap.containsKey(o)) { |
113 | IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); | 116 | if (o instanceof IntegerElement) { |
114 | Integer oSol = Integer.parseInt(val.toString()); | 117 | IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); |
118 | Integer oSol = Integer.parseInt(val.toString()); | ||
119 | sol.put(o, oSol); | ||
120 | } else { | ||
121 | RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); | ||
122 | Long oSol = Long.parseLong(val.toString()); | ||
123 | sol.put(o, oSol); | ||
124 | } | ||
115 | //System.out.println("Solution:" + o + "->" + oSol); | 125 | //System.out.println("Solution:" + o + "->" + oSol); |
116 | sol.put(o, oSol); | 126 | |
117 | } else { | 127 | } else { |
118 | //System.out.println("not used var:" + o); | 128 | //System.out.println("not used var:" + o); |
119 | } | 129 | } |
@@ -162,23 +172,32 @@ public class NumericProblemSolver { | |||
162 | return constraint; | 172 | return constraint; |
163 | } | 173 | } |
164 | 174 | ||
165 | // TODO: add variable: state of the solver | ||
166 | private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { | 175 | private ArithExpr formNumericConstraintHelper(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception { |
167 | ArithExpr expr = null; | 176 | ArithExpr expr = null; |
168 | // Variables | 177 | // Variables |
169 | if (e instanceof XFeatureCall) { | 178 | if (e instanceof XFeatureCall) { |
170 | PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); | 179 | PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); |
180 | boolean isInt = matchedObj instanceof IntegerElement; | ||
171 | if (!matchedObj.isValueSet()) { | 181 | if (!matchedObj.isValueSet()) { |
172 | if (varMap.get(matchedObj) == null) { | 182 | if (varMap.get(matchedObj) == null) { |
173 | String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString(); | 183 | String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString(); |
174 | expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); | 184 | if (isInt) { |
185 | expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); | ||
186 | } else { | ||
187 | expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getRealSort()); | ||
188 | } | ||
175 | varMap.put(matchedObj, expr); | 189 | varMap.put(matchedObj, expr); |
176 | } else { | 190 | } else { |
177 | expr = (ArithExpr) varMap.get(matchedObj); | 191 | expr = (ArithExpr) varMap.get(matchedObj); |
178 | } | 192 | } |
179 | } else { | 193 | } else { |
180 | int value = ((IntegerElement) matchedObj).getValue(); | 194 | if (isInt) { |
181 | expr = (ArithExpr) ctx.mkInt(value); | 195 | int value = ((IntegerElement) matchedObj).getValue(); |
196 | expr = (ArithExpr) ctx.mkInt(value); | ||
197 | } else { | ||
198 | long value = (long) ((RealElement) matchedObj).getValue().doubleValue(); | ||
199 | expr = (ArithExpr) ctx.mkReal(value); | ||
200 | } | ||
182 | varMap.put(matchedObj, expr); | 201 | varMap.put(matchedObj, expr); |
183 | } | 202 | } |
184 | } | 203 | } |
@@ -186,6 +205,7 @@ public class NumericProblemSolver { | |||
186 | else if (e instanceof XNumberLiteral) { | 205 | else if (e instanceof XNumberLiteral) { |
187 | String value = ((XNumberLiteral) e).getValue(); | 206 | String value = ((XNumberLiteral) e).getValue(); |
188 | try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){} | 207 | try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){} |
208 | try{ long val = Long.parseLong(value); expr = (ArithExpr) ctx.mkReal(val);} catch(NumberFormatException err){} | ||
189 | } | 209 | } |
190 | // Expressions with operators | 210 | // Expressions with operators |
191 | else if (e instanceof XBinaryOperation) { | 211 | else if (e instanceof XBinaryOperation) { |
@@ -300,13 +320,13 @@ public class NumericProblemSolver { | |||
300 | } | 320 | } |
301 | */ | 321 | */ |
302 | 322 | ||
303 | /*public void testGetOneSol(XExpression expression, Term t) throws Exception { | 323 | /* public void testGetOneSol(XExpression expression, Term t) throws Exception { |
304 | int count = 10; | 324 | int count = 10; |
305 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | 325 | Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>>(); |
306 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); | 326 | Iterable<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new ArrayList<Map<JvmIdentifiableElement,PrimitiveElement>>(); |
307 | 327 | ||
308 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | 328 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); |
309 | List<Object> obj = new ArrayList<Object>(); | 329 | List<PrimitiveElement> obj = new ArrayList<PrimitiveElement>(); |
310 | 330 | ||
311 | for (int i = 0; i < count; i++) { | 331 | for (int i = 0; i < count; i++) { |
312 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | 332 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); |
@@ -315,12 +335,12 @@ public class NumericProblemSolver { | |||
315 | obj.add(intE); | 335 | obj.add(intE); |
316 | match.put(e, intE); | 336 | match.put(e, intE); |
317 | } | 337 | } |
318 | matchSet.add(match); | 338 | ((ArrayList) matchSet).add(match); |
319 | matches.put(expression, matchSet); | 339 | matches.put(expression, matchSet); |
320 | } | 340 | } |
321 | 341 | ||
322 | long start = System.currentTimeMillis(); | 342 | long start = System.currentTimeMillis(); |
323 | Map<Object,Integer> sol = getOneSolution(obj, matches); | 343 | Map<PrimitiveElement,Integer> sol = getOneSolution(obj, matches); |
324 | long end = System.currentTimeMillis(); | 344 | long end = System.currentTimeMillis(); |
325 | 345 | ||
326 | 346 | ||