diff options
author | 20001LastOrder <boqi.chen@mail.mcgill.ca> | 2020-11-04 01:16:22 -0500 |
---|---|---|
committer | 20001LastOrder <boqi.chen@mail.mcgill.ca> | 2020-11-04 01:16:22 -0500 |
commit | 93243cb3faf1ccd733081fcf380559ac03c9ad35 (patch) | |
tree | 421f9f174eb77c387b5acaa05f01e64a62cab3a7 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |
parent | add realistic solver (diff) | |
parent | Optimizing generator with linear objective functions (diff) | |
download | VIATRA-Generator-93243cb3faf1ccd733081fcf380559ac03c9ad35.tar.gz VIATRA-Generator-93243cb3faf1ccd733081fcf380559ac03c9ad35.tar.zst VIATRA-Generator-93243cb3faf1ccd733081fcf380559ac03c9ad35.zip |
merge with current master, comment numerical solver related logging
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | 522 |
1 files changed, 522 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend new file mode 100644 index 00000000..ad8f94ab --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |||
@@ -0,0 +1,522 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import com.google.common.collect.ImmutableSet | ||
6 | import com.google.common.collect.Maps | ||
7 | import com.google.common.collect.Sets | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnifinishedMultiplicityQueries | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
16 | import java.util.ArrayDeque | ||
17 | import java.util.ArrayList | ||
18 | import java.util.Collection | ||
19 | import java.util.HashMap | ||
20 | import java.util.HashSet | ||
21 | import java.util.List | ||
22 | import java.util.Map | ||
23 | import java.util.Set | ||
24 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
25 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
26 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
27 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
28 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
29 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
30 | |||
31 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | ||
32 | val boolean updateHeuristic | ||
33 | val Map<Scope, LinearBoundedExpression> scopeBounds | ||
34 | val LinearBoundedExpression topLevelBounds | ||
35 | val Polyhedron polyhedron | ||
36 | val PolyhedronScopePropagatorStrategy strategy | ||
37 | val Set<Relation> relevantRelations | ||
38 | List<RelationConstraintUpdater> updaters = emptyList | ||
39 | |||
40 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, | ||
41 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, | ||
42 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | ||
43 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, | ||
44 | Collection<LinearTypeConstraintHint> hints, PolyhedronScopePropagatorStrategy strategy, | ||
45 | boolean propagateRelations, boolean updateHeuristic) { | ||
46 | super(p, statistics) | ||
47 | this.updateHeuristic = updateHeuristic | ||
48 | this.strategy = strategy | ||
49 | val builder = new PolyhedronBuilder(p) | ||
50 | builder.buildPolyhedron(possibleNewDynamicTypes) | ||
51 | scopeBounds = builder.scopeBounds | ||
52 | topLevelBounds = builder.topLevelBounds | ||
53 | polyhedron = builder.polyhedron | ||
54 | strategy.setPolyhedron(polyhedron, builder.typeBounds, builder.expressionsCache) | ||
55 | propagateAllScopeConstraints() | ||
56 | if (propagateRelations) { | ||
57 | val maximumNumberOfNewNodes = topLevelBounds.upperBound | ||
58 | if (maximumNumberOfNewNodes === null) { | ||
59 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") | ||
60 | } | ||
61 | if (maximumNumberOfNewNodes <= 0) { | ||
62 | throw new IllegalStateException("Maximum number of new nodes is not positive") | ||
63 | } | ||
64 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, | ||
65 | allPatternsByName, hints, maximumNumberOfNewNodes) | ||
66 | relevantRelations = builder.relevantRelations | ||
67 | updaters = builder.updaters | ||
68 | } else { | ||
69 | relevantRelations = emptySet | ||
70 | } | ||
71 | } | ||
72 | |||
73 | override void doPropagateAllScopeConstraints() { | ||
74 | super.doPropagateAllScopeConstraints() | ||
75 | resetBounds() | ||
76 | populatePolyhedronFromScope() | ||
77 | // println(polyhedron) | ||
78 | if (strategy.saturate) { | ||
79 | populateScopesFromPolyhedron() | ||
80 | } else { | ||
81 | setScopesInvalid() | ||
82 | } | ||
83 | // println(polyhedron) | ||
84 | if (updateHeuristic) { | ||
85 | copyScopeBoundsToHeuristic() | ||
86 | } | ||
87 | } | ||
88 | |||
89 | override isPropagationNeededAfterAdditionToRelation(Relation r) { | ||
90 | relevantRelations.contains(r) || strategy.isRelevantRelation(r) || super.isPropagationNeededAfterAdditionToRelation(r) | ||
91 | } | ||
92 | |||
93 | override isQueryEngineFlushRequiredBeforePropagation() { | ||
94 | true | ||
95 | } | ||
96 | |||
97 | def resetBounds() { | ||
98 | for (dimension : polyhedron.dimensions) { | ||
99 | dimension.lowerBound = 0 | ||
100 | dimension.upperBound = null | ||
101 | } | ||
102 | for (constraint : polyhedron.constraints) { | ||
103 | constraint.lowerBound = null | ||
104 | constraint.upperBound = null | ||
105 | } | ||
106 | } | ||
107 | |||
108 | private def populatePolyhedronFromScope() { | ||
109 | topLevelBounds.tightenLowerBound(partialInterpretation.minNewElements) | ||
110 | if (partialInterpretation.maxNewElements >= 0) { | ||
111 | topLevelBounds.tightenUpperBound(partialInterpretation.maxNewElements) | ||
112 | } | ||
113 | for (pair : scopeBounds.entrySet) { | ||
114 | val scope = pair.key | ||
115 | val bounds = pair.value | ||
116 | bounds.tightenLowerBound(scope.minNewElements) | ||
117 | if (scope.maxNewElements >= 0) { | ||
118 | bounds.tightenUpperBound(scope.maxNewElements) | ||
119 | } | ||
120 | } | ||
121 | for (updater : updaters) { | ||
122 | updater.update(partialInterpretation) | ||
123 | } | ||
124 | } | ||
125 | |||
126 | private def populateScopesFromPolyhedron() { | ||
127 | checkBounds(topLevelBounds) | ||
128 | if (partialInterpretation.minNewElements > topLevelBounds.lowerBound) { | ||
129 | throw new IllegalArgumentException('''Lower bound of «topLevelBounds» smaller than top-level scope: «partialInterpretation.minNewElements»''') | ||
130 | } else if (partialInterpretation.minNewElements != topLevelBounds.lowerBound) { | ||
131 | partialInterpretation.minNewElements = topLevelBounds.lowerBound | ||
132 | } | ||
133 | val topLevelUpperBound = topLevelBounds.upperBound ?: -1 | ||
134 | if (partialInterpretation.maxNewElements >= 0 && topLevelUpperBound >= 0 && | ||
135 | partialInterpretation.maxNewElements < topLevelUpperBound) { | ||
136 | throw new IllegalArgumentException('''Upper bound of «topLevelBounds» larger than top-level scope: «partialInterpretation.maxNewElements»''') | ||
137 | } else if (partialInterpretation.maxNewElements != topLevelUpperBound) { | ||
138 | partialInterpretation.maxNewElements = topLevelUpperBound | ||
139 | } | ||
140 | for (pair : scopeBounds.entrySet) { | ||
141 | val scope = pair.key | ||
142 | val bounds = pair.value | ||
143 | checkBounds(bounds) | ||
144 | if (scope.minNewElements > bounds.lowerBound) { | ||
145 | throw new IllegalArgumentException('''Lower bound of «bounds» smaller than «scope.targetTypeInterpretation» scope: «scope.minNewElements»''') | ||
146 | } else if (scope.minNewElements != bounds.lowerBound) { | ||
147 | scope.minNewElements = bounds.lowerBound | ||
148 | } | ||
149 | val upperBound = bounds.upperBound ?: -1 | ||
150 | if (scope.maxNewElements >= 0 && upperBound >= 0 && scope.maxNewElements < upperBound) { | ||
151 | throw new IllegalArgumentException('''Upper bound of «bounds» larger than «scope.targetTypeInterpretation» scope: «scope.maxNewElements»''') | ||
152 | } else if (scope.maxNewElements != upperBound) { | ||
153 | scope.maxNewElements = upperBound | ||
154 | } | ||
155 | } | ||
156 | } | ||
157 | |||
158 | private def checkBounds(LinearBoundedExpression bounds) { | ||
159 | if (bounds.lowerBound === null) { | ||
160 | throw new IllegalArgumentException("Infinite lower bound: " + bounds) | ||
161 | } else if (bounds.lowerBound < 0) { | ||
162 | throw new IllegalArgumentException("Negative lower bound: " + bounds) | ||
163 | } | ||
164 | if (bounds.upperBound !== null && bounds.upperBound < 0) { | ||
165 | throw new IllegalArgumentException("Negative upper bound: " + bounds) | ||
166 | } | ||
167 | } | ||
168 | |||
169 | @FinalFieldsConstructor | ||
170 | private static class PolyhedronBuilder implements LinearTypeExpressionBuilderFactory { | ||
171 | static val INFINITY_SCALE = 10 | ||
172 | |||
173 | val PartialInterpretation p | ||
174 | |||
175 | Map<Type, Dimension> instanceCounts | ||
176 | Map<Type, Map<Dimension, Integer>> subtypeDimensions | ||
177 | Map<Map<Dimension, Integer>, LinearBoundedExpression> expressionsCache | ||
178 | Map<Type, LinearBoundedExpression> typeBounds | ||
179 | int infinity | ||
180 | ViatraQueryEngine queryEngine | ||
181 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName | ||
182 | ImmutableList.Builder<RelationConstraintUpdater> updatersBuilder | ||
183 | |||
184 | Map<Scope, LinearBoundedExpression> scopeBounds | ||
185 | LinearBoundedExpression topLevelBounds | ||
186 | Polyhedron polyhedron | ||
187 | Set<Relation> relevantRelations | ||
188 | List<RelationConstraintUpdater> updaters | ||
189 | |||
190 | def buildPolyhedron(Set<? extends Type> possibleNewDynamicTypes) { | ||
191 | instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] | ||
192 | val types = p.problem.types | ||
193 | expressionsCache = Maps.newHashMapWithExpectedSize(types.size) | ||
194 | subtypeDimensions = types.toInvertedMap[findSubtypeDimensions.toInvertedMap[1]] | ||
195 | typeBounds = ImmutableMap.copyOf(subtypeDimensions.mapValues[toExpression]) | ||
196 | scopeBounds = buildScopeBounds | ||
197 | topLevelBounds = instanceCounts.values.toInvertedMap[1].toExpression | ||
198 | val dimensions = ImmutableList.copyOf(instanceCounts.values) | ||
199 | val expressionsToSaturate = ImmutableList.copyOf(scopeBounds.values) | ||
200 | polyhedron = new Polyhedron(dimensions, new ArrayList, expressionsToSaturate) | ||
201 | addCachedConstraintsToPolyhedron() | ||
202 | } | ||
203 | |||
204 | def buildMultiplicityConstraints( | ||
205 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> constraints, | ||
206 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | ||
207 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, | ||
208 | Collection<LinearTypeConstraintHint> hints, int maximumNuberOfNewNodes) { | ||
209 | infinity = if (maximumNuberOfNewNodes <= Integer.MAX_VALUE / INFINITY_SCALE) { | ||
210 | maximumNuberOfNewNodes * INFINITY_SCALE | ||
211 | } else { | ||
212 | Integer.MAX_VALUE | ||
213 | } | ||
214 | |||
215 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) | ||
216 | this.allPatternsByName = allPatternsByName | ||
217 | updatersBuilder = ImmutableList.builder | ||
218 | val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType] | ||
219 | for (pair : containmentConstraints.entrySet) { | ||
220 | buildContainmentConstraints(pair.key, pair.value) | ||
221 | } | ||
222 | buildConstainmentRootConstraints(containmentConstraints.keySet, hasElementInContainmentQuery) | ||
223 | for (pair : constraints.entrySet) { | ||
224 | val constraint = pair.key | ||
225 | if (!constraint.containment && !constraint.container) { | ||
226 | buildNonContainmentConstraints(constraint, pair.value) | ||
227 | } | ||
228 | } | ||
229 | buildRelevantRelations(constraints.keySet) | ||
230 | for (hint : hints) { | ||
231 | val updater = hint.createConstraintUpdater(this) | ||
232 | if (updater !== null) { | ||
233 | updatersBuilder.add(updater) | ||
234 | } | ||
235 | } | ||
236 | updaters = updatersBuilder.build | ||
237 | addCachedConstraintsToPolyhedron() | ||
238 | } | ||
239 | |||
240 | private def buildRelevantRelations(Set<RelationMultiplicityConstraint> constraints) { | ||
241 | val builder = ImmutableSet.builder | ||
242 | for (constraint : constraints) { | ||
243 | builder.add(constraint.relation) | ||
244 | if (constraint.inverseRelation !== null) { | ||
245 | builder.add(constraint.inverseRelation) | ||
246 | } | ||
247 | } | ||
248 | relevantRelations = builder.build | ||
249 | } | ||
250 | |||
251 | private def addCachedConstraintsToPolyhedron() { | ||
252 | val constraints = new HashSet | ||
253 | constraints.addAll(expressionsCache.values.filter(LinearConstraint)) | ||
254 | constraints.removeAll(polyhedron.constraints) | ||
255 | polyhedron.constraints.addAll(constraints) | ||
256 | } | ||
257 | |||
258 | private def buildContainmentConstraints(Type containedType, | ||
259 | List<Map.Entry<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries>> constraints) { | ||
260 | val typeCoefficients = subtypeDimensions.get(containedType) | ||
261 | val orphansLowerBoundCoefficients = new HashMap(typeCoefficients) | ||
262 | val orphansUpperBoundCoefficients = new HashMap(typeCoefficients) | ||
263 | val unfinishedMultiplicitiesBuilder = ImmutableList.builder | ||
264 | val remainingContentsBuilder = ImmutableList.builder | ||
265 | for (pair : constraints) { | ||
266 | val constraint = pair.key | ||
267 | val containerCoefficients = subtypeDimensions.get(constraint.sourceType) | ||
268 | if (constraint.isUpperBoundFinite) { | ||
269 | orphansLowerBoundCoefficients.addCoefficients(-constraint.upperBound, containerCoefficients) | ||
270 | } else { | ||
271 | orphansLowerBoundCoefficients.addCoefficients(-infinity, containerCoefficients) | ||
272 | } | ||
273 | orphansUpperBoundCoefficients.addCoefficients(-constraint.lowerBound, containerCoefficients) | ||
274 | val queries = pair.value | ||
275 | if (queries.existingMultiplicityQuery !== null) { | ||
276 | val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine) | ||
277 | if (constraint.constrainsUnfinished) { | ||
278 | unfinishedMultiplicitiesBuilder.add( | ||
279 | RemainingMultiplicityCalculator.of(matcher, constraint.lowerBound)) | ||
280 | } | ||
281 | remainingContentsBuilder.add(RemainingMultiplicityCalculator.of(matcher, constraint.upperBound)) | ||
282 | } else if (constraint.constrainsUnfinished) { | ||
283 | throw new IllegalArgumentException("Containment constraints need multiplicity queries") | ||
284 | } | ||
285 | } | ||
286 | val orphanLowerBound = orphansLowerBoundCoefficients.toExpression | ||
287 | val orphanUpperBound = orphansUpperBoundCoefficients.toExpression | ||
288 | val updater = new ContainmentConstraintUpdater(orphanLowerBound, orphanUpperBound, | ||
289 | unfinishedMultiplicitiesBuilder.build, remainingContentsBuilder.build) | ||
290 | updatersBuilder.add(updater) | ||
291 | } | ||
292 | |||
293 | private def buildConstainmentRootConstraints(Set<Type> containedTypes, | ||
294 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery) { | ||
295 | val matcher = hasElementInContainmentQuery.getMatcher(queryEngine) | ||
296 | val rootDimensions = Sets.newHashSet(instanceCounts.values) | ||
297 | for (type : containedTypes) { | ||
298 | val containedDimensions = subtypeDimensions.get(type).keySet | ||
299 | rootDimensions.removeAll(containedDimensions) | ||
300 | } | ||
301 | for (dimension : rootDimensions) { | ||
302 | updatersBuilder.add(new ContainmentRootConstraintUpdater(dimension, matcher)) | ||
303 | } | ||
304 | } | ||
305 | |||
306 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, | ||
307 | UnifinishedMultiplicityQueries queries) { | ||
308 | if (!constraint.reference) { | ||
309 | return | ||
310 | } | ||
311 | if (constraint.constrainsRemainingInverse) { | ||
312 | if (queries.getExistingMultiplicityQuery === null) { | ||
313 | throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries: " + | ||
314 | constraint.relation) | ||
315 | } | ||
316 | val existingMultiplicityMatcher = queries.getExistingMultiplicityQuery.getMatcher(queryEngine) | ||
317 | val unfinishedMultiplicityCalculator = RemainingMultiplicityCalculator.of(existingMultiplicityMatcher, | ||
318 | constraint.lowerBound) | ||
319 | val existingInverseMultiplicityMatcher = queries.existingInverseMultiplicityQuery.getMatcher( | ||
320 | queryEngine) | ||
321 | val remainingInverseMultiplicityCalculator = new RemainingInverseMultiplicityCalculator( | ||
322 | existingInverseMultiplicityMatcher, constraint.upperBound) | ||
323 | val availableMultiplicityCoefficients = new HashMap | ||
324 | availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, | ||
325 | subtypeDimensions.get(constraint.targetType)) | ||
326 | availableMultiplicityCoefficients.addCoefficients(-constraint.lowerBound, | ||
327 | subtypeDimensions.get(constraint.targetType)) | ||
328 | val availableMultiplicity = availableMultiplicityCoefficients.toExpression | ||
329 | updatersBuilder.add( | ||
330 | new UnfinishedMultiplicityConstraintUpdater(availableMultiplicity, unfinishedMultiplicityCalculator, | ||
331 | remainingInverseMultiplicityCalculator)) | ||
332 | } | ||
333 | if (constraint.constrainsUnrepairable) { | ||
334 | if (queries.existingMultiplicityQuery.parameters.size < 5) { | ||
335 | throw new IllegalArgumentException("Reference constraints need repairable multiplicity queries: " + | ||
336 | constraint.relation) | ||
337 | } | ||
338 | val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine) | ||
339 | val calculator = new UnrepairableMultiplicityCalculator(matcher, constraint.lowerBound) | ||
340 | val targetTypeCardinality = typeBounds.get(constraint.targetType) | ||
341 | updatersBuilder.add(new UnrepairableMultiplicityConstraintUpdater(targetTypeCardinality, calculator)) | ||
342 | } | ||
343 | } | ||
344 | |||
345 | private static def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { | ||
346 | for (pair : a.entrySet) { | ||
347 | val dimension = pair.key | ||
348 | val currentValue = accumulator.get(pair.key) ?: 0 | ||
349 | val newValue = currentValue + scale * pair.value | ||
350 | if (newValue == 0) { | ||
351 | accumulator.remove(dimension) | ||
352 | } else { | ||
353 | accumulator.put(dimension, newValue) | ||
354 | } | ||
355 | } | ||
356 | } | ||
357 | |||
358 | private def findSubtypeDimensions(Type type) { | ||
359 | val subtypes = new HashSet | ||
360 | val dimensions = new HashSet | ||
361 | val stack = new ArrayDeque | ||
362 | stack.addLast(type) | ||
363 | while (!stack.empty) { | ||
364 | val subtype = stack.removeLast | ||
365 | if (subtypes.add(subtype)) { | ||
366 | val dimension = instanceCounts.get(subtype) | ||
367 | if (dimension !== null) { | ||
368 | dimensions.add(dimension) | ||
369 | } | ||
370 | stack.addAll(subtype.subtypes) | ||
371 | } | ||
372 | } | ||
373 | dimensions | ||
374 | } | ||
375 | |||
376 | private def toExpression(Map<Dimension, Integer> coefficients) { | ||
377 | expressionsCache.computeIfAbsent(coefficients) [ c | | ||
378 | if (c.size == 1 && c.entrySet.head.value == 1) { | ||
379 | c.entrySet.head.key | ||
380 | } else { | ||
381 | new LinearConstraint(c, null, null) | ||
382 | } | ||
383 | ] | ||
384 | } | ||
385 | |||
386 | private def buildScopeBounds() { | ||
387 | val scopeBoundsBuilder = ImmutableMap.builder | ||
388 | for (scope : p.scopes) { | ||
389 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { | ||
390 | PartialPrimitiveInterpretation: | ||
391 | throw new IllegalStateException("Primitive type scopes are not yet implemented") | ||
392 | PartialComplexTypeInterpretation: { | ||
393 | val complexType = targetTypeInterpretation.interpretationOf | ||
394 | val typeBound = typeBounds.get(complexType) | ||
395 | if (typeBound === null) { | ||
396 | if (scope.minNewElements > 0) { | ||
397 | throw new IllegalArgumentException("Found scope for " + complexType.name + | ||
398 | ", but the type cannot be instantiated") | ||
399 | } | ||
400 | } else { | ||
401 | scopeBoundsBuilder.put(scope, typeBound) | ||
402 | } | ||
403 | } | ||
404 | default: | ||
405 | throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + | ||
406 | targetTypeInterpretation) | ||
407 | } | ||
408 | } | ||
409 | scopeBoundsBuilder.build | ||
410 | } | ||
411 | |||
412 | override createMatcher(String queryName) { | ||
413 | val querySpecification = allPatternsByName.get(queryName) | ||
414 | if (querySpecification === null) { | ||
415 | throw new IllegalArgumentException("Unknown pattern: " + queryName) | ||
416 | } | ||
417 | querySpecification.getMatcher(queryEngine) | ||
418 | } | ||
419 | |||
420 | override createBuilder() { | ||
421 | new PolyhedronBuilderLinearTypeExpressionBuilder(this) | ||
422 | } | ||
423 | } | ||
424 | |||
425 | @FinalFieldsConstructor | ||
426 | private static class PolyhedronBuilderLinearTypeExpressionBuilder implements LinearTypeExpressionBuilder { | ||
427 | val PolyhedronBuilder polyhedronBuilder | ||
428 | val Map<Dimension, Integer> coefficients = new HashMap | ||
429 | |||
430 | override add(int scale, Type type) { | ||
431 | val typeCoefficients = polyhedronBuilder.subtypeDimensions.get(type) | ||
432 | if (typeCoefficients === null) { | ||
433 | throw new IllegalArgumentException("Unknown type: " + type) | ||
434 | } | ||
435 | PolyhedronBuilder.addCoefficients(coefficients, scale, typeCoefficients) | ||
436 | this | ||
437 | } | ||
438 | |||
439 | override build() { | ||
440 | polyhedronBuilder.toExpression(coefficients) | ||
441 | } | ||
442 | } | ||
443 | |||
444 | @FinalFieldsConstructor | ||
445 | private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { | ||
446 | val LinearBoundedExpression orphansLowerBound | ||
447 | val LinearBoundedExpression orphansUpperBound | ||
448 | val List<MultiplicityCalculator<? extends IPatternMatch>> unfinishedMultiplicities | ||
449 | val List<MultiplicityCalculator<? extends IPatternMatch>> remainingContents | ||
450 | |||
451 | override update(PartialInterpretation p) { | ||
452 | tightenLowerBound(p) | ||
453 | tightenUpperBound(p) | ||
454 | } | ||
455 | |||
456 | private def tightenLowerBound(PartialInterpretation p) { | ||
457 | var int sum = 0 | ||
458 | for (calculator : remainingContents) { | ||
459 | val value = calculator.getMultiplicity(p) | ||
460 | if (value < 0) { | ||
461 | // Infinite upper bound, no need to tighten. | ||
462 | return | ||
463 | } | ||
464 | sum += value | ||
465 | } | ||
466 | orphansLowerBound.tightenUpperBound(sum) | ||
467 | } | ||
468 | |||
469 | private def tightenUpperBound(PartialInterpretation p) { | ||
470 | var int sum = 0 | ||
471 | for (calculator : unfinishedMultiplicities) { | ||
472 | val value = calculator.getMultiplicity(p) | ||
473 | sum += value | ||
474 | } | ||
475 | orphansUpperBound.tightenLowerBound(sum) | ||
476 | } | ||
477 | } | ||
478 | |||
479 | @FinalFieldsConstructor | ||
480 | private static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { | ||
481 | val LinearBoundedExpression typeCardinality | ||
482 | val ViatraQueryMatcher<? extends IPatternMatch> hasElementInContainmentMatcher | ||
483 | |||
484 | override update(PartialInterpretation p) { | ||
485 | if (hasElementInContainmentMatcher.hasMatch(p)) { | ||
486 | typeCardinality.tightenUpperBound(0) | ||
487 | } else { | ||
488 | typeCardinality.tightenUpperBound(1) | ||
489 | } | ||
490 | } | ||
491 | |||
492 | private static def <T extends IPatternMatch> hasMatch(ViatraQueryMatcher<T> matcher, PartialInterpretation p) { | ||
493 | val match = matcher.newMatch(p.problem, p) | ||
494 | matcher.countMatches(match) != 0 | ||
495 | } | ||
496 | } | ||
497 | |||
498 | @FinalFieldsConstructor | ||
499 | private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { | ||
500 | val LinearBoundedExpression availableMultiplicityExpression | ||
501 | val MultiplicityCalculator<? extends IPatternMatch> unfinishedMultiplicityCalculator | ||
502 | val MultiplicityCalculator<? extends IPatternMatch> remainingInverseMultiplcityCalculator | ||
503 | |||
504 | override update(PartialInterpretation p) { | ||
505 | val unfinishedMultiplicity = unfinishedMultiplicityCalculator.getMultiplicity(p) | ||
506 | val remainingInverseMultiplicity = remainingInverseMultiplcityCalculator.getMultiplicity(p) | ||
507 | val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity | ||
508 | availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) | ||
509 | } | ||
510 | } | ||
511 | |||
512 | @FinalFieldsConstructor | ||
513 | private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { | ||
514 | val LinearBoundedExpression targetCardinalityExpression | ||
515 | val MultiplicityCalculator<? extends IPatternMatch> calculator | ||
516 | |||
517 | override update(PartialInterpretation p) { | ||
518 | val value = calculator.getMultiplicity(p) | ||
519 | targetCardinalityExpression.tightenLowerBound(value) | ||
520 | } | ||
521 | } | ||
522 | } | ||