diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-28 20:33:48 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-28 20:33:48 +0200 |
commit | 07ae9155ce0ab9407566b075356f9b7220ee8380 (patch) | |
tree | 5c088de7741b575e6fb5b517bb694428f80c661c /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |
parent | Fix scope + numerical propagation WIP (diff) | |
download | VIATRA-Generator-07ae9155ce0ab9407566b075356f9b7220ee8380.tar.gz VIATRA-Generator-07ae9155ce0ab9407566b075356f9b7220ee8380.tar.zst VIATRA-Generator-07ae9155ce0ab9407566b075356f9b7220ee8380.zip |
Fix scope + numerical solver interaction
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 | 133 |
1 files changed, 53 insertions, 80 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 index 9b4dff0f..db22b95c 100644 --- 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 | |||
@@ -33,7 +33,7 @@ import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | |||
33 | 33 | ||
34 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | 34 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { |
35 | static val CACHE_SIZE = 10000 | 35 | static val CACHE_SIZE = 10000 |
36 | 36 | ||
37 | val boolean updateHeuristic | 37 | val boolean updateHeuristic |
38 | val Map<Scope, LinearBoundedExpression> scopeBounds | 38 | val Map<Scope, LinearBoundedExpression> scopeBounds |
39 | val LinearBoundedExpression topLevelBounds | 39 | val LinearBoundedExpression topLevelBounds |
@@ -185,22 +185,6 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
185 | if (bounds.upperBound !== null && bounds.upperBound < 0) { | 185 | if (bounds.upperBound !== null && bounds.upperBound < 0) { |
186 | throw new IllegalArgumentException("Negative upper bound: " + bounds) | 186 | throw new IllegalArgumentException("Negative upper bound: " + bounds) |
187 | } | 187 | } |
188 | } | ||
189 | |||
190 | private static def <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> matcher, | ||
191 | PartialInterpretation p) { | ||
192 | val match = matcher.newEmptyMatch | ||
193 | match.set(0, p.problem) | ||
194 | match.set(1, p) | ||
195 | val iterator = matcher.streamAllMatches(match).iterator | ||
196 | if (!iterator.hasNext) { | ||
197 | return null | ||
198 | } | ||
199 | val value = iterator.next.get(2) as Integer | ||
200 | if (iterator.hasNext) { | ||
201 | throw new IllegalArgumentException("Multiplicity calculation query has more than one match") | ||
202 | } | ||
203 | value | ||
204 | } | 188 | } |
205 | 189 | ||
206 | @FinalFieldsConstructor | 190 | @FinalFieldsConstructor |
@@ -243,7 +227,12 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
243 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | 227 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, |
244 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, | 228 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, |
245 | Collection<LinearTypeConstraintHint> hints, int maximumNuberOfNewNodes) { | 229 | Collection<LinearTypeConstraintHint> hints, int maximumNuberOfNewNodes) { |
246 | infinity = maximumNuberOfNewNodes * INFINITY_SCALE | 230 | infinity = if (maximumNuberOfNewNodes <= Integer.MAX_VALUE / INFINITY_SCALE) { |
231 | maximumNuberOfNewNodes * INFINITY_SCALE | ||
232 | } else { | ||
233 | Integer.MAX_VALUE | ||
234 | } | ||
235 | |||
247 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) | 236 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) |
248 | this.allPatternsByName = allPatternsByName | 237 | this.allPatternsByName = allPatternsByName |
249 | updatersBuilder = ImmutableList.builder | 238 | updatersBuilder = ImmutableList.builder |
@@ -254,7 +243,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
254 | buildConstainmentRootConstraints(containmentConstraints.keySet, hasElementInContainmentQuery) | 243 | buildConstainmentRootConstraints(containmentConstraints.keySet, hasElementInContainmentQuery) |
255 | for (pair : constraints.entrySet) { | 244 | for (pair : constraints.entrySet) { |
256 | val constraint = pair.key | 245 | val constraint = pair.key |
257 | if (!constraint.containment) { | 246 | if (!constraint.containment && !constraint.container) { |
258 | buildNonContainmentConstraints(constraint, pair.value) | 247 | buildNonContainmentConstraints(constraint, pair.value) |
259 | } | 248 | } |
260 | } | 249 | } |
@@ -289,8 +278,8 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
289 | val typeCoefficients = subtypeDimensions.get(containedType) | 278 | val typeCoefficients = subtypeDimensions.get(containedType) |
290 | val orphansLowerBoundCoefficients = new HashMap(typeCoefficients) | 279 | val orphansLowerBoundCoefficients = new HashMap(typeCoefficients) |
291 | val orphansUpperBoundCoefficients = new HashMap(typeCoefficients) | 280 | val orphansUpperBoundCoefficients = new HashMap(typeCoefficients) |
292 | val unfinishedMultiplicitiesMatchersBuilder = ImmutableList.builder | 281 | val unfinishedMultiplicitiesBuilder = ImmutableList.builder |
293 | val remainingContentsQueriesBuilder = ImmutableList.builder | 282 | val remainingContentsBuilder = ImmutableList.builder |
294 | for (pair : constraints) { | 283 | for (pair : constraints) { |
295 | val constraint = pair.key | 284 | val constraint = pair.key |
296 | val containerCoefficients = subtypeDimensions.get(constraint.sourceType) | 285 | val containerCoefficients = subtypeDimensions.get(constraint.sourceType) |
@@ -301,23 +290,21 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
301 | } | 290 | } |
302 | orphansUpperBoundCoefficients.addCoefficients(-constraint.lowerBound, containerCoefficients) | 291 | orphansUpperBoundCoefficients.addCoefficients(-constraint.lowerBound, containerCoefficients) |
303 | val queries = pair.value | 292 | val queries = pair.value |
304 | if (constraint.constrainsUnfinished) { | 293 | if (queries.existingMultiplicityQuery !== null) { |
305 | if (queries.unfinishedMultiplicityQuery === null) { | 294 | val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine) |
306 | throw new IllegalArgumentException( | 295 | if (constraint.constrainsUnfinished) { |
307 | "Containment constraints need unfinished multiplicity queries") | 296 | unfinishedMultiplicitiesBuilder.add( |
297 | RemainingMultiplicityCalculator.of(matcher, constraint.lowerBound)) | ||
308 | } | 298 | } |
309 | unfinishedMultiplicitiesMatchersBuilder.add( | 299 | remainingContentsBuilder.add(RemainingMultiplicityCalculator.of(matcher, constraint.upperBound)) |
310 | queries.unfinishedMultiplicityQuery.getMatcher(queryEngine)) | 300 | } else if (constraint.constrainsUnfinished) { |
311 | } | 301 | throw new IllegalArgumentException("Containment constraints need multiplicity queries") |
312 | if (queries.remainingContentsQuery === null) { | ||
313 | throw new IllegalArgumentException("Containment constraints need remaining contents queries") | ||
314 | } | 302 | } |
315 | remainingContentsQueriesBuilder.add(queries.remainingContentsQuery.getMatcher(queryEngine)) | ||
316 | } | 303 | } |
317 | val orphanLowerBound = orphansLowerBoundCoefficients.toExpression | 304 | val orphanLowerBound = orphansLowerBoundCoefficients.toExpression |
318 | val orphanUpperBound = orphansUpperBoundCoefficients.toExpression | 305 | val orphanUpperBound = orphansUpperBoundCoefficients.toExpression |
319 | val updater = new ContainmentConstraintUpdater(containedType.name, orphanLowerBound, orphanUpperBound, | 306 | val updater = new ContainmentConstraintUpdater(orphanLowerBound, orphanUpperBound, |
320 | unfinishedMultiplicitiesMatchersBuilder.build, remainingContentsQueriesBuilder.build) | 307 | unfinishedMultiplicitiesBuilder.build, remainingContentsBuilder.build) |
321 | updatersBuilder.add(updater) | 308 | updatersBuilder.add(updater) |
322 | } | 309 | } |
323 | 310 | ||
@@ -336,17 +323,21 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
336 | 323 | ||
337 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, | 324 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, |
338 | UnifinishedMultiplicityQueries queries) { | 325 | UnifinishedMultiplicityQueries queries) { |
326 | if (!constraint.reference) { | ||
327 | return | ||
328 | } | ||
339 | if (constraint.constrainsRemainingInverse) { | 329 | if (constraint.constrainsRemainingInverse) { |
340 | if (queries.unfinishedMultiplicityQuery === null) { | 330 | if (queries.getExistingMultiplicityQuery === null) { |
341 | throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries") | 331 | throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries: " + |
342 | } | 332 | constraint.relation) |
343 | val unfinishedMultiplicityMatcher = queries.unfinishedMultiplicityQuery.getMatcher(queryEngine) | ||
344 | if (queries.remainingInverseMultiplicityQuery === null) { | ||
345 | throw new IllegalArgumentException( | ||
346 | "Reference constraints need remaining inverse multiplicity queries") | ||
347 | } | 333 | } |
348 | val remainingInverseMultiplicityMatcher = queries.remainingInverseMultiplicityQuery.getMatcher( | 334 | val existingMultiplicityMatcher = queries.getExistingMultiplicityQuery.getMatcher(queryEngine) |
335 | val unfinishedMultiplicityCalculator = RemainingMultiplicityCalculator.of(existingMultiplicityMatcher, | ||
336 | constraint.lowerBound) | ||
337 | val existingInverseMultiplicityMatcher = queries.existingInverseMultiplicityQuery.getMatcher( | ||
349 | queryEngine) | 338 | queryEngine) |
339 | val remainingInverseMultiplicityCalculator = new RemainingInverseMultiplicityCalculator( | ||
340 | existingInverseMultiplicityMatcher, constraint.upperBound) | ||
350 | val availableMultiplicityCoefficients = new HashMap | 341 | val availableMultiplicityCoefficients = new HashMap |
351 | availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, | 342 | availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, |
352 | subtypeDimensions.get(constraint.targetType)) | 343 | subtypeDimensions.get(constraint.targetType)) |
@@ -354,18 +345,18 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
354 | subtypeDimensions.get(constraint.targetType)) | 345 | subtypeDimensions.get(constraint.targetType)) |
355 | val availableMultiplicity = availableMultiplicityCoefficients.toExpression | 346 | val availableMultiplicity = availableMultiplicityCoefficients.toExpression |
356 | updatersBuilder.add( | 347 | updatersBuilder.add( |
357 | new UnfinishedMultiplicityConstraintUpdater(constraint.relation.name, availableMultiplicity, | 348 | new UnfinishedMultiplicityConstraintUpdater(availableMultiplicity, unfinishedMultiplicityCalculator, |
358 | unfinishedMultiplicityMatcher, remainingInverseMultiplicityMatcher)) | 349 | remainingInverseMultiplicityCalculator)) |
359 | } | 350 | } |
360 | if (constraint.constrainsUnrepairable) { | 351 | if (constraint.constrainsUnrepairable) { |
361 | if (queries.unrepairableMultiplicityQuery === null) { | 352 | if (queries.existingMultiplicityQuery.parameters.size < 5) { |
362 | throw new IllegalArgumentException("Reference constraints need unrepairable multiplicity queries") | 353 | throw new IllegalArgumentException("Reference constraints need repairable multiplicity queries: " + |
354 | constraint.relation) | ||
363 | } | 355 | } |
364 | val unrepairableMultiplicityMatcher = queries.unrepairableMultiplicityQuery.getMatcher(queryEngine) | 356 | val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine) |
357 | val calculator = new UnrepairableMultiplicityCalculator(matcher, constraint.lowerBound) | ||
365 | val targetTypeCardinality = typeBounds.get(constraint.targetType) | 358 | val targetTypeCardinality = typeBounds.get(constraint.targetType) |
366 | updatersBuilder.add( | 359 | updatersBuilder.add(new UnrepairableMultiplicityConstraintUpdater(targetTypeCardinality, calculator)) |
367 | new UnrepairableMultiplicityConstraintUpdater(constraint.relation.name, targetTypeCardinality, | ||
368 | unrepairableMultiplicityMatcher)) | ||
369 | } | 360 | } |
370 | } | 361 | } |
371 | 362 | ||
@@ -470,11 +461,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
470 | 461 | ||
471 | @FinalFieldsConstructor | 462 | @FinalFieldsConstructor |
472 | private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { | 463 | private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { |
473 | val String name | ||
474 | val LinearBoundedExpression orphansLowerBound | 464 | val LinearBoundedExpression orphansLowerBound |
475 | val LinearBoundedExpression orphansUpperBound | 465 | val LinearBoundedExpression orphansUpperBound |
476 | val List<ViatraQueryMatcher<? extends IPatternMatch>> unfinishedMultiplicitiesMatchers | 466 | val List<MultiplicityCalculator<? extends IPatternMatch>> unfinishedMultiplicities |
477 | val List<ViatraQueryMatcher<? extends IPatternMatch>> remainingContentsQueries | 467 | val List<MultiplicityCalculator<? extends IPatternMatch>> remainingContents |
478 | 468 | ||
479 | override update(PartialInterpretation p) { | 469 | override update(PartialInterpretation p) { |
480 | tightenLowerBound(p) | 470 | tightenLowerBound(p) |
@@ -483,12 +473,9 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
483 | 473 | ||
484 | private def tightenLowerBound(PartialInterpretation p) { | 474 | private def tightenLowerBound(PartialInterpretation p) { |
485 | var int sum = 0 | 475 | var int sum = 0 |
486 | for (matcher : remainingContentsQueries) { | 476 | for (calculator : remainingContents) { |
487 | val value = matcher.getCalculatedMultiplicity(p) | 477 | val value = calculator.getMultiplicity(p) |
488 | if (value === null) { | 478 | if (value < 0) { |
489 | throw new IllegalArgumentException("Remaining contents count is missing for " + name) | ||
490 | } | ||
491 | if (value == -1) { | ||
492 | // Infinite upper bound, no need to tighten. | 479 | // Infinite upper bound, no need to tighten. |
493 | return | 480 | return |
494 | } | 481 | } |
@@ -499,11 +486,8 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
499 | 486 | ||
500 | private def tightenUpperBound(PartialInterpretation p) { | 487 | private def tightenUpperBound(PartialInterpretation p) { |
501 | var int sum = 0 | 488 | var int sum = 0 |
502 | for (matcher : unfinishedMultiplicitiesMatchers) { | 489 | for (calculator : unfinishedMultiplicities) { |
503 | val value = matcher.getCalculatedMultiplicity(p) | 490 | val value = calculator.getMultiplicity(p) |
504 | if (value === null) { | ||
505 | throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) | ||
506 | } | ||
507 | sum += value | 491 | sum += value |
508 | } | 492 | } |
509 | orphansUpperBound.tightenLowerBound(sum) | 493 | orphansUpperBound.tightenLowerBound(sum) |
@@ -531,20 +515,13 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
531 | 515 | ||
532 | @FinalFieldsConstructor | 516 | @FinalFieldsConstructor |
533 | private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { | 517 | private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { |
534 | val String name | ||
535 | val LinearBoundedExpression availableMultiplicityExpression | 518 | val LinearBoundedExpression availableMultiplicityExpression |
536 | val ViatraQueryMatcher<? extends IPatternMatch> unfinishedMultiplicityMatcher | 519 | val MultiplicityCalculator<? extends IPatternMatch> unfinishedMultiplicityCalculator |
537 | val ViatraQueryMatcher<? extends IPatternMatch> remainingInverseMultiplicityMatcher | 520 | val MultiplicityCalculator<? extends IPatternMatch> remainingInverseMultiplcityCalculator |
538 | 521 | ||
539 | override update(PartialInterpretation p) { | 522 | override update(PartialInterpretation p) { |
540 | val unfinishedMultiplicity = unfinishedMultiplicityMatcher.getCalculatedMultiplicity(p) | 523 | val unfinishedMultiplicity = unfinishedMultiplicityCalculator.getMultiplicity(p) |
541 | if (unfinishedMultiplicity === null) { | 524 | val remainingInverseMultiplicity = remainingInverseMultiplcityCalculator.getMultiplicity(p) |
542 | throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) | ||
543 | } | ||
544 | val remainingInverseMultiplicity = remainingInverseMultiplicityMatcher.getCalculatedMultiplicity(p) | ||
545 | if (remainingInverseMultiplicity === null) { | ||
546 | throw new IllegalArgumentException("Remaining inverse multiplicity is missing for " + name) | ||
547 | } | ||
548 | val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity | 525 | val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity |
549 | availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) | 526 | availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) |
550 | } | 527 | } |
@@ -552,15 +529,11 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
552 | 529 | ||
553 | @FinalFieldsConstructor | 530 | @FinalFieldsConstructor |
554 | private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { | 531 | private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { |
555 | val String name | ||
556 | val LinearBoundedExpression targetCardinalityExpression | 532 | val LinearBoundedExpression targetCardinalityExpression |
557 | val ViatraQueryMatcher<? extends IPatternMatch> unrepairableMultiplicityMatcher | 533 | val MultiplicityCalculator<? extends IPatternMatch> calculator |
558 | 534 | ||
559 | override update(PartialInterpretation p) { | 535 | override update(PartialInterpretation p) { |
560 | val value = unrepairableMultiplicityMatcher.getCalculatedMultiplicity(p) | 536 | val value = calculator.getMultiplicity(p) |
561 | if (value === null) { | ||
562 | throw new IllegalArgumentException("Unrepairable multiplicity is missing for " + name) | ||
563 | } | ||
564 | targetCardinalityExpression.tightenLowerBound(value) | 537 | targetCardinalityExpression.tightenLowerBound(value) |
565 | } | 538 | } |
566 | } | 539 | } |