diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java | 43 |
1 files changed, 0 insertions, 43 deletions
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 deleted file mode 100644 index e8c20138..00000000 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java +++ /dev/null | |||
@@ -1,43 +0,0 @@ | |||
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 NumericDynamicProblemSolver extends NumericProblemSolver{ | ||
13 | |||
14 | // private NumericZ3ProblemSolver z3Solver; | ||
15 | private NumericDrealProblemSolver drealSolver; | ||
16 | private int timeout; | ||
17 | |||
18 | public NumericDynamicProblemSolver(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 | }} | ||