diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme')
5 files changed, 32 insertions, 40 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 00cf7e59..b9942a17 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 | |||
@@ -14,10 +14,10 @@ import org.eclipse.xtext.xbase.XUnaryOperation | |||
14 | 14 | ||
15 | class ExpressionEvaluation2Logic { | 15 | class ExpressionEvaluation2Logic { |
16 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | 16 | val extension LogicProblemBuilder builder = new LogicProblemBuilder |
17 | var NumericZ3ProblemSolver _numericSolver = null //new NumericProblemSolver | 17 | var NumericProblemSolver _numericSolver = null //new NumericProblemSolver |
18 | def getNumericSolver() { | 18 | def getNumericSolver() { |
19 | if(_numericSolver === null) { | 19 | if(_numericSolver === null) { |
20 | _numericSolver = new NumericZ3ProblemSolver | 20 | _numericSolver = (new NumericTranslator).selectProblemSolver |
21 | } | 21 | } |
22 | return _numericSolver | 22 | return _numericSolver |
23 | } | 23 | } |
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 94dfdac0..1e5742b7 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 | |||
@@ -18,7 +18,7 @@ import org.eclipse.xtext.xbase.XExpression; | |||
18 | 18 | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
20 | 20 | ||
21 | public class NumericDrealProblemSolver { | 21 | public class NumericDrealProblemSolver extends NumericProblemSolver{ |
22 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; | 22 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; |
23 | private static final String N_PLUS = "operator_plus"; | 23 | private static final String N_PLUS = "operator_plus"; |
24 | private static final String N_MINUS = "operator_minus"; | 24 | private static final String N_MINUS = "operator_minus"; |
@@ -40,10 +40,6 @@ public class NumericDrealProblemSolver { | |||
40 | private String containerName; | 40 | private String containerName; |
41 | private Map<Object, String> varMap; | 41 | private Map<Object, String> varMap; |
42 | 42 | ||
43 | long endformingProblem=0; | ||
44 | long endSolvingProblem=0; | ||
45 | long endFormingSolution=0; | ||
46 | |||
47 | public NumericDrealProblemSolver() throws IOException, InterruptedException { | 43 | public NumericDrealProblemSolver() throws IOException, InterruptedException { |
48 | //setup smt2 input file | 44 | //setup smt2 input file |
49 | tempFile = File.createTempFile("smt", ".smt2"); | 45 | tempFile = File.createTempFile("smt", ".smt2"); |
@@ -70,7 +66,7 @@ public class NumericDrealProblemSolver { | |||
70 | varMap = new HashMap<Object, String>(); | 66 | varMap = new HashMap<Object, String>(); |
71 | } | 67 | } |
72 | 68 | ||
73 | public Process runProcess(List<String> cmd) throws IOException, InterruptedException { | 69 | private Process runProcess(List<String> cmd) throws IOException, InterruptedException { |
74 | // println(cmd) | 70 | // println(cmd) |
75 | ProcessBuilder pb = new ProcessBuilder(cmd); | 71 | ProcessBuilder pb = new ProcessBuilder(cmd); |
76 | pb.redirectOutput(); | 72 | pb.redirectOutput(); |
@@ -84,17 +80,6 @@ public class NumericDrealProblemSolver { | |||
84 | return p; | 80 | return p; |
85 | } | 81 | } |
86 | 82 | ||
87 | public long getEndformingProblem() { | ||
88 | return endformingProblem; | ||
89 | } | ||
90 | |||
91 | public long getEndSolvingProblem() { | ||
92 | return endSolvingProblem; | ||
93 | } | ||
94 | |||
95 | public long getEndFormingSolution() { | ||
96 | return endFormingSolution; | ||
97 | } | ||
98 | // | 83 | // |
99 | // private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { | 84 | // private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { |
100 | // ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | 85 | // ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); |
@@ -115,7 +100,7 @@ public class NumericDrealProblemSolver { | |||
115 | // } | 100 | // } |
116 | // } | 101 | // } |
117 | 102 | ||
118 | public Process callDreal() throws IOException, InterruptedException { | 103 | private Process callDreal() throws IOException, InterruptedException { |
119 | List<String> drealCmd = new ArrayList<String>( | 104 | List<String> drealCmd = new ArrayList<String>( |
120 | Arrays.asList("docker", "exec", | 105 | Arrays.asList("docker", "exec", |
121 | containerName, | 106 | containerName, |
@@ -125,7 +110,7 @@ public class NumericDrealProblemSolver { | |||
125 | return runProcess(drealCmd); | 110 | return runProcess(drealCmd); |
126 | } | 111 | } |
127 | 112 | ||
128 | public boolean getDrealResult(Process p) throws IOException { | 113 | private boolean getDrealResult(Process p) throws IOException { |
129 | if (p.exitValue() == 1) {return false;} | 114 | if (p.exitValue() == 1) {return false;} |
130 | 115 | ||
131 | BufferedReader output = new BufferedReader(new InputStreamReader(p.getInputStream())); | 116 | BufferedReader output = new BufferedReader(new InputStreamReader(p.getInputStream())); |
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 new file mode 100644 index 00000000..d818ec91 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | |||
@@ -0,0 +1,23 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.util.List; | ||
4 | import java.util.Map; | ||
5 | |||
6 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | ||
7 | import org.eclipse.xtext.xbase.XExpression; | ||
8 | |||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | ||
10 | |||
11 | public abstract class NumericProblemSolver { | ||
12 | |||
13 | long endformingProblem=0; | ||
14 | long endSolvingProblem=0; | ||
15 | long endFormingSolution=0; | ||
16 | |||
17 | public long getEndformingProblem() {return endformingProblem;} | ||
18 | public long getEndSolvingProblem() {return endSolvingProblem;} | ||
19 | public long getEndFormingSolution() {return endFormingSolution;} | ||
20 | |||
21 | public abstract boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception; | ||
22 | public abstract Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception; | ||
23 | } | ||
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 873dbed3..d63604b0 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 | |||
@@ -50,7 +50,7 @@ class NumericTranslator { | |||
50 | return res | 50 | return res |
51 | } | 51 | } |
52 | 52 | ||
53 | def selectProblemSolver() { | 53 | def NumericProblemSolver selectProblemSolver() { |
54 | // return new NumericProblemSolver | 54 | // return new NumericProblemSolver |
55 | return new NumericDrealProblemSolver | 55 | return new NumericDrealProblemSolver |
56 | } | 56 | } |
@@ -71,7 +71,7 @@ class NumericTranslator { | |||
71 | return solution | 71 | return solution |
72 | } | 72 | } |
73 | 73 | ||
74 | private def updateTimes(NumericDrealProblemSolver s) { | 74 | private def updateTimes(NumericProblemSolver s) { |
75 | this.formingProblemTime += s.getEndformingProblem | 75 | this.formingProblemTime += s.getEndformingProblem |
76 | this.solvingProblemTime += s.getEndSolvingProblem | 76 | this.solvingProblemTime += s.getEndSolvingProblem |
77 | this.formingSolutionTime += s.getEndFormingSolution | 77 | this.formingSolutionTime += s.getEndFormingSolution |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java index 8b7ee043..a594eb60 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | |||
@@ -27,7 +27,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; | 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; |
28 | 28 | ||
29 | 29 | ||
30 | public class NumericZ3ProblemSolver { | 30 | public class NumericZ3ProblemSolver extends NumericProblemSolver{ |
31 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; | 31 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; |
32 | private static final String N_PLUS = "operator_plus"; | 32 | private static final String N_PLUS = "operator_plus"; |
33 | private static final String N_MINUS = "operator_minus"; | 33 | private static final String N_MINUS = "operator_minus"; |
@@ -49,10 +49,6 @@ public class NumericZ3ProblemSolver { | |||
49 | private Solver s; | 49 | private Solver s; |
50 | private Map<Object, Expr> varMap; | 50 | private Map<Object, Expr> varMap; |
51 | 51 | ||
52 | long endformingProblem=0; | ||
53 | long endSolvingProblem=0; | ||
54 | long endFormingSolution=0; | ||
55 | |||
56 | public NumericZ3ProblemSolver() { | 52 | public NumericZ3ProblemSolver() { |
57 | HashMap<String, String> cfg = new HashMap<String, String>(); | 53 | HashMap<String, String> cfg = new HashMap<String, String>(); |
58 | cfg.put("model", "true"); | 54 | cfg.put("model", "true"); |
@@ -66,18 +62,6 @@ public class NumericZ3ProblemSolver { | |||
66 | return ctx; | 62 | return ctx; |
67 | } | 63 | } |
68 | 64 | ||
69 | public long getEndformingProblem() { | ||
70 | return endformingProblem; | ||
71 | } | ||
72 | |||
73 | public long getEndSolvingProblem() { | ||
74 | return endSolvingProblem; | ||
75 | } | ||
76 | |||
77 | public long getEndFormingSolution() { | ||
78 | return endFormingSolution; | ||
79 | } | ||
80 | |||
81 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { | 65 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { |
82 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | 66 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); |
83 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); | 67 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); |