From bc403272d867f82edd623179d82c080e57154c1a Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 16 Feb 2021 09:01:25 +0100 Subject: CrossingScenario case study is ready for server --- .../reasoner/dse/BestFirstStrategyForModelGeneration.java | 1 + .../dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | 10 +++++----- 2 files changed, 6 insertions(+), 5 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index a8d2381c..c62d124a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java @@ -222,6 +222,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // } // } +// System.out.println("--------NEXT"); boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness); if(consistencyCheckResult == true) { continue mainLoop; } 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 8281c3c3..a228afc6 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 @@ -55,7 +55,7 @@ class NumericSolver { this.caching = caching this.drealLocalPath = config.drealLocalPath this.strategy = config.strategy - this.t = new NumericTranslator(createNumericTranslator(config)) + this.t = new NumericTranslator(createNumericTranslator(config), config.drealTimeout) } def createNumericTranslator(ViatraReasonerConfiguration config) { @@ -77,7 +77,7 @@ class NumericSolver { System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); // System.load("libz3.so"); // System.load("libz3java.so"); - return new NumericZ3ProblemSolver + return new NumericZ3ProblemSolver(config.drealTimeout) } } else { @@ -150,9 +150,9 @@ class NumericSolver { //Filter constraints if there are phase-related restricutions //null whitelist means accept everything - println("<<<>>> (" + phase + ")") +// println("<<<>>> (" + phase + ")") if (phase == -2) { - println("Skipping numeric check") +// println("Skipping numeric check") //TODO Big assumption return true } @@ -235,7 +235,7 @@ class NumericSolver { def selectSolver(int phase) { if (strategy === ExplorationStrategy.CrossingScenario){ - if (phase == 1) return "dreal" + if (phase == 1) return "z3" else return "dreal" } return "irrelevant" -- cgit v1.2.3-54-g00ecf