diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2020-12-13 21:11:34 -0500 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2020-12-13 21:11:34 -0500 |
commit | 9c575fee851ea3a5498289041f6651ae97869556 (patch) | |
tree | 77b7b9375a0b9d568a0d3b78c62a01c8d523e684 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | |
parent | prep for refactoring Numeric Probelm Solvers (diff) | |
download | VIATRA-Generator-9c575fee851ea3a5498289041f6651ae97869556.tar.gz VIATRA-Generator-9c575fee851ea3a5498289041f6651ae97869556.tar.zst VIATRA-Generator-9c575fee851ea3a5498289041f6651ae97869556.zip |
add numericProblemSolver supertype
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java | 18 |
1 files changed, 1 insertions, 17 deletions
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 | |||
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; | 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; |
28 | 28 | ||
29 | 29 | ||
30 | public class NumericZ3ProblemSolver { | 30 | public class NumericZ3ProblemSolver extends NumericProblemSolver{ |
31 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; | 31 | private static final String N_Base = "org.eclipse.xtext.xbase.lib."; |
32 | private static final String N_PLUS = "operator_plus"; | 32 | private static final String N_PLUS = "operator_plus"; |
33 | private static final String N_MINUS = "operator_minus"; | 33 | private static final String N_MINUS = "operator_minus"; |
@@ -49,10 +49,6 @@ public class NumericZ3ProblemSolver { | |||
49 | private Solver s; | 49 | private Solver s; |
50 | private Map<Object, Expr> varMap; | 50 | private Map<Object, Expr> varMap; |
51 | 51 | ||
52 | long endformingProblem=0; | ||
53 | long endSolvingProblem=0; | ||
54 | long endFormingSolution=0; | ||
55 | |||
56 | public NumericZ3ProblemSolver() { | 52 | public NumericZ3ProblemSolver() { |
57 | HashMap<String, String> cfg = new HashMap<String, String>(); | 53 | HashMap<String, String> cfg = new HashMap<String, String>(); |
58 | cfg.put("model", "true"); | 54 | cfg.put("model", "true"); |
@@ -66,18 +62,6 @@ public class NumericZ3ProblemSolver { | |||
66 | return ctx; | 62 | return ctx; |
67 | } | 63 | } |
68 | 64 | ||
69 | public long getEndformingProblem() { | ||
70 | return endformingProblem; | ||
71 | } | ||
72 | |||
73 | public long getEndSolvingProblem() { | ||
74 | return endSolvingProblem; | ||
75 | } | ||
76 | |||
77 | public long getEndFormingSolution() { | ||
78 | return endFormingSolution; | ||
79 | } | ||
80 | |||
81 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { | 65 | private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) { |
82 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); | 66 | ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>(); |
83 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); | 67 | XExpression left = ((XBinaryOperation) expression).getLeftOperand(); |