From 0ebddc8dd265cd5b1b439e3c06f1de1047641559 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 16 Feb 2021 03:06:22 +0100 Subject: add dreal-timeout flag --- .../mit/inf/dslreasoner/application/execution/SolverLoader.xtend | 4 ++++ Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig | 1 + .../inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | 7 ++++--- .../inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java | 4 ++-- .../viatrasolver/reasoner/ViatraReasonerConfiguration.xtend | 1 + .../inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | 6 +++--- 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 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(); 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 = ""; + public var drealTimeout = 10000; public var Map> 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-54-g00ecf