diff options
author | 2021-02-15 07:42:02 +0100 | |
---|---|---|
committer | 2021-02-15 07:42:02 +0100 | |
commit | 0c56d765b120654bfd3534aa5b6d12476070515b (patch) | |
tree | 10a01c11769364116061e33fda4167db68a4c8be /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme | |
parent | finished first impl that works sometimes (issue w/ SAT in Dreal rerun) (diff) | |
download | VIATRA-Generator-0c56d765b120654bfd3534aa5b6d12476070515b.tar.gz VIATRA-Generator-0c56d765b120654bfd3534aa5b6d12476070515b.tar.zst VIATRA-Generator-0c56d765b120654bfd3534aa5b6d12476070515b.zip |
fix dreal call on solved problem imprecision issue
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | 7 |
1 files changed, 5 insertions, 2 deletions
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 bb2c7dbf..44964079 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 | |||
@@ -131,7 +131,6 @@ class NumericSolver { | |||
131 | } | 131 | } |
132 | def boolean currentSatisfiable() { | 132 | def boolean currentSatisfiable() { |
133 | val int phase = determinePhase() | 133 | val int phase = determinePhase() |
134 | //TODO generalize this | ||
135 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) | 134 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) |
136 | } | 135 | } |
137 | 136 | ||
@@ -223,7 +222,11 @@ class NumericSolver { | |||
223 | } | 222 | } |
224 | } | 223 | } |
225 | this.runtime+=System.nanoTime-start | 224 | this.runtime+=System.nanoTime-start |
226 | if (phase == 2) finalResult = isSatisfiable(matches, 3) | 225 | //STRATEGY |
226 | if (phase == 2) { | ||
227 | if (!finalResult) return finalResult | ||
228 | else finalResult = isSatisfiable(matches, 3) | ||
229 | } | ||
227 | return finalResult | 230 | return finalResult |
228 | } | 231 | } |
229 | 232 | ||