diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | 110 |
1 files changed, 110 insertions, 0 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 ff3a85eb..529f8e4c 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 | |||
@@ -256,6 +256,52 @@ public class NumericProblemSolver { | |||
256 | } | 256 | } |
257 | } | 257 | } |
258 | 258 | ||
259 | // Get a solution that has at least 1 different value from the given solution | ||
260 | public void testGetOneDiffSol(XExpression expression, Term t) throws Exception { | ||
261 | int count = 5000; | ||
262 | Random rand = new Random(); | ||
263 | Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches = new HashMap<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>>(); | ||
264 | Set<Map<JvmIdentifiableElement,PrimitiveElement>> matchSet = new HashSet<Map<JvmIdentifiableElement,PrimitiveElement>>(); | ||
265 | ArrayList<JvmIdentifiableElement> allElem = getJvmIdentifiableElements(expression); | ||
266 | List<Object> obj = new ArrayList<Object>(); | ||
267 | for (int i = 0; i < count; i++) { | ||
268 | Map<JvmIdentifiableElement,PrimitiveElement> match = new HashMap<JvmIdentifiableElement,PrimitiveElement>(); | ||
269 | if (obj.size() > 1) { | ||
270 | for (JvmIdentifiableElement e: allElem) { | ||
271 | FakeIntegerElement intE = null; | ||
272 | int useOld = rand.nextInt(10); | ||
273 | if (useOld == 1) { | ||
274 | System.out.println("here "); | ||
275 | int index = rand.nextInt(obj.size()); | ||
276 | intE = (FakeIntegerElement) obj.get(index); | ||
277 | } else { | ||
278 | intE = new FakeIntegerElement(); | ||
279 | } | ||
280 | obj.add(intE); | ||
281 | match.put(e, intE); | ||
282 | } | ||
283 | } else { | ||
284 | for (JvmIdentifiableElement e: allElem) { | ||
285 | FakeIntegerElement intE = new FakeIntegerElement(); | ||
286 | obj.add(intE); | ||
287 | match.put(e, intE); | ||
288 | } | ||
289 | } | ||
290 | matchSet.add(match); | ||
291 | } | ||
292 | matches.put(expression, matchSet); | ||
293 | |||
294 | Map<Object,Integer> sol1 = getOneSolution(obj, matches); | ||
295 | System.out.println("*************Get diff sol******************"); | ||
296 | for (int i = 0; i < 10; i++) { | ||
297 | long start = System.currentTimeMillis(); | ||
298 | Map<Object,Integer> sol2 = getOneDiffSolution1(obj, matches, sol1); | ||
299 | long end = System.currentTimeMillis(); | ||
300 | System.out.println(end - start); | ||
301 | Thread.sleep(3000); | ||
302 | } | ||
303 | } | ||
304 | |||
259 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { | 305 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { |
260 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | 306 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); |
261 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); | 307 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); |
@@ -281,6 +327,68 @@ public class NumericProblemSolver { | |||
281 | return s.check() == Status.SATISFIABLE; | 327 | return s.check() == Status.SATISFIABLE; |
282 | } | 328 | } |
283 | 329 | ||
330 | public Map<Object,Integer> getOneDiffSolution1(List<Object> objs, Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches, Map<Object,Integer> aSolution) throws Exception { | ||
331 | Map<Object,Integer> sol = new HashMap<Object, Integer>(); | ||
332 | BoolExpr problemInstance = formNumericProblemInstance(matches); | ||
333 | |||
334 | BoolExpr diffSolConstraint = ctx.mkFalse(); | ||
335 | for (Object o: objs) { | ||
336 | Expr var = varMap.get(o); | ||
337 | Integer oldValue = aSolution.get(o); | ||
338 | IntExpr oldValueExpr = ctx.mkInt(oldValue); | ||
339 | diffSolConstraint = ctx.mkOr(diffSolConstraint, ctx.mkDistinct(var, oldValueExpr)); | ||
340 | } | ||
341 | |||
342 | problemInstance = ctx.mkAnd(problemInstance, diffSolConstraint); | ||
343 | s.add(problemInstance); | ||
344 | |||
345 | if (s.check() == Status.SATISFIABLE) { | ||
346 | Model m = s.getModel(); | ||
347 | for (Object o: objs) { | ||
348 | IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); | ||
349 | Integer oSol = Integer.parseInt(val.toString()); | ||
350 | sol.put(o, oSol); | ||
351 | } | ||
352 | } else { | ||
353 | System.out.println("Unsatisfiable"); | ||
354 | } | ||
355 | |||
356 | return sol; | ||
357 | } | ||
358 | |||
359 | public Map<Object,Integer> getOneDiffSolution2(List<Object> objs, Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches, Map<Object,Integer> aSolution) throws Exception { | ||
360 | Map<Object,Integer> sol = new HashMap<Object, Integer>(); | ||
361 | BoolExpr problemInstance = formNumericProblemInstance(matches); | ||
362 | ArithExpr sum = ctx.mkInt(0); | ||
363 | |||
364 | for (Object o: objs) { | ||
365 | IntExpr var = (IntExpr) varMap.get(o); | ||
366 | Integer oldValue = aSolution.get(o); | ||
367 | IntExpr oldValueExpr = ctx.mkInt(oldValue); | ||
368 | // Calculate the difference. Notice that this is not the abs value!!! | ||
369 | ArithExpr diff = ctx.mkAdd(var, ctx.mkUnaryMinus(oldValueExpr)); | ||
370 | // Add up the difference | ||
371 | sum = ctx.mkAdd(diff, sum); | ||
372 | } | ||
373 | |||
374 | BoolExpr diffSolConstraint = ctx.mkLt(sum, ctx.mkInt(3)); | ||
375 | problemInstance = ctx.mkAnd(problemInstance, diffSolConstraint); | ||
376 | s.add(problemInstance); | ||
377 | |||
378 | if (s.check() == Status.SATISFIABLE) { | ||
379 | Model m = s.getModel(); | ||
380 | for (Object o: objs) { | ||
381 | IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); | ||
382 | Integer oSol = Integer.parseInt(val.toString()); | ||
383 | sol.put(o, oSol); | ||
384 | } | ||
385 | } else { | ||
386 | System.out.println("Unsatisfiable"); | ||
387 | } | ||
388 | |||
389 | return sol; | ||
390 | } | ||
391 | |||
284 | public Map<Object,Integer> getOneSolution(List<Object> objs, Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { | 392 | public Map<Object,Integer> getOneSolution(List<Object> objs, Map<XExpression, Set<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception { |
285 | Map<Object,Integer> sol = new HashMap<Object, Integer>(); | 393 | Map<Object,Integer> sol = new HashMap<Object, Integer>(); |
286 | long startformingProblem = System.currentTimeMillis(); | 394 | long startformingProblem = System.currentTimeMillis(); |
@@ -411,4 +519,6 @@ public class NumericProblemSolver { | |||
411 | } | 519 | } |
412 | return constraintInstances; | 520 | return constraintInstances; |
413 | } | 521 | } |
522 | |||
523 | |||
414 | } | 524 | } |