From a22bd211a42eebed6ee5ddf67e1836aad2bad0e3 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Sun, 13 Dec 2020 21:11:34 -0500 Subject: add numericProblemSolver supertype --- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 4 ++-- .../viatra2logic/NumericDrealProblemSolver.java | 23 ++++------------------ .../viatra2logic/NumericProblemSolver.java | 23 ++++++++++++++++++++++ .../viatra2logic/NumericTranslator.xtend | 4 ++-- .../viatra2logic/NumericZ3ProblemSolver.java | 18 +---------------- 5 files changed, 32 insertions(+), 40 deletions(-) create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf') 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 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(); } - public Process runProcess(List cmd) throws IOException, InterruptedException { + private Process runProcess(List 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 getJvmIdentifiableElements(XExpression expression) { // ArrayList allElem = new ArrayList(); @@ -115,7 +100,7 @@ public class NumericDrealProblemSolver { // } // } - public Process callDreal() throws IOException, InterruptedException { + private Process callDreal() throws IOException, InterruptedException { List drealCmd = new ArrayList( 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>> matches) throws Exception; + public abstract Map getOneSolution(List objs, Map>> 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 varMap; - long endformingProblem=0; - long endSolvingProblem=0; - long endFormingSolution=0; - public NumericZ3ProblemSolver() { HashMap cfg = new HashMap(); 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 getJvmIdentifiableElements(XExpression expression) { ArrayList allElem = new ArrayList(); XExpression left = ((XBinaryOperation) expression).getLeftOperand(); -- cgit v1.2.3-70-g09d2