diff options
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 | 63 |
1 files changed, 55 insertions, 8 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 e1745854..71793aa6 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 | |||
@@ -19,13 +19,23 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
20 | import java.util.List | 20 | import java.util.List |
21 | import java.math.BigDecimal | 21 | import java.math.BigDecimal |
22 | import java.util.LinkedHashSet | ||
23 | import java.util.LinkedHashMap | ||
22 | 24 | ||
23 | class NumericSolver { | 25 | class NumericSolver { |
24 | val ThreadContext threadContext; | 26 | val ThreadContext threadContext; |
25 | val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 27 | val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
26 | NumericTranslator t = new NumericTranslator | 28 | NumericTranslator t = new NumericTranslator |
27 | 29 | ||
28 | new(ThreadContext threadContext, ModelGenerationMethod method) { | 30 | val boolean caching; |
31 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | ||
32 | |||
33 | var long runtime = 0 | ||
34 | var long cachingTime = 0 | ||
35 | var int numberOfSolverCalls = 0 | ||
36 | var int numberOfCachedSolverCalls = 0 | ||
37 | |||
38 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { | ||
29 | this.threadContext = threadContext | 39 | this.threadContext = threadContext |
30 | val engine = threadContext.queryEngine | 40 | val engine = threadContext.queryEngine |
31 | for(entry : method.unitPropagationPreconditions.entrySet) { | 41 | for(entry : method.unitPropagationPreconditions.entrySet) { |
@@ -34,11 +44,20 @@ class NumericSolver { | |||
34 | val matcher = querySpec.getMatcher(engine); | 44 | val matcher = querySpec.getMatcher(engine); |
35 | constraint2UnitPropagationPrecondition.put(constraint,matcher) | 45 | constraint2UnitPropagationPrecondition.put(constraint,matcher) |
36 | } | 46 | } |
47 | this.caching = caching | ||
37 | } | 48 | } |
38 | 49 | ||
50 | def getRuntime(){runtime} | ||
51 | def getCachingTime(){cachingTime} | ||
52 | def getNumberOfSolverCalls(){numberOfSolverCalls} | ||
53 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} | ||
54 | |||
39 | def boolean isSatisfiable() { | 55 | def boolean isSatisfiable() { |
40 | if(constraint2UnitPropagationPrecondition.empty) return true | 56 | val start = System.nanoTime |
41 | else { | 57 | var boolean finalResult |
58 | if(constraint2UnitPropagationPrecondition.empty){ | ||
59 | finalResult=true | ||
60 | } else { | ||
42 | val propagatedConstraints = new HashMap | 61 | val propagatedConstraints = new HashMap |
43 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { | 62 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { |
44 | val constraint = entry.key | 63 | val constraint = entry.key |
@@ -47,15 +66,43 @@ class NumericSolver { | |||
47 | //println(allMatches.toList) | 66 | //println(allMatches.toList) |
48 | propagatedConstraints.put(constraint,allMatches) | 67 | propagatedConstraints.put(constraint,allMatches) |
49 | } | 68 | } |
50 | |||
51 | if(propagatedConstraints.values.forall[empty]) { | 69 | if(propagatedConstraints.values.forall[empty]) { |
52 | return true | 70 | finalResult=true |
53 | } else { | 71 | } else { |
54 | val res = t.delegateIsSatisfiable(propagatedConstraints) | 72 | if(caching) { |
55 | //println(res) | 73 | val code = getCode(propagatedConstraints) |
56 | return res | 74 | val cachedResult = satisfiabilityCache.get(code) |
75 | if(cachedResult === null) { | ||
76 | // println('''new problem, call solver''') | ||
77 | // for(entry : code.entrySet) { | ||
78 | // println('''«entry.key» -> «entry.value»''') | ||
79 | // } | ||
80 | //println(code.hashCode) | ||
81 | this.numberOfSolverCalls++ | ||
82 | val res = t.delegateIsSatisfiable(propagatedConstraints) | ||
83 | satisfiabilityCache.put(code,res) | ||
84 | finalResult=res | ||
85 | } else { | ||
86 | //println('''similar problem, answer from cache''') | ||
87 | finalResult=cachedResult | ||
88 | this.numberOfCachedSolverCalls++ | ||
89 | } | ||
90 | } else { | ||
91 | finalResult= t.delegateIsSatisfiable(propagatedConstraints) | ||
92 | this.numberOfSolverCalls++ | ||
93 | } | ||
57 | } | 94 | } |
58 | } | 95 | } |
96 | this.runtime+=System.nanoTime-start | ||
97 | return finalResult | ||
98 | } | ||
99 | |||
100 | def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) { | ||
101 | val start = System.nanoTime | ||
102 | val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList | ||
103 | val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) | ||
104 | this.cachingTime += System.nanoTime-start | ||
105 | return res | ||
59 | } | 106 | } |
60 | 107 | ||
61 | def fillSolutionCopy(Map<EObject, EObject> trace) { | 108 | def fillSolutionCopy(Map<EObject, EObject> trace) { |