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 {
         def getNumericSolver() {

                 if(_numericSolver === null) {

                         // it seems like this getter has no use

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

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

                 }

                 return _numericSolver

         }

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{
         private Map<String, String> curVar2Decl;

         

         private final int TIMEOUT_DOCKER = 5000;

-        private final int TIMEOUT_LOCAL = 10000;

-        private final boolean DEBUG_PRINT = false;

+        private final int TIMEOUT_LOCAL = 100000;

+        private final int DEBUG_PRINT = 3;

 

         public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException {

                 this.useDocker = useDocker;

@@ -87,7 +87,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                         }

                         return null;

                 }

-                if (DEBUG_PRINT) {

+                if (DEBUG_PRINT > 1) {

                         double duration = (double) (System.nanoTime() - startTime) / 1000000000;

                         System.out.println("Dur = " + duration + " : ");

                 }

@@ -404,11 +404,13 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                         System.err.println("TIMEOUT");

 //                      printOutput(numProbContent);

                 }

-                if (DEBUG_PRINT) {

-        //              printOutput(numProbContent);

-        //              if (outputs != null) printOutput(outputs.get(0));

+                if (DEBUG_PRINT > 1) {

                         System.out.println(result);

                 }

+                if (DEBUG_PRINT > 2) {

+                        printOutput(numProbContent);

+                        if (outputs != null) printOutput(outputs.get(0));

+                }

                 

                 return result;

         }

@@ -455,16 +457,30 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                 Process outputProcess;

                 if (this.useDocker) outputProcess = callDrealDocker(numProbContent, true);

                 else outputProcess = callDrealLocal(numProbContent, true);

-                        

-                List<List<String>> outputs = getProcessOutput(outputProcess);

-                boolean result = getDrealResult(outputProcess.exitValue(), outputs);

+                

+                boolean result = false;

+                List<List<String>> outputs = null;

+                if (outputProcess != null) { 

+                        outputs = getProcessOutput(outputProcess);

+                        result = getDrealResult(outputProcess.exitValue(), outputs);

+                }

+                

                 endSolvingProblem = System.nanoTime()-startSolvingProblem;

                 

-                if (DEBUG_PRINT) {

-                        System.out.println("Getting Solution!");

-        //              printOutput(numProbContent);

-        //              printOutput(outputs.get(0));

-        //              System.out.println(result);

+                if (outputProcess == null) {    

+                        System.err.println("TIMEOUT");

+//                      printOutput(numProbContent);

+                } else {

+                        if (DEBUG_PRINT > 0) {

+                                System.out.println("Getting Solution!");

+                        }

+                }

+                if (DEBUG_PRINT > 1) {

+                        System.out.println(result);

+                }

+                if (DEBUG_PRINT > 2) {

+                        printOutput(numProbContent);

+                        if (outputs != null) printOutput(outputs.get(0));

                 }

                                 

                 //GET SOLUTION          

@@ -498,7 +514,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                         endFormingSolution = System.nanoTime() - startFormingSolution;

                 }

                 else {

-                        System.out.println("Unsatisfiable numerical problem");

+                        System.out.println("Unsatisfiable numerical problem (trying to get solution...)");

                 }               

                 return sol;

         }

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 @@
+package hu.bme.mit.inf.dslreasoner.viatra2logic;
+
+import java.io.IOException;
+import java.util.List;
+import java.util.Map;
+
+import org.eclipse.xtext.common.types.JvmIdentifiableElement;
+import org.eclipse.xtext.xbase.XExpression;
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;
+
+public class NumericDynamicProblemSolver extends NumericProblemSolver{
+        
+//      private NumericZ3ProblemSolver z3Solver;
+        private NumericDrealProblemSolver drealSolver;
+        
+        public NumericDynamicProblemSolver(String drealLocalPath) throws IOException, InterruptedException {
+//              this.z3Solver = new NumericZ3ProblemSolver();
+                this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath);
+        }
+        
+        public NumericProblemSolver selectSolver(String selection) {
+                switch (selection) {
+                case "z3":
+                        return new NumericZ3ProblemSolver();
+                case "dreal":
+                        return this.drealSolver;
+                default:
+                throw new IllegalArgumentException("Unknown numeric solver selection: " + selection);
+                }
+        }
+
+        public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches)
+                        throws Exception {
+                throw new Exception("Should not reach here - isSatisfiable");
+        }
+
+        public Map<PrimitiveElement, Number> getOneSolution(List<PrimitiveElement> objs,
+                        Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception {
+                throw new Exception("Should not reach here - getOneSolution");
+        }}
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 {
                 return res

         }

         

-        def NumericProblemSolver selectProblemSolver() {

+        def NumericProblemSolver selectProblemSolver(String selection) {

 //              return new NumericProblemSolver

 //              add numeric solver decision procedure here

-                if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver

-                return numericSolver;

+                if (numericSolver instanceof NumericDynamicProblemSolver) {

+                        val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver

+                        return dynamicSolver.selectSolver(selection);

+                } else{

+                        if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver
+                        return numericSolver;

+                }
         }

         

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

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

                 val input = formNumericProblemInstance(matches)

-                val solver = selectProblemSolver

+                val solver = selectProblemSolver(select)

                 val satisfiability = solver.isSatisfiable(input)

                 solver.updateTimes

                 return satisfiability

         }

         

-        def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) {

+        def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches, String select) {

                 val input = formNumericProblemInstance(matches)

-                val solver = selectProblemSolver

+                val solver = selectProblemSolver(select)

                 val solution = solver.getOneSolution(primitiveElements,input)

                 solver.updateTimes

                 return solution