From 1d64b93a6dd242b688562a85a0be9bf2d7b8ba05 Mon Sep 17 00:00:00 2001
From: Aren Babikian <aren.babikian@mail.mcgill.ca>
Date: Tue, 15 Dec 2020 13:18:17 -0500
Subject: Add config flag for selecting numeric solver. Integ with Z3

---
 .../viatra2logic/ExpressionEvaluation2Logic.xtend           |  3 ++-
 .../inf/dslreasoner/viatra2logic/NumericTranslator.xtend    | 13 ++++++++++---
 2 files changed, 12 insertions(+), 4 deletions(-)

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

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
index b9942a17..1b68fed2 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
@@ -17,7 +17,8 @@ class ExpressionEvaluation2Logic {
 	var NumericProblemSolver _numericSolver = null //new NumericProblemSolver
 	def getNumericSolver() {
 		if(_numericSolver === null) {
-			_numericSolver = (new NumericTranslator).selectProblemSolver
+			// it seems like this getter has no use
+			_numericSolver = (new NumericTranslator(null)).selectProblemSolver
 		}
 		return _numericSolver
 	}
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 22ea41bf..3d3f2f4a 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
@@ -16,7 +16,7 @@ import org.eclipse.xtext.xbase.XFeatureCall
 class NumericTranslator {
 	
 	private XExpressionExtractor extractor = new XExpressionExtractor();
-	private NumericDrealProblemSolver drealSolver = new NumericDrealProblemSolver();
+	private NumericProblemSolver numericSolver;
 	
 	long formingProblemTime=0;
 	long solvingProblemTime=0;
@@ -28,6 +28,11 @@ class NumericTranslator {
 				o1.simpleName.compareTo(o2.simpleName)
 			}
 		}
+		
+	new(NumericProblemSolver numericProblemSolver){
+		this.numericSolver = numericProblemSolver
+	}
+	
 	def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) {
 		val res = new HashMap
 		for(var i=0; i<tuple.length; i++) {
@@ -53,7 +58,9 @@ class NumericTranslator {
 	
 	def NumericProblemSolver selectProblemSolver() {
 //		return new NumericProblemSolver
-		return drealSolver;
+// 		add numeric solver decision procedure here
+		if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver
+		return numericSolver;
 	}
 	
 	def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) {
@@ -81,5 +88,5 @@ class NumericTranslator {
 	def getFormingProblemTime() {formingProblemTime}
 	def getSolvingProblemTime() {solvingProblemTime}
 	def getFormingSolutionTime() {formingSolutionTime}
-	def getDrealSolver(){return drealSolver}
+	def getNumericSolver(){numericSolver}
 }
\ No newline at end of file
-- 
cgit v1.2.3-54-g00ecf