15 files changed, 2242 insertions, 0 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend
new file mode 100644
index 00000000..94f97e94
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend
@@ -0,0 +1,53 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import com.google.common.collect.ImmutableList
+import org.eclipse.xtend.lib.annotations.Accessors
+
+abstract class AbstractPolyhedronSaturationOperator implements PolyhedronSaturationOperator {
+        @Accessors val Polyhedron polyhedron
+
+        new(Polyhedron polyhedron) {
+                if (polyhedron.dimensions.empty) {
+                        throw new IllegalArgumentException("Polyhedron must have at least one dimension.")
+                }
+                this.polyhedron = polyhedron
+        }
+
+        override saturate() {
+                if (polyhedron.expressionsToSaturate.empty) {
+                        return PolyhedronSaturationResult.SATURATED
+                }
+                for (constraint : polyhedron.constraints) {
+                        if (constraint.zero) {
+                                if (constraint.lowerBound !== null && constraint.lowerBound > 0) {
+                                        return PolyhedronSaturationResult.EMPTY
+                                }
+                                if (constraint.upperBound !== null && constraint.upperBound < 0) {
+                                        return PolyhedronSaturationResult.EMPTY
+                                }
+                        } else {
+                                if (constraint.lowerBound !== null && constraint.upperBound !== null &&
+                                        constraint.upperBound < constraint.lowerBound) {
+                                        return PolyhedronSaturationResult.EMPTY
+                                }
+                        }
+                }
+                doSaturate()
+        }
+
+        protected def PolyhedronSaturationResult doSaturate()
+
+        protected def getNonTrivialConstraints() {
+                ImmutableList.copyOf(polyhedron.constraints.filter [ constraint |
+                        (constraint.lowerBound !== null || constraint.upperBound !== null) && !constraint.zero
+                ])
+        }
+
+        private static def isZero(LinearConstraint constraint) {
+                constraint.coefficients.values.forall[it == 0]
+        }
+
+        override close() throws Exception {
+                // Nothing to close by default.
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend
new file mode 100644
index 00000000..708f93dc
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend
@@ -0,0 +1,241 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import com.google.common.collect.ImmutableList
+import com.google.common.collect.ImmutableMap
+import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult
+import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver
+import java.util.HashSet
+import java.util.List
+import java.util.Map
+import java.util.Set
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+@FinalFieldsConstructor
+class CbcPolyhedronSolver implements PolyhedronSolver {
+        val boolean lpRelaxation
+        val double timeoutSeconds
+        val boolean silent
+
+        new() {
+                this(false, -1, true)
+        }
+
+        override createSaturationOperator(Polyhedron polyhedron) {
+                new CbcSaturationOperator(polyhedron, lpRelaxation, timeoutSeconds, silent)
+        }
+}
+
+class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator {
+        static val EPSILON = 1e-6
+
+        val boolean lpRelaxation
+        val double timeoutSeconds
+        val boolean silent
+        val double[] columnLowerBounds
+        val double[] columnUpperBounds
+        val double[] objective
+        val Map<Dimension, Integer> dimensionsToIndicesMap
+
+        new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds, boolean silent) {
+                super(polyhedron)
+                this.lpRelaxation = lpRelaxation
+                this.timeoutSeconds = timeoutSeconds
+                this.silent = silent
+                val numDimensions = polyhedron.dimensions.size
+                columnLowerBounds = newDoubleArrayOfSize(numDimensions)
+                columnUpperBounds = newDoubleArrayOfSize(numDimensions)
+                objective = newDoubleArrayOfSize(numDimensions)
+                dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key]))
+        }
+
+        override doSaturate() {
+                val numDimensions = polyhedron.dimensions.size
+                for (var int j = 0; j < numDimensions; j++) {
+                        val dimension = polyhedron.dimensions.get(j)
+                        columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY))
+                        columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY))
+                }
+                val constraints = nonTrivialConstraints
+                val numConstraints = constraints.size
+                val rowStarts = newIntArrayOfSize(numConstraints + 1)
+                val rowLowerBounds = newDoubleArrayOfSize(numConstraints)
+                val rowUpperBounds = newDoubleArrayOfSize(numConstraints)
+                val numEntries = constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0
+                rowStarts.set(numConstraints, numEntries)
+                val columnIndices = newIntArrayOfSize(numEntries)
+                val entries = newDoubleArrayOfSize(numEntries)
+                val unconstrainedDimensions = new HashSet
+                for (dimension : polyhedron.dimensions) {
+                        if (dimension.lowerBound === null && dimension.upperBound === null) {
+                                unconstrainedDimensions += dimension
+                        }
+                }
+                var int index = 0
+                for (var int i = 0; i < numConstraints; i++) {
+                        rowStarts.set(i, index)
+                        val constraint = constraints.get(i)
+                        rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY))
+                        rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY))
+                        if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) {
+                                throw new IllegalArgumentException("Constrains has unknown dimensions")
+                        }
+                        for (var int j = 0; j < numDimensions; j++) {
+                                val dimension = polyhedron.dimensions.get(j)
+                                val coefficient = constraint.coefficients.get(dimension)
+                                if (coefficient !== null && coefficient != 0) {
+                                        unconstrainedDimensions -= dimension
+                                        columnIndices.set(index, j)
+                                        entries.set(index, coefficient)
+                                        index++
+                                }
+                        }
+                }
+                if (index != numEntries) {
+                        throw new AssertionError("Last entry does not equal the number of entries in the constraint matrix")
+                }
+                for (expressionToSaturate : polyhedron.expressionsToSaturate) {
+                        val result = saturate(expressionToSaturate, rowStarts, columnIndices, entries, rowLowerBounds,
+                                rowUpperBounds, unconstrainedDimensions, constraints)
+                        if (result != PolyhedronSaturationResult.SATURATED) {
+                                return result
+                        }
+                }
+                PolyhedronSaturationResult.SATURATED
+        }
+
+        protected def saturate(LinearBoundedExpression expressionToSaturate, int[] rowStarts, int[] columnIndices,
+                double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, Set<Dimension> unconstrainedDimensions,
+                ImmutableList<LinearConstraint> constraints) {
+                val numDimensions = objective.size
+                for (var int j = 0; j < numDimensions; j++) {
+                        objective.set(j, 0)
+                }
+                switch (expressionToSaturate) {
+                        Dimension: {
+                                // CBC will return nonsensical results or call free() with invalid arguments if
+                                // it is passed a fully unconstrained (-Inf lower and +Int upper bound, no inequalities) variable
+                                // in the objective function.
+                                if (unconstrainedDimensions.contains(expressionToSaturate)) {
+                                        return PolyhedronSaturationResult.SATURATED
+                                }
+                                val j = getIndex(expressionToSaturate)
+                                objective.set(j, 1)
+                        }
+                        LinearConstraint: {
+                                for (pair : expressionToSaturate.coefficients.entrySet) {
+                                        val dimension = pair.key
+                                        // We also have to check for unconstrained dimensions here to avoid crashing.
+                                        if (unconstrainedDimensions.contains(dimension)) {
+                                                expressionToSaturate.lowerBound = null
+                                                expressionToSaturate.upperBound = null
+                                                return PolyhedronSaturationResult.SATURATED
+                                        }
+                                        val j = getIndex(dimension)
+                                        objective.set(j, pair.value)
+                                }
+                        }
+                        default:
+                                throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate)
+                }
+                val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices,
+                        entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent)
+                switch (minimizationResult) {
+                        CbcResult.SolutionBounded: {
+                                val doubleValue = minimizationResult.value
+                                val roundedValue = Math.ceil(doubleValue - EPSILON)
+                                val intValue = roundedValue as int
+                                val oldBound = expressionToSaturate.lowerBound
+                                if (oldBound === null || intValue >= oldBound) {
+                                        expressionToSaturate.lowerBound = intValue
+                                        setBound(expressionToSaturate, constraints, roundedValue, columnLowerBounds, rowLowerBounds)
+                                } else {
+                                        throw new IllegalStateException("Unexpected decrease of lower bound by " + (oldBound - doubleValue))
+                                }
+                        }
+                        case CbcResult.SOLUTION_UNBOUNDED: {
+                                if (expressionToSaturate.lowerBound !== null) {
+                                        throw new IllegalStateException("Finite lower bound became infinite")
+                                }
+                                setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds)
+                        }
+                        case CbcResult.UNSAT:
+                                return PolyhedronSaturationResult.EMPTY
+                        case CbcResult.ABANDONED,
+                        case CbcResult.TIMEOUT:
+                                return PolyhedronSaturationResult.UNKNOWN
+                        default:
+                                throw new RuntimeException("Unknown CbcResult: " + minimizationResult)
+                }
+                for (var int j = 0; j < numDimensions; j++) {
+                        val objectiveCoefficient = objective.get(j)
+                        objective.set(j, -objectiveCoefficient)
+                }
+                val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices,
+                        entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent)
+                switch (maximizationResult) {
+                        CbcResult.SolutionBounded: {
+                                val doubleValue = -maximizationResult.value
+                                val roundedValue = Math.floor(doubleValue + EPSILON)
+                                val intValue = roundedValue as int
+                                val oldBound = expressionToSaturate.upperBound
+                                if (oldBound === null || intValue <= oldBound) {
+                                        expressionToSaturate.upperBound = intValue
+                                        setBound(expressionToSaturate, constraints, roundedValue, columnUpperBounds, rowUpperBounds)
+                                } else {
+                                        throw new IllegalStateException("Unexpected increase of upper bound by " + (doubleValue - oldBound))
+                                }
+                        }
+                        case CbcResult.SOLUTION_UNBOUNDED: {
+                                if (expressionToSaturate.lowerBound !== null) {
+                                        throw new IllegalStateException("Finite upper bound became infinite")
+                                }
+                                expressionToSaturate.upperBound = null
+                                setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds)
+                        }
+                        case CbcResult.UNSAT:
+                                if (lpRelaxation) {
+                                        return PolyhedronSaturationResult.EMPTY
+                                } else {
+                                        throw new RuntimeException("Minimization was SAT, but maximization is UNSAT")
+                                }
+                        case CbcResult.ABANDONED,
+                        case CbcResult.TIMEOUT:
+                                return PolyhedronSaturationResult.UNKNOWN
+                        default:
+                                throw new RuntimeException("Unknown CbcResult: " + maximizationResult)
+                }
+                return PolyhedronSaturationResult.SATURATED
+        }
+
+        private def toDouble(Integer nullableInt, double defaultValue) {
+                if (nullableInt === null) {
+                        defaultValue
+                } else {
+                        nullableInt.doubleValue
+                }
+        }
+
+        private def int getIndex(Dimension dimension) {
+                val index = dimensionsToIndicesMap.get(dimension)
+                if (index === null) {
+                        throw new IllegalArgumentException("Unknown dimension: " + dimension)
+                }
+                index
+        }
+
+        private def void setBound(LinearBoundedExpression expression, List<LinearConstraint> constraints, double bound,
+                double[] columnBounds, double[] rowBounds) {
+                switch (expression) {
+                        Dimension: {
+                                val j = getIndex(expression)
+                                columnBounds.set(j, bound)
+                        }
+                        LinearConstraint: {
+                                val i = constraints.indexOf(expression)
+                                if (i >= 0) {
+                                        rowBounds.set(i, bound)
+                                }
+                        }
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend
new file mode 100644
index 00000000..e97fa5d7
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend
@@ -0,0 +1,140 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import com.google.common.collect.ImmutableList
+import com.google.common.collect.ImmutableMap
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+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 org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+interface BoundSaturationListener {
+        def void boundsSaturated(Integer lower, Integer upper)
+}
+
+interface ExtendedLinearExpressionBuilderFactory {
+        def ExtendedLinearExpressionBuilder createBuilder()
+
+        def Dimension getDimension(IPatternMatch patternMatch)
+}
+
+interface ExtendedLinearExpressionBuilder extends LinearTypeExpressionBuilder {
+        override ExtendedLinearExpressionBuilder add(int scale, Type type)
+
+        def ExtendedLinearExpressionBuilder add(int scale, IPatternMatch patternMatch)
+
+        def ExtendedLinearExpressionBuilder add(int scale, Dimension dimension)
+
+        def LinearBoundedExpression build(BoundSaturationListener listener)
+}
+
+class ExtendedPolyhedronBuilder implements ExtendedLinearExpressionBuilderFactory {
+        val Map<Type, LinearBoundedExpression> typeBounds
+        val Map<Map<Dimension, Integer>, LinearBoundedExpression> expressionsCache
+
+        val ImmutableList.Builder<Dimension> dimensions = ImmutableList.builder
+        val Set<LinearConstraint> constraints = new HashSet
+        val Set<LinearBoundedExpression> expressionsToSaturate = new HashSet
+        val Map<IPatternMatch, Dimension> patternMatchCounts = new HashMap
+        @Accessors(PUBLIC_GETTER) val List<Pair<LinearBoundedExpression, BoundSaturationListener>> saturationListeners = new ArrayList
+
+        new(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds,
+                Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) {
+                this.typeBounds = typeBounds
+                this.expressionsCache = new HashMap(initialExpressionsCache)
+                dimensions.addAll(polyhedron.dimensions)
+                constraints.addAll(polyhedron.constraints)
+                expressionsToSaturate.addAll(polyhedron.expressionsToSaturate)
+        }
+
+        override createBuilder() {
+                new ExtendedLinearExpressionBuilderImpl(this)
+        }
+
+        override getDimension(IPatternMatch patternMatch) {
+                patternMatchCounts.computeIfAbsent(patternMatch) [ key |
+                        val dimension = new Dimension(key.toString, 0, null)
+                        dimensions.add(dimension)
+                        dimension
+                ]
+        }
+
+        def buildPolyhedron() {
+                new Polyhedron(
+                        dimensions.build,
+                        ImmutableList.copyOf(constraints),
+                        ImmutableList.copyOf(expressionsToSaturate)
+                )
+        }
+
+        @FinalFieldsConstructor
+        private static class ExtendedLinearExpressionBuilderImpl implements ExtendedLinearExpressionBuilder {
+                val ExtendedPolyhedronBuilder polyhedronBuilder
+
+                val Map<Dimension, Integer> coefficients = new HashMap
+
+                override add(int scale, Type type) {
+                        val expression = polyhedronBuilder.typeBounds.get(type)
+                        if (expression === null) {
+                                throw new IllegalArgumentException("Unknown Type: " + type)
+                        }
+                        add(scale, expression)
+                }
+
+                override add(int scale, IPatternMatch patternMatch) {
+                        val dimension = polyhedronBuilder.getDimension(patternMatch)
+                        add(scale, dimension)
+                }
+
+                private def add(int scale, LinearBoundedExpression expression) {
+                        switch (expression) {
+                                Dimension: add(scale, expression)
+                                LinearConstraint: add(scale, expression.coefficients)
+                                default: throw new IllegalArgumentException("Unknown LinearBoundedExpression: " + expression)
+                        }
+                }
+
+                private def add(int scale, Map<Dimension, Integer> coefficients) {
+                        for (pair : coefficients.entrySet) {
+                                add(scale * pair.value, pair.key)
+                        }
+                        this
+                }
+
+                override add(int scale, Dimension dimension) {
+                        coefficients.merge(dimension, scale)[a, b|a + b]
+                        this
+                }
+
+                override build() {
+                        val filteredCoefficients = ImmutableMap.copyOf(coefficients.filter [ x, coefficient |
+                                coefficient != 0
+                        ])
+                        polyhedronBuilder.expressionsCache.computeIfAbsent(filteredCoefficients) [ map |
+                                if (map.size == 1) {
+                                        val pair = map.entrySet.head
+                                        if (pair.value == 1) {
+                                                return pair.key
+                                        }
+                                }
+                                val constraint = new LinearConstraint(map)
+                                polyhedronBuilder.constraints.add(constraint)
+                                constraint
+                        ]
+                }
+
+                override build(BoundSaturationListener listener) {
+                        val expression = build()
+                        if (listener !== null) {
+                                polyhedronBuilder.expressionsToSaturate.add(expression)
+                                polyhedronBuilder.saturationListeners.add(expression -> listener)
+                        }
+                        expression
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend
new file mode 100644
index 00000000..32923396
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend
@@ -0,0 +1,63 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
+import java.util.Collection
+import java.util.Map
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+
+interface PolyhedronExtensionOperator {
+        def void extendPolyhedron(ExtendedLinearExpressionBuilderFactory factory)
+}
+
+class ExtendedPolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy {
+        val PolyhedronSolver solver
+        val Collection<PolyhedronExtensionOperator> extensionOperators
+
+        var Map<Type, LinearBoundedExpression> typeBounds
+        var Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache
+
+        new(PolyhedronSolver solver, Collection<PolyhedronExtensionOperator> extensionOperators,
+                ModelGenerationStatistics statistics) {
+                super(statistics)
+                this.solver = solver
+                this.extensionOperators = extensionOperators
+        }
+
+        override setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds,
+                Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) {
+                super.setPolyhedron(polyhedron, typeBounds, initialExpressionsCache)
+                this.typeBounds = typeBounds
+                this.initialExpressionsCache = initialExpressionsCache
+        }
+
+        override isRelevantRelation(Relation relation) {
+                true
+        }
+
+        override protected doSaturate() {
+                val builder = new ExtendedPolyhedronBuilder(polyhedron, typeBounds, initialExpressionsCache)
+                for (extensionOperator : extensionOperators) {
+                        extensionOperator.extendPolyhedron(builder)
+                }
+                val extendedPolyhedron = builder.buildPolyhedron()
+                val saturationOperator = solver.createSaturationOperator(extendedPolyhedron)
+                val result = try {
+                                saturationOperator.saturate()
+                        } finally {
+                                saturationOperator.close()
+                        }
+                if (result == PolyhedronSaturationResult.EMPTY) {
+                        // The partial model cannot be refined any more, we can't provide objective bounds.
+                        for (pair : builder.saturationListeners) {
+                                pair.value.boundsSaturated(null, null)
+                        }
+                        return false
+                }
+                for (pair : builder.saturationListeners) {
+                        val expression = pair.key
+                        pair.value.boundsSaturated(expression.lowerBound, expression.upperBound)
+                }
+                true
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend
new file mode 100644
index 00000000..31f98e36
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend
@@ -0,0 +1,32 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
+
+interface LinearTypeExpressionBuilderFactory {
+        def ViatraQueryMatcher<? extends IPatternMatch> createMatcher(String queryName)
+        
+        def LinearTypeExpressionBuilder createBuilder()
+}
+
+interface LinearTypeExpressionBuilder {
+        def LinearTypeExpressionBuilder add(int scale, Type type)
+
+        def LinearBoundedExpression build()
+}
+
+@FunctionalInterface
+interface RelationConstraintUpdater {
+        def void update(PartialInterpretation p)
+}
+
+interface LinearTypeConstraintHint {
+        def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator, Map<String, PQuery> fqnToPQuery)
+        
+        def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory)
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
new file mode 100644
index 00000000..273e0ac3
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
@@ -0,0 +1,57 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality

+

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

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

+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine

+import org.eclipse.viatra.query.runtime.emf.EMFScope

+

+class MultiplicityGoalConstraintCalculator {

+        val String targetRelationName

+        val IQuerySpecification<?> querySpecification

+        var MultiplicityCalculator<?> calculator

+        val boolean containment

+        val int lowerBound

+        val int cost

+                

+        new(String targetRelationName, IQuerySpecification<?> querySpecification, boolean containment, int lowerBound, int cost) {

+                if (lowerBound <= 0) {

+                        throw new IllegalArgumentException("Invalid lower bound: " + lowerBound)

+                }

+                this.targetRelationName = targetRelationName

+                this.querySpecification = querySpecification

+                this.calculator = null

+                this.containment = containment

+                this.lowerBound = lowerBound

+                this.cost = cost

+        }

+        

+        new(MultiplicityGoalConstraintCalculator other) {

+                this.targetRelationName = other.targetRelationName

+                this.querySpecification = other.querySpecification

+                this.calculator = null

+                this.containment = other.containment

+                this.lowerBound = other.lowerBound

+                this.cost = other.cost

+        }

+        

+        def getName() {

+                targetRelationName

+        }

+        

+        def isContainment() {

+                return containment

+        }

+

+        def init(Notifier notifier) {

+                val engine = ViatraQueryEngine.on(new EMFScope(notifier))

+                val matcher = querySpecification.getMatcher(engine)

+                calculator = RemainingMultiplicityCalculator.of(matcher, lowerBound)

+        }

+        

+        def calculateValue() {

+                val res = calculator.multiplicity

+//              if(res>0)

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

+                return res*cost

+        }

+}
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
new file mode 100644
index 00000000..ad8f94ab
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
@@ -0,0 +1,522 @@
+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.ImmutableSet
+import com.google.common.collect.Maps
+import com.google.common.collect.Sets
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
+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.Collection
+import java.util.HashMap
+import java.util.HashSet
+import java.util.List
+import java.util.Map
+import java.util.Set
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.IQuerySpecification
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+import org.eclipse.viatra.query.runtime.emf.EMFScope
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
+        val boolean updateHeuristic
+        val Map<Scope, LinearBoundedExpression> scopeBounds
+        val LinearBoundedExpression topLevelBounds
+        val Polyhedron polyhedron
+        val PolyhedronScopePropagatorStrategy strategy
+        val Set<Relation> relevantRelations
+        List<RelationConstraintUpdater> updaters = emptyList
+
+        new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes,
+                Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries,
+                IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery,
+                Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName,
+                Collection<LinearTypeConstraintHint> hints, PolyhedronScopePropagatorStrategy strategy,
+                boolean propagateRelations, boolean updateHeuristic) {
+                super(p, statistics)
+                this.updateHeuristic = updateHeuristic
+                this.strategy = strategy
+                val builder = new PolyhedronBuilder(p)
+                builder.buildPolyhedron(possibleNewDynamicTypes)
+                scopeBounds = builder.scopeBounds
+                topLevelBounds = builder.topLevelBounds
+                polyhedron = builder.polyhedron
+                strategy.setPolyhedron(polyhedron, builder.typeBounds, builder.expressionsCache)
+                propagateAllScopeConstraints()
+                if (propagateRelations) {
+                        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 not positive")
+                        }
+                        builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery,
+                                allPatternsByName, hints, maximumNumberOfNewNodes)
+                        relevantRelations = builder.relevantRelations
+                        updaters = builder.updaters
+                } else {
+                        relevantRelations = emptySet
+                }
+        }
+
+        override void doPropagateAllScopeConstraints() {
+                super.doPropagateAllScopeConstraints()
+                resetBounds()
+                populatePolyhedronFromScope()
+//              println(polyhedron)
+                if (strategy.saturate) {
+                        populateScopesFromPolyhedron()
+                } else {
+                        setScopesInvalid()
+                }
+//              println(polyhedron)
+                if (updateHeuristic) {
+                        copyScopeBoundsToHeuristic()
+                }
+        }
+
+        override isPropagationNeededAfterAdditionToRelation(Relation r) {
+                relevantRelations.contains(r) || strategy.isRelevantRelation(r) || super.isPropagationNeededAfterAdditionToRelation(r)
+        }
+
+        override isQueryEngineFlushRequiredBeforePropagation() {
+                true
+        }
+
+        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.tightenLowerBound(partialInterpretation.minNewElements)
+                if (partialInterpretation.maxNewElements >= 0) {
+                        topLevelBounds.tightenUpperBound(partialInterpretation.maxNewElements)
+                }
+                for (pair : scopeBounds.entrySet) {
+                        val scope = pair.key
+                        val bounds = pair.value
+                        bounds.tightenLowerBound(scope.minNewElements)
+                        if (scope.maxNewElements >= 0) {
+                                bounds.tightenUpperBound(scope.maxNewElements)
+                        }
+                }
+                for (updater : updaters) {
+                        updater.update(partialInterpretation)
+                }
+        }
+
+        private def populateScopesFromPolyhedron() {
+                checkBounds(topLevelBounds)
+                if (partialInterpretation.minNewElements > topLevelBounds.lowerBound) {
+                        throw new IllegalArgumentException('''Lower bound of «topLevelBounds» smaller than top-level scope: «partialInterpretation.minNewElements»''')
+                } else if (partialInterpretation.minNewElements != topLevelBounds.lowerBound) {
+                        partialInterpretation.minNewElements = topLevelBounds.lowerBound
+                }
+                val topLevelUpperBound = topLevelBounds.upperBound ?: -1
+                if (partialInterpretation.maxNewElements >= 0 && topLevelUpperBound >= 0 &&
+                        partialInterpretation.maxNewElements < topLevelUpperBound) {
+                        throw new IllegalArgumentException('''Upper bound of «topLevelBounds» larger than top-level scope: «partialInterpretation.maxNewElements»''')
+                } else if (partialInterpretation.maxNewElements != topLevelUpperBound) {
+                        partialInterpretation.maxNewElements = topLevelUpperBound
+                }
+                for (pair : scopeBounds.entrySet) {
+                        val scope = pair.key
+                        val bounds = pair.value
+                        checkBounds(bounds)
+                        if (scope.minNewElements > bounds.lowerBound) {
+                                throw new IllegalArgumentException('''Lower bound of «bounds» smaller than «scope.targetTypeInterpretation» scope: «scope.minNewElements»''')
+                        } else if (scope.minNewElements != bounds.lowerBound) {
+                                scope.minNewElements = bounds.lowerBound
+                        }
+                        val upperBound = bounds.upperBound ?: -1
+                        if (scope.maxNewElements >= 0 && upperBound >= 0 && scope.maxNewElements < upperBound) {
+                                throw new IllegalArgumentException('''Upper bound of «bounds» larger than «scope.targetTypeInterpretation» scope: «scope.maxNewElements»''')
+                        } else if (scope.maxNewElements != upperBound) {
+                                scope.maxNewElements = upperBound
+                        }
+                }
+        }
+
+        private def checkBounds(LinearBoundedExpression bounds) {
+                if (bounds.lowerBound === null) {
+                        throw new IllegalArgumentException("Infinite lower bound: " + bounds)
+                } else if (bounds.lowerBound < 0) {
+                        throw new IllegalArgumentException("Negative lower bound: " + bounds)
+                }
+                if (bounds.upperBound !== null && bounds.upperBound < 0) {
+                        throw new IllegalArgumentException("Negative upper bound: " + bounds)
+                }
+        }
+
+        @FinalFieldsConstructor
+        private static class PolyhedronBuilder implements LinearTypeExpressionBuilderFactory {
+                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
+                Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName
+                ImmutableList.Builder<RelationConstraintUpdater> updatersBuilder
+
+                Map<Scope, LinearBoundedExpression> scopeBounds
+                LinearBoundedExpression topLevelBounds
+                Polyhedron polyhedron
+                Set<Relation> relevantRelations
+                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,
+                        IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery,
+                        Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName,
+                        Collection<LinearTypeConstraintHint> hints, int maximumNuberOfNewNodes) {
+                        infinity = if (maximumNuberOfNewNodes <= Integer.MAX_VALUE / INFINITY_SCALE) {
+                                maximumNuberOfNewNodes * INFINITY_SCALE
+                        } else {
+                                Integer.MAX_VALUE
+                        }
+
+                        queryEngine = ViatraQueryEngine.on(new EMFScope(p))
+                        this.allPatternsByName = allPatternsByName
+                        updatersBuilder = ImmutableList.builder
+                        val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType]
+                        for (pair : containmentConstraints.entrySet) {
+                                buildContainmentConstraints(pair.key, pair.value)
+                        }
+                        buildConstainmentRootConstraints(containmentConstraints.keySet, hasElementInContainmentQuery)
+                        for (pair : constraints.entrySet) {
+                                val constraint = pair.key
+                                if (!constraint.containment && !constraint.container) {
+                                        buildNonContainmentConstraints(constraint, pair.value)
+                                }
+                        }
+                        buildRelevantRelations(constraints.keySet)
+                        for (hint : hints) {
+                                val updater = hint.createConstraintUpdater(this)
+                                if (updater !== null) {
+                                        updatersBuilder.add(updater)
+                                }
+                        }
+                        updaters = updatersBuilder.build
+                        addCachedConstraintsToPolyhedron()
+                }
+
+                private def buildRelevantRelations(Set<RelationMultiplicityConstraint> constraints) {
+                        val builder = ImmutableSet.builder
+                        for (constraint : constraints) {
+                                builder.add(constraint.relation)
+                                if (constraint.inverseRelation !== null) {
+                                        builder.add(constraint.inverseRelation)
+                                }
+                        }
+                        relevantRelations = builder.build
+                }
+
+                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 unfinishedMultiplicitiesBuilder = ImmutableList.builder
+                        val remainingContentsBuilder = 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 (queries.existingMultiplicityQuery !== null) {
+                                        val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine)
+                                        if (constraint.constrainsUnfinished) {
+                                                unfinishedMultiplicitiesBuilder.add(
+                                                        RemainingMultiplicityCalculator.of(matcher, constraint.lowerBound))
+                                        }
+                                        remainingContentsBuilder.add(RemainingMultiplicityCalculator.of(matcher, constraint.upperBound))
+                                } else if (constraint.constrainsUnfinished) {
+                                        throw new IllegalArgumentException("Containment constraints need multiplicity queries")
+                                }
+                        }
+                        val orphanLowerBound = orphansLowerBoundCoefficients.toExpression
+                        val orphanUpperBound = orphansUpperBoundCoefficients.toExpression
+                        val updater = new ContainmentConstraintUpdater(orphanLowerBound, orphanUpperBound,
+                                unfinishedMultiplicitiesBuilder.build, remainingContentsBuilder.build)
+                        updatersBuilder.add(updater)
+                }
+
+                private def buildConstainmentRootConstraints(Set<Type> containedTypes,
+                        IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery) {
+                        val matcher = hasElementInContainmentQuery.getMatcher(queryEngine)
+                        val rootDimensions = Sets.newHashSet(instanceCounts.values)
+                        for (type : containedTypes) {
+                                val containedDimensions = subtypeDimensions.get(type).keySet
+                                rootDimensions.removeAll(containedDimensions)
+                        }
+                        for (dimension : rootDimensions) {
+                                updatersBuilder.add(new ContainmentRootConstraintUpdater(dimension, matcher))
+                        }
+                }
+
+                private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint,
+                        UnifinishedMultiplicityQueries queries) {
+                        if (!constraint.reference) {
+                                return
+                        }
+                        if (constraint.constrainsRemainingInverse) {
+                                if (queries.getExistingMultiplicityQuery === null) {
+                                        throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries: " +
+                                                constraint.relation)
+                                }
+                                val existingMultiplicityMatcher = queries.getExistingMultiplicityQuery.getMatcher(queryEngine)
+                                val unfinishedMultiplicityCalculator = RemainingMultiplicityCalculator.of(existingMultiplicityMatcher,
+                                        constraint.lowerBound)
+                                val existingInverseMultiplicityMatcher = queries.existingInverseMultiplicityQuery.getMatcher(
+                                        queryEngine)
+                                val remainingInverseMultiplicityCalculator = new RemainingInverseMultiplicityCalculator(
+                                        existingInverseMultiplicityMatcher, constraint.upperBound)
+                                val availableMultiplicityCoefficients = new HashMap
+                                availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound,
+                                        subtypeDimensions.get(constraint.targetType))
+                                availableMultiplicityCoefficients.addCoefficients(-constraint.lowerBound,
+                                        subtypeDimensions.get(constraint.targetType))
+                                val availableMultiplicity = availableMultiplicityCoefficients.toExpression
+                                updatersBuilder.add(
+                                        new UnfinishedMultiplicityConstraintUpdater(availableMultiplicity, unfinishedMultiplicityCalculator,
+                                                remainingInverseMultiplicityCalculator))
+                        }
+                        if (constraint.constrainsUnrepairable) {
+                                if (queries.existingMultiplicityQuery.parameters.size < 5) {
+                                        throw new IllegalArgumentException("Reference constraints need repairable multiplicity queries: " +
+                                                constraint.relation)
+                                }
+                                val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine)
+                                val calculator = new UnrepairableMultiplicityCalculator(matcher, constraint.lowerBound)
+                                val targetTypeCardinality = typeBounds.get(constraint.targetType)
+                                updatersBuilder.add(new UnrepairableMultiplicityConstraintUpdater(targetTypeCardinality, calculator))
+                        }
+                }
+
+                private static 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 IllegalStateException("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
+                }
+
+                override createMatcher(String queryName) {
+                        val querySpecification = allPatternsByName.get(queryName)
+                        if (querySpecification === null) {
+                                throw new IllegalArgumentException("Unknown pattern: " + queryName)
+                        }
+                        querySpecification.getMatcher(queryEngine)
+                }
+
+                override createBuilder() {
+                        new PolyhedronBuilderLinearTypeExpressionBuilder(this)
+                }
+        }
+
+        @FinalFieldsConstructor
+        private static class PolyhedronBuilderLinearTypeExpressionBuilder implements LinearTypeExpressionBuilder {
+                val PolyhedronBuilder polyhedronBuilder
+                val Map<Dimension, Integer> coefficients = new HashMap
+
+                override add(int scale, Type type) {
+                        val typeCoefficients = polyhedronBuilder.subtypeDimensions.get(type)
+                        if (typeCoefficients === null) {
+                                throw new IllegalArgumentException("Unknown type: " + type)
+                        }
+                        PolyhedronBuilder.addCoefficients(coefficients, scale, typeCoefficients)
+                        this
+                }
+
+                override build() {
+                        polyhedronBuilder.toExpression(coefficients)
+                }
+        }
+
+        @FinalFieldsConstructor
+        private static class ContainmentConstraintUpdater implements RelationConstraintUpdater {
+                val LinearBoundedExpression orphansLowerBound
+                val LinearBoundedExpression orphansUpperBound
+                val List<MultiplicityCalculator<? extends IPatternMatch>> unfinishedMultiplicities
+                val List<MultiplicityCalculator<? extends IPatternMatch>> remainingContents
+
+                override update(PartialInterpretation p) {
+                        tightenLowerBound(p)
+                        tightenUpperBound(p)
+                }
+
+                private def tightenLowerBound(PartialInterpretation p) {
+                        var int sum = 0
+                        for (calculator : remainingContents) {
+                                val value = calculator.getMultiplicity(p)
+                                if (value < 0) {
+                                        // Infinite upper bound, no need to tighten.
+                                        return
+                                }
+                                sum += value
+                        }
+                        orphansLowerBound.tightenUpperBound(sum)
+                }
+
+                private def tightenUpperBound(PartialInterpretation p) {
+                        var int sum = 0
+                        for (calculator : unfinishedMultiplicities) {
+                                val value = calculator.getMultiplicity(p)
+                                sum += value
+                        }
+                        orphansUpperBound.tightenLowerBound(sum)
+                }
+        }
+
+        @FinalFieldsConstructor
+        private static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater {
+                val LinearBoundedExpression typeCardinality
+                val ViatraQueryMatcher<? extends IPatternMatch> hasElementInContainmentMatcher
+
+                override update(PartialInterpretation p) {
+                        if (hasElementInContainmentMatcher.hasMatch(p)) {
+                                typeCardinality.tightenUpperBound(0)
+                        } else {
+                                typeCardinality.tightenUpperBound(1)
+                        }
+                }
+
+                private static def <T extends IPatternMatch> hasMatch(ViatraQueryMatcher<T> matcher, PartialInterpretation p) {
+                        val match = matcher.newMatch(p.problem, p)
+                        matcher.countMatches(match) != 0
+                }
+        }
+
+        @FinalFieldsConstructor
+        private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater {
+                val LinearBoundedExpression availableMultiplicityExpression
+                val MultiplicityCalculator<? extends IPatternMatch> unfinishedMultiplicityCalculator
+                val MultiplicityCalculator<? extends IPatternMatch> remainingInverseMultiplcityCalculator
+
+                override update(PartialInterpretation p) {
+                        val unfinishedMultiplicity = unfinishedMultiplicityCalculator.getMultiplicity(p)
+                        val remainingInverseMultiplicity = remainingInverseMultiplcityCalculator.getMultiplicity(p)
+                        val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity
+                        availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity)
+                }
+        }
+
+        @FinalFieldsConstructor
+        private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater {
+                val LinearBoundedExpression targetCardinalityExpression
+                val MultiplicityCalculator<? extends IPatternMatch> calculator
+
+                override update(PartialInterpretation p) {
+                        val value = calculator.getMultiplicity(p)
+                        targetCardinalityExpression.tightenLowerBound(value)
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend
new file mode 100644
index 00000000..f93dcd18
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend
@@ -0,0 +1,92 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import com.google.common.cache.Cache
+import com.google.common.cache.CacheBuilder
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
+import java.util.Map
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+@FinalFieldsConstructor
+abstract class PolyhedronScopePropagatorStrategy {
+        val ModelGenerationStatistics statistics
+
+        @Accessors(PUBLIC_GETTER) var Polyhedron polyhedron
+
+        def void setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds,
+                Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) {
+                if (this.polyhedron !== null) {
+                        throw new IllegalStateException("polyhedron was already set")
+                }
+                this.polyhedron = polyhedron
+                initialize()
+        }
+
+        def boolean saturate() {
+                if (polyhedron === null) {
+                        throw new IllegalStateException("polyhedron was not set")
+                }
+                doSaturate()
+        }
+        
+        def boolean isRelevantRelation(Relation relation) {
+                false
+        }
+
+        protected def incrementScopePropagationSolverCount() {
+                statistics.incrementScopePropagationSolverCount()
+        }
+
+        protected def void initialize() {
+        }
+
+        protected def boolean doSaturate()
+}
+
+@FinalFieldsConstructor
+class CachingSimplePolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy {
+        static val CACHE_SIZE = 10000
+
+        val PolyhedronSolver solver
+
+        val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build
+        var PolyhedronSaturationOperator operator
+
+        new(PolyhedronSolver solver, ModelGenerationStatistics statistics) {
+                super(statistics)
+                this.solver = solver
+        }
+
+        override protected initialize() {
+                operator = solver.createSaturationOperator(polyhedron)
+        }
+
+        override protected doSaturate() {
+                val signature = polyhedron.createSignature
+                val cachedSignature = cache.getIfPresent(signature)
+                switch (cachedSignature) {
+                        case null: {
+                                incrementScopePropagationSolverCount()
+                                val result = operator.saturate()
+                                if (result == PolyhedronSaturationResult.EMPTY) {
+                                        cache.put(signature, PolyhedronSignature.EMPTY)
+                                        false
+                                } else {
+                                        val resultSignature = polyhedron.createSignature
+                                        cache.put(signature, resultSignature)
+                                        true
+                                }
+                        }
+                        case PolyhedronSignature.EMPTY:
+                                false
+                        PolyhedronSignature.Bounds: {
+                                polyhedron.applySignature(signature)
+                                true
+                        }
+                        default:
+                                throw new IllegalStateException("Unknown polyhedron signature: " + signature)
+                }
+        }
+}
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
new file mode 100644
index 00000000..21bd2d9e
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend
@@ -0,0 +1,186 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import java.util.List
+import java.util.Map
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+interface PolyhedronSolver {
+        def PolyhedronSaturationOperator createSaturationOperator(Polyhedron polyhedron)
+}
+
+enum PolyhedronSaturationResult {
+        SATURATED,
+        EMPTY,
+        UNKNOWN
+}
+
+interface PolyhedronSaturationOperator extends AutoCloseable {
+        def Polyhedron getPolyhedron()
+
+        def PolyhedronSaturationResult saturate()
+}
+
+@FinalFieldsConstructor
+@Accessors
+class Polyhedron {
+        /**
+         * The list of dimensions (variables) for this polyhedron.
+         * 
+         * This list must not be modified after the polyhedron was created.
+         * However, lower and upper bounds of the dimensions may be changed.
+         * 
+         * Names of dimensions in this list are assumed to be unique.
+         */
+        val List<Dimension> dimensions
+
+        /**
+         * The list of constraints defining this polyhedron.
+         * 
+         * The list and its elements may be freely modified.
+         */
+        val List<LinearConstraint> constraints
+
+        /**
+         * The list of constraints that should be saturated (tightened)
+         * when a {@link PolyhedronSaturationOperator} is invoked.
+         * 
+         * This list may be freely modified.
+         * 
+         * Place all dimensions and constraints here to saturate all the bounds.
+         */
+        val List<LinearBoundedExpression> expressionsToSaturate
+
+        override toString() '''
+                Dimensions:
+                        «FOR dimension : dimensions»
+                                «dimension»
+                        «ENDFOR»
+                Constraints:
+                        «FOR constraint : constraints»
+                                «constraint»
+                        «ENDFOR»
+        '''
+
+        def createSignature() {
+                val size = dimensions.size + constraints.size
+                val lowerBounds = newArrayOfSize(size)
+                val upperBounds = newArrayOfSize(size)
+                var int i = 0
+                for (dimension : dimensions) {
+                        lowerBounds.set(i, dimension.lowerBound)
+                        upperBounds.set(i, dimension.upperBound)
+                        i++
+                }
+                for (constraint : constraints) {
+                        lowerBounds.set(i, constraint.lowerBound)
+                        upperBounds.set(i, constraint.upperBound)
+                        i++
+                }
+                new PolyhedronSignature.Bounds(lowerBounds, upperBounds)
+        }
+
+        def applySignature(PolyhedronSignature.Bounds signature) {
+                val lowerBounds = signature.lowerBounds
+                val upperBounds = signature.upperBounds
+                var int i = 0
+                for (dimension : dimensions) {
+                        dimension.lowerBound = lowerBounds.get(i)
+                        dimension.upperBound = upperBounds.get(i)
+                        i++
+                }
+                for (constraint : constraints) {
+                        constraint.lowerBound = lowerBounds.get(i)
+                        constraint.upperBound = upperBounds.get(i)
+                        i++
+                }
+        }
+}
+
+abstract class PolyhedronSignature {
+        public static val EMPTY = new PolyhedronSignature {
+                override toString() {
+                        "PolyhedronSignature.EMPTY"
+                }
+        }
+
+        private new() {
+        }
+
+        @Data
+        static class Bounds extends PolyhedronSignature {
+                val Integer[] lowerBounds
+                val Integer[] upperBounds
+        }
+}
+
+@Accessors
+class Bounds {
+        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
+                }
+        }
+
+        def void assertBetween(Integer tighterLowerBound, Integer tighterUpperBound) {
+                tightenLowerBound(tighterLowerBound)
+                tightenUpperBound(tighterUpperBound)
+        }
+
+        def void assertEqualsTo(int bound) {
+                assertBetween(bound, bound)
+        }
+}
+
+abstract class LinearBoundedExpression extends Bounds {
+}
+
+@Accessors
+class Dimension extends LinearBoundedExpression {
+        val String name
+
+        @FinalFieldsConstructor
+        new() {
+        }
+
+        new(String name, Integer lowerBound, Integer upperBound) {
+                this(name)
+                this.lowerBound = lowerBound
+                this.upperBound = upperBound
+        }
+
+        override toString() {
+                '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«name»«IF upperBound !== null» <= «upperBound»«ENDIF»'''
+        }
+
+}
+
+@Accessors
+class LinearConstraint extends LinearBoundedExpression {
+        val Map<Dimension, Integer> coefficients
+
+        @FinalFieldsConstructor
+        new() {
+        }
+
+        new(Map<Dimension, Integer> coefficients, Integer lowerBound, Integer upperBound) {
+                this(coefficients)
+                this.lowerBound = lowerBound
+                this.upperBound = upperBound
+        }
+
+        override toString() {
+                '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«FOR pair : coefficients.entrySet SEPARATOR " + "»«IF pair.value != 1»«pair.value» * «ENDIF»«pair.key.name»«ENDFOR»«IF upperBound !== null» <= «upperBound»«ENDIF»'''
+        }
+
+}
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..abf65be3
--- /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,156 @@
+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
+        Relation inverseRelation
+        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() {
+                // TODO Optimize the unrepairable matches computation,
+                // or come up with a heuristic when does computing unrepairables worth the overhead.
+                false && constrainsUnfinished && canHaveMultipleSourcesPerTarget && reference
+        }
+
+        def constrainsRemainingInverse() {
+                lowerBound >= 1 && !containment && !container && inverseUpperBoundFinite && reference
+        }
+
+        def constrainsRemainingContents() {
+                containment
+        }
+
+        def isActive() {
+                constrainsUnfinished || constrainsUnrepairable || constrainsRemainingInverse || constrainsRemainingContents
+        }
+
+        def isSourceTypeComplex() {
+                getParamTypeReference(0) instanceof ComplexTypeReference
+        }
+        
+        def isTargetTypeComplex() {
+                getParamTypeReference(1) instanceof ComplexTypeReference
+        }
+        
+        def isReference() {
+                sourceTypeComplex && targetTypeComplex
+        }
+
+        def getSourceType() {
+                getParamType(0)
+        }
+
+        def getTargetType() {
+                getParamType(1)
+        }
+
+        private def getParamTypeReference(int i) {
+                val parameters = relation.parameters
+                if (i < parameters.size) {
+                        return parameters.get(i)
+                }
+                throw new IllegalArgumentException("Argument index out of range")
+        }
+        
+        private def getParamType(int i) {
+                val reference = getParamTypeReference(i)
+                if (reference instanceof ComplexTypeReference) {
+                        return reference.referred
+                }
+                throw new IllegalArgumentException("Constraint with primitive 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(inverseRelation)
+                                container = containmentRelations.contains(inverseRelation)
+                        }
+                        if (containment) {
+                                inverseUpperMultiplicity = 1
+                        }
+                        val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, 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/RemainingMultiplicityCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend
new file mode 100644
index 00000000..48b52d28
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend
@@ -0,0 +1,111 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import java.util.Iterator
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+@FinalFieldsConstructor
+abstract class MultiplicityCalculator<Match extends IPatternMatch> {
+        val ViatraQueryMatcher<Match> matcher
+
+        def getMultiplicity() {
+                val iterator = matcher.streamAllMatches.iterator
+                getMultiplicity(iterator)
+        }
+        
+        def getMultiplicity(PartialInterpretation interpretation) {
+                val partialMatch = matcher.newEmptyMatch
+                partialMatch.set(0, interpretation.problem)
+                partialMatch.set(1, interpretation)
+                val iterator = matcher.streamAllMatches(partialMatch).iterator
+                getMultiplicity(iterator)
+        }
+
+        protected def int getMultiplicity(Iterator<? extends Match> iterator)
+}
+
+class RemainingMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> {
+        val int bound
+
+        @FinalFieldsConstructor
+        private new() {
+        }
+
+        protected override getMultiplicity(Iterator<? extends Match> iterator) {
+                var res = 0
+                while (iterator.hasNext) {
+                        val match = iterator.next
+                        val existingMultiplicity = match.get(3) as Integer
+                        if (existingMultiplicity < bound) {
+                                res += bound - existingMultiplicity
+                        }
+                }
+                res
+        }
+        
+        static def <Match extends IPatternMatch> of(ViatraQueryMatcher<Match> matcher, int bound) {
+                if (bound < 0) {
+                        new RemainingInfiniteMultiplicityCalculator(matcher)
+                } else {
+                        new RemainingMultiplicityCalculator(matcher, bound)
+                }
+        }
+}
+
+package class RemainingInfiniteMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> {
+        
+        @FinalFieldsConstructor
+        package new() {
+        }
+        
+        protected override getMultiplicity(Iterator<? extends Match> iterator) {
+                if (iterator.hasNext) {
+                        -1
+                } else {
+                        0
+                }
+        }
+}
+
+@FinalFieldsConstructor
+class UnrepairableMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> {
+        val int lowerBound
+        
+        override protected getMultiplicity(Iterator<? extends Match> iterator) {
+                var res = 0
+                while (iterator.hasNext) {
+                        val match = iterator.next
+                        val existingMultiplicity = match.get(3) as Integer
+                        if (existingMultiplicity < lowerBound) {
+                                val missingMultiplcity = lowerBound - existingMultiplicity
+                                val numerOfRepairMatches = match.get(4) as Integer
+                                val unrepairableMultiplicty = missingMultiplcity - numerOfRepairMatches
+                                if (unrepairableMultiplicty > res) {
+                                        res = unrepairableMultiplicty
+                                }
+                        }
+                }
+                res
+        }
+}
+
+@FinalFieldsConstructor
+class RemainingInverseMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> {
+        val int upperBound
+        
+        override protected getMultiplicity(Iterator<? extends Match> iterator) {
+                var res = 0
+                while (iterator.hasNext) {
+                        val match = iterator.next
+                        val existingMultiplicity = match.get(3) as Integer
+                        if (existingMultiplicity < upperBound) {
+                                val availableMultiplicity = upperBound - existingMultiplicity
+                                val numberOfRepairMatches = match.get(4) as Integer
+                                res += Math.min(availableMultiplicity, numberOfRepairMatches)
+                        }
+                }
+                res
+        }
+}
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
new file mode 100644
index 00000000..cacba3c6
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
@@ -0,0 +1,161 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality

+

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation

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

+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.PartialTypeInterpratation

+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope

+import java.util.HashMap

+import java.util.HashSet

+import java.util.Map

+import java.util.Set

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

+

+class ScopePropagator {

+        @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation

+        @Accessors(PROTECTED_GETTER) val ModelGenerationStatistics statistics

+        val Map<PartialTypeInterpratation, Scope> type2Scope

+        @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes

+        @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes

+        

+        @Accessors(PUBLIC_GETTER) var scopePropagationNeeded = false

+

+        new(PartialInterpretation p, ModelGenerationStatistics statistics) {

+                partialInterpretation = p

+                this.statistics = statistics

+                type2Scope = new HashMap

+                for (scope : p.scopes) {

+                        type2Scope.put(scope.targetTypeInterpretation, scope)

+                }

+

+                superScopes = new HashMap

+                subScopes = new HashMap

+                for (scope : p.scopes) {

+                        superScopes.put(scope, new HashSet)

+                        subScopes.put(scope, new HashSet)

+                }

+

+                for (scope : p.scopes) {

+                        val target = scope.targetTypeInterpretation

+                        if (target instanceof PartialComplexTypeInterpretation) {

+                                val supertypeInterpretations = target.supertypeInterpretation

+                                for (supertypeInterpretation : supertypeInterpretations) {

+                                        val supertypeScope = type2Scope.get(supertypeInterpretation)

+                                        superScopes.get(scope).add(supertypeScope)

+                                        subScopes.get(supertypeScope).add(scope)

+                                }

+                        }

+                }

+                var boolean changed

+                do {

+                        changed = false

+                        for (scope : p.scopes) {

+                                val subScopeSet = subScopes.get(scope)

+                                val superScopeSet = superScopes.get(scope)

+                                for (subScope : subScopeSet) {

+                                        changed = changed || superScopes.get(subScope).addAll(superScopeSet)

+                                }

+                                for (superScope : superScopeSet) {

+                                        changed = changed || subScopes.get(superScope).addAll(subScopeSet)

+                                }

+                        }

+                } while (changed)

+

+                copyScopeBoundsToHeuristic()

+        }

+

+        def void propagateAllScopeConstraints() {

+                scopePropagationNeeded = false

+                if (!valid) {

+                        return

+                }

+                statistics.incrementScopePropagationCount()

+                doPropagateAllScopeConstraints()

+        }

+

+        def isValid() {

+                partialInterpretation.maxNewElements == -1 ||

+                        partialInterpretation.minNewElements <= partialInterpretation.maxNewElements

+        }

+

+        protected def copyScopeBoundsToHeuristic() {

+                partialInterpretation.minNewElementsHeuristic = partialInterpretation.minNewElements

+                for (scope : partialInterpretation.scopes) {

+                        scope.minNewElementsHeuristic = scope.minNewElements

+                }

+        }

+

+        protected def void doPropagateAllScopeConstraints() {

+                // Nothing to propagate.

+        }

+

+        def decrementTypeScope(PartialTypeInterpratation t) {

+                val isPrimitive = t instanceof PartialPrimitiveInterpretation || t === null

+                if (isPrimitive) {

+                        return

+                }

+                scopePropagationNeeded = true

+//              println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')

+                val targetScope = type2Scope.get(t)

+                if (targetScope !== null) {

+                        targetScope.removeOne

+                        val sups = superScopes.get(targetScope)

+                        sups.forEach[removeOne]

+                }

+                if (this.partialInterpretation.minNewElements > 0) {

+                        this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1

+                }

+                if (this.partialInterpretation.minNewElementsHeuristic > 0) {

+                        this.partialInterpretation.minNewElementsHeuristic = this.partialInterpretation.minNewElementsHeuristic - 1

+                }

+                if (this.partialInterpretation.maxNewElements > 0) {

+                        this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1

+                } else if (this.partialInterpretation.maxNewElements === 0) {

+                        setScopesInvalid()

+                }

+

+//              println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''')

+//              println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''')

+//              this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]

+//              println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')

+        }

+        

+        def addedToRelation(Relation r) {

+                if (isPropagationNeededAfterAdditionToRelation(r)) {

+                        scopePropagationNeeded = true

+                }

+        }

+

+        protected def setScopesInvalid() {

+                partialInterpretation.minNewElements = Integer.MAX_VALUE

+                partialInterpretation.maxNewElements = 0

+                for (scope : partialInterpretation.scopes) {

+                        scope.minNewElements = Integer.MAX_VALUE

+                        scope.maxNewElements = 0

+                }

+        }

+

+        protected def isPropagationNeededAfterAdditionToRelation(Relation r) {

+                false

+        }

+        

+        def isQueryEngineFlushRequiredBeforePropagation() {

+                false

+        }

+

+        private def removeOne(Scope scope) {

+                if (scope.minNewElements > 0) {

+                        scope.minNewElements = scope.minNewElements - 1

+                }

+                if (scope.minNewElementsHeuristic > 0) {

+                        scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1

+                }

+                if (scope.maxNewElements > 0) {

+                        scope.maxNewElements = scope.maxNewElements - 1

+                } else if (scope.maxNewElements === 0) {

+                        setScopesInvalid()

+                }

+        }

+}

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend
new file mode 100644
index 00000000..3165917a
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend
@@ -0,0 +1,71 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+enum PolyhedralScopePropagatorConstraints {
+        TypeHierarchy,
+        Relational
+}
+
+enum PolyhedralScopePropagatorSolver {
+        Z3Real,
+        Z3Integer,
+        Cbc,
+        Clp
+}
+
+abstract class ScopePropagatorStrategy {
+        public static val None = new Simple("None")
+        
+        public static val Basic = new Simple("Basic")
+
+        public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy")
+
+        private new() {
+        }
+
+        def boolean requiresUpperBoundIndexing()
+
+        static class Simple extends ScopePropagatorStrategy {
+                val String name
+
+                @FinalFieldsConstructor
+                private new() {
+                }
+
+                override requiresUpperBoundIndexing() {
+                        false
+                }
+
+                override toString() {
+                        name
+                }
+        }
+
+        @Data
+        static class Polyhedral extends ScopePropagatorStrategy {
+                public static val UNLIMITED_TIME = -1
+
+                val PolyhedralScopePropagatorConstraints constraints
+                val PolyhedralScopePropagatorSolver solver
+                val boolean updateHeuristic
+                val double timeoutSeconds
+
+                @FinalFieldsConstructor
+                new() {
+                }
+
+                new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver, boolean updateHeuristic) {
+                        this(constraints, solver, updateHeuristic, UNLIMITED_TIME)
+                }
+                
+                new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) {
+                        this(constraints, solver, true)
+                }
+
+                override requiresUpperBoundIndexing() {
+                        constraints == PolyhedralScopePropagatorConstraints.Relational
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend
new file mode 100644
index 00000000..d1704b39
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend
@@ -0,0 +1,85 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
+
+class TypeHierarchyScopePropagator extends ScopePropagator {
+
+        new(PartialInterpretation p, ModelGenerationStatistics statistics) {
+                super(p, statistics)
+        }
+
+        protected override doPropagateAllScopeConstraints() {
+                var boolean hadChanged
+                do {
+                        hadChanged = false
+                        for (superScopeEntry : superScopes.entrySet) {
+                                val sub = superScopeEntry.key
+                                hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged
+                                hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged
+                                for (sup : superScopeEntry.value) {
+                                        hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged
+                                        hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged
+                                }
+                        }
+                } while (hadChanged)
+        }
+
+        private def propagateLowerLimitUp(Scope subScope, Scope superScope) {
+                var changed = false
+                if (subScope.minNewElements > superScope.minNewElements) {
+                        superScope.minNewElements = subScope.minNewElements
+                        changed = true
+                }
+                if (subScope.minNewElementsHeuristic > superScope.minNewElementsHeuristic) {
+                        superScope.minNewElementsHeuristic = subScope.minNewElementsHeuristic
+                        changed = true
+                }
+                changed
+        }
+
+        private def propagateUpperLimitDown(Scope subScope, Scope superScope) {
+                if (superScope.maxNewElements >= 0 &&
+                        (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) {
+//                      println('''
+//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»
+//                      subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements»
+//                      ''')
+                        subScope.maxNewElements = superScope.maxNewElements
+                        return true
+                } else {
+                        return false
+                }
+        }
+
+        private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) {
+                var changed = false
+                if (subScope.minNewElements > p.minNewElements) {
+//                      println('''
+//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes
+//                      p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements»
+//                      ''')
+                        p.minNewElements = subScope.minNewElements
+                        changed = true
+                }
+                if (subScope.minNewElementsHeuristic > p.minNewElementsHeuristic) {
+                        p.minNewElementsHeuristic = subScope.minNewElementsHeuristic
+                        changed = true
+                }
+                changed
+        }
+
+        private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) {
+                if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) {
+//                      println('''
+//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes
+//                      subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements»
+//                      ''')
+                        subScope.maxNewElements = p.maxNewElements
+                        return true
+                } else {
+                        return false
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend
new file mode 100644
index 00000000..3b831433
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend
@@ -0,0 +1,272 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import com.microsoft.z3.AlgebraicNum
+import com.microsoft.z3.ArithExpr
+import com.microsoft.z3.Context
+import com.microsoft.z3.Expr
+import com.microsoft.z3.IntNum
+import com.microsoft.z3.Optimize
+import com.microsoft.z3.RatNum
+import com.microsoft.z3.Status
+import com.microsoft.z3.Symbol
+import java.math.BigDecimal
+import java.math.MathContext
+import java.math.RoundingMode
+import java.util.Map
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+class Z3PolyhedronSolver implements PolyhedronSolver {
+        val boolean lpRelaxation
+        val double timeoutSeconds
+
+        @FinalFieldsConstructor
+        new() {
+        }
+
+        new() {
+                this(false, -1)
+        }
+
+        override createSaturationOperator(Polyhedron polyhedron) {
+                new DisposingZ3SaturationOperator(this, polyhedron)
+        }
+
+        def createPersistentSaturationOperator(Polyhedron polyhedron) {
+                new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds)
+        }
+}
+
+@FinalFieldsConstructor
+class DisposingZ3SaturationOperator implements PolyhedronSaturationOperator {
+        val Z3PolyhedronSolver solver
+        @Accessors val Polyhedron polyhedron
+
+        override saturate() {
+                val persistentOperator = solver.createPersistentSaturationOperator(polyhedron)
+                try {
+                        persistentOperator.saturate
+                } finally {
+                        persistentOperator.close
+                }
+        }
+
+        override close() throws Exception {
+                // Nothing to close.
+        }
+}
+
+class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
+        static val INFINITY_SYMBOL_NAME = "oo"
+        static val MULT_SYMBOL_NAME = "*"
+        static val TIMEOUT_SYMBOL_NAME = "timeout"
+        static val INTEGER_PRECISION = new BigDecimal(Integer.MAX_VALUE).precision
+        static val ROUND_DOWN = new MathContext(INTEGER_PRECISION, RoundingMode.FLOOR)
+        static val ROUND_UP = new MathContext(INTEGER_PRECISION, RoundingMode.CEILING)
+        // The interval isolating the number is smaller than 1/10^precision. 
+        static val ALGEBRAIC_NUMBER_ROUNDING = 0
+
+        extension val Context context
+        val Symbol infinitySymbol
+        val Symbol multSymbol
+        val Map<Dimension, ArithExpr> variables
+        val int timeoutMilliseconds
+
+        new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds) {
+                super(polyhedron)
+                context = new Context
+                infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME)
+                multSymbol = context.mkSymbol(MULT_SYMBOL_NAME)
+                variables = polyhedron.dimensions.toInvertedMap [ dimension |
+                        val name = dimension.name
+                        if (lpRelaxation) {
+                                mkRealConst(name)
+                        } else {
+                                mkIntConst(name)
+                        }
+                ]
+                timeoutMilliseconds = Math.ceil(timeoutSeconds * 1000) as int
+        }
+
+        override doSaturate() {
+                val status = executeSolver()
+                convertStatusToSaturationResult(status)
+        }
+
+        private def convertStatusToSaturationResult(Status status) {
+                switch (status) {
+                        case SATISFIABLE:
+                                PolyhedronSaturationResult.SATURATED
+                        case UNSATISFIABLE:
+                                PolyhedronSaturationResult.EMPTY
+                        case UNKNOWN:
+                                PolyhedronSaturationResult.UNKNOWN
+                        default:
+                                throw new IllegalArgumentException("Unknown Status: " + status)
+                }
+        }
+
+        private def executeSolver() {
+                for (expressionToSaturate : polyhedron.expressionsToSaturate) {
+                        val expr = expressionToSaturate.toExpr
+                        val lowerResult = saturateLowerBound(expr, expressionToSaturate)
+                        if (lowerResult != Status.SATISFIABLE) {
+                                return lowerResult
+                        }
+                        val upperResult = saturateUpperBound(expr, expressionToSaturate)
+                        if (upperResult != Status.SATISFIABLE) {
+                                return upperResult
+                        }
+                }
+                Status.SATISFIABLE
+        }
+
+        private def saturateLowerBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) {
+                val optimize = prepareOptimize
+                val handle = optimize.MkMinimize(expr)
+                val status = optimize.Check()
+                if (status == Status.SATISFIABLE) {
+                        val value = switch (resultExpr : handle.lower) {
+                                IntNum:
+                                        resultExpr.getInt()
+                                RatNum:
+                                        ceil(resultExpr)
+                                AlgebraicNum:
+                                        ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING))
+                                default:
+                                        if (isNegativeInfinity(resultExpr)) {
+                                                null
+                                        } else {
+                                                throw new IllegalArgumentException("Integer result expected, got: " + resultExpr)
+                                        }
+                        }
+                        expressionToSaturate.lowerBound = value
+                }
+                status
+        }
+
+        private def floor(RatNum ratNum) {
+                val numerator = new BigDecimal(ratNum.numerator.bigInteger)
+                val denominator = new BigDecimal(ratNum.denominator.bigInteger)
+                numerator.divide(denominator, ROUND_DOWN).setScale(0, RoundingMode.FLOOR).intValue
+        }
+
+        private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) {
+                val optimize = prepareOptimize
+                val handle = optimize.MkMaximize(expr)
+                val status = optimize.Check()
+                if (status == Status.SATISFIABLE) {
+                        val value = switch (resultExpr : handle.upper) {
+                                IntNum:
+                                        resultExpr.getInt()
+                                RatNum:
+                                        floor(resultExpr)
+                                AlgebraicNum:
+                                        floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING))
+                                default:
+                                        if (isPositiveInfinity(resultExpr)) {
+                                                null
+                                        } else {
+                                                throw new IllegalArgumentException("Integer result expected, got: " + resultExpr)
+                                        }
+                        }
+                        expressionToSaturate.upperBound = value
+                }
+                status
+        }
+
+        private def ceil(RatNum ratNum) {
+                val numerator = new BigDecimal(ratNum.numerator.bigInteger)
+                val denominator = new BigDecimal(ratNum.denominator.bigInteger)
+                numerator.divide(denominator, ROUND_UP).setScale(0, RoundingMode.CEILING).intValue
+        }
+
+        private def isPositiveInfinity(Expr expr) {
+                expr.app && expr.getFuncDecl.name == infinitySymbol
+        }
+
+        private def isNegativeInfinity(Expr expr) {
+                // Negative infinity is represented as (* (- 1) oo)
+                if (!expr.app || expr.getFuncDecl.name != multSymbol || expr.numArgs != 2) {
+                        return false
+                }
+                isPositiveInfinity(expr.args.get(1))
+        }
+
+        private def prepareOptimize() {
+                val optimize = mkOptimize()
+                if (timeoutMilliseconds >= 0) {
+                        val params = mkParams()
+                        // We cannot turn TIMEOUT_SYMBOL_NAME into a Symbol in the constructor,
+                        // because there is no add(Symbol, int) overload.
+                        params.add(TIMEOUT_SYMBOL_NAME, timeoutMilliseconds)
+                        optimize.parameters = params
+                }
+                assertConstraints(optimize)
+                optimize
+        }
+
+        private def assertConstraints(Optimize it) {
+                for (pair : variables.entrySet) {
+                        assertBounds(pair.value, pair.key)
+                }
+                for (constraint : nonTrivialConstraints) {
+                        val expr = createLinearCombination(constraint.coefficients)
+                        assertBounds(expr, constraint)
+                }
+        }
+
+        private def assertBounds(Optimize it, ArithExpr expression, LinearBoundedExpression bounds) {
+                val lowerBound = bounds.lowerBound
+                val upperBound = bounds.upperBound
+                if (lowerBound == upperBound) {
+                        if (lowerBound === null) {
+                                return
+                        }
+                        Assert(mkEq(expression, mkInt(lowerBound)))
+                } else {
+                        if (lowerBound !== null) {
+                                Assert(mkGe(expression, mkInt(lowerBound)))
+                        }
+                        if (upperBound !== null) {
+                                Assert(mkLe(expression, mkInt(upperBound)))
+                        }
+                }
+        }
+
+        private def toExpr(LinearBoundedExpression linearBoundedExpression) {
+                switch (linearBoundedExpression) {
+                        Dimension: variables.get(linearBoundedExpression)
+                        LinearConstraint: createLinearCombination(linearBoundedExpression.coefficients)
+                        default: throw new IllegalArgumentException("Unknown linear bounded expression:" + linearBoundedExpression)
+                }
+        }
+
+        private def createLinearCombination(Map<Dimension, Integer> coefficients) {
+                val size = coefficients.size
+                if (size == 0) {
+                        return mkInt(0)
+                }
+                val array = newArrayOfSize(size)
+                var int i = 0
+                for (pair : coefficients.entrySet) {
+                        val variable = variables.get(pair.key)
+                        if (variable === null) {
+                                throw new IllegalArgumentException("Unknown dimension: " + pair.key.name)
+                        }
+                        val coefficient = pair.value
+                        val term = if (coefficient == 1) {
+                                        variable
+                                } else {
+                                        mkMul(mkInt(coefficient), variable)
+                                }
+                        array.set(i, term)
+                        i++
+                }
+                mkAdd(array)
+        }
+
+        override close() throws Exception {
+                context.close()
+        }
+}