6 files changed, 506 insertions, 83 deletions

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<Scope, LinearBoundedExpression> scopeBounds
-        val LinearConstraint topLevelBounds
+        val LinearBoundedExpression topLevelBounds
+        val Polyhedron polyhedron
         val PolyhedronSaturationOperator operator
+        List<RelationConstraintUpdater> updaters = emptyList
 
-        new(PartialInterpretation p, Set<? extends Type> possibleNewDynamicTypes, PolyhedronSolver solver) {
+        new(PartialInterpretation p, Set<? extends Type> possibleNewDynamicTypes,
+                Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> 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<Type, Dimension> 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 <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> 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<Type, Dimension> instanceCounts
+                Map<Type, Map<Dimension, Integer>> subtypeDimensions
+                Map<Map<Dimension, Integer>, LinearBoundedExpression> expressionsCache
+                Map<Type, LinearBoundedExpression> typeBounds
+                int infinity
+                ViatraQueryEngine queryEngine
+                ImmutableList.Builder<RelationConstraintUpdater> updatersBuilder
+
+                Map<Scope, LinearBoundedExpression> scopeBounds
+                LinearBoundedExpression topLevelBounds
+                Polyhedron polyhedron
+                List<RelationConstraintUpdater> updaters
+
+                def buildPolyhedron(Set<? extends Type> 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<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> 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<Map.Entry<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries>> 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<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> 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<Dimension, Integer> 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<ViatraQueryMatcher<? extends IPatternMatch>> unfinishedMultiplicitiesMatchers
+                val List<ViatraQueryMatcher<? extends IPatternMatch>> 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<LinearBoundedExpression> 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<RelationMultiplicityConstraint> 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:
+                                <Relation>emptySet
+                        case 1:
+                                ImmutableSet.copyOf(problem.containmentHierarchies.head.containmentRelations)
+                        default:
+                                throw new IllegalArgumentException("Only a single containment hierarchy is supported")
+                }
+                val inverseRelations = new HashMap<Relation, Relation>
+                val lowerMultiplicities = new HashMap<Relation, Integer>
+                val upperMultiplicities = new HashMap<Relation, Integer>
+                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<PartialTypeInterpratation, Scope> 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;
+        }
+}