Cardinality propagator WIP

16 files changed, 859 insertions, 337 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
index 0ceb5b2e..3a99d3bf 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
@@ -5,7 +5,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem

 import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns

@@ -61,6 +63,7 @@ class ModelGenerationMethodProvider {
         val PatternProvider patternProvider = new PatternProvider

         val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider

         val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider

+        val relationConstraintCalculator = new RelationConstraintCalculator

 

         def ModelGenerationMethod createModelGenerationMethod(

                 LogicProblem logicProblem,

@@ -77,8 +80,9 @@ class ModelGenerationMethodProvider {
                 val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery).

                         map[it.patternPQuery as PQuery].toSet

 

+                val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem)

                 val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries,

-                        workspace, typeInferenceMethod, writeFiles)

+                        workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles)

                 val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries)

                 scopePropagator.propagateAllScopeConstraints

                 val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>>

@@ -117,10 +121,12 @@ class ModelGenerationMethodProvider {
                 switch (scopePropagatorStrategy) {

                         case BasicTypeHierarchy:

                                 new ScopePropagator(emptySolution)

-                        case PolyhedralTypeHierarchy: {

+                        case PolyhedralTypeHierarchy,

+                        case PolyhedralRelations: {

                                 val types = queries.refineObjectQueries.keySet.map[newType].toSet

                                 val solver = new CbcPolyhedronSolver

-                                new PolyhedronScopePropagator(emptySolution, types, solver)

+                                new PolyhedronScopePropagator(emptySolution, types, queries.multiplicityConstraintQueries, solver,

+                                        scopePropagatorStrategy.requiresUpperBoundIndexing)

                         }

                         default:

                                 throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy)

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
index 4b9629df..86a59aa1 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
@@ -1,4 +1,4 @@
-package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra

+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality

 

 import org.eclipse.emf.common.notify.Notifier

 import org.eclipse.viatra.query.runtime.api.IQuerySpecification

@@ -37,10 +37,10 @@ class MultiplicityGoalConstraintCalculator {
                 val allMatches = this.matcher.allMatches

                 for(match : allMatches) {

                         //println(targetRelationName+ " missing multiplicity: "+match.get(3))

-                        val missingMultiplicity = match.get(4) as Integer

+                        val missingMultiplicity = match.get(2) as Integer

                         res += missingMultiplicity

                 }

                 //println(targetRelationName+ " all missing multiplicities: "+res)

                 return res

         }

-}
\ No newline at end of file
+}
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;
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
index 24b3e870..1b0db90e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
@@ -1,7 +1,6 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns

 

 import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion

-import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference

@@ -17,6 +16,7 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Transform
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation

 import java.util.HashMap

 import java.util.Map

@@ -26,22 +26,26 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
 import org.eclipse.xtend.lib.annotations.Accessors

 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy

 

 class PatternGenerator {

-        @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this)

-        @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer(this)

-        @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer(this)

+        @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this)

+        @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer(

+                this)

+        @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer(

+                this)

         @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this)

         @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this)

-        @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer = new UnfinishedIndexer(this)

-        @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this)

-        @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this)

-        

-        public new(TypeInferenceMethod typeInferenceMethod) {

-                if(typeInferenceMethod == TypeInferenceMethod.Generic) {

+        @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer

+        @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator // = new RefinementGenerator(this)

+        @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(

+                this)

+

+        new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) {

+                if (typeInferenceMethod == TypeInferenceMethod.Generic) {

                         this.typeIndexer = new GenericTypeIndexer(this)

                         this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this)

-                } else if(typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) {

+                } else if (typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) {

                         this.typeIndexer = new TypeIndexerWithPreliminaryTypeAnalysis(this)

                         this.typeRefinementGenerator = new TypeRefinementWithPreliminaryTypeAnalysis(this)

                 } else {

@@ -49,112 +53,100 @@ class PatternGenerator {
                         this.typeRefinementGenerator = null

                         throw new IllegalArgumentException('''Unknown type indexing technique : «typeInferenceMethod.name»''')

                 }

+                this.unfinishedIndexer = new UnfinishedIndexer(this, scopePropagatorStrategy.requiresUpperBoundIndexing)

         }

-        

-        public def requiresTypeAnalysis() {

+

+        def requiresTypeAnalysis() {

                 typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis

         }

-        

-        public dispatch def CharSequence referRelation(

-                RelationDeclaration referred,

-                String sourceVariable,

-                String targetVariable,

-                Modality modality,

-                Map<String,PQuery> fqn2PQuery)

-        {

-                return this.relationDeclarationIndexer.referRelation(referred,sourceVariable,targetVariable,modality)

+

+        dispatch def CharSequence referRelation(RelationDeclaration referred, String sourceVariable, String targetVariable,

+                Modality modality, Map<String, PQuery> fqn2PQuery) {

+                return this.relationDeclarationIndexer.referRelation(referred, sourceVariable, targetVariable, modality)

         }

-        public dispatch def CharSequence referRelation(

-                RelationDefinition referred,

-                String sourceVariable,

-                String targetVariable,

-                Modality modality,

-                Map<String,PQuery> fqn2PQuery)

-        {

-                val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery)

-                return this.relationDefinitionIndexer.referPattern(pattern,#[sourceVariable,targetVariable],modality,true,false)

+

+        dispatch def CharSequence referRelation(RelationDefinition referred, String sourceVariable, String targetVariable,

+                Modality modality, Map<String, PQuery> fqn2PQuery) {

+                val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(

+                        fqn2PQuery)

+                return this.relationDefinitionIndexer.referPattern(pattern, #[sourceVariable, targetVariable], modality, true,

+                        false)

         }

-        

-        def public referRelationByName(EReference reference,

-                String sourceVariable,

-                String targetVariable,

-                Modality modality)

-        {

-                '''find «modality.name.toLowerCase»InRelation«canonizeName('''«reference.name» reference «reference.EContainingClass.name»''')

-                »(problem,interpretation,«sourceVariable»,«targetVariable»);'''

+

+        def referRelationByName(EReference reference, String sourceVariable, String targetVariable, Modality modality) {

+                '''find «modality.name.toLowerCase»InRelation«canonizeName('''«reference.name» reference «reference.EContainingClass.name»''')»(problem,interpretation,«sourceVariable»,«targetVariable»);'''

         }

-        

-        def public CharSequence referAttributeByName(EAttribute attribute,

-                String sourceVariable,

-                String targetVariable,

-                Modality modality)

-        {

-                '''find «modality.name.toLowerCase»InRelation«canonizeName('''«attribute.name» attribute «attribute.EContainingClass.name»''')

-                »(problem,interpretation,«sourceVariable»,«targetVariable»);'''

+

+        def CharSequence referAttributeByName(EAttribute attribute, String sourceVariable, String targetVariable,

+                Modality modality) {

+                '''find «modality.name.toLowerCase»InRelation«canonizeName('''«attribute.name» attribute «attribute.EContainingClass.name»''')»(problem,interpretation,«sourceVariable»,«targetVariable»);'''

         }

-        

-        public def canonizeName(String name) {

+

+        def canonizeName(String name) {

                 name.split(' ').join('_')

         }

-        

-        public def lowerMultiplicities(LogicProblem problem) {

-                problem.assertions.map[annotations].flatten.filter(LowerMultiplicityAssertion).filter[!it.relation.isDerived]

-        }

-        public def wfQueries(LogicProblem problem) {

-                problem.assertions.map[it.annotations]

-                        .flatten

-                        .filter(TransformedViatraWellformednessConstraint)

-                        .map[it.query]

+

+        def wfQueries(LogicProblem problem) {

+                problem.assertions.map[it.annotations].flatten.filter(TransformedViatraWellformednessConstraint).map[it.query]

         }

-        public def getContainments(LogicProblem p) {

+

+        def getContainments(LogicProblem p) {

                 return p.containmentHierarchies.head.containmentRelations

         }

-        public def getInverseRelations(LogicProblem p) {

+

+        def getInverseRelations(LogicProblem p) {

                 val inverseRelations = new HashMap

-                p.annotations.filter(InverseRelationAssertion).forEach[

-                        inverseRelations.put(it.inverseA,it.inverseB)

-                        inverseRelations.put(it.inverseB,it.inverseA)

+                p.annotations.filter(InverseRelationAssertion).forEach [

+                        inverseRelations.put(it.inverseA, it.inverseB)

+                        inverseRelations.put(it.inverseB, it.inverseA)

                 ]

                 return inverseRelations

         }

-        public def isRepresentative(Relation relation, Relation inverse) {

-                if(inverse == null) {

+

+        def isRepresentative(Relation relation, Relation inverse) {

+                if (inverse === null) {

                         return true

                 } else {

-                        relation.name.compareTo(inverse.name)<1

+                        relation.name.compareTo(inverse.name) < 1

                 }

         }

-        

-        public def isDerived(Relation relation) {

+

+        def isDerived(Relation relation) {

                 relation.annotations.exists[it instanceof DefinedByDerivedFeature]

         }

-        public def getDerivedDefinition(RelationDeclaration relation) {

+

+        def getDerivedDefinition(RelationDeclaration relation) {

                 relation.annotations.filter(DefinedByDerivedFeature).head.query

         }

-        

+

         private def allTypeReferences(LogicProblem problem) {

                 problem.eAllContents.filter(TypeReference).toIterable

         }

+

         protected def hasBoolean(LogicProblem problem) {

                 problem.allTypeReferences.exists[it instanceof BoolTypeReference]

         }

+

         protected def hasInteger(LogicProblem problem) {

                 problem.allTypeReferences.exists[it instanceof IntTypeReference]

         }

+

         protected def hasReal(LogicProblem problem) {

                 problem.allTypeReferences.exists[it instanceof RealTypeReference]

         }

+

         protected def hasString(LogicProblem problem) {

                 problem.allTypeReferences.exists[it instanceof StringTypeReference]

         }

-        

-        public def transformBaseProperties(

+

+        def transformBaseProperties(

                 LogicProblem problem,

                 PartialInterpretation emptySolution,

-                Map<String,PQuery> fqn2PQuery,

-                TypeAnalysisResult typeAnalysisResult

+                Map<String, PQuery> fqn2PQuery,

+                TypeAnalysisResult typeAnalysisResult,

+                RelationConstraints constraints

         ) {

-                

+

                 return '''

                         import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage"

                         import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"

@@ -188,7 +180,7 @@ class PatternGenerator {
                         

                         private pattern elementCloseWorld(element:DefinedElement) {

                                 PartialInterpretation.openWorldElements(i,element);

-                            PartialInterpretation.maxNewElements(i,0);

+                                PartialInterpretation.maxNewElements(i,0);

                         } or {

                                 Scope.targetTypeInterpretation(scope,interpretation);

                                 PartialTypeInterpratation.elements(interpretation,element);

@@ -221,7 +213,7 @@ class PatternGenerator {
                         //////////

                         // 1.1.1 primitive Type Indexers

                         //////////

-«««                  pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {

+                        «««                  pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {

 «««                          find interpretation(problem,interpretation);

 «««                          PartialInterpretation.booleanelements(interpretation,element);

 «««                  }

@@ -279,7 +271,7 @@ class PatternGenerator {
                         //////////

                         // 3.1 Unfinishedness Measured by Multiplicity

                         //////////

-                        «unfinishedIndexer.generateUnfinishedMultiplicityQueries(problem,fqn2PQuery)»

+                        «unfinishedIndexer.generateUnfinishedMultiplicityQueries(constraints.multiplicityConstraints,fqn2PQuery)»

                         

                         //////////

                         // 3.2 Unfinishedness Measured by WF Queries

@@ -302,6 +294,6 @@ class PatternGenerator {
                         // 4.3 Relation refinement

                         //////////

                         «relationRefinementGenerator.generateRefineReference(problem)»

-                        '''

+                '''

         }

 }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
index e87f52af..90f79810 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
@@ -10,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStati
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation

 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace

@@ -23,78 +25,96 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
 import org.eclipse.xtend.lib.annotations.Data

 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy

 

-@Data class GeneratedPatterns {

-        public Map<Relation,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries

-        public Map<Relation,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries

-        public Map<Relation,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedMulticiplicityQueries

-        public Map<ObjectCreationPrecondition,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries

-        public Map<? extends Type,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries

-        public Map<Pair<RelationDeclaration, Relation>,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries

+@Data

+class GeneratedPatterns {

+        public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries

+        public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries

+        public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries

+        public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedMulticiplicityQueries

+        public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries

+        public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries

+        public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries

         public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries

         public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries

 }

 

-@Data class ModalPatternQueries {

+@Data

+class ModalPatternQueries {

         val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayQuery

         val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustQuery

         val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentQuery

 }

 

+@Data

+class UnifinishedMultiplicityQueries {

+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unfinishedMultiplicityQuery

+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unrepairableMultiplicityQuery

+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingInverseMultiplicityQuery

+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingContentsQuery

+}

+

 class PatternProvider {

-        

+

         val TypeAnalysis typeAnalysis = new TypeAnalysis

-        

-        public def generateQueries(

-                LogicProblem problem,

-                PartialInterpretation emptySolution,

-                ModelGenerationStatistics statistics,

-                Set<PQuery> existingQueries,

-                ReasonerWorkspace workspace,

-                TypeInferenceMethod typeInferenceMethod,

-                boolean writeToFile)

-        {

+

+        def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics,

+                Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod,

+                ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, boolean writeToFile) {

                 val fqn2Query = existingQueries.toMap[it.fullyQualifiedName]

-                val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod)

-                val typeAnalysisResult = if(patternGenerator.requiresTypeAnalysis) {

-                        val startTime = System.nanoTime

-                        val result = typeAnalysis.performTypeAnalysis(problem,emptySolution)

-                        val typeAnalysisTime = System.nanoTime - startTime

-                        statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime

-                        result

-                } else {

-                        null

-                }

-                val baseIndexerFile = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult)

-                if(writeToFile) {

-                        workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile)

+                val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy)

+                val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) {

+                                val startTime = System.nanoTime

+                                val result = typeAnalysis.performTypeAnalysis(problem, emptySolution)

+                                val typeAnalysisTime = System.nanoTime - startTime

+                                statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime

+                                result

+                        } else {

+                                null

+                        }

+                val baseIndexerFile = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query,

+                        typeAnalysisResult, relationConstraints)

+                if (writeToFile) {

+                        workspace.writeText('''generated3valued.vql_deactivated''', baseIndexerFile)

                 }

                 val ParseUtil parseUtil = new ParseUtil

                 val generatedQueries = parseUtil.parse(baseIndexerFile)

-                val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,generatedQueries);

+                val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult,

+                        relationConstraints, generatedQueries)

                 return runtimeQueries

         }

-        

+

         private def GeneratedPatterns calclulateRuntimeQueries(

                 PatternGenerator patternGenerator,

                 LogicProblem problem,

                 PartialInterpretation emptySolution,

                 TypeAnalysisResult typeAnalysisResult,

+                RelationConstraints relationConstraints,

                 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries

         ) {

-                val Map<Relation,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]

-                val Map<Relation,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)]

-                val Map<Relation,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)]

-                val Map<ObjectCreationPrecondition,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]

-                val Map<? extends Type,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]

-                val Map<Pair<RelationDeclaration, Relation>,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]

-                val Map<RelationDefinition, ModalPatternQueries> modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition |

+                val invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues [

+                        it.lookup(queries)

+                ]

+                val unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues [

+                        it.lookup(queries)

+                ]

+                val multiplicityConstraintQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(

+                        relationConstraints.multiplicityConstraints).mapValues [

+                        new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries),

+                                unrepairableMultiplicityQueryName?.lookup(queries),

+                                remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries))

+                ]

+                val unfinishedMultiplicityQueries = multiplicityConstraintQueries.entrySet.filter [

+                        value.unfinishedMultiplicityQuery !== null

+                ].toMap([key.relation], [value.unfinishedMultiplicityQuery])

+                val refineObjectsQueries = patternGenerator.typeRefinementGenerator.

+                        getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues[it.lookup(queries)]

+                val refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution,

+                        typeAnalysisResult).mapValues[it.lookup(queries)]

+                val refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).

+                        mapValues[it.lookup(queries)]

+                val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition |

                         val indexer = patternGenerator.relationDefinitionIndexer

                         new ModalPatternQueries(

                                 indexer.relationDefinitionName(relationDefinition, Modality.MAY).lookup(queries),

@@ -105,6 +125,7 @@ class PatternProvider {
                 return new GeneratedPatterns(

                         invalidWFQueries,

                         unfinishedWFQueries,

+                        multiplicityConstraintQueries,

                         unfinishedMultiplicityQueries,

                         refineObjectsQueries,

                         refineTypeQueries,

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
index f9e9baea..fa73c861 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
@@ -9,77 +9,71 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
 

 class RelationRefinementGenerator {

         PatternGenerator base;

+

         public new(PatternGenerator base) {

                 this.base = base

         }

-        

-        def CharSequence generateRefineReference(LogicProblem p) {

-                return '''

-                «FOR relationRefinement: this.getRelationRefinements(p)»

-                pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»(

-                        problem:LogicProblem, interpretation:PartialInterpretation,

-                        relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value != null», oppositeInterpretation:PartialRelationInterpretation«ENDIF»,

-                        from: DefinedElement, to: DefinedElement)

-                {

-                        find interpretation(problem,interpretation);

-                        PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);

-                        PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»");

-                        «IF relationRefinement.value != null»

-                                PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);

-                                PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»");

-                        «ENDIF»

-                        find mustExist(problem, interpretation, from);

-                        find mustExist(problem, interpretation, to);

-                        «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")»

-                        «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")»

-                        «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)»

-                        neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)»

-                }

+

+        def CharSequence generateRefineReference(LogicProblem p) '''

+                «FOR relationRefinement : this.getRelationRefinements(p)»

+                        pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»(

+                                problem:LogicProblem, interpretation:PartialInterpretation,

+                                relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF»,

+                                from: DefinedElement, to: DefinedElement)

+                        {

+                                find interpretation(problem,interpretation);

+                                PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);

+                                PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»");

+                                «IF relationRefinement.value !== null»

+                                        PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);

+                                        PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»");

+                                «ENDIF»

+                                find mustExist(problem, interpretation, from);

+                                find mustExist(problem, interpretation, to);

+                                «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")»

+                                «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")»

+                                «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)»

+                                neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)»

+                        }

                 «ENDFOR»

-                '''

-        }

-        

+        '''

+

         def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) {

-                '''«IF inverseRelation != null

-                »refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«

-                        ELSE

-                »refineRelation_«base.canonizeName(relation.name)»«ENDIF»'''

+                '''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»'''

         }

-        

+

         def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName,

-                String inverseInterpretationName, String sourceName, String targetName)

-        '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation != null»inverseInterpretationName, «ENDIF»«sourceName», «targetName»);'''

-        

+                String inverseInterpretationName, String sourceName,

+                String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»inverseInterpretationName, «ENDIF»«sourceName», «targetName»);'''

+

         def getRefineRelationQueries(LogicProblem p) {

 //              val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet

 //              p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»''']

                 /*

-                val res = new LinkedHashMap

-                for(relation: getRelationRefinements(p)) {

-                        if(inverseRelations.containsKey(relation)) {

-                                val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»'''

-                                res.put(relation -> inverseRelations.get(relation),name)

-                        } else {

-                                val name = '''refineRelation_«base.canonizeName(relation.name)»'''

-                                res.put(relation -> null,name)

-                        }

-                }

-                return res*/

-                

-                getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key,it.value)]

+                 * val res = new LinkedHashMap

+                 * for(relation: getRelationRefinements(p)) {

+                 *      if(inverseRelations.containsKey(relation)) {

+                 *              val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»'''

+                 *              res.put(relation -> inverseRelations.get(relation),name)

+                 *      } else {

+                 *              val name = '''refineRelation_«base.canonizeName(relation.name)»'''

+                 *              res.put(relation -> null,name)

+                 *      }

+                 * }

+                 return res*/

+                getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)]

         }

-        

 

         def getRelationRefinements(LogicProblem p) {

                 val inverses = base.getInverseRelations(p)

                 val containments = base.getContainments(p)

                 val list = new LinkedList

-                for(relation : p.relations.filter(RelationDeclaration)) {

-                        if(!containments.contains(relation)) {

-                                if(inverses.containsKey(relation)) {

+                for (relation : p.relations.filter(RelationDeclaration)) {

+                        if (!containments.contains(relation)) {

+                                if (inverses.containsKey(relation)) {

                                         val inverse = inverses.get(relation)

-                                        if(!containments.contains(inverse)) {

-                                                if(base.isRepresentative(relation,inverse)) {

+                                        if (!containments.contains(inverse)) {

+                                                if (base.isRepresentative(relation, inverse)) {

                                                         list += (relation -> inverse)

                                                 }

                                         }

@@ -90,4 +84,4 @@ class RelationRefinementGenerator {
                 }

                 return list

         }

-}
\ No newline at end of file
+}

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend
index 7e3fad91..ee7299cd 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend
@@ -86,8 +86,8 @@ abstract class TypeRefinementGenerator {
         }

         

         protected def String patternName(Relation containmentRelation, Relation inverseContainment, Type newType) {

-                if(containmentRelation != null) {

-                        if(inverseContainment != null) {

+                if(containmentRelation !== null) {

+                        if(inverseContainment !== null) {

                                 '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»_with_«base.canonizeName(inverseContainment.name)»'''

                         } else {

                                 '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»'''

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend
index ad1c9033..286756a8 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend
@@ -1,85 +1,195 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns

 

-import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem

-import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransformedViatraWellformednessConstraint

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint

+import java.util.LinkedHashMap

+import java.util.List

 import java.util.Map

 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery

+import org.eclipse.xtend.lib.annotations.Data

 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

-import java.util.LinkedHashMap

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference

+

+@Data

+class UnifinishedMultiplicityQueryNames {

+        val String unfinishedMultiplicityQueryName

+        val String unrepairableMultiplicityQueryName

+        val String remainingInverseMultiplicityQueryName

+        val String remainingContentsQueryName

+}

 

 class UnfinishedIndexer {

         val PatternGenerator base

-        

-        new(PatternGenerator patternGenerator) {

+        val boolean indexUpperMultiplicities

+

+        new(PatternGenerator patternGenerator, boolean indexUpperMultiplicities) {

                 this.base = patternGenerator

+                this.indexUpperMultiplicities = indexUpperMultiplicities

         }

-        

-        def generateUnfinishedWfQueries(LogicProblem problem, Map<String,PQuery> fqn2PQuery) {

+

+        def generateUnfinishedWfQueries(LogicProblem problem, Map<String, PQuery> fqn2PQuery) {

                 val wfQueries = base.wfQueries(problem)

                 '''

-                «FOR wfQuery: wfQueries»

-                        pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation,

-                                «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR»)

-                        {

-                                «base.relationDefinitionIndexer.referPattern(

+                        «FOR wfQuery : wfQueries»

+                                pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation,

+                                        «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR»)

+                                {

+                                        «base.relationDefinitionIndexer.referPattern(

                                         wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery),

                                         wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters.map['''var_«it.name»'''],

                                         Modality.CURRENT,

                                         true,false)»

-                        }

-                «ENDFOR»

+                                }

+                        «ENDFOR»

                 '''

         }

+

         def getUnfinishedWFQueryNames(LogicProblem problem) {

                 val wfQueries = base.wfQueries(problem)

                 val map = new LinkedHashMap

-                for(wfQuery : wfQueries) {

-                        map.put(wfQuery.target,'''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''')

+                for (wfQuery : wfQueries) {

+                        map.put(wfQuery.target, '''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''')

                 }

                 return map

         }

-        def generateUnfinishedMultiplicityQueries(LogicProblem problem, Map<String,PQuery> fqn2PQuery) {

-                val lowerMultiplicities = base.lowerMultiplicities(problem)

-                return '''

-                «FOR lowerMultiplicity : lowerMultiplicities»

-                        pattern «unfinishedMultiplicityName(lowerMultiplicity)»(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,missingMultiplicity) {

-                                find interpretation(problem,interpretation);

-                                PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);

-                                PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«lowerMultiplicity.relation.name»");

-                                «base.typeIndexer.referInstanceOf(lowerMultiplicity.firstParamTypeOfRelation,Modality::MUST,"object")»

-                                numberOfExistingReferences == count «base.referRelation(lowerMultiplicity.relation,"object","_",Modality.MUST,fqn2PQuery)»

-                                check(numberOfExistingReferences < «lowerMultiplicity.lower»);

-                                missingMultiplicity == eval(«lowerMultiplicity.lower»-numberOfExistingReferences);

-                        }

+

+        def generateUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints,

+                Map<String, PQuery> fqn2PQuery) '''

+                «FOR constraint : constraints»

+                        «IF constraint.constrainsUnfinished»

+                                private pattern «unfinishedMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, missingMultiplicity:java Integer) {

+                                        find interpretation(problem,interpretation);

+                                        find mustExist(problem,interpretation,object);

+                                        «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")»

+                                        numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)»

+                                        check(numberOfExistingReferences < «constraint.lowerBound»);

+                                        missingMultiplicity == eval(«constraint.lowerBound»-numberOfExistingReferences);

+                                }

+                                

+                                pattern «unfinishedMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, missingMultiplicity:java Integer) {

+                                        find interpretation(problem,interpretation);

+                                        missingMultiplicity == sum find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, _, #_);

+                                }

+                        «ENDIF»

+                        

+                        «IF indexUpperMultiplicities»

+                                «IF constraint.constrainsUnrepairable»

+                                        private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) {

+                                                find interpretation(problem,interpretation);

+                                                find mustExist(problem,interpretation,source);

+                                                «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")»

+                                                find mustExist(problem,interpretation,target);

+                                                «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")»

+                                                neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)»

+                                                «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)»

+                                        }

+                                        

+                                        private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) {

+                                                find interpretation(problem,interpretation);

+                                                find mustExist(problem,interpretation,object);

+                                                «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")»

+                                                find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity);

+                                                numerOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _);

+                                                check(numerOfRepairMatches < missingMultiplicity);

+                                                unrepairableMultiplicity == eval(missingMultiplicity-numerOfRepairMatches);

+                                        }

+                                        

+                                        private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) {

+                                                find interpretation(problem,interpretation);

+                                                unrepairableMultiplicity == max find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, #_);

+                                        } or {

+                                                find interpretation(problem,interpretation);

+                                                neg find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, _);

+                                                unrepairableMultiplicity == 0;

+                                        }

+                                «ENDIF»

+                                

+                                «IF constraint.constrainsRemainingInverse»

+                                        private pattern «remainingMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) {

+                                                find interpretation(problem,interpretation);

+                                                find mustExist(problem,interpretation,object);

+                                                «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")»

+                                                numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)»

+                                                check(numberOfExistingReferences < «constraint.inverseUpperBound»);

+                                                remainingMultiplicity == eval(«constraint.inverseUpperBound»-numberOfExistingReferences);

+                                        }

+                                        

+                                        pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) {

+                                                find interpretation(problem,interpretation);

+                                                remainingMultiplicity == sum find «remainingMultiplicityName(constraint)»_helper(problem, interpretation, _, #_);

+                                        }

+                                «ENDIF»

+                                

+                                «IF constraint.constrainsRemainingContents»

+                                        «IF constraint.upperBoundFinite»

+                                                private pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) {

+                                                        find interpretation(problem,interpretation);

+                                                        find mustExist(problem,interpretation,object);

+                                                        «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")»

+                                                        numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)»

+                                                        check(numberOfExistingReferences < «constraint.upperBound»);

+                                                        remainingMultiplicity == eval(«constraint.upperBound»-numberOfExistingReferences);

+                                                }

+                                                

+                                                pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) {

+                                                        find interpretation(problem,interpretation);

+                                                        remainingMultiplicity == sum find «remainingContentsName(constraint)»_helper(problem, interpretation, _, #_);

+                                                }

+                                        «ELSE»

+                                                pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation) {

+                                                        find interpretation(problem,interpretation);

+                                                        find mustExist(problem,interpretation,object);

+                                                        «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")»

+                                                }

+                                                

+                                                pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) {

+                                                        find interpretation(problem,interpretation);

+                                                        find «remainingContentsName(constraint)»_helper(problem, interpretation);

+                                                        remainingMultiplicity == -1;

+                                                } or {

+                                                        find interpretation(problem,interpretation);

+                                                        neg find «remainingContentsName(constraint)»_helper(problem, interpretation);

+                                                        remainingMultiplicity == 0;

+                                                }

+                                        «ENDIF»

+                                «ENDIF»

+                        «ENDIF»

                 «ENDFOR»

-                '''

-        }

-        def String unfinishedMultiplicityName(LowerMultiplicityAssertion lowerMultiplicityAssertion) 

-                '''unfinishedLowerMultiplicity_«base.canonizeName(lowerMultiplicityAssertion.relation.name)»'''

-        

-        def public referUnfinishedMultiplicityQuery(LowerMultiplicityAssertion lowerMultiplicityAssertion)

-                '''find «unfinishedMultiplicityName(lowerMultiplicityAssertion)»(problem, interpretation ,object, missingMultiplicity);'''

-        

-        def getFirstParamTypeOfRelation(LowerMultiplicityAssertion lowerMultiplicityAssertion) {

-                val parameters = lowerMultiplicityAssertion.relation.parameters

-                if(parameters.size == 2) {

-                        val firstParam = parameters.get(0)

-                        if(firstParam instanceof ComplexTypeReference) {

-                                return firstParam.referred

-                        }

-                }

-        }

-        

-        def getUnfinishedMultiplicityQueries(LogicProblem problem) {

-                val lowerMultiplicities = base.lowerMultiplicities(problem)

-                val map = new LinkedHashMap

-                for(lowerMultiplicity : lowerMultiplicities) {

-                        map.put(lowerMultiplicity.relation,unfinishedMultiplicityName(lowerMultiplicity))

-                }

-                return map

+        '''

+

+        def String unfinishedMultiplicityName(

+                RelationMultiplicityConstraint constraint) '''unfinishedLowerMultiplicity_«base.canonizeName(constraint.relation.name)»'''

+

+        def String unrepairableMultiplicityName(

+                RelationMultiplicityConstraint constraint) '''unrepairableLowerMultiplicity_«base.canonizeName(constraint.relation.name)»'''

+

+        private def String repairMatchName(

+                RelationMultiplicityConstraint constraint) '''repair_«base.canonizeName(constraint.relation.name)»'''

+

+        def String remainingMultiplicityName(

+                RelationMultiplicityConstraint constraint) '''remainingInverseUpperMultiplicity_«base.canonizeName(constraint.relation.name)»'''

+

+        def String remainingContentsName(

+                RelationMultiplicityConstraint constraint) '''remainingContents_«base.canonizeName(constraint.relation.name)»'''

+

+        def getUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints) {

+                constraints.toInvertedMap [ constraint |

+                        new UnifinishedMultiplicityQueryNames(

+                                if(constraint.constrainsUnfinished) unfinishedMultiplicityName(constraint) else null,

+                                if (indexUpperMultiplicities && constraint.constrainsUnrepairable)

+                                        unrepairableMultiplicityName(constraint)

+                                else

+                                        null,

+                                if (indexUpperMultiplicities && constraint.constrainsRemainingInverse)

+                                        remainingMultiplicityName(constraint)

+                                else

+                                        null,

+                                if (indexUpperMultiplicities && constraint.constrainsRemainingContents)

+                                        remainingContentsName(constraint)

+                                else

+                                        null

+                        )

+                ]

         }

 }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
index e1be2742..b6fdbe06 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
@@ -1,6 +1,6 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules

 

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns

 import java.util.ArrayList

 

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index 7a3a2d67..3c9ef74c 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -51,7 +51,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
          */

         public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint

         

-        public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.PolyhedralTypeHierarchy

+        public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.PolyhedralRelations

 

         public var List<CostObjectiveConfiguration> costObjectives = newArrayList

 }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
index 7d0a7884..9f0c642f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
@@ -1,10 +1,10 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator

 import java.util.Comparator

 import org.eclipse.viatra.dse.base.ThreadContext

-import org.eclipse.viatra.dse.objectives.IObjective

 import org.eclipse.viatra.dse.objectives.Comparators

+import org.eclipse.viatra.dse.objectives.IObjective

 

 class UnfinishedMultiplicityObjective implements IObjective {

         val MultiplicityGoalConstraintCalculator unfinishedMultiplicity;

@@ -29,9 +29,9 @@ class UnfinishedMultiplicityObjective implements IObjective {
         override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }

         

         override setComparator(Comparator<Double> comparator) {

-                throw new UnsupportedOperationException("TODO: auto-generated method stub")

+                throw new UnsupportedOperationException

         }

         override setLevel(int level) {

-                throw new UnsupportedOperationException("TODO: auto-generated method stub")

+                throw new UnsupportedOperationException

         }

-}
\ No newline at end of file
+}

diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend
index 789018cb..15758985 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend
@@ -17,7 +17,7 @@ abstract class PolyhedronSolverTest {
         var PolyhedronSaturationOperator operator
 
         protected def PolyhedronSolver createSolver()
-        
+
         @Before
         def void setUp() {
                 solver = createSolver()
@@ -183,7 +183,7 @@ abstract class PolyhedronSolverTest {
 
                 assertEquals(PolyhedronSaturationResult.EMPTY, result)
         }
-        
+
         @Test
         def void unboundedRelaxationWithNoIntegerSolutionTest() {
                 val x = new Dimension("x", 0, 1)
@@ -193,7 +193,29 @@ abstract class PolyhedronSolverTest {
                         #[new LinearConstraint(#{x -> 2}, 1, 1)],
                         #[x, y]
                 ))
-                
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.EMPTY, result)
+        }
+
+        @Test
+        def void emptyConstraintTest() {
+                val constraint = new LinearConstraint(emptyMap, 0, 1)
+                createSaturationOperator(new Polyhedron(#[], #[constraint], #[constraint]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(0, constraint.lowerBound)
+                assertEquals(0, constraint.upperBound)
+        }
+
+        @Test
+        def void emptyConstraintUnsatisfiableTest() {
+                val constraint = new LinearConstraint(emptyMap, 1, 0)
+                createSaturationOperator(new Polyhedron(#[], #[constraint], #[constraint]))
+
                 val result = saturate()
 
                 assertEquals(PolyhedronSaturationResult.EMPTY, result)