diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-30 18:57:01 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-30 18:57:01 +0200 |
commit | 4cb0aa5a0b9adac2bb8d4a995be015651bdd5628 (patch) | |
tree | 5c917ffa6f334e6b4c268b94fb0bd8910cf892b2 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality | |
parent | Allow infiite upper scope bound in PolyhedronScopePropagator (diff) | |
download | VIATRA-Generator-4cb0aa5a0b9adac2bb8d4a995be015651bdd5628.tar.gz VIATRA-Generator-4cb0aa5a0b9adac2bb8d4a995be015651bdd5628.tar.zst VIATRA-Generator-4cb0aa5a0b9adac2bb8d4a995be015651bdd5628.zip |
Polyhedron scope propagator for non-containment references
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | 80 |
1 files changed, 78 insertions, 2 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 e9c155f5..f6b101b6 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 | |||
@@ -50,7 +50,7 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
50 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") | 50 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") |
51 | } | 51 | } |
52 | if (maximumNumberOfNewNodes <= 0) { | 52 | if (maximumNumberOfNewNodes <= 0) { |
53 | throw new IllegalStateException("Maximum number of new nodes is negative") | 53 | throw new IllegalStateException("Maximum number of new nodes is not positive") |
54 | } | 54 | } |
55 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, | 55 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, |
56 | maximumNumberOfNewNodes) | 56 | maximumNumberOfNewNodes) |
@@ -65,7 +65,7 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
65 | val result = operator.saturate() | 65 | val result = operator.saturate() |
66 | // println(polyhedron) | 66 | // println(polyhedron) |
67 | if (result == PolyhedronSaturationResult.EMPTY) { | 67 | if (result == PolyhedronSaturationResult.EMPTY) { |
68 | throw new IllegalStateException("Scope bounds cannot be satisfied") | 68 | setScopesInvalid() |
69 | } else { | 69 | } else { |
70 | populateScopesFromPolyhedron() | 70 | populateScopesFromPolyhedron() |
71 | if (result != PolyhedronSaturationResult.SATURATED) { | 71 | if (result != PolyhedronSaturationResult.SATURATED) { |
@@ -146,6 +146,15 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
146 | } | 146 | } |
147 | } | 147 | } |
148 | 148 | ||
149 | private def setScopesInvalid() { | ||
150 | partialInterpretation.minNewElements = Integer.MAX_VALUE | ||
151 | partialInterpretation.maxNewElements = 0 | ||
152 | for (scope : partialInterpretation.scopes) { | ||
153 | scope.minNewElements = Integer.MAX_VALUE | ||
154 | scope.maxNewElements = 0 | ||
155 | } | ||
156 | } | ||
157 | |||
149 | private static def <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> matcher, | 158 | private static def <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> matcher, |
150 | PartialInterpretation p) { | 159 | PartialInterpretation p) { |
151 | val match = matcher.newEmptyMatch | 160 | val match = matcher.newEmptyMatch |
@@ -276,6 +285,37 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
276 | 285 | ||
277 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, | 286 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, |
278 | UnifinishedMultiplicityQueries queries) { | 287 | UnifinishedMultiplicityQueries queries) { |
288 | if (constraint.constrainsRemainingInverse) { | ||
289 | if (queries.unfinishedMultiplicityQuery === null) { | ||
290 | throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries") | ||
291 | } | ||
292 | val unfinishedMultiplicityMatcher = queries.unfinishedMultiplicityQuery.getMatcher(queryEngine) | ||
293 | if (queries.remainingInverseMultiplicityQuery === null) { | ||
294 | throw new IllegalArgumentException( | ||
295 | "Reference constraints need remaining inverse multiplicity queries") | ||
296 | } | ||
297 | val remainingInverseMultiplicityMatcher = queries.remainingInverseMultiplicityQuery.getMatcher( | ||
298 | queryEngine) | ||
299 | val availableMultiplicityCoefficients = new HashMap | ||
300 | availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, | ||
301 | subtypeDimensions.get(constraint.targetType)) | ||
302 | availableMultiplicityCoefficients.addCoefficients(-constraint.lowerBound, | ||
303 | subtypeDimensions.get(constraint.targetType)) | ||
304 | val availableMultiplicity = availableMultiplicityCoefficients.toExpression | ||
305 | updatersBuilder.add( | ||
306 | new UnfinishedMultiplicityConstraintUpdater(constraint.relation.name, availableMultiplicity, | ||
307 | unfinishedMultiplicityMatcher, remainingInverseMultiplicityMatcher)) | ||
308 | } | ||
309 | if (constraint.constrainsUnrepairable) { | ||
310 | if (queries.unrepairableMultiplicityQuery === null) { | ||
311 | throw new IllegalArgumentException("Reference constraints need unrepairable multiplicity queries") | ||
312 | } | ||
313 | val unrepairableMultiplicityMatcher = queries.unrepairableMultiplicityQuery.getMatcher(queryEngine) | ||
314 | val targetTypeCardinality = typeBounds.get(constraint.targetType) | ||
315 | updatersBuilder.add( | ||
316 | new UnrepairableMultiplicityConstraintUpdater(constraint.relation.name, targetTypeCardinality, | ||
317 | unrepairableMultiplicityMatcher)) | ||
318 | } | ||
279 | } | 319 | } |
280 | 320 | ||
281 | private def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { | 321 | private def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { |
@@ -410,4 +450,40 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
410 | matcher.countMatches(match) != 0 | 450 | matcher.countMatches(match) != 0 |
411 | } | 451 | } |
412 | } | 452 | } |
453 | |||
454 | @FinalFieldsConstructor | ||
455 | static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { | ||
456 | val String name | ||
457 | val LinearBoundedExpression availableMultiplicityExpression | ||
458 | val ViatraQueryMatcher<? extends IPatternMatch> unfinishedMultiplicityMatcher | ||
459 | val ViatraQueryMatcher<? extends IPatternMatch> remainingInverseMultiplicityMatcher | ||
460 | |||
461 | override update(PartialInterpretation p) { | ||
462 | val unfinishedMultiplicity = unfinishedMultiplicityMatcher.getCalculatedMultiplicity(p) | ||
463 | if (unfinishedMultiplicity === null) { | ||
464 | throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) | ||
465 | } | ||
466 | val remainingInverseMultiplicity = remainingInverseMultiplicityMatcher.getCalculatedMultiplicity(p) | ||
467 | if (remainingInverseMultiplicity === null) { | ||
468 | throw new IllegalArgumentException("Remaining inverse multiplicity is missing for " + name) | ||
469 | } | ||
470 | val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity | ||
471 | availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) | ||
472 | } | ||
473 | } | ||
474 | |||
475 | @FinalFieldsConstructor | ||
476 | static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { | ||
477 | val String name | ||
478 | val LinearBoundedExpression targetCardinalityExpression | ||
479 | val ViatraQueryMatcher<? extends IPatternMatch> unrepairableMultiplicityMatcher | ||
480 | |||
481 | override update(PartialInterpretation p) { | ||
482 | val value = unrepairableMultiplicityMatcher.getCalculatedMultiplicity(p) | ||
483 | if (value === null) { | ||
484 | throw new IllegalArgumentException("Unrepairable multiplicity is missing for " + name) | ||
485 | } | ||
486 | targetCardinalityExpression.tightenLowerBound(value) | ||
487 | } | ||
488 | } | ||
413 | } | 489 | } |