From 0c56d765b120654bfd3534aa5b6d12476070515b Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Mon, 15 Feb 2021 07:42:02 +0100 Subject: fix dreal call on solved problem imprecision issue --- .../inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend') 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 { } def boolean currentSatisfiable() { val int phase = determinePhase() - //TODO generalize this isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) } @@ -223,7 +222,11 @@ class NumericSolver { } } this.runtime+=System.nanoTime-start - if (phase == 2) finalResult = isSatisfiable(matches, 3) + //STRATEGY + if (phase == 2) { + if (!finalResult) return finalResult + else finalResult = isSatisfiable(matches, 3) + } return finalResult } -- cgit v1.2.3-54-g00ecf