From 4cb0aa5a0b9adac2bb8d4a995be015651bdd5628 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 30 Jul 2019 18:57:01 +0200 Subject: Polyhedron scope propagator for non-containment references --- .../cardinality/PolyhedronScopePropagator.xtend | 80 +++++++++++++++++++++- 1 file changed, 78 insertions(+), 2 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality') 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 { throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") } if (maximumNumberOfNewNodes <= 0) { - throw new IllegalStateException("Maximum number of new nodes is negative") + throw new IllegalStateException("Maximum number of new nodes is not positive") } builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, maximumNumberOfNewNodes) @@ -65,7 +65,7 @@ class PolyhedronScopePropagator extends ScopePropagator { val result = operator.saturate() // println(polyhedron) if (result == PolyhedronSaturationResult.EMPTY) { - throw new IllegalStateException("Scope bounds cannot be satisfied") + setScopesInvalid() } else { populateScopesFromPolyhedron() if (result != PolyhedronSaturationResult.SATURATED) { @@ -146,6 +146,15 @@ class PolyhedronScopePropagator extends ScopePropagator { } } + private def setScopesInvalid() { + partialInterpretation.minNewElements = Integer.MAX_VALUE + partialInterpretation.maxNewElements = 0 + for (scope : partialInterpretation.scopes) { + scope.minNewElements = Integer.MAX_VALUE + scope.maxNewElements = 0 + } + } + private static def getCalculatedMultiplicity(ViatraQueryMatcher matcher, PartialInterpretation p) { val match = matcher.newEmptyMatch @@ -276,6 +285,37 @@ class PolyhedronScopePropagator extends ScopePropagator { private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, UnifinishedMultiplicityQueries queries) { + if (constraint.constrainsRemainingInverse) { + if (queries.unfinishedMultiplicityQuery === null) { + throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries") + } + val unfinishedMultiplicityMatcher = queries.unfinishedMultiplicityQuery.getMatcher(queryEngine) + if (queries.remainingInverseMultiplicityQuery === null) { + throw new IllegalArgumentException( + "Reference constraints need remaining inverse multiplicity queries") + } + val remainingInverseMultiplicityMatcher = queries.remainingInverseMultiplicityQuery.getMatcher( + queryEngine) + val availableMultiplicityCoefficients = new HashMap + availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, + subtypeDimensions.get(constraint.targetType)) + availableMultiplicityCoefficients.addCoefficients(-constraint.lowerBound, + subtypeDimensions.get(constraint.targetType)) + val availableMultiplicity = availableMultiplicityCoefficients.toExpression + updatersBuilder.add( + new UnfinishedMultiplicityConstraintUpdater(constraint.relation.name, availableMultiplicity, + unfinishedMultiplicityMatcher, remainingInverseMultiplicityMatcher)) + } + if (constraint.constrainsUnrepairable) { + if (queries.unrepairableMultiplicityQuery === null) { + throw new IllegalArgumentException("Reference constraints need unrepairable multiplicity queries") + } + val unrepairableMultiplicityMatcher = queries.unrepairableMultiplicityQuery.getMatcher(queryEngine) + val targetTypeCardinality = typeBounds.get(constraint.targetType) + updatersBuilder.add( + new UnrepairableMultiplicityConstraintUpdater(constraint.relation.name, targetTypeCardinality, + unrepairableMultiplicityMatcher)) + } } private def addCoefficients(Map accumulator, int scale, Map a) { @@ -410,4 +450,40 @@ class PolyhedronScopePropagator extends ScopePropagator { matcher.countMatches(match) != 0 } } + + @FinalFieldsConstructor + static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { + val String name + val LinearBoundedExpression availableMultiplicityExpression + val ViatraQueryMatcher unfinishedMultiplicityMatcher + val ViatraQueryMatcher remainingInverseMultiplicityMatcher + + override update(PartialInterpretation p) { + val unfinishedMultiplicity = unfinishedMultiplicityMatcher.getCalculatedMultiplicity(p) + if (unfinishedMultiplicity === null) { + throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) + } + val remainingInverseMultiplicity = remainingInverseMultiplicityMatcher.getCalculatedMultiplicity(p) + if (remainingInverseMultiplicity === null) { + throw new IllegalArgumentException("Remaining inverse multiplicity is missing for " + name) + } + val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity + availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) + } + } + + @FinalFieldsConstructor + static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { + val String name + val LinearBoundedExpression targetCardinalityExpression + val ViatraQueryMatcher unrepairableMultiplicityMatcher + + override update(PartialInterpretation p) { + val value = unrepairableMultiplicityMatcher.getCalculatedMultiplicity(p) + if (value === null) { + throw new IllegalArgumentException("Unrepairable multiplicity is missing for " + name) + } + targetCardinalityExpression.tightenLowerBound(value) + } + } } -- cgit v1.2.3-54-g00ecf