add dreal-timeout flag

6 files changed, 15 insertions, 8 deletions

diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
index 045387a0..ac4f29a9 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
@@ -156,6 +156,10 @@ class SolverLoader {
                                                 c.drealLocalPath = stringValue; 

                                         }

                                 }

+                                if (config.containsKey("dreal-timeout")) {

+                                        val stringValue = config.get("dreal-timeout")

+                                                c.drealTimeout = Integer.parseInt(stringValue)

+                                }

                                 if (config.containsKey("scopePropagator")) {

                                         val stringValue = config.get("scopePropagator")

                                         c.scopePropagatorStrategy = switch (stringValue) {

diff --git a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig
index db00ed7b..401273b2 100644
--- a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig
+++ b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig
@@ -22,6 +22,7 @@ generate {
                 log-level = none,

                 "numeric-solver" = "dreal-local",

                 "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal",

+                "dreal-timeout" = "10000",

                 "strategy" = "crossingScenario",

                 "ignored-attributes" = "

                         Pedestrian.xPos=*, 

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
index f098d575..eb63d96a 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
@@ -43,13 +43,14 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
         private Map<String, String> curVar2Decl;

         

         private final int TIMEOUT_DOCKER = 5000;

-        private final int TIMEOUT_LOCAL = -1;

-        private final int DEBUG_PRINT = 3;

+        private int TIMEOUT_LOCAL = -1;

+        private final int DEBUG_PRINT = 2;

 

-        public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException {

+        public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath, int drealTimeout) throws IOException, InterruptedException {

                 this.useDocker = useDocker;

                 this.varMap = new HashMap<Object, String>();

                 this.drealLocalPath = drealLocalPath;

+                this.TIMEOUT_LOCAL = drealTimeout;

                 

                 if (useDocker) setupDocker();

         }

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
index bd4a10ff..1e5c1f29 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java
@@ -14,9 +14,9 @@ public class NumericDynamicProblemSolver extends NumericProblemSolver{
 //      private NumericZ3ProblemSolver z3Solver;
         private NumericDrealProblemSolver drealSolver;
         
-        public NumericDynamicProblemSolver(String drealLocalPath) throws IOException, InterruptedException {
+        public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException {
 //              this.z3Solver = new NumericZ3ProblemSolver();
-                this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath);
+                this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout);
         }
         
         public NumericProblemSolver selectSolver(String selection) {
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)

                 }

         }