prep for refactoring Numeric Probelm Solvers

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
 

 class ExpressionEvaluation2Logic {

         val extension LogicProblemBuilder builder = new LogicProblemBuilder

-        var NumericProblemSolver _numericSolver = null //new NumericProblemSolver

+        var NumericZ3ProblemSolver _numericSolver = null //new NumericProblemSolver

         def getNumericSolver() {

                 if(_numericSolver === null) {

-                        _numericSolver = new NumericProblemSolver

+                        _numericSolver = new NumericZ3ProblemSolver

                 }

                 return _numericSolver

         }

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;
 

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;

 

-public class DrealProblemSolver {

+public class NumericDrealProblemSolver {

         private static final String N_Base = "org.eclipse.xtext.xbase.lib.";

         private static final String N_PLUS = "operator_plus";

         private static final String N_MINUS = "operator_minus";

@@ -44,7 +44,7 @@ public class DrealProblemSolver {
         long endSolvingProblem=0;

         long endFormingSolution=0;

 

-        public DrealProblemSolver() throws IOException, InterruptedException {

+        public NumericDrealProblemSolver() throws IOException, InterruptedException {

                 //setup smt2 input file

                 tempFile = File.createTempFile("smt", ".smt2");

                 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 {
         

         def selectProblemSolver() {

 //              return new NumericProblemSolver

-                return new DrealProblemSolver

+                return new NumericDrealProblemSolver

         }

         

         def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) {

@@ -71,7 +71,7 @@ class NumericTranslator {
                 return solution

         }

         

-        private def updateTimes(DrealProblemSolver s) {

+        private def updateTimes(NumericDrealProblemSolver s) {

                 this.formingProblemTime += s.getEndformingProblem

                 this.solvingProblemTime += s.getEndSolvingProblem

                 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
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement;

 

 

-public class NumericProblemSolver {

+public class NumericZ3ProblemSolver {

         private static final String N_Base = "org.eclipse.xtext.xbase.lib.";

         private static final String N_PLUS = "operator_plus";

         private static final String N_MINUS = "operator_minus";

@@ -53,7 +53,7 @@ public class NumericProblemSolver {
         long endSolvingProblem=0;

         long endFormingSolution=0;

 

-        public NumericProblemSolver() {

+        public NumericZ3ProblemSolver() {

                 HashMap<String, String> cfg = new HashMap<String, String>();

                 cfg.put("model", "true");

                 ctx = new Context(cfg);