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

---
 .../dslreasoner/viatra2logic/NumericTranslator.xtend  | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

(limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend')

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 3d3f2f4a..791dd644 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
@@ -56,24 +56,29 @@ class NumericTranslator {
 		return res
 	}
 	
-	def NumericProblemSolver selectProblemSolver() {
+	def NumericProblemSolver selectProblemSolver(String selection) {
 //		return new NumericProblemSolver
 // 		add numeric solver decision procedure here
-		if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver
-		return numericSolver;
+		if (numericSolver instanceof NumericDynamicProblemSolver) {
+			val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver
+			return dynamicSolver.selectSolver(selection);
+		} else{
+			if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver
+			return numericSolver;
+		}
 	}
 	
-	def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) {
+	def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches, String select) {
 		val input = formNumericProblemInstance(matches)
-		val solver = selectProblemSolver
+		val solver = selectProblemSolver(select)
 		val satisfiability = solver.isSatisfiable(input)
 		solver.updateTimes
 		return satisfiability
 	}
 	
-	def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches) {
+	def delegateGetSolution(List<PrimitiveElement> primitiveElements, Map<PConstraint, Iterable<Object[]>> matches, String select) {
 		val input = formNumericProblemInstance(matches)
-		val solver = selectProblemSolver
+		val solver = selectProblemSolver(select)
 		val solution = solver.getOneSolution(primitiveElements,input)
 		solver.updateTimes
 		return solution
-- 
cgit v1.2.3-70-g09d2