diff options
| author |  Oszkar Semerath <semerath@mit.bme.hu> | 2020-05-19 02:07:37 +0200 |
|---|---|---|
| committer | Oszkar Semerath <semerath@mit.bme.hu> | 2020-05-19 02:07:37 +0200 |
| commit | 0f5bf3097038ff39171fb3548dc80073d237d162 (patch) | |
| tree | bb613f72bd0c70ca8463d87a071cb5d2e448f085 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu | |
| parent | removed every occurence of check expressions (diff) | |
| download | VIATRA-Generator-0f5bf3097038ff39171fb3548dc80073d237d162.tar.gz VIATRA-Generator-0f5bf3097038ff39171fb3548dc80073d237d162.tar.zst VIATRA-Generator-0f5bf3097038ff39171fb3548dc80073d237d162.zip | |
intermediateConsistencyCheck controls the maySatisfiable only
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu')
| -rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | 74 |
1 files changed, 37 insertions, 37 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 a012f51b..ed8bdae3 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 | |||
| @@ -64,7 +64,11 @@ class NumericSolver { | |||
| 64 | def getSolverSolution(){this.t.formingSolutionTime} | 64 | def getSolverSolution(){this.t.formingSolutionTime} |
| 65 | 65 | ||
| 66 | def boolean maySatisfiable() { | 66 | def boolean maySatisfiable() { |
| 67 | isSatisfiable(this.constraint2MustUnitPropagationPrecondition) | 67 | if(intermediateConsistencyCheck) { |
| 68 | return isSatisfiable(this.constraint2MustUnitPropagationPrecondition) | ||
| 69 | } else { | ||
| 70 | return true | ||
| 71 | } | ||
| 68 | } | 72 | } |
| 69 | def boolean currentSatisfiable() { | 73 | def boolean currentSatisfiable() { |
| 70 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition) | 74 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition) |
| @@ -73,48 +77,44 @@ class NumericSolver { | |||
| 73 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { | 77 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { |
| 74 | val start = System.nanoTime | 78 | val start = System.nanoTime |
| 75 | var boolean finalResult | 79 | var boolean finalResult |
| 76 | if(intermediateConsistencyCheck) { | 80 | if(matches.empty){ |
| 77 | if(matches.empty){ | 81 | finalResult=true |
| 82 | } else { | ||
| 83 | val propagatedConstraints = new HashMap | ||
| 84 | for(entry : matches.entrySet) { | ||
| 85 | val constraint = entry.key | ||
| 86 | //println(constraint) | ||
| 87 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
| 88 | //println(allMatches.toList) | ||
| 89 | propagatedConstraints.put(constraint,allMatches) | ||
| 90 | } | ||
| 91 | if(propagatedConstraints.values.forall[empty]) { | ||
| 78 | finalResult=true | 92 | finalResult=true |
| 79 | } else { | 93 | } else { |
| 80 | val propagatedConstraints = new HashMap | 94 | if(caching) { |
| 81 | for(entry : matches.entrySet) { | 95 | val code = getCode(propagatedConstraints) |
| 82 | val constraint = entry.key | 96 | val cachedResult = satisfiabilityCache.get(code) |
| 83 | //println(constraint) | 97 | if(cachedResult === null) { |
| 84 | val allMatches = entry.value.allMatches.map[it.toArray] | 98 | // println('''new problem, call solver''') |
| 85 | //println(allMatches.toList) | 99 | // for(entry : code.entrySet) { |
| 86 | propagatedConstraints.put(constraint,allMatches) | 100 | // println('''«entry.key» -> «entry.value»''') |
| 87 | } | 101 | // } |
| 88 | if(propagatedConstraints.values.forall[empty]) { | 102 | //println(code.hashCode) |
| 89 | finalResult=true | ||
| 90 | } else { | ||
| 91 | if(caching) { | ||
| 92 | val code = getCode(propagatedConstraints) | ||
| 93 | val cachedResult = satisfiabilityCache.get(code) | ||
| 94 | if(cachedResult === null) { | ||
| 95 | // println('''new problem, call solver''') | ||
| 96 | // for(entry : code.entrySet) { | ||
| 97 | // println('''«entry.key» -> «entry.value»''') | ||
| 98 | // } | ||
| 99 | //println(code.hashCode) | ||
| 100 | this.numberOfSolverCalls++ | ||
| 101 | val res = t.delegateIsSatisfiable(propagatedConstraints) | ||
| 102 | satisfiabilityCache.put(code,res) | ||
| 103 | finalResult=res | ||
| 104 | } else { | ||
| 105 | //println('''similar problem, answer from cache''') | ||
| 106 | finalResult=cachedResult | ||
| 107 | this.numberOfCachedSolverCalls++ | ||
| 108 | } | ||
| 109 | } else { | ||
| 110 | finalResult= t.delegateIsSatisfiable(propagatedConstraints) | ||
| 111 | this.numberOfSolverCalls++ | 103 | this.numberOfSolverCalls++ |
| 104 | val res = t.delegateIsSatisfiable(propagatedConstraints) | ||
| 105 | satisfiabilityCache.put(code,res) | ||
| 106 | finalResult=res | ||
| 107 | } else { | ||
| 108 | //println('''similar problem, answer from cache''') | ||
| 109 | finalResult=cachedResult | ||
| 110 | this.numberOfCachedSolverCalls++ | ||
| 112 | } | 111 | } |
| 112 | } else { | ||
| 113 | finalResult= t.delegateIsSatisfiable(propagatedConstraints) | ||
| 114 | this.numberOfSolverCalls++ | ||
| 113 | } | 115 | } |
| 114 | } | 116 | } |
| 115 | } else { | 117 | } |
| 116 | finalResult = true | ||
| 117 | } | ||
| 118 | this.runtime+=System.nanoTime-start | 118 | this.runtime+=System.nanoTime-start |
| 119 | return finalResult | 119 | return finalResult |
| 120 | } | 120 | } |