diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf')
4 files changed, 85 insertions, 23 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend index 9e11d2cf..ae94c327 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend | |||
@@ -21,7 +21,7 @@ class ExpressionEvaluation2Logic { | |||
21 | def getNumericSolver() { | 21 | def getNumericSolver() { |
22 | if(_numericSolver === null) { | 22 | if(_numericSolver === null) { |
23 | // it seems like this getter has no use | 23 | // it seems like this getter has no use |
24 | _numericSolver = (new NumericTranslator(null)).selectProblemSolver | 24 | _numericSolver = (new NumericTranslator(null)).selectProblemSolver("z3") |
25 | } | 25 | } |
26 | return _numericSolver | 26 | return _numericSolver |
27 | } | 27 | } |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java index e0ebcb6b..36ea64aa 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | |||
@@ -43,8 +43,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
43 | private Map<String, String> curVar2Decl; | 43 | private Map<String, String> curVar2Decl; |
44 | 44 | ||
45 | private final int TIMEOUT_DOCKER = 5000; | 45 | private final int TIMEOUT_DOCKER = 5000; |
46 | private final int TIMEOUT_LOCAL = 10000; | 46 | private final int TIMEOUT_LOCAL = 100000; |
47 | private final boolean DEBUG_PRINT = false; | 47 | private final int DEBUG_PRINT = 3; |
48 | 48 | ||
49 | public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { | 49 | public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { |
50 | this.useDocker = useDocker; | 50 | this.useDocker = useDocker; |
@@ -87,7 +87,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
87 | } | 87 | } |
88 | return null; | 88 | return null; |
89 | } | 89 | } |
90 | if (DEBUG_PRINT) { | 90 | if (DEBUG_PRINT > 1) { |
91 | double duration = (double) (System.nanoTime() - startTime) / 1000000000; | 91 | double duration = (double) (System.nanoTime() - startTime) / 1000000000; |
92 | System.out.println("Dur = " + duration + " : "); | 92 | System.out.println("Dur = " + duration + " : "); |
93 | } | 93 | } |
@@ -404,11 +404,13 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
404 | System.err.println("TIMEOUT"); | 404 | System.err.println("TIMEOUT"); |
405 | // printOutput(numProbContent); | 405 | // printOutput(numProbContent); |
406 | } | 406 | } |
407 | if (DEBUG_PRINT) { | 407 | if (DEBUG_PRINT > 1) { |
408 | // printOutput(numProbContent); | ||
409 | // if (outputs != null) printOutput(outputs.get(0)); | ||
410 | System.out.println(result); | 408 | System.out.println(result); |
411 | } | 409 | } |
410 | if (DEBUG_PRINT > 2) { | ||
411 | printOutput(numProbContent); | ||
412 | if (outputs != null) printOutput(outputs.get(0)); | ||
413 | } | ||
412 | 414 | ||
413 | return result; | 415 | return result; |
414 | } | 416 | } |
@@ -455,16 +457,30 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
455 | Process outputProcess; | 457 | Process outputProcess; |
456 | if (this.useDocker) outputProcess = callDrealDocker(numProbContent, true); | 458 | if (this.useDocker) outputProcess = callDrealDocker(numProbContent, true); |
457 | else outputProcess = callDrealLocal(numProbContent, true); | 459 | else outputProcess = callDrealLocal(numProbContent, true); |
458 | 460 | ||
459 | List<List<String>> outputs = getProcessOutput(outputProcess); | 461 | boolean result = false; |
460 | boolean result = getDrealResult(outputProcess.exitValue(), outputs); | 462 | List<List<String>> outputs = null; |
463 | if (outputProcess != null) { | ||
464 | outputs = getProcessOutput(outputProcess); | ||
465 | result = getDrealResult(outputProcess.exitValue(), outputs); | ||
466 | } | ||
467 | |||
461 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 468 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
462 | 469 | ||
463 | if (DEBUG_PRINT) { | 470 | if (outputProcess == null) { |
464 | System.out.println("Getting Solution!"); | 471 | System.err.println("TIMEOUT"); |
465 | // printOutput(numProbContent); | 472 | // printOutput(numProbContent); |
466 | // printOutput(outputs.get(0)); | 473 | } else { |
467 | // System.out.println(result); | 474 | if (DEBUG_PRINT > 0) { |
475 | System.out.println("Getting Solution!"); | ||
476 | } | ||
477 | } | ||
478 | if (DEBUG_PRINT > 1) { | ||
479 | System.out.println(result); | ||
480 | } | ||
481 | if (DEBUG_PRINT > 2) { | ||
482 | printOutput(numProbContent); | ||
483 | if (outputs != null) printOutput(outputs.get(0)); | ||
468 | } | 484 | } |
469 | 485 | ||
470 | //GET SOLUTION | 486 | //GET SOLUTION |
@@ -498,7 +514,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
498 | endFormingSolution = System.nanoTime() - startFormingSolution; | 514 | endFormingSolution = System.nanoTime() - startFormingSolution; |
499 | } | 515 | } |
500 | else { | 516 | else { |
501 | System.out.println("Unsatisfiable numerical problem"); | 517 | System.out.println("Unsatisfiable numerical problem (trying to get solution...)"); |
502 | } | 518 | } |
503 | return sol; | 519 | return sol; |
504 | } | 520 | } |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java new file mode 100644 index 00000000..bd4a10ff --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java | |||
@@ -0,0 +1,41 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.io.IOException; | ||
4 | import java.util.List; | ||
5 | import java.util.Map; | ||
6 | |||
7 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | ||
8 | import org.eclipse.xtext.xbase.XExpression; | ||
9 | |||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | ||
11 | |||
12 | public class NumericDynamicProblemSolver extends NumericProblemSolver{ | ||
13 | |||
14 | // private NumericZ3ProblemSolver z3Solver; | ||
15 | private NumericDrealProblemSolver drealSolver; | ||
16 | |||
17 | public NumericDynamicProblemSolver(String drealLocalPath) throws IOException, InterruptedException { | ||
18 | // this.z3Solver = new NumericZ3ProblemSolver(); | ||
19 | this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath); | ||
20 | } | ||
21 | |||
22 | public NumericProblemSolver selectSolver(String selection) { | ||
23 | switch (selection) { | ||
24 | case "z3": | ||
25 | return new NumericZ3ProblemSolver(); | ||
26 | case "dreal": | ||
27 | return this.drealSolver; | ||
28 | default: | ||
29 | throw new IllegalArgumentException("Unknown numeric solver selection: " + selection); | ||
30 | } | ||
31 | } | ||
32 | |||
33 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) | ||
34 | throws Exception { | ||
35 | throw new Exception("Should not reach here - isSatisfiable"); | ||
36 | } | ||
37 | |||
38 | public Map<PrimitiveElement, Number> getOneSolution(List<PrimitiveElement> objs, | ||
39 | Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { | ||
40 | throw new Exception("Should not reach here - getOneSolution"); | ||
41 | }} | ||
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 3d3f2f4a..791dd644 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 | |||
@@ -56,24 +56,29 @@ class NumericTranslator { | |||
56 | return res | 56 | return res |
57 | } | 57 | } |
58 | 58 | ||
59 | def NumericProblemSolver selectProblemSolver() { | 59 | def NumericProblemSolver selectProblemSolver(String selection) { |
60 | // return new NumericProblemSolver | 60 | // return new NumericProblemSolver |
61 | // add numeric solver decision procedure here | 61 | // add numeric solver decision procedure here |
62 | if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver | 62 | if (numericSolver instanceof NumericDynamicProblemSolver) { |
63 | return numericSolver; | 63 | val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver |
64 | return dynamicSolver.selectSolver(selection); | ||
65 | } else{ | ||
66 | if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver | ||
67 | return numericSolver; | ||
68 | } | ||
64 | } | 69 | } |
65 | 70 | ||
66 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { | 71 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches, String select) { |
67 | val input = formNumericProblemInstance(matches) | 72 | val input = formNumericProblemInstance(matches) |
68 | val solver = selectProblemSolver | 73 | val solver = selectProblemSolver(select) |
69 | val satisfiability = solver.isSatisfiable(input) | 74 | val satisfiability = solver.isSatisfiable(input) |
70 | solver.updateTimes | 75 | solver.updateTimes |
71 | return satisfiability | 76 | return satisfiability |
72 | } | 77 | } |
73 | 78 | ||
74 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) { | 79 | def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches, String select) { |
75 | val input = formNumericProblemInstance(matches) | 80 | val input = formNumericProblemInstance(matches) |
76 | val solver = selectProblemSolver | 81 | val solver = selectProblemSolver(select) |
77 | val solution = solver.getOneSolution(primitiveElements,input) | 82 | val solution = solver.getOneSolution(primitiveElements,input) |
78 | solver.updateTimes | 83 | solver.updateTimes |
79 | return solution | 84 | return solution |