Add config flag for selecting numeric solver. Integ with Z3

2 files changed, 12 insertions, 4 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 b9942a17..1b68fed2 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
@@ -17,7 +17,8 @@ class ExpressionEvaluation2Logic {
         var NumericProblemSolver _numericSolver = null //new NumericProblemSolver

         def getNumericSolver() {

                 if(_numericSolver === null) {

-                        _numericSolver = (new NumericTranslator).selectProblemSolver

+                        // it seems like this getter has no use

+                        _numericSolver = (new NumericTranslator(null)).selectProblemSolver

                 }

                 return _numericSolver

         }

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 22ea41bf..3d3f2f4a 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
@@ -16,7 +16,7 @@ import org.eclipse.xtext.xbase.XFeatureCall
 class NumericTranslator {

         

         private XExpressionExtractor extractor = new XExpressionExtractor();

-        private NumericDrealProblemSolver drealSolver = new NumericDrealProblemSolver();

+        private NumericProblemSolver numericSolver;

         

         long formingProblemTime=0;

         long solvingProblemTime=0;

@@ -28,6 +28,11 @@ class NumericTranslator {
                                 o1.simpleName.compareTo(o2.simpleName)

                         }

                 }

+                

+        new(NumericProblemSolver numericProblemSolver){

+                this.numericSolver = numericProblemSolver

+        }

+        

         def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) {

                 val res = new HashMap

                 for(var i=0; i<tuple.length; i++) {

@@ -53,7 +58,9 @@ class NumericTranslator {
         

         def NumericProblemSolver selectProblemSolver() {

 //              return new NumericProblemSolver

-                return drealSolver;

+//              add numeric solver decision procedure here

+                if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver

+                return numericSolver;

         }

         

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

@@ -81,5 +88,5 @@ class NumericTranslator {
         def getFormingProblemTime() {formingProblemTime}

         def getSolvingProblemTime() {solvingProblemTime}

         def getFormingSolutionTime() {formingSolutionTime}

-        def getDrealSolver(){return drealSolver}

+        def getNumericSolver(){numericSolver}

 }
\ No newline at end of file