diff options
author | 2021-02-16 09:01:25 +0100 | |
---|---|---|
committer | 2021-02-16 09:01:25 +0100 | |
commit | bc403272d867f82edd623179d82c080e57154c1a (patch) | |
tree | 3551ba142ed725595ee684981fc8973cade2ebf4 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src | |
parent | add dreal-timeout flag (diff) | |
download | VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.tar.gz VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.tar.zst VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.zip |
CrossingScenario case study is ready for serverdreal-integration
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src')
2 files changed, 6 insertions, 5 deletions
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 { | |||
222 | // } | 222 | // } |
223 | // } | 223 | // } |
224 | 224 | ||
225 | // System.out.println("--------NEXT"); | ||
225 | boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness); | 226 | boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness); |
226 | if(consistencyCheckResult == true) { continue mainLoop; } | 227 | if(consistencyCheckResult == true) { continue mainLoop; } |
227 | 228 | ||
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 { | |||
55 | this.caching = caching | 55 | this.caching = caching |
56 | this.drealLocalPath = config.drealLocalPath | 56 | this.drealLocalPath = config.drealLocalPath |
57 | this.strategy = config.strategy | 57 | this.strategy = config.strategy |
58 | this.t = new NumericTranslator(createNumericTranslator(config)) | 58 | this.t = new NumericTranslator(createNumericTranslator(config), config.drealTimeout) |
59 | } | 59 | } |
60 | 60 | ||
61 | def createNumericTranslator(ViatraReasonerConfiguration config) { | 61 | def createNumericTranslator(ViatraReasonerConfiguration config) { |
@@ -77,7 +77,7 @@ class NumericSolver { | |||
77 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | 77 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); |
78 | // System.load("libz3.so"); | 78 | // System.load("libz3.so"); |
79 | // System.load("libz3java.so"); | 79 | // System.load("libz3java.so"); |
80 | return new NumericZ3ProblemSolver | 80 | return new NumericZ3ProblemSolver(config.drealTimeout) |
81 | } | 81 | } |
82 | } | 82 | } |
83 | else { | 83 | else { |
@@ -150,9 +150,9 @@ class NumericSolver { | |||
150 | //Filter constraints if there are phase-related restricutions | 150 | //Filter constraints if there are phase-related restricutions |
151 | //null whitelist means accept everything | 151 | //null whitelist means accept everything |
152 | 152 | ||
153 | println("<<<<START-STEP>>>> (" + phase + ")") | 153 | // println("<<<<START-STEP>>>> (" + phase + ")") |
154 | if (phase == -2) { | 154 | if (phase == -2) { |
155 | println("Skipping numeric check") | 155 | // println("Skipping numeric check") |
156 | //TODO Big assumption | 156 | //TODO Big assumption |
157 | return true | 157 | return true |
158 | } | 158 | } |
@@ -235,7 +235,7 @@ class NumericSolver { | |||
235 | 235 | ||
236 | def selectSolver(int phase) { | 236 | def selectSolver(int phase) { |
237 | if (strategy === ExplorationStrategy.CrossingScenario){ | 237 | if (strategy === ExplorationStrategy.CrossingScenario){ |
238 | if (phase == 1) return "dreal" | 238 | if (phase == 1) return "z3" |
239 | else return "dreal" | 239 | else return "dreal" |
240 | } | 240 | } |
241 | return "irrelevant" | 241 | return "irrelevant" |