From 8fd50f7d4a979117a1e643f5384b76f4a3e36801 Mon Sep 17 00:00:00 2001
From: Aren Babikian <aren.babikian@mail.mcgill.ca>
Date: Mon, 14 Dec 2020 03:27:43 -0500
Subject: implement isSatisfiable with Dreal integration

---
 .../hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend   | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(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 d63604b0..22ea41bf 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,6 +16,7 @@ import org.eclipse.xtext.xbase.XFeatureCall
 class NumericTranslator {
 	
 	private XExpressionExtractor extractor = new XExpressionExtractor();
+	private NumericDrealProblemSolver drealSolver = new NumericDrealProblemSolver();
 	
 	long formingProblemTime=0;
 	long solvingProblemTime=0;
@@ -52,7 +53,7 @@ class NumericTranslator {
 	
 	def NumericProblemSolver selectProblemSolver() {
 //		return new NumericProblemSolver
-		return new NumericDrealProblemSolver
+		return drealSolver;
 	}
 	
 	def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) {
@@ -80,4 +81,5 @@ class NumericTranslator {
 	def getFormingProblemTime() {formingProblemTime}
 	def getSolvingProblemTime() {solvingProblemTime}
 	def getFormingSolutionTime() {formingSolutionTime}
+	def getDrealSolver(){return drealSolver}
 }
\ No newline at end of file
-- 
cgit v1.2.3-70-g09d2