From 64138e8d91bc8d7bb54d9b042f872b43550dec16 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 24 Jul 2019 10:59:02 +0200 Subject: Cardinality propagator WIP --- .../MultiplicityGoalConstraintCalculator.xtend | 46 +++ .../cardinality/PolyhedronScopePropagator.xtend | 355 +++++++++++++++++---- .../cardinality/PolyhedronSolver.xtend | 32 +- .../cardinality/RelationConstraintCalculator.xtend | 133 ++++++++ .../logic2viatra/cardinality/ScopePropagator.xtend | 5 - .../cardinality/ScopePropagatorStrategy.java | 18 ++ 6 files changed, 506 insertions(+), 83 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java (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/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend new file mode 100644 index 00000000..86a59aa1 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend @@ -0,0 +1,46 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import org.eclipse.emf.common.notify.Notifier +import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.emf.EMFScope + +class MultiplicityGoalConstraintCalculator { + val String targetRelationName; + val IQuerySpecification querySpecification; + var ViatraQueryMatcher matcher; + + new(String targetRelationName, IQuerySpecification querySpecification) { + this.targetRelationName = targetRelationName + this.querySpecification = querySpecification + this.matcher = null + } + + new(MultiplicityGoalConstraintCalculator other) { + this.targetRelationName = other.targetRelationName + this.querySpecification = other.querySpecification + this.matcher = null + } + + def getName() { + targetRelationName + } + + def init(Notifier notifier) { + val engine = ViatraQueryEngine.on(new EMFScope(notifier)) + matcher = querySpecification.getMatcher(engine) + } + + def calculateValue() { + var res = 0 + val allMatches = this.matcher.allMatches + for(match : allMatches) { + //println(targetRelationName+ " missing multiplicity: "+match.get(3)) + val missingMultiplicity = match.get(2) as Integer + res += missingMultiplicity + } + //println(targetRelationName+ " all missing multiplicities: "+res) + return res + } +} 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 cebd89da..4f0c8f20 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 @@ -2,90 +2,60 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality import com.google.common.collect.ImmutableList import com.google.common.collect.ImmutableMap +import com.google.common.collect.Maps import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnifinishedMultiplicityQueries import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope import java.util.ArrayDeque +import java.util.ArrayList import java.util.HashMap import java.util.HashSet +import java.util.List import java.util.Map import java.util.Set +import javax.naming.OperationNotSupportedException +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.emf.EMFScope +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor class PolyhedronScopePropagator extends ScopePropagator { val Map scopeBounds - val LinearConstraint topLevelBounds + val LinearBoundedExpression topLevelBounds + val Polyhedron polyhedron val PolyhedronSaturationOperator operator + List updaters = emptyList - new(PartialInterpretation p, Set possibleNewDynamicTypes, PolyhedronSolver solver) { + new(PartialInterpretation p, Set possibleNewDynamicTypes, + Map unfinishedMultiplicityQueries, + PolyhedronSolver solver, boolean propagateRelations) { super(p) - val instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] - val primitiveDimensions = new HashMap - val constraintsBuilder = ImmutableList.builder - val scopeBoundsBuilder = ImmutableMap.builder - // Dimensions for instantiable types were created according to the type analysis, - // but for any possible primitive types, we create them on demand, - // as there is no Type directly associated with a PartialPrimitiveInterpretation. - // Below we will assume that each PartialTypeInterpretation has at most one Scope. - for (scope : p.scopes) { - switch (targetTypeInterpretation : scope.targetTypeInterpretation) { - PartialPrimitiveInterpretation: { - val dimension = primitiveDimensions.computeIfAbsent(targetTypeInterpretation) [ interpretation | - new Dimension(interpretation.eClass.name, 0, null) - ] - scopeBoundsBuilder.put(scope, dimension) - } - PartialComplexTypeInterpretation: { - val complexType = targetTypeInterpretation.interpretationOf - val dimensions = findSubtypeDimensions(complexType, instanceCounts) - switch (dimensions.size) { - case 0: - if (scope.minNewElements > 0) { - throw new IllegalArgumentException("Found scope for " + complexType.name + - ", but the type cannot be instantiated") - } - case 1: - scopeBoundsBuilder.put(scope, dimensions.head) - default: { - val constraint = new LinearConstraint(dimensions.toInvertedMap[1], null, null) - constraintsBuilder.add(constraint) - scopeBoundsBuilder.put(scope, constraint) - } - } - } - default: - throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + targetTypeInterpretation) - } - } - val allDimensions = ImmutableList.builder.addAll(instanceCounts.values).addAll(primitiveDimensions.values).build - scopeBounds = scopeBoundsBuilder.build - topLevelBounds = new LinearConstraint(allDimensions.toInvertedMap[1], null, null) - constraintsBuilder.add(topLevelBounds) - val expressionsToSaturate = ImmutableList.builder.addAll(scopeBounds.values).add(topLevelBounds).build - val polyhedron = new Polyhedron(allDimensions, constraintsBuilder.build, expressionsToSaturate) + val builder = new PolyhedronBuilder(p) + builder.buildPolyhedron(possibleNewDynamicTypes) + scopeBounds = builder.scopeBounds + topLevelBounds = builder.topLevelBounds + polyhedron = builder.polyhedron operator = solver.createSaturationOperator(polyhedron) - } - - private def findSubtypeDimensions(Type type, Map instanceCounts) { - val subtypes = new HashSet - val dimensions = new HashSet - val stack = new ArrayDeque - stack.addLast(type) - while (!stack.empty) { - val subtype = stack.removeLast - if (subtypes.add(subtype)) { - val dimension = instanceCounts.get(subtype) - if (dimension !== null) { - dimensions.add(dimension) - } - stack.addAll(subtype.subtypes) + if (propagateRelations) { + propagateAllScopeConstraints() + val maximumNumberOfNewNodes = topLevelBounds.upperBound + if (maximumNumberOfNewNodes === null) { + 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") } + builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, maximumNumberOfNewNodes) + updaters = builder.updaters } - dimensions } override void propagateAllScopeConstraints() { + resetBounds() populatePolyhedronFromScope() val result = operator.saturate() if (result == PolyhedronSaturationResult.EMPTY) { @@ -96,21 +66,36 @@ class PolyhedronScopePropagator extends ScopePropagator { super.propagateAllScopeConstraints() } } + // println(polyhedron) + } + + def resetBounds() { + for (dimension : polyhedron.dimensions) { + dimension.lowerBound = 0 + dimension.upperBound = null + } + for (constraint : polyhedron.constraints) { + constraint.lowerBound = null + constraint.upperBound = null + } } private def populatePolyhedronFromScope() { - topLevelBounds.lowerBound = partialInterpretation.minNewElements + topLevelBounds.tightenLowerBound(partialInterpretation.minNewElements) if (partialInterpretation.maxNewElements >= 0) { - topLevelBounds.upperBound = partialInterpretation.maxNewElements + topLevelBounds.tightenUpperBound(partialInterpretation.maxNewElements) } for (pair : scopeBounds.entrySet) { val scope = pair.key val bounds = pair.value - bounds.lowerBound = scope.minNewElements + bounds.tightenLowerBound(scope.minNewElements) if (scope.maxNewElements >= 0) { - bounds.upperBound = scope.maxNewElements + bounds.tightenUpperBound(scope.maxNewElements) } } + for (updater : updaters) { + updater.update(partialInterpretation) + } } private def populateScopesFromPolyhedron() { @@ -151,4 +136,242 @@ class PolyhedronScopePropagator extends ScopePropagator { throw new IllegalArgumentException("Infinite upper bound: " + bounds) } } + + private static def getCalculatedMultiplicity(ViatraQueryMatcher matcher, + PartialInterpretation p) { + val match = matcher.newEmptyMatch + match.set(0, p.problem) + match.set(1, p) + val iterator = matcher.streamAllMatches(match).iterator + if (!iterator.hasNext) { + return null + } + val value = iterator.next.get(2) as Integer + if (iterator.hasNext) { + throw new IllegalArgumentException("Multiplicity calculation query has more than one match") + } + value + } + + @FinalFieldsConstructor + private static class PolyhedronBuilder { + static val INFINITY_SCALE = 10 + + val PartialInterpretation p + + Map instanceCounts + Map> subtypeDimensions + Map, LinearBoundedExpression> expressionsCache + Map typeBounds + int infinity + ViatraQueryEngine queryEngine + ImmutableList.Builder updatersBuilder + + Map scopeBounds + LinearBoundedExpression topLevelBounds + Polyhedron polyhedron + List updaters + + def buildPolyhedron(Set possibleNewDynamicTypes) { + instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] + val types = p.problem.types + expressionsCache = Maps.newHashMapWithExpectedSize(types.size) + subtypeDimensions = types.toInvertedMap[findSubtypeDimensions.toInvertedMap[1]] + typeBounds = ImmutableMap.copyOf(subtypeDimensions.mapValues[toExpression]) + scopeBounds = buildScopeBounds + topLevelBounds = instanceCounts.values.toInvertedMap[1].toExpression + val dimensions = ImmutableList.copyOf(instanceCounts.values) + val expressionsToSaturate = ImmutableList.copyOf(scopeBounds.values) + polyhedron = new Polyhedron(dimensions, new ArrayList, expressionsToSaturate) + addCachedConstraintsToPolyhedron() + } + + def buildMultiplicityConstraints( + Map constraints, + int maximumNuberOfNewNodes) { + infinity = maximumNuberOfNewNodes * INFINITY_SCALE + queryEngine = ViatraQueryEngine.on(new EMFScope(p)) + updatersBuilder = ImmutableList.builder + for (pair : constraints.entrySet.filter[key.containment].groupBy[key.targetType].entrySet) { + buildContainmentConstraints(pair.key, pair.value) + } + for (pair : constraints.entrySet) { + val constraint = pair.key + if (!constraint.containment) { + buildNonContainmentConstraints(constraint, pair.value) + } + } + updaters = updatersBuilder.build + addCachedConstraintsToPolyhedron() + } + + private def addCachedConstraintsToPolyhedron() { + val constraints = new HashSet + constraints.addAll(expressionsCache.values.filter(LinearConstraint)) + constraints.removeAll(polyhedron.constraints) + polyhedron.constraints.addAll(constraints) + } + + private def buildContainmentConstraints(Type containedType, + List> constraints) { + val typeCoefficients = subtypeDimensions.get(containedType) + val orphansLowerBoundCoefficients = new HashMap(typeCoefficients) + val orphansUpperBoundCoefficients = new HashMap(typeCoefficients) + val unfinishedMultiplicitiesMatchersBuilder = ImmutableList.builder + val remainingContentsQueriesBuilder = ImmutableList.builder + for (pair : constraints) { + val constraint = pair.key + val containerCoefficients = subtypeDimensions.get(constraint.sourceType) + if (constraint.isUpperBoundFinite) { + orphansLowerBoundCoefficients.addCoefficients(-constraint.upperBound, containerCoefficients) + } else { + orphansLowerBoundCoefficients.addCoefficients(-infinity, containerCoefficients) + } + orphansUpperBoundCoefficients.addCoefficients(-constraint.lowerBound, containerCoefficients) + val queries = pair.value + if (constraint.constrainsUnfinished) { + if (queries.unfinishedMultiplicityQuery === null) { + throw new IllegalArgumentException( + "Containment constraints need unfinished multiplicity queries") + } + unfinishedMultiplicitiesMatchersBuilder.add( + queries.unfinishedMultiplicityQuery.getMatcher(queryEngine)) + } + if (queries.remainingContentsQuery === null) { + throw new IllegalArgumentException("Containment constraints need remaining contents queries") + } + remainingContentsQueriesBuilder.add(queries.remainingContentsQuery.getMatcher(queryEngine)) + } + val orphanLowerBound = orphansLowerBoundCoefficients.toExpression + val orphanUpperBound = orphansUpperBoundCoefficients.toExpression + val updater = new ContainmentConstraintUpdater(containedType.name, orphanLowerBound, orphanUpperBound, + unfinishedMultiplicitiesMatchersBuilder.build, remainingContentsQueriesBuilder.build) + updatersBuilder.add(updater) + } + + private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, + UnifinishedMultiplicityQueries queries) { + } + + private def addCoefficients(Map accumulator, int scale, Map a) { + for (pair : a.entrySet) { + val dimension = pair.key + val currentValue = accumulator.get(pair.key) ?: 0 + val newValue = currentValue + scale * pair.value + if (newValue == 0) { + accumulator.remove(dimension) + } else { + accumulator.put(dimension, newValue) + } + } + } + + private def findSubtypeDimensions(Type type) { + val subtypes = new HashSet + val dimensions = new HashSet + val stack = new ArrayDeque + stack.addLast(type) + while (!stack.empty) { + val subtype = stack.removeLast + if (subtypes.add(subtype)) { + val dimension = instanceCounts.get(subtype) + if (dimension !== null) { + dimensions.add(dimension) + } + stack.addAll(subtype.subtypes) + } + } + dimensions + } + + private def toExpression(Map coefficients) { + expressionsCache.computeIfAbsent(coefficients) [ c | + if (c.size == 1 && c.entrySet.head.value == 1) { + c.entrySet.head.key + } else { + new LinearConstraint(c, null, null) + } + ] + } + + private def buildScopeBounds() { + val scopeBoundsBuilder = ImmutableMap.builder + for (scope : p.scopes) { + switch (targetTypeInterpretation : scope.targetTypeInterpretation) { + PartialPrimitiveInterpretation: + throw new OperationNotSupportedException("Primitive type scopes are not yet implemented") + PartialComplexTypeInterpretation: { + val complexType = targetTypeInterpretation.interpretationOf + val typeBound = typeBounds.get(complexType) + if (typeBound === null) { + if (scope.minNewElements > 0) { + throw new IllegalArgumentException("Found scope for " + complexType.name + + ", but the type cannot be instantiated") + } + } else { + scopeBoundsBuilder.put(scope, typeBound) + } + } + default: + throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + + targetTypeInterpretation) + } + } + scopeBoundsBuilder.build + } + } + + private static interface RelationConstraintUpdater { + def void update(PartialInterpretation p) + } + + @FinalFieldsConstructor + static class ContainmentConstraintUpdater implements RelationConstraintUpdater { + val String name + val LinearBoundedExpression orphansLowerBound + val LinearBoundedExpression orphansUpperBound + val List> unfinishedMultiplicitiesMatchers + val List> remainingContentsQueries + + override update(PartialInterpretation p) { + tightenLowerBound(p) + tightenUpperBound(p) + } + + private def tightenLowerBound(PartialInterpretation p) { + var int sum = 0 + for (matcher : remainingContentsQueries) { + val value = matcher.getCalculatedMultiplicity(p) + if (value === null) { + throw new IllegalArgumentException("Remaining contents count is missing for " + name) + } + if (value == -1) { + // Infinite upper bound, no need to tighten. + return + } + sum += value + } + orphansLowerBound.tightenUpperBound(sum) + } + + private def tightenUpperBound(PartialInterpretation p) { + var int sum = 0 + for (matcher : unfinishedMultiplicitiesMatchers) { + val value = matcher.getCalculatedMultiplicity(p) + if (value === null) { + throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) + } + sum += value + } + orphansUpperBound.tightenLowerBound(sum) + } + } + + @FinalFieldsConstructor + static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { + + override update(PartialInterpretation p) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend index 08bf25b9..9c6cb82e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend @@ -52,18 +52,14 @@ class Polyhedron { val List expressionsToSaturate override toString() ''' - Dimensions: - «FOR dimension : dimensions» - «dimension» - «ENDFOR» - Constraints: - «FOR constraint : constraints» - «constraint» - «ENDFOR» -««« Saturate: -««« «FOR expression : expressionsToSaturate» -««« «IF expression instanceof Dimension»dimension«ELSEIF expression instanceof LinearConstraint»constraint«ELSE»unknown«ENDIF» «expression» -««« «ENDFOR» + Dimensions: + «FOR dimension : dimensions» + «dimension» + «ENDFOR» + Constraints: + «FOR constraint : constraints» + «constraint» + «ENDFOR» ''' } @@ -72,6 +68,18 @@ class Polyhedron { abstract class LinearBoundedExpression { var Integer lowerBound var Integer upperBound + + def void tightenLowerBound(Integer tighterBound) { + if (lowerBound === null || (tighterBound !== null && lowerBound < tighterBound)) { + lowerBound = tighterBound + } + } + + def void tightenUpperBound(Integer tighterBound) { + if (upperBound === null || (tighterBound !== null && upperBound > tighterBound)) { + upperBound = tighterBound + } + } } @Accessors diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend new file mode 100644 index 00000000..ffa9e6e6 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend @@ -0,0 +1,133 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import com.google.common.collect.ImmutableList +import com.google.common.collect.ImmutableSet +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import java.util.HashMap +import java.util.List +import org.eclipse.xtend.lib.annotations.Data + +@Data +class RelationConstraints { + val List multiplicityConstraints +} + +@Data +class RelationMultiplicityConstraint { + Relation relation + boolean containment + boolean container + int lowerBound + int upperBound + int inverseUpperBound + + def isUpperBoundFinite() { + upperBound >= 0 + } + + private def isInverseUpperBoundFinite() { + inverseUpperBound >= 0 + } + + private def canHaveMultipleSourcesPerTarget() { + inverseUpperBound != 1 + } + + def constrainsUnfinished() { + lowerBound >= 1 && (!container || lowerBound >= 2) + } + + def constrainsUnrepairable() { + constrainsUnfinished && canHaveMultipleSourcesPerTarget + } + + def constrainsRemainingInverse() { + !containment && inverseUpperBoundFinite + } + + def constrainsRemainingContents() { + containment + } + + def isActive() { + constrainsUnfinished || constrainsUnrepairable || constrainsRemainingInverse || constrainsRemainingContents + } + + def getSourceType() { + getParamType(0) + } + + def getTargetType() { + getParamType(1) + } + + private def getParamType(int i) { + val parameters = relation.parameters + if (i < parameters.size) { + val firstParam = parameters.get(i) + if (firstParam instanceof ComplexTypeReference) { + return firstParam.referred + } + } + throw new IllegalArgumentException("Constraint with unknown source type") + } +} + +class RelationConstraintCalculator { + def calculateRelationConstraints(LogicProblem problem) { + val containmentRelations = switch (problem.containmentHierarchies.size) { + case 0: + emptySet + case 1: + ImmutableSet.copyOf(problem.containmentHierarchies.head.containmentRelations) + default: + throw new IllegalArgumentException("Only a single containment hierarchy is supported") + } + val inverseRelations = new HashMap + val lowerMultiplicities = new HashMap + val upperMultiplicities = new HashMap + for (relation : problem.relations) { + lowerMultiplicities.put(relation, 0) + upperMultiplicities.put(relation, -1) + } + for (annotation : problem.annotations) { + switch (annotation) { + InverseRelationAssertion: { + inverseRelations.put(annotation.inverseA, annotation.inverseB) + inverseRelations.put(annotation.inverseB, annotation.inverseA) + } + LowerMultiplicityAssertion: + lowerMultiplicities.put(annotation.relation, annotation.lower) + UpperMultiplicityAssertion: + upperMultiplicities.put(annotation.relation, annotation.upper) + } + } + val multiplicityConstraintsBuilder = ImmutableList.builder() + for (relation : problem.relations) { + val containment = containmentRelations.contains(relation) + val lowerMultiplicity = lowerMultiplicities.get(relation) + val upperMultiplicity = upperMultiplicities.get(relation) + var container = false + var inverseUpperMultiplicity = -1 + val inverseRelation = inverseRelations.get(relation) + if (inverseRelation !== null) { + inverseUpperMultiplicity = upperMultiplicities.get(relation) + container = containmentRelations.contains(inverseRelation) + } + val constraint = new RelationMultiplicityConstraint(relation, containment, container, lowerMultiplicity, + upperMultiplicity, inverseUpperMultiplicity) + if (constraint.isActive) { + if (relation.parameters.size != 2) { + throw new IllegalArgumentException('''Relation «relation.name» has multiplicity or containment constraints, but it is not binary''') + } + multiplicityConstraintsBuilder.add(constraint) + } + } + new RelationConstraints(multiplicityConstraintsBuilder.build) + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend index f0494214..3b442cd3 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend @@ -10,11 +10,6 @@ import java.util.Map import java.util.Set import org.eclipse.xtend.lib.annotations.Accessors -enum ScopePropagatorStrategy { - BasicTypeHierarchy, - PolyhedralTypeHierarchy -} - class ScopePropagator { @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation Map type2Scope diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java new file mode 100644 index 00000000..b1c5a658 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java @@ -0,0 +1,18 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality; + +public enum ScopePropagatorStrategy { + BasicTypeHierarchy, + + PolyhedralTypeHierarchy, + + PolyhedralRelations { + @Override + public boolean requiresUpperBoundIndexing() { + return true; + } + }; + + public boolean requiresUpperBoundIndexing() { + return false; + } +} -- cgit v1.2.3-70-g09d2