diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 81 |
1 files changed, 40 insertions, 41 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 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 { | |||
52 | private static final String N_EQUALS3 = "operator_tripleEquals"; | 52 | private static final String N_EQUALS3 = "operator_tripleEquals"; |
53 | private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; | 53 | private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; |
54 | 54 | ||
55 | 55 | ||
56 | private Context ctx; | 56 | private Context ctx; |
57 | private Solver s; | 57 | private Solver s; |
58 | private Map<Object, Expr> varMap; | 58 | private Map<Object, Expr> varMap; |
59 | 59 | ||
60 | long endformingProblem=0; | 60 | long endformingProblem=0; |
61 | long endSolvingProblem=0; | 61 | long endSolvingProblem=0; |
62 | long endFormingSolution=0; | 62 | long endFormingSolution=0; |
@@ -73,7 +73,7 @@ public class NumericProblemSolver { | |||
73 | public Context getNumericProblemContext() { | 73 | public Context getNumericProblemContext() { |
74 | return ctx; | 74 | return ctx; |
75 | } | 75 | } |
76 | 76 | ||
77 | public long getEndformingProblem() { | 77 | public long getEndformingProblem() { |
78 | return endformingProblem; | 78 | return endformingProblem; |
79 | } | 79 | } |
@@ -90,12 +90,12 @@ public class NumericProblemSolver { | |||
90 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | 90 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); |
91 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); | 91 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); |
92 | XExpression right = ((XBinaryOperation) expression).getRightOperand(); | 92 | XExpression right = ((XBinaryOperation) expression).getRightOperand(); |
93 | 93 | ||
94 | getJvmIdentifiableElementsHelper(left, allElem); | 94 | getJvmIdentifiableElementsHelper(left, allElem); |
95 | getJvmIdentifiableElementsHelper(right, allElem); | 95 | getJvmIdentifiableElementsHelper(right, allElem); |
96 | return allElem; | 96 | return allElem; |
97 | } | 97 | } |
98 | 98 | ||
99 | private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) { | 99 | private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) { |
100 | if (e instanceof XFeatureCall) { | 100 | if (e instanceof XFeatureCall) { |
101 | allElem.add(((XFeatureCall) e).getFeature()); | 101 | allElem.add(((XFeatureCall) e).getFeature()); |
@@ -104,7 +104,7 @@ public class NumericProblemSolver { | |||
104 | getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); | 104 | getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); |
105 | } | 105 | } |
106 | } | 106 | } |
107 | 107 | ||
108 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 108 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
109 | long startformingProblem = System.nanoTime(); | 109 | long startformingProblem = System.nanoTime(); |
110 | BoolExpr problemInstance = formNumericProblemInstance(matches); | 110 | BoolExpr problemInstance = formNumericProblemInstance(matches); |
@@ -116,7 +116,7 @@ public class NumericProblemSolver { | |||
116 | this.ctx.close(); | 116 | this.ctx.close(); |
117 | return result; | 117 | return result; |
118 | } | 118 | } |
119 | 119 | ||
120 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 120 | public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
121 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); | 121 | Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>(); |
122 | long startformingProblem = System.nanoTime(); | 122 | long startformingProblem = System.nanoTime(); |
@@ -138,11 +138,11 @@ public class NumericProblemSolver { | |||
138 | sol.put(o, oSol); | 138 | sol.put(o, oSol); |
139 | } else { | 139 | } else { |
140 | RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); | 140 | RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false); |
141 | Long oSol = Long.parseLong(val.toString()); | 141 | Double oSol = Double.parseDouble(val.toString()); |
142 | sol.put(o, oSol); | 142 | sol.put(o, oSol); |
143 | } | 143 | } |
144 | //System.out.println("Solution:" + o + "->" + oSol); | 144 | //System.out.println("Solution:" + o + "->" + oSol); |
145 | 145 | ||
146 | } else { | 146 | } else { |
147 | //System.out.println("not used var:" + o); | 147 | //System.out.println("not used var:" + o); |
148 | } | 148 | } |
@@ -164,7 +164,7 @@ public class NumericProblemSolver { | |||
164 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); | 164 | String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); |
165 | 165 | ||
166 | BoolExpr constraint = null; | 166 | BoolExpr constraint = null; |
167 | 167 | ||
168 | ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); | 168 | ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); |
169 | ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); | 169 | ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); |
170 | 170 | ||
@@ -187,7 +187,7 @@ public class NumericProblemSolver { | |||
187 | } else { | 187 | } else { |
188 | throw new Exception ("Unsupported binary operation " + name); | 188 | throw new Exception ("Unsupported binary operation " + name); |
189 | } | 189 | } |
190 | 190 | ||
191 | return constraint; | 191 | return constraint; |
192 | } | 192 | } |
193 | 193 | ||
@@ -214,8 +214,8 @@ public class NumericProblemSolver { | |||
214 | int value = ((IntegerElement) matchedObj).getValue(); | 214 | int value = ((IntegerElement) matchedObj).getValue(); |
215 | expr = (ArithExpr) ctx.mkInt(value); | 215 | expr = (ArithExpr) ctx.mkInt(value); |
216 | } else { | 216 | } else { |
217 | long value = (long) ((RealElement) matchedObj).getValue().doubleValue(); | 217 | double value = ((RealElement) matchedObj).getValue().doubleValue(); |
218 | expr = (ArithExpr) ctx.mkReal(value); | 218 | expr = (ArithExpr) ctx.mkReal(String.valueOf(value)); |
219 | } | 219 | } |
220 | varMap.put(matchedObj, expr); | 220 | varMap.put(matchedObj, expr); |
221 | } | 221 | } |
@@ -228,8 +228,7 @@ public class NumericProblemSolver { | |||
228 | expr = (ArithExpr) ctx.mkInt(val); | 228 | expr = (ArithExpr) ctx.mkInt(val); |
229 | } catch(NumberFormatException err){ | 229 | } catch(NumberFormatException err){ |
230 | try{ | 230 | try{ |
231 | long val = Long.parseLong(value); | 231 | expr = (ArithExpr) ctx.mkReal(value); |
232 | expr = (ArithExpr) ctx.mkReal(val); | ||
233 | } catch(NumberFormatException err2){} | 232 | } catch(NumberFormatException err2){} |
234 | } | 233 | } |
235 | } | 234 | } |
@@ -264,7 +263,7 @@ public class NumericProblemSolver { | |||
264 | private boolean nameEndsWith(String name, String end) { | 263 | private boolean nameEndsWith(String name, String end) { |
265 | return name.startsWith(N_Base) && name.endsWith(end); | 264 | return name.startsWith(N_Base) && name.endsWith(end); |
266 | } | 265 | } |
267 | 266 | ||
268 | private BoolExpr formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 267 | private BoolExpr formNumericProblemInstance(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
269 | BoolExpr constraintInstances = ctx.mkTrue(); | 268 | BoolExpr constraintInstances = ctx.mkTrue(); |
270 | for (XExpression e: matches.keySet()) { | 269 | for (XExpression e: matches.keySet()) { |
@@ -276,15 +275,15 @@ public class NumericProblemSolver { | |||
276 | } | 275 | } |
277 | return constraintInstances; | 276 | return constraintInstances; |
278 | } | 277 | } |
279 | 278 | ||
280 | 279 | ||
281 | /* | 280 | /* |
282 | public void testIsSat(XExpression expression, Term t) throws Exception { | 281 | public void testIsSat(XExpression expression, Term t) throws Exception { |
283 | int count = 10000; | 282 | int count = 10000; |
284 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | 283 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); |
285 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); | 284 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); |
286 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | 285 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); |
287 | 286 | ||
288 | for (int i = 0; i < count; i++) { | 287 | for (int i = 0; i < count; i++) { |
289 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | 288 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); |
290 | for (JvmIdentifiableElement e: allElem) { | 289 | for (JvmIdentifiableElement e: allElem) { |
@@ -293,7 +292,7 @@ public class NumericProblemSolver { | |||
293 | } | 292 | } |
294 | matchSet.add(match); | 293 | matchSet.add(match); |
295 | } | 294 | } |
296 | 295 | ||
297 | matches.put(expression, matchSet); | 296 | matches.put(expression, matchSet); |
298 | long start = System.currentTimeMillis(); | 297 | long start = System.currentTimeMillis(); |
299 | boolean sat = isSatisfiable(matches); | 298 | boolean sat = isSatisfiable(matches); |
@@ -302,7 +301,7 @@ public class NumericProblemSolver { | |||
302 | System.out.println("Number of matches: " + count); | 301 | System.out.println("Number of matches: " + count); |
303 | System.out.println("Running time:" + (end - start)); | 302 | System.out.println("Running time:" + (end - start)); |
304 | } | 303 | } |
305 | 304 | ||
306 | public void testIsNotSat(XExpression expression, Term t) throws Exception { | 305 | public void testIsNotSat(XExpression expression, Term t) throws Exception { |
307 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | 306 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); |
308 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); | 307 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); |
@@ -319,11 +318,11 @@ public class NumericProblemSolver { | |||
319 | } else { | 318 | } else { |
320 | int2 = intE; | 319 | int2 = intE; |
321 | } | 320 | } |
322 | 321 | ||
323 | match.put(e, intE); | 322 | match.put(e, intE); |
324 | } | 323 | } |
325 | matchSet.add(match); | 324 | matchSet.add(match); |
326 | 325 | ||
327 | Map<JvmIdentifiableElement,PrimitiveElement> match2 = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | 326 | Map<JvmIdentifiableElement,PrimitiveElement> match2 = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); |
328 | boolean first2 = true; | 327 | boolean first2 = true; |
329 | for (JvmIdentifiableElement e: allElem) { | 328 | for (JvmIdentifiableElement e: allElem) { |
@@ -335,7 +334,7 @@ public class NumericProblemSolver { | |||
335 | } | 334 | } |
336 | } | 335 | } |
337 | matchSet.add(match2); | 336 | matchSet.add(match2); |
338 | 337 | ||
339 | matches.put(expression, matchSet); | 338 | matches.put(expression, matchSet); |
340 | long start = System.currentTimeMillis(); | 339 | long start = System.currentTimeMillis(); |
341 | boolean sat = isSatisfiable(matches); | 340 | boolean sat = isSatisfiable(matches); |
@@ -344,16 +343,16 @@ public class NumericProblemSolver { | |||
344 | System.out.println("Number of matches: "); | 343 | System.out.println("Number of matches: "); |
345 | System.out.println("Running time:" + (end - start)); | 344 | System.out.println("Running time:" + (end - start)); |
346 | } | 345 | } |
347 | */ | 346 | */ |
348 | 347 | ||
349 | /* public void testGetOneSol(XExpression expression, Term t) throws Exception { | 348 | /* public void testGetOneSol(XExpression expression, Term t) throws Exception { |
350 | int count = 10; | 349 | int count = 10; |
351 | Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | 350 | Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>>(); |
352 | Iterable<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new ArrayList<Map<JvmIdentifiableElement,PrimitiveElement>>(); | 351 | Iterable<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new ArrayList<Map<JvmIdentifiableElement,PrimitiveElement>>(); |
353 | 352 | ||
354 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | 353 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); |
355 | List<PrimitiveElement> obj = new ArrayList<PrimitiveElement>(); | 354 | List<PrimitiveElement> obj = new ArrayList<PrimitiveElement>(); |
356 | 355 | ||
357 | for (int i = 0; i < count; i++) { | 356 | for (int i = 0; i < count; i++) { |
358 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | 357 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); |
359 | for (JvmIdentifiableElement e: allElem) { | 358 | for (JvmIdentifiableElement e: allElem) { |
@@ -364,18 +363,18 @@ public class NumericProblemSolver { | |||
364 | ((ArrayList) matchSet).add(match); | 363 | ((ArrayList) matchSet).add(match); |
365 | matches.put(expression, matchSet); | 364 | matches.put(expression, matchSet); |
366 | } | 365 | } |
367 | 366 | ||
368 | long start = System.currentTimeMillis(); | 367 | long start = System.currentTimeMillis(); |
369 | Map<PrimitiveElement,Integer> sol = getOneSolution(obj, matches); | 368 | Map<PrimitiveElement,Integer> sol = getOneSolution(obj, matches); |
370 | long end = System.currentTimeMillis(); | 369 | long end = System.currentTimeMillis(); |
371 | 370 | ||
372 | 371 | ||
373 | // Print sol | 372 | // Print sol |
374 | for (Object o: sol.keySet()) { | 373 | for (Object o: sol.keySet()) { |
375 | System.out.println(o + " :" + sol.get(o)); | 374 | System.out.println(o + " :" + sol.get(o)); |
376 | } | 375 | } |
377 | 376 | ||
378 | 377 | ||
379 | System.out.println("Number of matches: " + count); | 378 | System.out.println("Number of matches: " + count); |
380 | System.out.println("Running time:" + (end - start)); | 379 | System.out.println("Running time:" + (end - start)); |
381 | }*/ | 380 | }*/ |
@@ -400,7 +399,7 @@ public class NumericProblemSolver { | |||
400 | obj.add(intE); | 399 | obj.add(intE); |
401 | match.put(e, intE); | 400 | match.put(e, intE); |
402 | } | 401 | } |
403 | 402 | ||
404 | Map<JvmIdentifiableElement,PrimitiveElement> match2 = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | 403 | Map<JvmIdentifiableElement,PrimitiveElement> match2 = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); |
405 | boolean first2 = true; | 404 | boolean first2 = true; |
406 | for (JvmIdentifiableElement e: allElem) { | 405 | for (JvmIdentifiableElement e: allElem) { |
@@ -414,13 +413,13 @@ public class NumericProblemSolver { | |||
414 | obj.add(intE); | 413 | obj.add(intE); |
415 | match2.put(e, intE); | 414 | match2.put(e, intE); |
416 | } | 415 | } |
417 | 416 | ||
418 | 417 | ||
419 | matchSet.add(match); | 418 | matchSet.add(match); |
420 | matchSet.add(match2); | 419 | matchSet.add(match2); |
421 | } | 420 | } |
422 | matches.put(expression, matchSet); | 421 | matches.put(expression, matchSet); |
423 | 422 | ||
424 | System.out.println("Number of matches: " + matchSet.size()); | 423 | System.out.println("Number of matches: " + matchSet.size()); |
425 | for (int i = 0; i < 10; i++) { | 424 | for (int i = 0; i < 10; i++) { |
426 | Map<Object,Integer> sol = getOneSolution(obj, matches); | 425 | Map<Object,Integer> sol = getOneSolution(obj, matches); |
@@ -428,7 +427,7 @@ public class NumericProblemSolver { | |||
428 | Thread.sleep(3000); | 427 | Thread.sleep(3000); |
429 | } | 428 | } |
430 | } | 429 | } |
431 | 430 | ||
432 | public void testGetOneSol3(XExpression expression, Term t) throws Exception { | 431 | public void testGetOneSol3(XExpression expression, Term t) throws Exception { |
433 | int count = 15000; | 432 | int count = 15000; |
434 | Random rand = new Random(); | 433 | Random rand = new Random(); |
@@ -462,7 +461,7 @@ public class NumericProblemSolver { | |||
462 | matchSet.add(match); | 461 | matchSet.add(match); |
463 | } | 462 | } |
464 | matches.put(expression, matchSet); | 463 | matches.put(expression, matchSet); |
465 | 464 | ||
466 | System.out.println("Number of matches: " + matchSet.size()); | 465 | System.out.println("Number of matches: " + matchSet.size()); |
467 | for (int i = 0; i < 10; i++) { | 466 | for (int i = 0; i < 10; i++) { |
468 | Map<Object,Integer> sol = getOneSolution(obj, matches); | 467 | Map<Object,Integer> sol = getOneSolution(obj, matches); |
@@ -470,5 +469,5 @@ public class NumericProblemSolver { | |||
470 | Thread.sleep(3000); | 469 | Thread.sleep(3000); |
471 | } | 470 | } |
472 | } | 471 | } |
473 | */ | 472 | */ |
474 | } | 473 | } |