diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2020-12-13 20:37:05 -0500 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-06 00:02:48 +0100 |
commit | ca1e53f0ca5e8d61699ce7c34494cb85c2b04ee8 (patch) | |
tree | 8a4614b464faf151409bbce112a9de9c1f734f62 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu | |
parent | implement setup for dreal calls (diff) | |
download | VIATRA-Generator-ca1e53f0ca5e8d61699ce7c34494cb85c2b04ee8.tar.gz VIATRA-Generator-ca1e53f0ca5e8d61699ce7c34494cb85c2b04ee8.tar.zst VIATRA-Generator-ca1e53f0ca5e8d61699ce7c34494cb85c2b04ee8.zip |
prep for refactoring Numeric Probelm Solvers
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend | 4 | ||||
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java (renamed from Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/DrealProblemSolver.java) | 4 | ||||
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend | 4 | ||||
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java (renamed from Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java) | 4 |
4 files changed, 8 insertions, 8 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 6393121b..00cf7e59 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 NumericProblemSolver _numericSolver = null //new NumericProblemSolver | 17 | var NumericZ3ProblemSolver _numericSolver = null //new NumericProblemSolver |
18 | def getNumericSolver() { | 18 | def getNumericSolver() { |
19 | if(_numericSolver === null) { | 19 | if(_numericSolver === null) { |
20 | _numericSolver = new NumericProblemSolver | 20 | _numericSolver = new NumericZ3ProblemSolver |
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/DrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java index d13990be..94dfdac0 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/DrealProblemSolver.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 DrealProblemSolver { | 21 | public class NumericDrealProblemSolver { |
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"; |
@@ -44,7 +44,7 @@ public class DrealProblemSolver { | |||
44 | long endSolvingProblem=0; | 44 | long endSolvingProblem=0; |
45 | long endFormingSolution=0; | 45 | long endFormingSolution=0; |
46 | 46 | ||
47 | public DrealProblemSolver() throws IOException, InterruptedException { | 47 | public NumericDrealProblemSolver() throws IOException, InterruptedException { |
48 | //setup smt2 input file | 48 | //setup smt2 input file |
49 | tempFile = File.createTempFile("smt", ".smt2"); | 49 | tempFile = File.createTempFile("smt", ".smt2"); |
50 | printer = new PrintWriter(tempFile); | 50 | printer = new PrintWriter(tempFile); |
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 21fbe589..873dbed3 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 | |||
@@ -52,7 +52,7 @@ class NumericTranslator { | |||
52 | 52 | ||
53 | def selectProblemSolver() { | 53 | def selectProblemSolver() { |
54 | // return new NumericProblemSolver | 54 | // return new NumericProblemSolver |
55 | return new DrealProblemSolver | 55 | return new NumericDrealProblemSolver |
56 | } | 56 | } |
57 | 57 | ||
58 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { | 58 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { |
@@ -71,7 +71,7 @@ class NumericTranslator { | |||
71 | return solution | 71 | return solution |
72 | } | 72 | } |
73 | 73 | ||
74 | private def updateTimes(DrealProblemSolver s) { | 74 | private def updateTimes(NumericDrealProblemSolver 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/NumericProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java index f1314925..8b7ee043 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/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 NumericProblemSolver { | 30 | public class NumericZ3ProblemSolver { |
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"; |
@@ -53,7 +53,7 @@ public class NumericProblemSolver { | |||
53 | long endSolvingProblem=0; | 53 | long endSolvingProblem=0; |
54 | long endFormingSolution=0; | 54 | long endFormingSolution=0; |
55 | 55 | ||
56 | public NumericProblemSolver() { | 56 | public NumericZ3ProblemSolver() { |
57 | HashMap<String, String> cfg = new HashMap<String, String>(); | 57 | HashMap<String, String> cfg = new HashMap<String, String>(); |
58 | cfg.put("model", "true"); | 58 | cfg.put("model", "true"); |
59 | ctx = new Context(cfg); | 59 | ctx = new Context(cfg); |