diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java new file mode 100644 index 00000000..199c089b --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java | |||
@@ -0,0 +1,63 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.io.IOException; | ||
4 | import java.util.List; | ||
5 | import java.util.Map; | ||
6 | |||
7 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | ||
8 | import org.eclipse.xtext.xbase.XExpression; | ||
9 | |||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | ||
11 | |||
12 | public class NumericDynamicProblemSolverXXX extends NumericProblemSolver{ | ||
13 | |||
14 | // private NumericZ3ProblemSolver z3Solver; | ||
15 | private NumericDrealProblemSolver drealSolver; | ||
16 | private int timeout; | ||
17 | |||
18 | public NumericDynamicProblemSolverXXX(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { | ||
19 | // this.z3Solver = new NumericZ3ProblemSolver(); | ||
20 | this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout); | ||
21 | this.timeout = drealTimeout; | ||
22 | } | ||
23 | |||
24 | public NumericProblemSolver selectSolver(String selection) { | ||
25 | switch (selection) { | ||
26 | case "z3": | ||
27 | return new NumericZ3ProblemSolver(timeout); | ||
28 | case "dreal": | ||
29 | return this.drealSolver; | ||
30 | default: | ||
31 | throw new IllegalArgumentException("Unknown numeric solver selection: " + selection); | ||
32 | } | ||
33 | } | ||
34 | |||
35 | public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) | ||
36 | throws Exception { | ||
37 | throw new Exception("Should not reach here - isSatisfiable"); | ||
38 | } | ||
39 | |||
40 | public Map<PrimitiveElement, Number> getOneSolution(List<PrimitiveElement> objs, | ||
41 | Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { | ||
42 | throw new Exception("Should not reach here - getOneSolution"); | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | protected void initialize() { | ||
47 | // TODO Auto-generated method stub | ||
48 | |||
49 | } | ||
50 | |||
51 | @Override | ||
52 | protected boolean internalIsSatisfiable( | ||
53 | Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { | ||
54 | // TODO Auto-generated method stub | ||
55 | return false; | ||
56 | } | ||
57 | |||
58 | @Override | ||
59 | protected Map<PrimitiveElement, Number> internalGetOneSolution(List<PrimitiveElement> objs, | ||
60 | Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception { | ||
61 | // TODO Auto-generated method stub | ||
62 | return null; | ||
63 | }} | ||