diff options
| author |  Oszkar Semerath <semerath@mit.bme.hu> | 2020-05-14 22:55:31 +0200 |
|---|---|---|
| committer | Oszkar Semerath <semerath@mit.bme.hu> | 2020-05-14 22:55:31 +0200 |
| commit | 6d5b1d25c162f105a2ba1f5019574943d4a3c0e0 (patch) | |
| tree | d2a333650e454649501f4104690a026495a31a0a /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | |
| parent | Merge branch 'master' of https://github.com/viatra/VIATRA-Generator (diff) | |
| download | VIATRA-Generator-6d5b1d25c162f105a2ba1f5019574943d4a3c0e0.tar.gz VIATRA-Generator-6d5b1d25c162f105a2ba1f5019574943d4a3c0e0.tar.zst VIATRA-Generator-6d5b1d25c162f105a2ba1f5019574943d4a3c0e0.zip | |
fixes for the measurement
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend')
| -rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | 73 |
1 files changed, 40 insertions, 33 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 0fb5d702..a012f51b 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 | |||
| @@ -26,6 +26,7 @@ class NumericSolver { | |||
| 26 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 26 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
| 27 | NumericTranslator t = new NumericTranslator | 27 | NumericTranslator t = new NumericTranslator |
| 28 | 28 | ||
| 29 | val boolean intermediateConsistencyCheck | ||
| 29 | val boolean caching; | 30 | val boolean caching; |
| 30 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | 31 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap |
| 31 | 32 | ||
| @@ -34,7 +35,7 @@ class NumericSolver { | |||
| 34 | var int numberOfSolverCalls = 0 | 35 | var int numberOfSolverCalls = 0 |
| 35 | var int numberOfCachedSolverCalls = 0 | 36 | var int numberOfCachedSolverCalls = 0 |
| 36 | 37 | ||
| 37 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { | 38 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) { |
| 38 | this.threadContext = threadContext | 39 | this.threadContext = threadContext |
| 39 | val engine = threadContext.queryEngine | 40 | val engine = threadContext.queryEngine |
| 40 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { | 41 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { |
| @@ -49,6 +50,8 @@ class NumericSolver { | |||
| 49 | val matcher = querySpec.getMatcher(engine); | 50 | val matcher = querySpec.getMatcher(engine); |
| 50 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) | 51 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) |
| 51 | } | 52 | } |
| 53 | this.intermediateConsistencyCheck = true | ||
| 54 | println() | ||
| 52 | this.caching = caching | 55 | this.caching = caching |
| 53 | } | 56 | } |
| 54 | 57 | ||
| @@ -70,44 +73,48 @@ class NumericSolver { | |||
| 70 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { | 73 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { |
| 71 | val start = System.nanoTime | 74 | val start = System.nanoTime |
| 72 | var boolean finalResult | 75 | var boolean finalResult |
| 73 | if(matches.empty){ | 76 | if(intermediateConsistencyCheck) { |
| 74 | finalResult=true | 77 | if(matches.empty){ |
| 75 | } else { | ||
| 76 | val propagatedConstraints = new HashMap | ||
| 77 | for(entry : matches.entrySet) { | ||
| 78 | val constraint = entry.key | ||
| 79 | //println(constraint) | ||
| 80 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
| 81 | //println(allMatches.toList) | ||
| 82 | propagatedConstraints.put(constraint,allMatches) | ||
| 83 | } | ||
| 84 | if(propagatedConstraints.values.forall[empty]) { | ||
| 85 | finalResult=true | 78 | finalResult=true |
| 86 | } else { | 79 | } else { |
| 87 | if(caching) { | 80 | val propagatedConstraints = new HashMap |
| 88 | val code = getCode(propagatedConstraints) | 81 | for(entry : matches.entrySet) { |
| 89 | val cachedResult = satisfiabilityCache.get(code) | 82 | val constraint = entry.key |
| 90 | if(cachedResult === null) { | 83 | //println(constraint) |
| 91 | // println('''new problem, call solver''') | 84 | val allMatches = entry.value.allMatches.map[it.toArray] |
| 92 | // for(entry : code.entrySet) { | 85 | //println(allMatches.toList) |
| 93 | // println('''«entry.key» -> «entry.value»''') | 86 | propagatedConstraints.put(constraint,allMatches) |
| 94 | // } | 87 | } |
| 95 | //println(code.hashCode) | 88 | if(propagatedConstraints.values.forall[empty]) { |
| 96 | this.numberOfSolverCalls++ | 89 | finalResult=true |
| 97 | val res = t.delegateIsSatisfiable(propagatedConstraints) | 90 | } else { |
| 98 | satisfiabilityCache.put(code,res) | 91 | if(caching) { |
| 99 | finalResult=res | 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 | } | ||
| 100 | } else { | 109 | } else { |
| 101 | //println('''similar problem, answer from cache''') | 110 | finalResult= t.delegateIsSatisfiable(propagatedConstraints) |
| 102 | finalResult=cachedResult | 111 | this.numberOfSolverCalls++ |
| 103 | this.numberOfCachedSolverCalls++ | ||
| 104 | } | 112 | } |
| 105 | } else { | ||
| 106 | finalResult= t.delegateIsSatisfiable(propagatedConstraints) | ||
| 107 | this.numberOfSolverCalls++ | ||
| 108 | } | 113 | } |
| 109 | } | 114 | } |
| 110 | } | 115 | } else { |
| 116 | finalResult = true | ||
| 117 | } | ||
| 111 | this.runtime+=System.nanoTime-start | 118 | this.runtime+=System.nanoTime-start |
| 112 | return finalResult | 119 | return finalResult |
| 113 | } | 120 | } |