From f5afda733ffdf4f52da932e03919c20b99bf7fa6 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 15 Dec 2020 13:18:17 -0500 Subject: Add config flag for selecting numeric solver. Integ with Z3 --- .../viatrasolver/reasoner/ViatraReasoner.xtend | 7 +++++-- .../reasoner/ViatraReasonerConfiguration.xtend | 6 ++++++ .../viatrasolver/reasoner/dse/NumericSolver.xtend | 18 ++++++++++++++---- 3 files changed, 25 insertions(+), 6 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf') 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 1f902b90..144e5e6f 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 @@ -38,6 +38,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel import org.eclipse.viatra.dse.solutionstore.SolutionStore import org.eclipse.viatra.dse.statecode.IStateCoderFactory +import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver class ViatraReasoner extends LogicReasoner { val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() @@ -109,7 +110,7 @@ class ViatraReasoner extends LogicReasoner { new SolutionStore(numberOfRequiredSolutions) } solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) - val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) + val numericSolver = new NumericSolver(method, viatraConfig, false) val solutionSaver = method.solutionSaver solutionSaver.numericSolver = numericSolver val solutionCopier = solutionSaver.solutionCopier @@ -165,7 +166,9 @@ class ViatraReasoner extends LogicReasoner { viatraConfig.progressMonitor.workedSearchFinished //dreal teardown - numericSolver.numericDrealSolver.teardown() + if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL){ + (numericSolver.numericSolverSelection as NumericDrealProblemSolver).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/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index fbe6da9d..ebfd5d81 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend @@ -33,6 +33,11 @@ enum PunishSizeStrategy { LARGER_IS_BETTER } +enum NumericSolverSelection { + DREAL, + Z3 +} + class ViatraReasonerConfiguration extends LogicSolverConfiguration { // public var Iterable existingQueries public var nameNewElements = false @@ -70,6 +75,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { public var nonContainmentWeight = 1 public var unfinishedWFWeight = 1 public var calculateObjectCreationCosts = false + public var numericSolverSelection = NumericSolverSelection.DREAL //currently defaulted to DREAL public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) 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 0e789671..4b0ea544 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 @@ -1,6 +1,8 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse +import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator +import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation @@ -8,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration import java.math.BigDecimal import java.util.HashMap import java.util.LinkedHashMap @@ -25,7 +29,7 @@ class NumericSolver { var ThreadContext threadContext val constraint2MustUnitPropagationPrecondition = new HashMap> val constraint2CurrentUnitPropagationPrecondition = new HashMap> - NumericTranslator t = new NumericTranslator + NumericTranslator t val boolean intermediateConsistencyCheck val boolean caching; @@ -36,12 +40,18 @@ class NumericSolver { var int numberOfSolverCalls = 0 var int numberOfCachedSolverCalls = 0 - new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) { + new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { this.method = method - this.intermediateConsistencyCheck = intermediateConsistencyCheck + this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks + this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) this.caching = caching } + def createNumericTranslator(NumericSolverSelection solverSelection) { + if (solverSelection == NumericSolverSelection.DREAL) return new NumericDrealProblemSolver + if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver + } + def init(ThreadContext context) { // This makes the NumericSolver single-threaded, // but that's not a problem, because we only use the solver on a single thread anyways. @@ -68,7 +78,7 @@ class NumericSolver { def getSolverFormingProblem(){this.t.formingProblemTime} def getSolverSolvingProblem(){this.t.solvingProblemTime} def getSolverSolution(){this.t.formingSolutionTime} - def getNumericDrealSolver(){this.t.drealSolver} + def getNumericSolverSelection(){this.t.numericSolver} def boolean maySatisfiable() { if(intermediateConsistencyCheck) { -- cgit v1.2.3-54-g00ecf