From 0ebddc8dd265cd5b1b439e3c06f1de1047641559 Mon Sep 17 00:00:00 2001
From: Aren Babikian <aren.babikian@mail.mcgill.ca>
Date: Tue, 16 Feb 2021 03:06:22 +0100
Subject: add dreal-timeout flag

---
 .../viatrasolver/reasoner/ViatraReasonerConfiguration.xtend         | 1 +
 .../inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend   | 6 +++---
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'Solvers/VIATRA-Solver')

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index 74388706..923c847e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -85,6 +85,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
 	public var calculateObjectCreationCosts = false
 	public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3
 	public var drealLocalPath = "<path-to-dreal>";
+	public var drealTimeout = 10000;
 	public var Map<String, Map<String, String>> ignoredAttributesMap = null;
 	public var ExplorationStrategy strategy = ExplorationStrategy.None
 	
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
index 28edff41..8281c3c3 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -64,9 +64,9 @@ class NumericSolver {
 		if (strategy == ExplorationStrategy.None) {
 			//initialise the specified
 			if (solverSelection == NumericSolverSelection.DREAL_DOCKER) 
-				return new NumericDrealProblemSolver(true, null)
+				return new NumericDrealProblemSolver(true, null, config.drealTimeout)
 			if (solverSelection == NumericSolverSelection.DREAL_LOCAL)
-				return new NumericDrealProblemSolver(false, drealLocalPath)
+				return new NumericDrealProblemSolver(false, drealLocalPath, config.drealTimeout)
 			if (solverSelection == NumericSolverSelection.Z3) {
 				//TODO THIS IS HARD-CODED for now
 //			val root = "/data/viatra/VIATRA-Generator";
@@ -90,7 +90,7 @@ class NumericSolver {
 //			String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
 	        System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
 	        System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
-			return new NumericDynamicProblemSolver(drealLocalPath)
+			return new NumericDynamicProblemSolver(drealLocalPath, config.drealTimeout)
 		}
 	}
 	
-- 
cgit v1.2.3-70-g09d2