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 | 58 |
1 files changed, 35 insertions, 23 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 71793aa6..fe378bd3 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 | |||
@@ -1,30 +1,29 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
5 | import java.util.HashMap | ||
6 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
7 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
9 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
10 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | 3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator |
11 | import org.eclipse.viatra.dse.base.ThreadContext | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod |
12 | import org.eclipse.emf.ecore.EObject | ||
13 | import java.util.Map | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement |
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
20 | import java.util.List | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement |
21 | import java.math.BigDecimal | 11 | import java.math.BigDecimal |
22 | import java.util.LinkedHashSet | 12 | import java.util.HashMap |
23 | import java.util.LinkedHashMap | 13 | import java.util.LinkedHashMap |
14 | import java.util.LinkedHashSet | ||
15 | import java.util.List | ||
16 | import java.util.Map | ||
17 | import org.eclipse.emf.ecore.EObject | ||
18 | import org.eclipse.viatra.dse.base.ThreadContext | ||
19 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
20 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
24 | 22 | ||
25 | class NumericSolver { | 23 | class NumericSolver { |
26 | val ThreadContext threadContext; | 24 | val ThreadContext threadContext; |
27 | val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 25 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
26 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | ||
28 | NumericTranslator t = new NumericTranslator | 27 | NumericTranslator t = new NumericTranslator |
29 | 28 | ||
30 | val boolean caching; | 29 | val boolean caching; |
@@ -38,11 +37,17 @@ class NumericSolver { | |||
38 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { | 37 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { |
39 | this.threadContext = threadContext | 38 | this.threadContext = threadContext |
40 | val engine = threadContext.queryEngine | 39 | val engine = threadContext.queryEngine |
41 | for(entry : method.unitPropagationPreconditions.entrySet) { | 40 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { |
41 | val constraint = entry.key | ||
42 | val querySpec = entry.value | ||
43 | val matcher = querySpec.getMatcher(engine); | ||
44 | constraint2MustUnitPropagationPrecondition.put(constraint,matcher) | ||
45 | } | ||
46 | for(entry : method.currentUnitPropagationPreconditions.entrySet) { | ||
42 | val constraint = entry.key | 47 | val constraint = entry.key |
43 | val querySpec = entry.value | 48 | val querySpec = entry.value |
44 | val matcher = querySpec.getMatcher(engine); | 49 | val matcher = querySpec.getMatcher(engine); |
45 | constraint2UnitPropagationPrecondition.put(constraint,matcher) | 50 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) |
46 | } | 51 | } |
47 | this.caching = caching | 52 | this.caching = caching |
48 | } | 53 | } |
@@ -52,14 +57,21 @@ class NumericSolver { | |||
52 | def getNumberOfSolverCalls(){numberOfSolverCalls} | 57 | def getNumberOfSolverCalls(){numberOfSolverCalls} |
53 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} | 58 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} |
54 | 59 | ||
55 | def boolean isSatisfiable() { | 60 | def boolean maySatisfiable() { |
61 | isSatisfiable(this.constraint2MustUnitPropagationPrecondition) | ||
62 | } | ||
63 | def boolean currentSatisfiable() { | ||
64 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition) | ||
65 | } | ||
66 | |||
67 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { | ||
56 | val start = System.nanoTime | 68 | val start = System.nanoTime |
57 | var boolean finalResult | 69 | var boolean finalResult |
58 | if(constraint2UnitPropagationPrecondition.empty){ | 70 | if(matches.empty){ |
59 | finalResult=true | 71 | finalResult=true |
60 | } else { | 72 | } else { |
61 | val propagatedConstraints = new HashMap | 73 | val propagatedConstraints = new HashMap |
62 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { | 74 | for(entry : matches.entrySet) { |
63 | val constraint = entry.key | 75 | val constraint = entry.key |
64 | //println(constraint) | 76 | //println(constraint) |
65 | val allMatches = entry.value.allMatches.map[it.toArray] | 77 | val allMatches = entry.value.allMatches.map[it.toArray] |
@@ -108,11 +120,11 @@ class NumericSolver { | |||
108 | def fillSolutionCopy(Map<EObject, EObject> trace) { | 120 | def fillSolutionCopy(Map<EObject, EObject> trace) { |
109 | val model = threadContext.getModel as PartialInterpretation | 121 | val model = threadContext.getModel as PartialInterpretation |
110 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | 122 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList |
111 | if(constraint2UnitPropagationPrecondition.empty) { | 123 | if(constraint2CurrentUnitPropagationPrecondition.empty) { |
112 | fillWithDefaultValues(dataObjects,trace) | 124 | fillWithDefaultValues(dataObjects,trace) |
113 | } else { | 125 | } else { |
114 | val propagatedConstraints = new HashMap | 126 | val propagatedConstraints = new HashMap |
115 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { | 127 | for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { |
116 | val constraint = entry.key | 128 | val constraint = entry.key |
117 | val allMatches = entry.value.allMatches.map[it.toArray] | 129 | val allMatches = entry.value.allMatches.map[it.toArray] |
118 | propagatedConstraints.put(constraint,allMatches) | 130 | propagatedConstraints.put(constraint,allMatches) |