From 8fd50f7d4a979117a1e643f5384b76f4a3e36801 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Mon, 14 Dec 2020 03:27:43 -0500 Subject: implement isSatisfiable with Dreal integration --- .../bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | 3 +++ .../mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | 1 + 2 files changed, 4 insertions(+) (limited to 'Solvers') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index 8e992741..1f902b90 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend @@ -163,6 +163,9 @@ class ViatraReasoner extends LogicReasoner { } val solverTime = System.nanoTime - solverStartTime viatraConfig.progressMonitor.workedSearchFinished + + //dreal teardown + numericSolver.numericDrealSolver.teardown() // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches val statistics = createStatistics => [ 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 70e8e9c2..0e789671 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 @@ -68,6 +68,7 @@ class NumericSolver { def getSolverFormingProblem(){this.t.formingProblemTime} def getSolverSolvingProblem(){this.t.solvingProblemTime} def getSolverSolution(){this.t.formingSolutionTime} + def getNumericDrealSolver(){this.t.drealSolver} def boolean maySatisfiable() { if(intermediateConsistencyCheck) { -- cgit v1.2.3-70-g09d2