fix dreal call on solved problem imprecision issue

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 {
         }

         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

         }