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