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 | 533 |
1 files changed, 0 insertions, 533 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 deleted file mode 100644 index a228afc6..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ /dev/null | |||
@@ -1,533 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver | ||
4 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDynamicProblemSolver | ||
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | ||
6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
20 | import java.util.HashMap | ||
21 | import java.util.LinkedHashMap | ||
22 | import java.util.LinkedHashSet | ||
23 | import java.util.List | ||
24 | import java.util.Map | ||
25 | import org.eclipse.emf.ecore.EObject | ||
26 | import org.eclipse.viatra.dse.base.ThreadContext | ||
27 | import org.eclipse.viatra.dse.objectives.Fitness | ||
28 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
29 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
30 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
31 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
32 | import org.eclipse.viatra.dse.objectives.IObjective | ||
33 | |||
34 | class NumericSolver { | ||
35 | val ModelGenerationMethod method | ||
36 | var ThreadContext threadContext | ||
37 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | ||
38 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | ||
39 | NumericTranslator t | ||
40 | |||
41 | val boolean intermediateConsistencyCheck | ||
42 | val boolean caching; | ||
43 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | ||
44 | val String drealLocalPath; | ||
45 | val ExplorationStrategy strategy; | ||
46 | |||
47 | var long runtime = 0 | ||
48 | var long cachingTime = 0 | ||
49 | var int numberOfSolverCalls = 0 | ||
50 | var int numberOfCachedSolverCalls = 0 | ||
51 | |||
52 | new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { | ||
53 | this.method = method | ||
54 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks | ||
55 | this.caching = caching | ||
56 | this.drealLocalPath = config.drealLocalPath | ||
57 | this.strategy = config.strategy | ||
58 | this.t = new NumericTranslator(createNumericTranslator(config), config.drealTimeout) | ||
59 | } | ||
60 | |||
61 | def createNumericTranslator(ViatraReasonerConfiguration config) { | ||
62 | val solverSelection = config.numericSolverSelection | ||
63 | val strategy = config.strategy | ||
64 | if (strategy == ExplorationStrategy.None) { | ||
65 | //initialise the specified | ||
66 | if (solverSelection == NumericSolverSelection.DREAL_DOCKER) | ||
67 | return new NumericDrealProblemSolver(true, null, config.drealTimeout) | ||
68 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) | ||
69 | return new NumericDrealProblemSolver(false, drealLocalPath, config.drealTimeout) | ||
70 | if (solverSelection == NumericSolverSelection.Z3) { | ||
71 | //TODO THIS IS HARD-CODED for now | ||
72 | // val root = "/data/viatra/VIATRA-Generator"; | ||
73 | val root = "/home/models/VIATRA-Generator"; | ||
74 | //END HARD-CODED | ||
75 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | ||
76 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | ||
77 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | ||
78 | // System.load("libz3.so"); | ||
79 | // System.load("libz3java.so"); | ||
80 | return new NumericZ3ProblemSolver(config.drealTimeout) | ||
81 | } | ||
82 | } | ||
83 | else { | ||
84 | //initialise both dreal-local and z3 | ||
85 | |||
86 | //TODO THIS IS HARD-CODED for now | ||
87 | // val root = "/data/viatra/VIATRA-Generator"; | ||
88 | val root = "/home/models/VIATRA-Generator"; | ||
89 | //END HARD-CODED | ||
90 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | ||
91 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | ||
92 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | ||
93 | return new NumericDynamicProblemSolver(drealLocalPath, config.drealTimeout) | ||
94 | } | ||
95 | } | ||
96 | |||
97 | def init(ThreadContext context) { | ||
98 | // This makes the NumericSolver single-threaded, | ||
99 | // but that's not a problem, because we only use the solver on a single thread anyways. | ||
100 | this.threadContext = context | ||
101 | val engine = threadContext.queryEngine | ||
102 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { | ||
103 | val constraint = entry.key | ||
104 | val querySpec = entry.value | ||
105 | val matcher = querySpec.getMatcher(engine); | ||
106 | constraint2MustUnitPropagationPrecondition.put(constraint,matcher) | ||
107 | } | ||
108 | for(entry : method.currentUnitPropagationPreconditions.entrySet) { | ||
109 | val constraint = entry.key | ||
110 | val querySpec = entry.value | ||
111 | val matcher = querySpec.getMatcher(engine); | ||
112 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) | ||
113 | } | ||
114 | } | ||
115 | |||
116 | def getRuntime(){runtime} | ||
117 | def getCachingTime(){cachingTime} | ||
118 | def getNumberOfSolverCalls(){numberOfSolverCalls} | ||
119 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} | ||
120 | def getSolverFormingProblem(){this.t.formingProblemTime} | ||
121 | def getSolverSolvingProblem(){this.t.solvingProblemTime} | ||
122 | def getSolverSolution(){this.t.formingSolutionTime} | ||
123 | def getNumericSolverSelection(){this.t.numericSolver} | ||
124 | |||
125 | def boolean maySatisfiable() { | ||
126 | val int phase = determinePhase() | ||
127 | |||
128 | if(intermediateConsistencyCheck) { | ||
129 | return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase) | ||
130 | } else { | ||
131 | return true | ||
132 | } | ||
133 | } | ||
134 | def boolean currentSatisfiable() { | ||
135 | val int phase = determinePhase() | ||
136 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) | ||
137 | } | ||
138 | |||
139 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches, int phase) { | ||
140 | val start = System.nanoTime | ||
141 | var boolean finalResult | ||
142 | val boolean needsFilling = needsFilling | ||
143 | val model = threadContext.getModel as PartialInterpretation | ||
144 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | ||
145 | |||
146 | if(matches.empty){ | ||
147 | finalResult=true | ||
148 | } else { | ||
149 | val propagatedConstraints = new HashMap | ||
150 | //Filter constraints if there are phase-related restricutions | ||
151 | //null whitelist means accept everything | ||
152 | |||
153 | // println("<<<<START-STEP>>>> (" + phase + ")") | ||
154 | if (phase == -2) { | ||
155 | // println("Skipping numeric check") | ||
156 | //TODO Big assumption | ||
157 | return true | ||
158 | } | ||
159 | val whitelist = getConstraintWhitelist(phase) | ||
160 | for(entry : matches.entrySet) { | ||
161 | if (entry.value !== null){ | ||
162 | val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName | ||
163 | if (whitelist === null || whitelist.contains(name)) { | ||
164 | // println(name) | ||
165 | val constraint = entry.key | ||
166 | // println("--match?-- " + constraint) | ||
167 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
168 | // println("---------- " + entry.value.allMatches) | ||
169 | propagatedConstraints.put(constraint,allMatches) | ||
170 | } | ||
171 | } | ||
172 | } | ||
173 | //check numeric problem | ||
174 | if(propagatedConstraints.values.forall[empty]) { | ||
175 | finalResult=true | ||
176 | } else { | ||
177 | if(caching) { | ||
178 | val code = getCode(propagatedConstraints) | ||
179 | val cachedResult = satisfiabilityCache.get(code) | ||
180 | if(cachedResult === null) { | ||
181 | // println('''new problem, call solver''') | ||
182 | // for(entry : code.entrySet) { | ||
183 | // println('''«entry.key» -> «entry.value»''') | ||
184 | // } | ||
185 | //println(code.hashCode) | ||
186 | this.numberOfSolverCalls++ | ||
187 | var boolean res = false | ||
188 | if (needsFilling){ | ||
189 | //TODO ASSUME Always True | ||
190 | //GET LIST OF VARS TO FILL | ||
191 | val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) | ||
192 | if (fillMap === null) res = false | ||
193 | else { | ||
194 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | ||
195 | res = true | ||
196 | } | ||
197 | } else { | ||
198 | res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) | ||
199 | } | ||
200 | //TODO FIX CACHING | ||
201 | satisfiabilityCache.put(code,res) | ||
202 | finalResult=res | ||
203 | } else { | ||
204 | //println('''similar problem, answer from cache''') | ||
205 | println('''potential issue, answer from cache''') | ||
206 | finalResult=cachedResult | ||
207 | this.numberOfCachedSolverCalls++ | ||
208 | } | ||
209 | } else { | ||
210 | if (needsFilling){ | ||
211 | //GET LIST OF VARS TO FILL | ||
212 | val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) | ||
213 | if (fillMap === null) finalResult = false | ||
214 | else { | ||
215 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | ||
216 | finalResult = true | ||
217 | } | ||
218 | } else { | ||
219 | finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) | ||
220 | } | ||
221 | this.numberOfSolverCalls++ | ||
222 | } | ||
223 | } | ||
224 | } | ||
225 | this.runtime+=System.nanoTime-start | ||
226 | //STRATEGY | ||
227 | if (phase == 2) { | ||
228 | if (!finalResult) return finalResult | ||
229 | else { | ||
230 | finalResult = isSatisfiable(matches, 3) | ||
231 | } | ||
232 | } | ||
233 | return finalResult | ||
234 | } | ||
235 | |||
236 | def selectSolver(int phase) { | ||
237 | if (strategy === ExplorationStrategy.CrossingScenario){ | ||
238 | if (phase == 1) return "z3" | ||
239 | else return "dreal" | ||
240 | } | ||
241 | return "irrelevant" | ||
242 | } | ||
243 | |||
244 | def int determinePhase() { | ||
245 | // >= 0 : an actual phase | ||
246 | // -1 : take all numeric constraints | ||
247 | // -2 : SKIP (take no numeric constraints) | ||
248 | if (strategy == ExplorationStrategy.CrossingScenario) { | ||
249 | // //if has structural (non-WF) fitness issues, skip numeric handling | ||
250 | // val IObjective ob = threadContext.objectives.filter[it instanceof ModelGenerationCompositeObjective].get(0) | ||
251 | // val compo = ob as ModelGenerationCompositeObjective | ||
252 | // if (compo.getNonWFFitness(threadContext) > 0) { | ||
253 | // println("bootleg numeric-skip") | ||
254 | // return -2; | ||
255 | // } | ||
256 | |||
257 | //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors | ||
258 | val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; | ||
259 | val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation(); | ||
260 | var boolean foundBlockedBy = false; | ||
261 | |||
262 | var int numActors; | ||
263 | var int numPlacedOn; | ||
264 | var int numPlacements = 0; | ||
265 | |||
266 | for (PartialRelationInterpretation rel : relations) { | ||
267 | if(rel.getInterpretationOf().getName().equals("actors reference CrossingScenario")) { | ||
268 | numActors = rel.relationlinks.size | ||
269 | } | ||
270 | |||
271 | if(rel.getInterpretationOf().getName().equals("placedOn reference Actor")) { | ||
272 | numPlacedOn = rel.relationlinks.size | ||
273 | } | ||
274 | |||
275 | if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) { | ||
276 | for (RelationLink link : rel.getRelationlinks()) { | ||
277 | val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement; | ||
278 | if (param2.isValueSet()) { | ||
279 | numPlacements++ | ||
280 | } | ||
281 | } | ||
282 | } | ||
283 | |||
284 | if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { | ||
285 | if (!rel.getRelationlinks().isEmpty()) { | ||
286 | foundBlockedBy = true | ||
287 | } | ||
288 | } | ||
289 | } | ||
290 | val boolean unplacedActorExists = numPlacements < numActors | ||
291 | //it means that there is no blockedBy | ||
292 | //so we are at most at phase 2 | ||
293 | if (numPlacedOn == 1 && numPlacements == 0) return 1 | ||
294 | if (foundBlockedBy && unplacedActorExists) return 2 | ||
295 | if (numPlacements == numActors) return 3; | ||
296 | return -2; | ||
297 | } | ||
298 | return -1; | ||
299 | } | ||
300 | |||
301 | def getConstraintWhitelist(int phase) { | ||
302 | val List<String> wl = newArrayList | ||
303 | //null return means accept everything | ||
304 | if (strategy === ExplorationStrategy.None){ | ||
305 | return null | ||
306 | } else if (strategy === ExplorationStrategy.CrossingScenario){ | ||
307 | /* | ||
308 | "define_placedOn_actorOnVerticalLane", | ||
309 | "define_placedOn_actorOnHorizLane", | ||
310 | |||
311 | "define_actor_maxXp", | ||
312 | "define_actor_minXp", | ||
313 | "define_actor_maxYp", | ||
314 | "define_actor_minYp", | ||
315 | |||
316 | "define_actor_wrtLane", | ||
317 | |||
318 | "define_actor_minimumDistance", | ||
319 | |||
320 | "define_actor_actorOnVertLaneHasxSpeed0", | ||
321 | "define_actor_actorOnVertLaneMinYs", | ||
322 | "define_actor_actorOnVertLaneMaxYs", | ||
323 | "define_actor_actorOnHorizLaneHasySpeed0", | ||
324 | "define_actor_actorOnHorizLaneMinXs", | ||
325 | "define_actor_actorOnHorizLaneMaxXs", | ||
326 | |||
327 | "define_actor_pedestrianWidth", | ||
328 | "define_actor_pedestrianLength", | ||
329 | "define_actor_vehicleWidth", | ||
330 | "define_actor_vehicleWidth", | ||
331 | "define_actor_vehicleLength", | ||
332 | "define_actor_vehicleLength", | ||
333 | |||
334 | "collisionExists_timeWithinBound", | ||
335 | "collisionExists_timeNotNegative", | ||
336 | "collisionExists_defineCollision_y1", | ||
337 | "collisionExists_defineCollision_y2", | ||
338 | "collisionExists_defineCollision_x1", | ||
339 | "collisionExists_defineCollision_x2", | ||
340 | |||
341 | "visionBlocked_ites_notOnSameVertLine", | ||
342 | "visionBlocked_ites_top", | ||
343 | "visionBlocked_ites_bottom", | ||
344 | "visionBlocked_xdistBSlargerThanxdistTS", | ||
345 | "visionBlocked_xdistBTlargerThanxdistST", | ||
346 | "visionBlocked_ydistBSlargerThanydistTS", | ||
347 | "visionBlocked_ydistBTlargerThanydistST" | ||
348 | */ | ||
349 | |||
350 | //HINTS: | ||
351 | //define_actor_wrtLane | ||
352 | //28.5 is structural hint | ||
353 | switch (phase) { | ||
354 | case 1: { | ||
355 | wl.addAll(#[ | ||
356 | "define_placedOn_actorOnVerticalLane", | ||
357 | "define_placedOn_actorOnHorizLane", | ||
358 | |||
359 | "define_actor_maxXp", | ||
360 | "define_actor_minXp", | ||
361 | "define_actor_maxYp", | ||
362 | "define_actor_minYp", | ||
363 | |||
364 | "define_actor_pedestrianWidth", | ||
365 | "define_actor_pedestrianLength", | ||
366 | "define_actor_vehicleWidth", | ||
367 | "define_actor_vehicleWidth", | ||
368 | "define_actor_vehicleLength", | ||
369 | "define_actor_vehicleLength" | ||
370 | |||
371 | ]) | ||
372 | } | ||
373 | case 2: { | ||
374 | wl.addAll(#[ | ||
375 | |||
376 | "define_placedOn_actorOnVerticalLane", | ||
377 | "define_placedOn_actorOnHorizLane", | ||
378 | |||
379 | "define_actor_maxXp", | ||
380 | "define_actor_minXp", | ||
381 | "define_actor_maxYp", | ||
382 | "define_actor_minYp", | ||
383 | |||
384 | "define_actor_minimumDistance", | ||
385 | |||
386 | "define_actor_pedestrianWidth", | ||
387 | "define_actor_pedestrianLength", | ||
388 | "define_actor_vehicleWidth", | ||
389 | "define_actor_vehicleWidth", | ||
390 | "define_actor_vehicleLength", | ||
391 | "define_actor_vehicleLength", | ||
392 | |||
393 | "visionBlocked_ites_notOnSameVertLine", | ||
394 | "visionBlocked_ites_top", | ||
395 | "visionBlocked_ites_bottom", | ||
396 | "visionBlocked_xdistBSlargerThanxdistTS", | ||
397 | "visionBlocked_xdistBTlargerThanxdistST", | ||
398 | "visionBlocked_ydistBSlargerThanydistTS", | ||
399 | "visionBlocked_ydistBTlargerThanydistST" | ||
400 | ]) | ||
401 | } | ||
402 | case 3: { | ||
403 | wl.addAll(#[ | ||
404 | |||
405 | "define_placedOn_actorOnVerticalLane", | ||
406 | "define_placedOn_actorOnHorizLane", | ||
407 | |||
408 | "define_actor_maxXp", | ||
409 | "define_actor_minXp", | ||
410 | "define_actor_maxYp", | ||
411 | "define_actor_minYp", | ||
412 | |||
413 | "define_actor_minimumDistance", | ||
414 | |||
415 | "define_actor_actorOnVertLaneHasxSpeed0", | ||
416 | "define_actor_actorOnVertLaneMinYs", | ||
417 | "define_actor_actorOnVertLaneMaxYs", | ||
418 | "define_actor_actorOnHorizLaneHasySpeed0", | ||
419 | "define_actor_actorOnHorizLaneMinXs", | ||
420 | "define_actor_actorOnHorizLaneMaxXs", | ||
421 | |||
422 | "define_actor_pedestrianWidth", | ||
423 | "define_actor_pedestrianLength", | ||
424 | "define_actor_vehicleWidth", | ||
425 | "define_actor_vehicleWidth", | ||
426 | "define_actor_vehicleLength", | ||
427 | "define_actor_vehicleLength", | ||
428 | |||
429 | "collisionExists_timeWithinBound", | ||
430 | "collisionExists_timeNotNegative", | ||
431 | "collisionExists_defineCollision_y1", | ||
432 | "collisionExists_defineCollision_y2", | ||
433 | "collisionExists_defineCollision_x1", | ||
434 | "collisionExists_defineCollision_x2" | ||
435 | ]) | ||
436 | } | ||
437 | default: { | ||
438 | //this is for 3 if we implement 4 | ||
439 | // bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7]) | ||
440 | |||
441 | //this is for 4 if we do it | ||
442 | wl.addAll(#[]) | ||
443 | return null | ||
444 | } | ||
445 | } | ||
446 | } | ||
447 | return wl | ||
448 | } | ||
449 | |||
450 | def getNeedsFilling(){ | ||
451 | if (strategy == ExplorationStrategy.CrossingScenario) return true | ||
452 | return false | ||
453 | } | ||
454 | |||
455 | def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) { | ||
456 | val start = System.nanoTime | ||
457 | val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList | ||
458 | val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) | ||
459 | this.cachingTime += System.nanoTime-start | ||
460 | return res | ||
461 | } | ||
462 | |||
463 | def fillSolutionCopy(Map<EObject, EObject> trace) { | ||
464 | //No need to do a final check to fill if we are using a strategy | ||
465 | if (strategy === ExplorationStrategy.CrossingScenario) return | ||
466 | val model = threadContext.getModel as PartialInterpretation | ||
467 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | ||
468 | if(constraint2CurrentUnitPropagationPrecondition.empty) { | ||
469 | fillWithDefaultValues(dataObjects,trace) | ||
470 | } else { | ||
471 | val propagatedConstraints = new HashMap | ||
472 | for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { | ||
473 | val constraint = entry.key | ||
474 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
475 | propagatedConstraints.put(constraint,allMatches) | ||
476 | } | ||
477 | |||
478 | if(propagatedConstraints.values.forall[empty]) { | ||
479 | fillWithDefaultValues(dataObjects,trace) | ||
480 | } else { | ||
481 | val solution = t.delegateGetSolution(dataObjects,propagatedConstraints, "dreal") | ||
482 | fillWithSolutions(dataObjects,solution,trace) | ||
483 | } | ||
484 | } | ||
485 | } | ||
486 | |||
487 | def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) { | ||
488 | for(element : elements) { | ||
489 | if(element.valueSet==false) { | ||
490 | val value = getDefaultValue(element) | ||
491 | val target = trace.get(element) as PrimitiveElement | ||
492 | target.fillWithValue(value) | ||
493 | } | ||
494 | } | ||
495 | } | ||
496 | |||
497 | def protected dispatch getDefaultValue(BooleanElement e) {false} | ||
498 | def protected dispatch getDefaultValue(IntegerElement e) {0} | ||
499 | def protected dispatch getDefaultValue(RealElement e) {0.0} | ||
500 | def protected dispatch getDefaultValue(StringElement e) {""} | ||
501 | |||
502 | def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) { | ||
503 | for(element : elements) { | ||
504 | if(element.valueSet==false) { | ||
505 | if(solution.containsKey(element)) { | ||
506 | val value = solution.get(element) | ||
507 | val target = trace.get(element) as PrimitiveElement | ||
508 | target.fillWithValue(value) | ||
509 | } else { | ||
510 | val target = trace.get(element) as PrimitiveElement | ||
511 | target.fillWithValue(target.defaultValue) | ||
512 | } | ||
513 | } | ||
514 | } | ||
515 | } | ||
516 | |||
517 | def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean} | ||
518 | def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} | ||
519 | def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double } | ||
520 | def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} | ||
521 | |||
522 | def protected fillWithPartialSolutionsDirectly(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution) { | ||
523 | for(element : elements) { | ||
524 | //we allow overwriting of already set variables | ||
525 | if(solution.containsKey(element)) { | ||
526 | val value = solution.get(element) | ||
527 | if (value !== null){ | ||
528 | element.fillWithValue(value) | ||
529 | } | ||
530 | } | ||
531 | } | ||
532 | } | ||
533 | } \ No newline at end of file | ||