From a8eb346fb97b54b6ee693da4840abd8be8b43843 Mon Sep 17 00:00:00 2001
From: Aren Babikian <aren.babikian@mail.mcgill.ca>
Date: Sun, 14 Feb 2021 08:01:00 +0100
Subject: Add strategy flag + implement alost working crossingScenarioStrategy

---
 .../viatra2logic/NumericDynamicProblemSolver.java  | 41 ++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java

(limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java')

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
new file mode 100644
index 00000000..bd4a10ff
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
@@ -0,0 +1,41 @@
+package hu.bme.mit.inf.dslreasoner.viatra2logic;
+
+import java.io.IOException;
+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 class NumericDynamicProblemSolver extends NumericProblemSolver{
+	
+//	private NumericZ3ProblemSolver z3Solver;
+	private NumericDrealProblemSolver drealSolver;
+	
+	public NumericDynamicProblemSolver(String drealLocalPath) throws IOException, InterruptedException {
+//		this.z3Solver = new NumericZ3ProblemSolver();
+		this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath);
+	}
+	
+	public NumericProblemSolver selectSolver(String selection) {
+		switch (selection) {
+		case "z3":
+			return new NumericZ3ProblemSolver();
+		case "dreal":
+			return this.drealSolver;
+		default:
+		throw new IllegalArgumentException("Unknown numeric solver selection: " + selection);
+		}
+	}
+
+	public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches)
+			throws Exception {
+		throw new Exception("Should not reach here - isSatisfiable");
+	}
+
+	public Map<PrimitiveElement, Number> getOneSolution(List<PrimitiveElement> objs,
+			Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception {
+		throw new Exception("Should not reach here - getOneSolution");
+	}}
-- 
cgit v1.2.3-54-g00ecf