diff options
author | 2021-01-19 01:15:32 +0100 | |
---|---|---|
committer | 2021-01-19 01:15:32 +0100 | |
commit | 598fa1dae639ac110b2f549e8c2978ae3974c53a (patch) | |
tree | 69bd6b39cdbd65833ce0f4656981ab25911c3bd1 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner | |
parent | add some actor-related queries, solve minor Z3 issue (diff) | |
download | VIATRA-Generator-598fa1dae639ac110b2f549e8c2978ae3974c53a.tar.gz VIATRA-Generator-598fa1dae639ac110b2f549e8c2978ae3974c53a.tar.zst VIATRA-Generator-598fa1dae639ac110b2f549e8c2978ae3974c53a.zip |
add vsconfig flag to allow running dreal locally
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner')
3 files changed, 16 insertions, 9 deletions
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 { | |||
165 | val solverTime = System.nanoTime - solverStartTime | 165 | val solverTime = System.nanoTime - solverStartTime |
166 | viatraConfig.progressMonitor.workedSearchFinished | 166 | viatraConfig.progressMonitor.workedSearchFinished |
167 | 167 | ||
168 | //dreal teardown | 168 | //dreal docker teardown |
169 | if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL){ | 169 | if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL_DOCKER){ |
170 | (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown() | 170 | (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown() |
171 | } | 171 | } |
172 | 172 | ||
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 { | |||
34 | } | 34 | } |
35 | 35 | ||
36 | enum NumericSolverSelection { | 36 | enum NumericSolverSelection { |
37 | DREAL, | 37 | DREAL_DOCKER, |
38 | DREAL_LOCAL, | ||
38 | Z3 | 39 | Z3 |
39 | } | 40 | } |
40 | 41 | ||
@@ -75,7 +76,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
75 | public var nonContainmentWeight = 1 | 76 | public var nonContainmentWeight = 1 |
76 | public var unfinishedWFWeight = 1 | 77 | public var unfinishedWFWeight = 1 |
77 | public var calculateObjectCreationCosts = false | 78 | public var calculateObjectCreationCosts = false |
78 | public var numericSolverSelection = NumericSolverSelection.DREAL //currently defaulted to DREAL | 79 | public var numericSolverSelection = NumericSolverSelection.DREAL_DOCKER //currently defaulted to DREAL |
80 | public var drealLocalPath = "<path-to-dreal>"; | ||
79 | 81 | ||
80 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( | 82 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( |
81 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) | 83 | 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 { | |||
34 | val boolean intermediateConsistencyCheck | 34 | val boolean intermediateConsistencyCheck |
35 | val boolean caching; | 35 | val boolean caching; |
36 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | 36 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap |
37 | val String drealLocalPath; | ||
37 | 38 | ||
38 | var long runtime = 0 | 39 | var long runtime = 0 |
39 | var long cachingTime = 0 | 40 | var long cachingTime = 0 |
@@ -43,12 +44,16 @@ class NumericSolver { | |||
43 | new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { | 44 | new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { |
44 | this.method = method | 45 | this.method = method |
45 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks | 46 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks |
46 | this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) | ||
47 | this.caching = caching | 47 | this.caching = caching |
48 | this.drealLocalPath = config.drealLocalPath | ||
49 | this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) | ||
48 | } | 50 | } |
49 | 51 | ||
50 | def createNumericTranslator(NumericSolverSelection solverSelection) { | 52 | def createNumericTranslator(NumericSolverSelection solverSelection) { |
51 | if (solverSelection == NumericSolverSelection.DREAL) return new NumericDrealProblemSolver | 53 | if (solverSelection == NumericSolverSelection.DREAL_DOCKER) |
54 | return new NumericDrealProblemSolver(true, null) | ||
55 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) | ||
56 | return new NumericDrealProblemSolver(false, drealLocalPath) | ||
52 | if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver | 57 | if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver |
53 | } | 58 | } |
54 | 59 | ||
@@ -98,12 +103,12 @@ class NumericSolver { | |||
98 | finalResult=true | 103 | finalResult=true |
99 | } else { | 104 | } else { |
100 | val propagatedConstraints = new HashMap | 105 | val propagatedConstraints = new HashMap |
101 | println("------ Any matches?") | 106 | println("<<<<START-STEP>>>>") |
102 | for(entry : matches.entrySet) { | 107 | for(entry : matches.entrySet) { |
103 | val constraint = entry.key | 108 | val constraint = entry.key |
104 | println("------ " + constraint) | 109 | // println("--match?-- " + constraint) |
105 | val allMatches = entry.value.allMatches.map[it.toArray] | 110 | val allMatches = entry.value.allMatches.map[it.toArray] |
106 | println("------ " + allMatches.toList) | 111 | // println("---------- " + entry.value.allMatches) |
107 | propagatedConstraints.put(constraint,allMatches) | 112 | propagatedConstraints.put(constraint,allMatches) |
108 | } | 113 | } |
109 | if(propagatedConstraints.values.forall[empty]) { | 114 | if(propagatedConstraints.values.forall[empty]) { |