aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar anqili426 <mollisterkl@outlook.com>2020-05-06 12:44:52 -0400
committerLibravatar anqili426 <mollisterkl@outlook.com>2020-05-06 12:44:52 -0400
commit12f66f547f1ef1a198ce5e099eda5328490899c3 (patch)
treef8af9f371b9b07412e7f302fe937918cf8f5d831
parentAdded FakeIntegerElement (diff)
downloadVIATRA-Generator-Attribute-Solver.tar.gz
VIATRA-Generator-Attribute-Solver.tar.zst
VIATRA-Generator-Attribute-Solver.zip
Get a different solutionAttribute-Solver
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java110
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}