add dreal-timeout flag

2 files changed, 4 insertions, 3 deletions

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)

                 }

         }