From 598fa1dae639ac110b2f549e8c2978ae3974c53a Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 19 Jan 2021 01:15:32 +0100 Subject: add vsconfig flag to allow running dreal locally --- .../viatrasolver/reasoner/ViatraReasoner.xtend | 4 ++-- .../reasoner/ViatraReasonerConfiguration.xtend | 6 ++++-- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 15 ++++++++++----- 3 files changed, 16 insertions(+), 9 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver') 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 d386241d..ed04ae4a 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 @@ -165,8 +165,8 @@ class ViatraReasoner extends LogicReasoner { val solverTime = System.nanoTime - solverStartTime viatraConfig.progressMonitor.workedSearchFinished - //dreal teardown - if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL){ + //dreal docker teardown + if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL_DOCKER){ (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown() } 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 ebfd5d81..c0daaad2 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 @@ -34,7 +34,8 @@ enum PunishSizeStrategy { } enum NumericSolverSelection { - DREAL, + DREAL_DOCKER, + DREAL_LOCAL, Z3 } @@ -75,7 +76,8 @@ 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 numericSolverSelection = NumericSolverSelection.DREAL_DOCKER //currently defaulted to DREAL + public var drealLocalPath = ""; 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 ab3e6601..9223ecc8 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 @@ -34,6 +34,7 @@ class NumericSolver { val boolean intermediateConsistencyCheck val boolean caching; Map>>,Boolean> satisfiabilityCache = new HashMap + val String drealLocalPath; var long runtime = 0 var long cachingTime = 0 @@ -43,12 +44,16 @@ class NumericSolver { new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { this.method = method this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks - this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) this.caching = caching + this.drealLocalPath = config.drealLocalPath + this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) } def createNumericTranslator(NumericSolverSelection solverSelection) { - if (solverSelection == NumericSolverSelection.DREAL) return new NumericDrealProblemSolver + if (solverSelection == NumericSolverSelection.DREAL_DOCKER) + return new NumericDrealProblemSolver(true, null) + if (solverSelection == NumericSolverSelection.DREAL_LOCAL) + return new NumericDrealProblemSolver(false, drealLocalPath) if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver } @@ -98,12 +103,12 @@ class NumericSolver { finalResult=true } else { val propagatedConstraints = new HashMap - println("------ Any matches?") + println("<<<>>>") for(entry : matches.entrySet) { val constraint = entry.key - println("------ " + constraint) +// println("--match?-- " + constraint) val allMatches = entry.value.allMatches.map[it.toArray] - println("------ " + allMatches.toList) +// println("---------- " + entry.value.allMatches) propagatedConstraints.put(constraint,allMatches) } if(propagatedConstraints.values.forall[empty]) { -- cgit v1.2.3-54-g00ecf