add numericProblemSolver supertype

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
 

 class ExpressionEvaluation2Logic {

         val extension LogicProblemBuilder builder = new LogicProblemBuilder

-        var NumericZ3ProblemSolver _numericSolver = null //new NumericProblemSolver

+        var NumericProblemSolver _numericSolver = null //new NumericProblemSolver

         def getNumericSolver() {

                 if(_numericSolver === null) {

-                        _numericSolver = new NumericZ3ProblemSolver

+                        _numericSolver = (new NumericTranslator).selectProblemSolver

                 }

                 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 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;
 

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

 

-public class NumericDrealProblemSolver {

+public class NumericDrealProblemSolver extends NumericProblemSolver{

         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";

@@ -40,10 +40,6 @@ public class NumericDrealProblemSolver {
         private String containerName;

         private Map<Object, String> varMap;

 

-        long endformingProblem=0;

-        long endSolvingProblem=0;

-        long endFormingSolution=0;

-

         public NumericDrealProblemSolver() throws IOException, InterruptedException {

                 //setup smt2 input file

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

@@ -70,7 +66,7 @@ public class NumericDrealProblemSolver {
                 varMap = new HashMap<Object, String>();

         }

         

-        public Process runProcess(List<String> cmd) throws IOException, InterruptedException {

+        private Process runProcess(List<String> cmd) throws IOException, InterruptedException {

 //              println(cmd)

                 ProcessBuilder pb = new ProcessBuilder(cmd);

                 pb.redirectOutput();

@@ -84,17 +80,6 @@ public class NumericDrealProblemSolver {
                 return p;

         }

 

-        public long getEndformingProblem() {

-                return endformingProblem;

-        }

-

-        public long getEndSolvingProblem() {

-                return endSolvingProblem;

-        }

-

-        public long getEndFormingSolution() {

-                return endFormingSolution;

-        }

 //

 //      private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) {

 //              ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>();

@@ -115,7 +100,7 @@ public class NumericDrealProblemSolver {
 //              }

 //      }

         

-        public Process callDreal() throws IOException, InterruptedException {

+        private Process callDreal() throws IOException, InterruptedException {

                 List<String> drealCmd = new ArrayList<String>(

                                 Arrays.asList("docker", "exec", 

                                                 containerName,

@@ -125,7 +110,7 @@ public class NumericDrealProblemSolver {
                 return runProcess(drealCmd);

         }

         

-        public boolean getDrealResult(Process p) throws IOException {

+        private boolean getDrealResult(Process p) throws IOException {

                 if (p.exitValue() == 1) {return false;}

                 

                 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 @@
+package hu.bme.mit.inf.dslreasoner.viatra2logic;

+

+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 abstract class NumericProblemSolver {

+        

+        long endformingProblem=0;

+        long endSolvingProblem=0;

+        long endFormingSolution=0;      

+

+        public long getEndformingProblem() {return endformingProblem;}

+        public long getEndSolvingProblem() {return endSolvingProblem;}

+        public long getEndFormingSolution() {return endFormingSolution;}

+        

+        public abstract  boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception;

+        public abstract Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception;

+}

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 {
                 return res

         }

         

-        def selectProblemSolver() {

+        def NumericProblemSolver selectProblemSolver() {

 //              return new NumericProblemSolver

                 return new NumericDrealProblemSolver

         }

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

         }

         

-        private def updateTimes(NumericDrealProblemSolver s) {

+        private def updateTimes(NumericProblemSolver 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/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
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement;

 

 

-public class NumericZ3ProblemSolver {

+public class NumericZ3ProblemSolver extends NumericProblemSolver{

         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";

@@ -49,10 +49,6 @@ public class NumericZ3ProblemSolver {
         private Solver s;

         private Map<Object, Expr> varMap;

 

-        long endformingProblem=0;

-        long endSolvingProblem=0;

-        long endFormingSolution=0;

-

         public NumericZ3ProblemSolver() {

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

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

@@ -66,18 +62,6 @@ public class NumericZ3ProblemSolver {
                 return ctx;

         }

 

-        public long getEndformingProblem() {

-                return endformingProblem;

-        }

-

-        public long getEndSolvingProblem() {

-                return endSolvingProblem;

-        }

-

-        public long getEndFormingSolution() {

-                return endFormingSolution;

-        }

-

         private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) {

                 ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>();

                 XExpression left = ((XBinaryOperation) expression).getLeftOperand();