diff options
author | 2021-02-14 08:01:00 +0100 | |
---|---|---|
committer | 2021-02-14 08:01:00 +0100 | |
commit | a8eb346fb97b54b6ee693da4840abd8be8b43843 (patch) | |
tree | 7f63b8432cd50150bff6509e3ff985a40b8763fb /Solvers/VIATRA-Solver | |
parent | add cs scalability case study artifacts (diff) | |
download | VIATRA-Generator-a8eb346fb97b54b6ee693da4840abd8be8b43843.tar.gz VIATRA-Generator-a8eb346fb97b54b6ee693da4840abd8be8b43843.tar.zst VIATRA-Generator-a8eb346fb97b54b6ee693da4840abd8be8b43843.zip |
Add strategy flag + implement alost working crossingScenarioStrategy
Diffstat (limited to 'Solvers/VIATRA-Solver')
3 files changed, 318 insertions, 23 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend index 338a9af2..0c9612e8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend | |||
@@ -11,6 +11,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction | |||
11 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 11 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
12 | 12 | ||
13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
14 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
14 | 15 | ||
15 | class RelationDefinitionIndexer { | 16 | class RelationDefinitionIndexer { |
16 | public val PatternGenerator base; | 17 | public val PatternGenerator base; |
@@ -70,6 +71,19 @@ class RelationDefinitionIndexer { | |||
70 | private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) { | 71 | private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) { |
71 | try { | 72 | try { |
72 | val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies | 73 | val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies |
74 | |||
75 | //TODO ISSUE if a structural and numeric constraint are ORed in the same pattern | ||
76 | var boolean isCheck = false | ||
77 | for (body : bodies) { | ||
78 | for (constraint : body.constraints) { | ||
79 | if (constraint instanceof ExpressionEvaluation) { | ||
80 | // below not working | ||
81 | // return "" | ||
82 | isCheck = true | ||
83 | } | ||
84 | } | ||
85 | } | ||
86 | |||
73 | return ''' | 87 | return ''' |
74 | private pattern «relationDefinitionName(relation,modality)»( | 88 | private pattern «relationDefinitionName(relation,modality)»( |
75 | problem:LogicProblem, interpretation:PartialInterpretation, | 89 | problem:LogicProblem, interpretation:PartialInterpretation, |
@@ -79,6 +93,7 @@ class RelationDefinitionIndexer { | |||
79 | «FOR constraint : body.constraints» | 93 | «FOR constraint : body.constraints» |
80 | «this.constraintTransformer.transformConstraint(constraint,modality,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | 94 | «this.constraintTransformer.transformConstraint(constraint,modality,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
81 | «ENDFOR» | 95 | «ENDFOR» |
96 | «IF isCheck»1 == 0;«ENDIF» | ||
82 | }«ENDFOR» | 97 | }«ENDFOR» |
83 | ''' | 98 | ''' |
84 | } catch(UnsupportedOperationException e) { | 99 | } catch(UnsupportedOperationException e) { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index 61a2ac41..74388706 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend | |||
@@ -40,6 +40,12 @@ enum NumericSolverSelection { | |||
40 | Z3 | 40 | Z3 |
41 | } | 41 | } |
42 | 42 | ||
43 | enum ExplorationStrategy { | ||
44 | None, | ||
45 | CrossingScenario, | ||
46 | CSHacker | ||
47 | } | ||
48 | |||
43 | class ViatraReasonerConfiguration extends LogicSolverConfiguration { | 49 | class ViatraReasonerConfiguration extends LogicSolverConfiguration { |
44 | // public var Iterable<PQuery> existingQueries | 50 | // public var Iterable<PQuery> existingQueries |
45 | public var nameNewElements = false | 51 | public var nameNewElements = false |
@@ -80,6 +86,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
80 | public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3 | 86 | public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3 |
81 | public var drealLocalPath = "<path-to-dreal>"; | 87 | public var drealLocalPath = "<path-to-dreal>"; |
82 | public var Map<String, Map<String, String>> ignoredAttributesMap = null; | 88 | public var Map<String, Map<String, String>> ignoredAttributesMap = null; |
89 | public var ExplorationStrategy strategy = ExplorationStrategy.None | ||
83 | 90 | ||
84 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( | 91 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( |
85 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) | 92 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) |
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 b8ea25e5..b8fcb6a0 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,14 +1,19 @@ | |||
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.NumericDrealProblemSolver | 3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver |
4 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDynamicProblemSolver | ||
4 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | 5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator |
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver | 6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement |
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration |
@@ -22,6 +27,7 @@ import org.eclipse.viatra.dse.base.ThreadContext | |||
22 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 27 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
23 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 28 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | 29 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint |
30 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
25 | 31 | ||
26 | class NumericSolver { | 32 | class NumericSolver { |
27 | val ModelGenerationMethod method | 33 | val ModelGenerationMethod method |
@@ -34,6 +40,7 @@ class NumericSolver { | |||
34 | val boolean caching; | 40 | val boolean caching; |
35 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | 41 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap |
36 | val String drealLocalPath; | 42 | val String drealLocalPath; |
43 | val ExplorationStrategy strategy; | ||
37 | 44 | ||
38 | var long runtime = 0 | 45 | var long runtime = 0 |
39 | var long cachingTime = 0 | 46 | var long cachingTime = 0 |
@@ -45,24 +52,43 @@ class NumericSolver { | |||
45 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks | 52 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks |
46 | this.caching = caching | 53 | this.caching = caching |
47 | this.drealLocalPath = config.drealLocalPath | 54 | this.drealLocalPath = config.drealLocalPath |
48 | this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) | 55 | this.strategy = config.strategy |
56 | this.t = new NumericTranslator(createNumericTranslator(config)) | ||
49 | } | 57 | } |
50 | 58 | ||
51 | def createNumericTranslator(NumericSolverSelection solverSelection) { | 59 | def createNumericTranslator(ViatraReasonerConfiguration config) { |
52 | if (solverSelection == NumericSolverSelection.DREAL_DOCKER) | 60 | val solverSelection = config.numericSolverSelection |
53 | return new NumericDrealProblemSolver(true, null) | 61 | val strategy = config.strategy |
54 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) | 62 | if (strategy == ExplorationStrategy.None) { |
55 | return new NumericDrealProblemSolver(false, drealLocalPath) | 63 | //initialise the specified |
56 | if (solverSelection == NumericSolverSelection.Z3) { | 64 | if (solverSelection == NumericSolverSelection.DREAL_DOCKER) |
65 | return new NumericDrealProblemSolver(true, null) | ||
66 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) | ||
67 | return new NumericDrealProblemSolver(false, drealLocalPath) | ||
68 | if (solverSelection == NumericSolverSelection.Z3) { | ||
69 | //TODO THIS IS HARD-CODED for now | ||
70 | // val root = "/data/viatra/VIATRA-Generator"; | ||
71 | val root = "/home/models/VIATRA-Generator"; | ||
72 | //END HARD-CODED | ||
73 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | ||
74 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | ||
75 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | ||
76 | // System.load("libz3.so"); | ||
77 | // System.load("libz3java.so"); | ||
78 | return new NumericZ3ProblemSolver | ||
79 | } | ||
80 | } | ||
81 | else { | ||
82 | //initialise both dreal-local and z3 | ||
83 | |||
57 | //TODO THIS IS HARD-CODED for now | 84 | //TODO THIS IS HARD-CODED for now |
58 | val root = "/data/viatra/VIATRA-Generator"; | 85 | // val root = "/data/viatra/VIATRA-Generator"; |
86 | val root = "/home/models/VIATRA-Generator"; | ||
59 | //END HARD-CODED | 87 | //END HARD-CODED |
60 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | 88 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); |
61 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | 89 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); |
62 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | 90 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); |
63 | // System.load("libz3.so"); | 91 | return new NumericDynamicProblemSolver(drealLocalPath) |
64 | // System.load("libz3java.so"); | ||
65 | return new NumericZ3ProblemSolver | ||
66 | } | 92 | } |
67 | } | 93 | } |
68 | 94 | ||
@@ -95,31 +121,49 @@ class NumericSolver { | |||
95 | def getNumericSolverSelection(){this.t.numericSolver} | 121 | def getNumericSolverSelection(){this.t.numericSolver} |
96 | 122 | ||
97 | def boolean maySatisfiable() { | 123 | def boolean maySatisfiable() { |
124 | val int phase = determinePhase() | ||
125 | |||
98 | if(intermediateConsistencyCheck) { | 126 | if(intermediateConsistencyCheck) { |
99 | return isSatisfiable(this.constraint2MustUnitPropagationPrecondition) | 127 | return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase) |
100 | } else { | 128 | } else { |
101 | return true | 129 | return true |
102 | } | 130 | } |
103 | } | 131 | } |
104 | def boolean currentSatisfiable() { | 132 | def boolean currentSatisfiable() { |
105 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition) | 133 | val int phase = determinePhase() |
134 | //TODO generalize this | ||
135 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) | ||
106 | } | 136 | } |
107 | 137 | ||
108 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { | 138 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches, int phase) { |
109 | val start = System.nanoTime | 139 | val start = System.nanoTime |
110 | var boolean finalResult | 140 | var boolean finalResult |
141 | val boolean needsFilling = needsFilling | ||
142 | val model = threadContext.getModel as PartialInterpretation | ||
143 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | ||
144 | |||
111 | if(matches.empty){ | 145 | if(matches.empty){ |
112 | finalResult=true | 146 | finalResult=true |
113 | } else { | 147 | } else { |
114 | val propagatedConstraints = new HashMap | 148 | val propagatedConstraints = new HashMap |
115 | // println("<<<<START-STEP>>>>") | 149 | //Filter constraints if there are phase-related restricutions |
150 | //null whitelist means accept everything | ||
151 | val whitelist = getConstraintWhitelist(phase) | ||
152 | println("<<<<START-STEP>>>> (" + phase + ")") | ||
116 | for(entry : matches.entrySet) { | 153 | for(entry : matches.entrySet) { |
117 | val constraint = entry.key | 154 | if (entry.value !== null){ |
118 | // println("--match?-- " + constraint) | 155 | val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName |
119 | val allMatches = entry.value.allMatches.map[it.toArray] | 156 | if (whitelist === null || whitelist.contains(name)) { |
120 | // println("---------- " + entry.value.allMatches) | 157 | // println(name) |
121 | propagatedConstraints.put(constraint,allMatches) | 158 | val constraint = entry.key |
159 | // println("--match?-- " + constraint) | ||
160 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
161 | // println("---------- " + entry.value.allMatches) | ||
162 | propagatedConstraints.put(constraint,allMatches) | ||
163 | } | ||
164 | } | ||
122 | } | 165 | } |
166 | //check numeric problem | ||
123 | if(propagatedConstraints.values.forall[empty]) { | 167 | if(propagatedConstraints.values.forall[empty]) { |
124 | finalResult=true | 168 | finalResult=true |
125 | } else { | 169 | } else { |
@@ -133,16 +177,35 @@ class NumericSolver { | |||
133 | // } | 177 | // } |
134 | //println(code.hashCode) | 178 | //println(code.hashCode) |
135 | this.numberOfSolverCalls++ | 179 | this.numberOfSolverCalls++ |
136 | val res = t.delegateIsSatisfiable(propagatedConstraints) | 180 | var boolean res = false |
181 | if (needsFilling){ | ||
182 | //TODO ASSUME Always True | ||
183 | //GET LIST OF VARS TO FILL | ||
184 | val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) | ||
185 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | ||
186 | res = true | ||
187 | } else { | ||
188 | res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) | ||
189 | } | ||
190 | //TODO FIX CACHING | ||
137 | satisfiabilityCache.put(code,res) | 191 | satisfiabilityCache.put(code,res) |
138 | finalResult=res | 192 | finalResult=res |
139 | } else { | 193 | } else { |
140 | //println('''similar problem, answer from cache''') | 194 | //println('''similar problem, answer from cache''') |
195 | println('''potential issue, answer from cache''') | ||
141 | finalResult=cachedResult | 196 | finalResult=cachedResult |
142 | this.numberOfCachedSolverCalls++ | 197 | this.numberOfCachedSolverCalls++ |
143 | } | 198 | } |
144 | } else { | 199 | } else { |
145 | finalResult= t.delegateIsSatisfiable(propagatedConstraints) | 200 | if (needsFilling){ |
201 | //TODO ASSUME Always True | ||
202 | //GET LIST OF VARS TO FILL | ||
203 | val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) | ||
204 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | ||
205 | finalResult = true | ||
206 | } else { | ||
207 | finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) | ||
208 | } | ||
146 | this.numberOfSolverCalls++ | 209 | this.numberOfSolverCalls++ |
147 | } | 210 | } |
148 | } | 211 | } |
@@ -151,6 +214,201 @@ class NumericSolver { | |||
151 | return finalResult | 214 | return finalResult |
152 | } | 215 | } |
153 | 216 | ||
217 | def selectSolver(int phase) { | ||
218 | if (strategy === ExplorationStrategy.CrossingScenario){ | ||
219 | if (phase == 1) return "dreal" | ||
220 | else return "dreal" | ||
221 | } | ||
222 | return "irrelevant" | ||
223 | } | ||
224 | |||
225 | def int determinePhase() { | ||
226 | // >= 0 : an actual phase | ||
227 | // -1 : take all numeric constraints | ||
228 | // -2 : SKIP (take no numeric constraints) | ||
229 | if (strategy == ExplorationStrategy.CrossingScenario) { | ||
230 | //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors | ||
231 | val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; | ||
232 | val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation(); | ||
233 | var boolean foundActorWithDefinedPos = false; | ||
234 | for (PartialRelationInterpretation rel : relations) { | ||
235 | if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) { | ||
236 | for (RelationLink link : rel.getRelationlinks()) { | ||
237 | val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement; | ||
238 | if (param2.isValueSet()) { | ||
239 | foundActorWithDefinedPos = true; | ||
240 | } | ||
241 | } | ||
242 | } | ||
243 | |||
244 | if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { | ||
245 | if (!rel.getRelationlinks().isEmpty()) { | ||
246 | return 3; | ||
247 | } | ||
248 | } | ||
249 | } | ||
250 | //it means that there is no blockedBy | ||
251 | //so we are at most at phase 2 | ||
252 | if (foundActorWithDefinedPos) return 2; | ||
253 | return 1; | ||
254 | } | ||
255 | return -1; | ||
256 | } | ||
257 | |||
258 | def getConstraintWhitelist(int phase) { | ||
259 | val List<String> wl = newArrayList | ||
260 | //null return means accept everything | ||
261 | if (strategy === ExplorationStrategy.None){ | ||
262 | return null | ||
263 | } else if (strategy === ExplorationStrategy.CrossingScenario){ | ||
264 | /* | ||
265 | "define_placedOn_actorOnVerticalLane", | ||
266 | "define_placedOn_actorOnHorizLane", | ||
267 | |||
268 | "define_actor_maxXp", | ||
269 | "define_actor_minXp", | ||
270 | "define_actor_maxYp", | ||
271 | "define_actor_minYp", | ||
272 | |||
273 | "define_actor_wrtLane", | ||
274 | |||
275 | "define_actor_minimumDistance", | ||
276 | |||
277 | "define_actor_actorOnVertLaneHasxSpeed0", | ||
278 | "define_actor_actorOnVertLaneMinYs", | ||
279 | "define_actor_actorOnVertLaneMaxYs", | ||
280 | "define_actor_actorOnHorizLaneHasySpeed0", | ||
281 | "define_actor_actorOnHorizLaneMinXs", | ||
282 | "define_actor_actorOnHorizLaneMaxXs", | ||
283 | |||
284 | "define_actor_pedestrianWidth", | ||
285 | "define_actor_pedestrianLength", | ||
286 | "define_actor_vehicleWidth", | ||
287 | "define_actor_vehicleWidth", | ||
288 | "define_actor_vehicleLength", | ||
289 | "define_actor_vehicleLength", | ||
290 | |||
291 | "collisionExists_timeWithinBound", | ||
292 | "collisionExists_timeNotNegative", | ||
293 | "collisionExists_defineCollision_y1", | ||
294 | "collisionExists_defineCollision_y2", | ||
295 | "collisionExists_defineCollision_x1", | ||
296 | "collisionExists_defineCollision_x2", | ||
297 | |||
298 | "visionBlocked_ites_notOnSameVertLine", | ||
299 | "visionBlocked_ites_top", | ||
300 | "visionBlocked_ites_bottom", | ||
301 | "visionBlocked_xdistBSlargerThanxdistTS", | ||
302 | "visionBlocked_xdistBTlargerThanxdistST", | ||
303 | "visionBlocked_ydistBSlargerThanydistTS", | ||
304 | "visionBlocked_ydistBTlargerThanydistST" | ||
305 | */ | ||
306 | |||
307 | //HINTS: | ||
308 | //define_actor_wrtLane | ||
309 | //28.5 is structural hint | ||
310 | switch (phase) { | ||
311 | case 1: { | ||
312 | wl.addAll(#[ | ||
313 | "define_placedOn_actorOnVerticalLane", | ||
314 | "define_placedOn_actorOnHorizLane", | ||
315 | |||
316 | "define_actor_maxXp", | ||
317 | "define_actor_minXp", | ||
318 | "define_actor_maxYp", | ||
319 | "define_actor_minYp", | ||
320 | |||
321 | "define_actor_pedestrianWidth", | ||
322 | "define_actor_pedestrianLength", | ||
323 | "define_actor_vehicleWidth", | ||
324 | "define_actor_vehicleWidth", | ||
325 | "define_actor_vehicleLength", | ||
326 | "define_actor_vehicleLength" | ||
327 | |||
328 | ]) | ||
329 | } | ||
330 | case 2: { | ||
331 | wl.addAll(#[ | ||
332 | |||
333 | "define_placedOn_actorOnVerticalLane", | ||
334 | "define_placedOn_actorOnHorizLane", | ||
335 | |||
336 | "define_actor_maxXp", | ||
337 | "define_actor_minXp", | ||
338 | "define_actor_maxYp", | ||
339 | "define_actor_minYp", | ||
340 | |||
341 | "define_actor_minimumDistance", | ||
342 | |||
343 | "define_actor_pedestrianWidth", | ||
344 | "define_actor_pedestrianLength", | ||
345 | "define_actor_vehicleWidth", | ||
346 | "define_actor_vehicleWidth", | ||
347 | "define_actor_vehicleLength", | ||
348 | "define_actor_vehicleLength", | ||
349 | |||
350 | "visionBlocked_ites_notOnSameVertLine", | ||
351 | "visionBlocked_ites_top", | ||
352 | "visionBlocked_ites_bottom", | ||
353 | "visionBlocked_xdistBSlargerThanxdistTS", | ||
354 | "visionBlocked_xdistBTlargerThanxdistST", | ||
355 | "visionBlocked_ydistBSlargerThanydistTS", | ||
356 | "visionBlocked_ydistBTlargerThanydistST" | ||
357 | ]) | ||
358 | } | ||
359 | case 3: { | ||
360 | wl.addAll(#[ | ||
361 | |||
362 | "define_placedOn_actorOnVerticalLane", | ||
363 | "define_placedOn_actorOnHorizLane", | ||
364 | |||
365 | "define_actor_maxXp", | ||
366 | "define_actor_minXp", | ||
367 | "define_actor_maxYp", | ||
368 | "define_actor_minYp", | ||
369 | |||
370 | "define_actor_minimumDistance", | ||
371 | |||
372 | "define_actor_actorOnVertLaneHasxSpeed0", | ||
373 | "define_actor_actorOnVertLaneMinYs", | ||
374 | "define_actor_actorOnVertLaneMaxYs", | ||
375 | "define_actor_actorOnHorizLaneHasySpeed0", | ||
376 | "define_actor_actorOnHorizLaneMinXs", | ||
377 | "define_actor_actorOnHorizLaneMaxXs", | ||
378 | |||
379 | "define_actor_pedestrianWidth", | ||
380 | "define_actor_pedestrianLength", | ||
381 | "define_actor_vehicleWidth", | ||
382 | "define_actor_vehicleWidth", | ||
383 | "define_actor_vehicleLength", | ||
384 | "define_actor_vehicleLength", | ||
385 | |||
386 | "collisionExists_timeWithinBound", | ||
387 | "collisionExists_timeNotNegative", | ||
388 | "collisionExists_defineCollision_y1", | ||
389 | "collisionExists_defineCollision_y2", | ||
390 | "collisionExists_defineCollision_x1", | ||
391 | "collisionExists_defineCollision_x2" | ||
392 | ]) | ||
393 | } | ||
394 | default: { | ||
395 | //this is for 3 if we implement 4 | ||
396 | // bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7]) | ||
397 | |||
398 | //this is for 4 if we do it | ||
399 | wl.addAll(#[]) | ||
400 | return null | ||
401 | } | ||
402 | } | ||
403 | } | ||
404 | return wl | ||
405 | } | ||
406 | |||
407 | def getNeedsFilling(){ | ||
408 | if (strategy == ExplorationStrategy.CrossingScenario) return true | ||
409 | return false | ||
410 | } | ||
411 | |||
154 | def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) { | 412 | def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) { |
155 | val start = System.nanoTime | 413 | val start = System.nanoTime |
156 | val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList | 414 | val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList |
@@ -175,7 +433,7 @@ class NumericSolver { | |||
175 | if(propagatedConstraints.values.forall[empty]) { | 433 | if(propagatedConstraints.values.forall[empty]) { |
176 | fillWithDefaultValues(dataObjects,trace) | 434 | fillWithDefaultValues(dataObjects,trace) |
177 | } else { | 435 | } else { |
178 | val solution = t.delegateGetSolution(dataObjects,propagatedConstraints) | 436 | val solution = t.delegateGetSolution(dataObjects,propagatedConstraints, "dreal") |
179 | fillWithSolutions(dataObjects,solution,trace) | 437 | fillWithSolutions(dataObjects,solution,trace) |
180 | } | 438 | } |
181 | } | 439 | } |
@@ -215,4 +473,19 @@ class NumericSolver { | |||
215 | def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} | 473 | def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} |
216 | def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double } | 474 | def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double } |
217 | def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} | 475 | def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} |
476 | |||
477 | def protected fillWithPartialSolutionsDirectly(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution) { | ||
478 | for(element : elements) { | ||
479 | //we allow overwriting of already set variables | ||
480 | if(solution.containsKey(element)) { | ||
481 | val value = solution.get(element) | ||
482 | if (value !== null){ | ||
483 | element.fillWithValue(value) | ||
484 | println("<" + element + "> is filled") | ||
485 | } else { | ||
486 | println("<" + element + "> is unfilled") | ||
487 | } | ||
488 | } | ||
489 | } | ||
490 | } | ||
218 | } \ No newline at end of file | 491 | } \ No newline at end of file |