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/viatrasolver/reasoner/dse | |
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/viatrasolver/reasoner/dse')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | 15 |
1 files changed, 10 insertions, 5 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 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]) { |