Optimizing generator with linear objective functions

23 files changed, 1236 insertions, 404 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
index b9da0f0b..ec1557e8 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
@@ -8,7 +8,8 @@ Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra,
  hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval,
  hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators,
  hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns,
- hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries
+ hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries,
+ hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules
 Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
  hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0",
  hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend
new file mode 100644
index 00000000..bd5bf807
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend
@@ -0,0 +1,47 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
+
+class ModelGenerationStatistics {
+        public var long transformationExecutionTime = 0
+
+        synchronized def addExecutionTime(long amount) {
+                transformationExecutionTime += amount
+        }
+
+        public var long scopePropagationTime = 0
+
+        synchronized def addScopePropagationTime(long amount) {
+                scopePropagationTime += amount
+        }
+
+        public var long mustRelationPropagationTime = 0
+
+        synchronized def addMustRelationPropagationTime(long amount) {
+                mustRelationPropagationTime += amount
+        }
+
+        public var long preliminaryTypeAnalisisTime = 0
+
+        public var int decisionsTried = 0
+
+        synchronized def incrementDecisionCount() {
+                decisionsTried++
+        }
+
+        public var int transformationInvocations
+
+        synchronized def incrementTransformationCount() {
+                transformationInvocations++
+        }
+
+        public var int scopePropagatorInvocations
+
+        synchronized def incrementScopePropagationCount() {
+                scopePropagatorInvocations++
+        }
+
+        public var int scopePropagatorSolverInvocations
+
+        synchronized def incrementScopePropagationSolverCount() {
+                scopePropagatorSolverInvocations++
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend
new file mode 100644
index 00000000..9296a0be
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend
@@ -0,0 +1,44 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra

+

+import com.google.common.collect.ImmutableMap

+import com.google.common.collect.ImmutableSet

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel

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

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

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

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

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

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

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

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

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

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

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

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

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

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider

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

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

+import java.util.Collection

+import java.util.List

+import java.util.Map

+import java.util.Set

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

+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.viatra.query.runtime.matchers.psystem.PConstraint

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

+import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule

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

+

+enum TypeInferenceMethod {

+        Generic,

+        PreliminaryAnalysis

+}
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/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..6054affe
--- /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 [ _, 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/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
index c28d4caa..ad8f94ab 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
@@ -1,7 +1,5 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
 
-import com.google.common.cache.Cache
-import com.google.common.cache.CacheBuilder
 import com.google.common.collect.ImmutableList
 import com.google.common.collect.ImmutableMap
 import com.google.common.collect.ImmutableSet
@@ -23,7 +21,6 @@ import java.util.HashSet
 import java.util.List
 import java.util.Map
 import java.util.Set
-import javax.naming.OperationNotSupportedException
 import org.eclipse.viatra.query.runtime.api.IPatternMatch
 import org.eclipse.viatra.query.runtime.api.IQuerySpecification
 import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
@@ -32,31 +29,29 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope
 import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
 
 class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
-        static val CACHE_SIZE = 10000
-
         val boolean updateHeuristic
         val Map<Scope, LinearBoundedExpression> scopeBounds
         val LinearBoundedExpression topLevelBounds
         val Polyhedron polyhedron
-        val PolyhedronSaturationOperator operator
+        val PolyhedronScopePropagatorStrategy strategy
         val Set<Relation> relevantRelations
-        val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build
         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, PolyhedronSolver solver, boolean propagateRelations,
-                boolean updateHeuristic) {
+                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
-                operator = solver.createSaturationOperator(polyhedron)
+                strategy.setPolyhedron(polyhedron, builder.typeBounds, builder.expressionsCache)
                 propagateAllScopeConstraints()
                 if (propagateRelations) {
                         val maximumNumberOfNewNodes = topLevelBounds.upperBound
@@ -80,30 +75,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                 resetBounds()
                 populatePolyhedronFromScope()
 //              println(polyhedron)
-                val signature = polyhedron.createSignature
-                val cachedSignature = cache.getIfPresent(signature)
-                switch (cachedSignature) {
-                        case null: {
-                                statistics.incrementScopePropagationSolverCount
-                                val result = operator.saturate()
-                                if (result == PolyhedronSaturationResult.EMPTY) {
-                                        cache.put(signature, PolyhedronSignature.EMPTY)
-//                                      println("INVALID")
-                                        setScopesInvalid()
-                                } else {
-                                        val resultSignature = polyhedron.createSignature
-                                        cache.put(signature, resultSignature)
-                                        populateScopesFromPolyhedron()
-                                }
-                        }
-                        case PolyhedronSignature.EMPTY:
-                                setScopesInvalid()
-                        PolyhedronSignature.Bounds: {
-                                polyhedron.applySignature(signature)
-                                populateScopesFromPolyhedron()
-                        }
-                        default:
-                                throw new IllegalStateException("Unknown polyhedron signature: " + signature)
+                if (strategy.saturate) {
+                        populateScopesFromPolyhedron()
+                } else {
+                        setScopesInvalid()
                 }
 //              println(polyhedron)
                 if (updateHeuristic) {
@@ -112,9 +87,9 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
         }
 
         override isPropagationNeededAfterAdditionToRelation(Relation r) {
-                relevantRelations.contains(r) || super.isPropagationNeededAfterAdditionToRelation(r)
+                relevantRelations.contains(r) || strategy.isRelevantRelation(r) || super.isPropagationNeededAfterAdditionToRelation(r)
         }
-        
+
         override isQueryEngineFlushRequiredBeforePropagation() {
                 true
         }
@@ -253,7 +228,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                         }
                         buildRelevantRelations(constraints.keySet)
                         for (hint : hints) {
-                                updatersBuilder.add(hint.createConstraintUpdater(this))
+                                val updater = hint.createConstraintUpdater(this)
+                                if (updater !== null) {
+                                        updatersBuilder.add(updater)
+                                }
                         }
                         updaters = updatersBuilder.build
                         addCachedConstraintsToPolyhedron()
@@ -410,7 +388,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                         for (scope : p.scopes) {
                                 switch (targetTypeInterpretation : scope.targetTypeInterpretation) {
                                         PartialPrimitiveInterpretation:
-                                                throw new OperationNotSupportedException("Primitive type scopes are not yet implemented")
+                                                throw new IllegalStateException("Primitive type scopes are not yet implemented")
                                         PartialComplexTypeInterpretation: {
                                                 val complexType = targetTypeInterpretation.interpretationOf
                                                 val typeBound = typeBounds.get(complexType)
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
index 4e046190..21bd2d9e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend
@@ -116,7 +116,7 @@ abstract class PolyhedronSignature {
 }
 
 @Accessors
-abstract class LinearBoundedExpression {
+class Bounds {
         var Integer lowerBound
         var Integer upperBound
 
@@ -132,12 +132,19 @@ abstract class LinearBoundedExpression {
                 }
         }
 
+        def void assertBetween(Integer tighterLowerBound, Integer tighterUpperBound) {
+                tightenLowerBound(tighterLowerBound)
+                tightenUpperBound(tighterUpperBound)
+        }
+
         def void assertEqualsTo(int bound) {
-                tightenLowerBound(bound)
-                tightenUpperBound(bound)
+                assertBetween(bound, bound)
         }
 }
 
+abstract class LinearBoundedExpression extends Bounds {
+}
+
 @Accessors
 class Dimension extends LinearBoundedExpression {
         val String name
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
index 4ad61ccb..402a0b7d 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
@@ -4,6 +4,7 @@ Bundle-Name: Reasoner
 Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
 Bundle-Version: 1.0.0.qualifier
 Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner,
+ hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse,
  hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
 Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
  hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend
index 9ef5e091..691e0645 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend
@@ -1,7 +1,6 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
 
 import org.eclipse.viatra.dse.objectives.IGlobalConstraint
-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
 
 abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint {
         val protected ModelGenerationMethod method
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend
index 3bcd9116..25137eba 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend
@@ -1,226 +1,201 @@
-package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra

-

-import com.google.common.collect.ImmutableMap

-import com.google.common.collect.ImmutableSet

-import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel

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

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

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

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint

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

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

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

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

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

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver

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

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider

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

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

-import java.util.Collection

-import java.util.List

-import java.util.Map

-import java.util.Set

-import org.eclipse.viatra.query.runtime.api.GenericQueryGroup

-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.viatra.query.runtime.matchers.psystem.PConstraint

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

-import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule

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

-

-class ModelGenerationStatistics {

-        public var long transformationExecutionTime = 0

-

-        synchronized def addExecutionTime(long amount) {

-                transformationExecutionTime += amount

-        }

-

-        public var long scopePropagationTime = 0

-

-        synchronized def addScopePropagationTime(long amount) {

-                scopePropagationTime += amount

-        }

-        

-        public var long mustRelationPropagationTime = 0

-

-        synchronized def addMustRelationPropagationTime(long amount) {

-                mustRelationPropagationTime += amount

-        }

-

-        public var long preliminaryTypeAnalisisTime = 0

-

-        public var int decisionsTried = 0

-

-        synchronized def incrementDecisionCount() {

-                decisionsTried++

-        }

-

-        public var int transformationInvocations

-

-        synchronized def incrementTransformationCount() {

-                transformationInvocations++

-        }

-

-        public var int scopePropagatorInvocations

-

-        synchronized def incrementScopePropagationCount() {

-                scopePropagatorInvocations++

-        }

-

-        public var int scopePropagatorSolverInvocations

-

-        synchronized def incrementScopePropagationSolverCount() {

-                scopePropagatorSolverInvocations++

-        }

-}

-

-@Data class ModelGenerationMethod {

-        ModelGenerationStatistics statistics

-

-        Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules

-        Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules

-

-        List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities

-

-        Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF

-

-        Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF

-

-        Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions

-        Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions

-

-        Map<String, ModalPatternQueries> modalRelationQueries

-

-        Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns

-}

-

-enum TypeInferenceMethod {

-        Generic,

-        PreliminaryAnalysis

-}

-

-class ModelGenerationMethodProvider {

-        val PatternProvider patternProvider = new PatternProvider

-        val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider

-        val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider

-        val relationConstraintCalculator = new RelationConstraintCalculator

-

-        def ModelGenerationMethod createModelGenerationMethod(

-                LogicProblem logicProblem,

-                PartialInterpretation emptySolution,

-                ReasonerWorkspace workspace,

-                boolean nameNewElements,

-                TypeInferenceMethod typeInferenceMethod,

-                boolean calculateObjectCreationCosts,

-                ScopePropagatorStrategy scopePropagatorStrategy,

-                Collection<LinearTypeConstraintHint> hints,

-                Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators,

-                DocumentationLevel debugLevel

-        ) {

-                val statistics = new ModelGenerationStatistics

-                val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL)

-

-                val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery).

-                        map[it.patternPQuery as PQuery].toSet

-

-                val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem)

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

-                        workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints,

-                        unitPropagationPatternGenerators, writeFiles)

-

-                val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics)

-                scopePropagator.propagateAllScopeConstraints

-                val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution,

-                        queries, scopePropagator, statistics)

-                val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution,

-                        queries, unitRulePropagator, nameNewElements, statistics)

-                val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator,

-                        statistics)

-

-                val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries,

-                        calculateObjectCreationCosts)

-

-                val unfinishedWF = queries.getUnfinishedWFQueries.values

-

-                val modalRelationQueriesBuilder = ImmutableMap.builder

-                for (entry : queries.modalRelationQueries.entrySet) {

-                        val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head

-                        if (annotation !== null) {

-                                modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value)

-                        }

-                }

-                val modalRelationQueries = modalRelationQueriesBuilder.build

-

-                val invalidWF = queries.getInvalidWFQueries.values

-

-                val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns

-                val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns

-

-                val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll(

-                        queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll(queries.

-                        multiplicityConstraintQueries.values.flatMap[allQueries]).addAll(queries.unfinishedWFQueries.values).addAll(

-                        queries.invalidWFQueries.values).addAll(queries.mustUnitPropagationPreconditionPatterns.values).addAll(

-                        queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build

-                val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution))

-                GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine)

-

-                return new ModelGenerationMethod(

-                        statistics,

-                        objectRefinementRules.values,

-                        relationRefinementRules.values,

-                        unfinishedMultiplicities,

-                        unfinishedWF,

-                        invalidWF,

-                        mustUnitPropagationPreconditions,

-                        currentUnitPropagationPreconditions,

-                        modalRelationQueries,

-                        queries.allQueries

-                )

-        }

-

-        private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy,

-                PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, GeneratedPatterns queries,

-                ModelGenerationStatistics statistics) {

-                if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) {

-                        throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.")

-                }

-                switch (scopePropagatorStrategy) {

-                        case ScopePropagatorStrategy.None,

-                        case ScopePropagatorStrategy.Basic:

-                                new ScopePropagator(emptySolution, statistics)

-                        case ScopePropagatorStrategy.BasicTypeHierarchy:

-                                new TypeHierarchyScopePropagator(emptySolution, statistics)

-                        ScopePropagatorStrategy.Polyhedral: {

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

-                                val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName]

-                                val solver = switch (scopePropagatorStrategy.solver) {

-                                        case Z3Integer:

-                                                new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds)

-                                        case Z3Real:

-                                                new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds)

-                                        case Cbc:

-                                                new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true)

-                                        case Clp:

-                                                new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true)

-                                        default:

-                                                throw new IllegalArgumentException("Unknown polyhedron solver: " +

-                                                        scopePropagatorStrategy.solver)

-                                }

-                                new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries,

-                                        queries.hasElementInContainmentQuery, allPatternsByName, hints, solver,

-                                        scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic)

-                        }

-                        default:

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

-                }

-        }

-}

+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
+
+import com.google.common.collect.ImmutableMap
+import com.google.common.collect.ImmutableSet
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CachingSimplePolyhedronScopePropagatorStrategy
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjectiveProvider
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import java.util.Collection
+import java.util.List
+import java.util.Map
+import java.util.Set
+import org.eclipse.viatra.dse.objectives.IObjective
+import org.eclipse.viatra.query.runtime.api.GenericQueryGroup
+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.viatra.query.runtime.matchers.psystem.PConstraint
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
+import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
+import org.eclipse.xtend.lib.annotations.Data
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedPolyhedronScopePropagatorStrategy
+
+@Data class ModelGenerationMethod {
+        ModelGenerationStatistics statistics
+
+        Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules
+        Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules
+
+        List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities
+
+        Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF
+
+        Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
+
+        Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions
+        Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions
+
+        Map<String, ModalPatternQueries> modalRelationQueries
+
+        Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
+
+        Collection<IObjective> costObjectives
+        boolean optimizationProblem
+        ViatraReasonerSolutionSaver solutionSaver
+}
+
+class ModelGenerationMethodProvider {
+        val PatternProvider patternProvider = new PatternProvider
+        val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider
+        val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider
+        val relationConstraintCalculator = new RelationConstraintCalculator
+
+        def ModelGenerationMethod createModelGenerationMethod(
+                LogicProblem logicProblem,
+                PartialInterpretation emptySolution,
+                ReasonerWorkspace workspace,
+                ViatraReasonerConfiguration config
+        ) {
+                val statistics = new ModelGenerationStatistics
+                val debugLevel = config.documentationLevel
+                val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL)
+
+                val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery).
+                        map[it.patternPQuery as PQuery].toSet
+
+                val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem)
+                val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries,
+                        workspace, config.typeInferenceMethod, config.scopePropagatorStrategy, relationConstraints, config.hints,
+                        config.unitPropagationPatternGenerators, writeFiles)
+
+                val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries,
+                        config.calculateObjectCreationCosts)
+                val unfinishedWF = queries.getUnfinishedWFQueries.values
+                val modalRelationQueriesBuilder = ImmutableMap.builder
+                for (entry : queries.modalRelationQueries.entrySet) {
+                        val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head
+                        if (annotation !== null) {
+                                modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value)
+                        }
+                }
+                val modalRelationQueries = modalRelationQueriesBuilder.build
+                val invalidWF = queries.getInvalidWFQueries.values
+                val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns
+                val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns
+                val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll(
+                        queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll(
+                        queries.mustRelationPropagationQueries.values).addAll(queries.multiplicityConstraintQueries.values.flatMap [
+                        allQueries
+                ]).addAll(queries.unfinishedWFQueries.values).addAll(queries.invalidWFQueries.values).addAll(
+                        queries.mustUnitPropagationPreconditionPatterns.values).addAll(
+                        queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build
+                val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution))
+                GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine)
+
+                val objectiveProvider = new ThreeValuedCostObjectiveProvider(queryEngine, emptySolution, modalRelationQueries)
+                val transformedObjectives = objectiveProvider.getCostObjectives(config.costObjectives)
+
+                val solutionSaver = new ViatraReasonerSolutionSaver(transformedObjectives.leveledExtremalObjectives,
+                        config.solutionScope.numberOfRequiredSolutions, DiversityChecker.of(config.diversityRequirement))
+
+                val allHints = ImmutableSet.builder
+                allHints.addAll(config.hints)
+                for (hint : transformedObjectives.hints) {
+                        hint.boundsProvider = solutionSaver
+                        allHints.add(hint)
+                }
+
+                val scopePropagator = createScopePropagator(config.scopePropagatorStrategy, emptySolution, allHints.build,
+                        transformedObjectives.extensionOperators, queries, statistics)
+                scopePropagator.propagateAllScopeConstraints
+                val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, queries,
+                        scopePropagator, statistics)
+                val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution,
+                        queries, unitRulePropagator, config.nameNewElements, statistics)
+                val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator,
+                        statistics)
+
+                return new ModelGenerationMethod(
+                        statistics,
+                        objectRefinementRules.values,
+                        relationRefinementRules.values,
+                        unfinishedMultiplicities,
+                        unfinishedWF,
+                        invalidWF,
+                        mustUnitPropagationPreconditions,
+                        currentUnitPropagationPreconditions,
+                        modalRelationQueries,
+                        queries.allQueries,
+                        transformedObjectives.objectives,
+                        transformedObjectives.optimizationProblem,
+                        solutionSaver
+                )
+        }
+
+        private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy,
+                PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints,
+                Collection<PolyhedronExtensionOperator> extensionOperators, GeneratedPatterns queries,
+                ModelGenerationStatistics statistics) {
+                if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) {
+                        throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.")
+                }
+                switch (scopePropagatorStrategy) {
+                        case ScopePropagatorStrategy.None,
+                        case ScopePropagatorStrategy.Basic:
+                                new ScopePropagator(emptySolution, statistics)
+                        case ScopePropagatorStrategy.BasicTypeHierarchy:
+                                new TypeHierarchyScopePropagator(emptySolution, statistics)
+                        ScopePropagatorStrategy.Polyhedral: {
+                                val types = queries.refineObjectQueries.keySet.map[newType].toSet
+                                val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName]
+                                val solver = switch (scopePropagatorStrategy.solver) {
+                                        case Z3Integer:
+                                                new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds)
+                                        case Z3Real:
+                                                new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds)
+                                        case Cbc:
+                                                new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true)
+                                        case Clp:
+                                                new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true)
+                                        default:
+                                                throw new IllegalArgumentException("Unknown polyhedron solver: " +
+                                                        scopePropagatorStrategy.solver)
+                                }
+                                val strategy = if (extensionOperators.empty) {
+                                                new CachingSimplePolyhedronScopePropagatorStrategy(solver, statistics)
+                                        } else {
+                                                new ExtendedPolyhedronScopePropagatorStrategy(solver, extensionOperators, statistics)
+                                        }
+                                new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries,
+                                        queries.hasElementInContainmentQuery, allPatternsByName, hints, strategy,
+                                        scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic)
+                        }
+                        default:
+                                throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy)
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index 8e05665c..8e992741 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -1,7 +1,5 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner

 

-import com.google.common.collect.ImmutableList

-import com.google.common.collect.Lists

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException

@@ -11,7 +9,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult

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

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

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser

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

@@ -22,7 +19,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.sta
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration

-import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective

@@ -32,11 +28,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective
 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective

-import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind

-import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement

-import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective

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

 import java.util.List

 import java.util.Map

@@ -86,13 +79,7 @@ class ViatraReasoner extends LogicReasoner {
                         problem,

                         emptySolution,

                         workspace,

-                        viatraConfig.nameNewElements,

-                        viatraConfig.typeInferenceMethod,

-                        viatraConfig.calculateObjectCreationCosts,

-                        viatraConfig.scopePropagatorStrategy,

-                        viatraConfig.hints,

-                        viatraConfig.unitPropagationPatternGenerators,

-                        viatraConfig.documentationLevel

+                        viatraConfig

                 )

 

                 val compositeObjective = new ModelGenerationCompositeObjective(

@@ -112,45 +99,21 @@ class ViatraReasoner extends LogicReasoner {
                         dse.addObjective(punishObjective)

                 }

 

-                val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size)

-                for (entry : viatraConfig.costObjectives.indexed) {

-                        val objectiveName = '''costObjective«entry.key»'''

-                        val objectiveConfig = entry.value

-                        val elementsBuilder = ImmutableList.builder

-                        for (elementConfig : objectiveConfig.elements) {

-                                val relationName = elementConfig.patternQualifiedName

-                                val modalQueries = method.modalRelationQueries.get(relationName)

-                                if (modalQueries === null) {

-                                        throw new IllegalArgumentException("Unknown relation: " + relationName)

-                                }

-                                elementsBuilder.add(new ThreeValuedCostElement(

-                                        modalQueries.currentQuery,

-                                        modalQueries.mayQuery,

-                                        modalQueries.mustQuery,

-                                        elementConfig.weight

-                                ))

-                        }

-                        val costElements = elementsBuilder.build

-                        val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind,

-                                objectiveConfig.threshold, 3)

+                for (costObjective : method.costObjectives) {

                         dse.addObjective(costObjective)

-                        if (objectiveConfig.findExtremum) {

-                                extremalObjectives += costObjective

-                        }

                 }

-

                 val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions

-                val solutionStore = if (extremalObjectives.empty) {

-                                new SolutionStore(numberOfRequiredSolutions)

-                        } else {

+                val solutionStore = if (method.optimizationProblem) {

                                 new SolutionStore()

+                        } else {

+                                new SolutionStore(numberOfRequiredSolutions)

                         }

                 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))

-                val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement)

                 val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false)

-                val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions,

-                        diversityChecker, numericSolver)

+                val solutionSaver = method.solutionSaver

+                solutionSaver.numericSolver = numericSolver

                 val solutionCopier = solutionSaver.solutionCopier

+                val diversityChecker = solutionSaver.diversityChecker

                 solutionStore.withSolutionSaver(solutionSaver)

                 dse.solutionStore = solutionStore

 

@@ -185,7 +148,8 @@ class ViatraReasoner extends LogicReasoner {
                         dse.addTransformationRule(rule)

                 }

 

-                val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, numericSolver)

+                val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver,

+                        numericSolver)

                 viatraConfig.progressMonitor.workedForwardTransformation

                 val transformationFinished = System.nanoTime

                 val transformationTime = transformationFinished - transformationStartTime

@@ -211,14 +175,15 @@ class ViatraReasoner extends LogicReasoner {
                                         it.value = (pair.value / 1000000) as int

                                 ]

                         }

-                        for(x: 0..<strategy.times.size) {

+                        for (x : 0 ..< strategy.times.size) {

                                 it.entries += createStringStatisticEntry => [

                                         it.name = '''Solution«x+1»DetailedStatistics'''

                                         it.value = strategy.times.get(x)

                                 ]

                         }

                         it.entries += createIntStatisticEntry => [

-                                it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int

+                                it.name = "ExplorationInitializationTime"

+                                it.value = ((strategy.explorationStarted - transformationFinished) / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

                                 it.name = "TransformationExecutionTime"

@@ -253,22 +218,28 @@ class ViatraReasoner extends LogicReasoner {
                                 it.value = dse.numberOfStates as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "ForwardTime" it.value = (strategy.forwardTime/1000000) as int

+                                it.name = "ForwardTime"

+                                it.value = (strategy.forwardTime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "BacktrackingTime" it.value = (strategy.backtrackingTime/1000000) as int

+                                it.name = "BacktrackingTime"

+                                it.value = (strategy.backtrackingTime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "GlobalConstraintEvaluationTime" it.value = (strategy.globalConstraintEvaluationTime/1000000) as int

+                                it.name = "GlobalConstraintEvaluationTime"

+                                it.value = (strategy.globalConstraintEvaluationTime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "FitnessCalculationTime" it.value = (strategy.fitnessCalculationTime/1000000) as int

+                                it.name = "FitnessCalculationTime"

+                                it.value = (strategy.fitnessCalculationTime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "SolutionCopyTime" it.value = (solutionSaver.totalCopierRuntime/1000000) as int

+                                it.name = "SolutionCopyTime"

+                                it.value = (solutionSaver.totalCopierRuntime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int

+                                it.name = "ActivationSelectionTime"

+                                it.value = (strategy.activationSelector.runtime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

                                 it.name = "Decisions"

@@ -287,27 +258,34 @@ class ViatraReasoner extends LogicReasoner {
                                 it.value = method.statistics.scopePropagatorSolverInvocations

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "NumericalSolverSumTime" it.value = (strategy.numericSolver.runtime/1000000) as int

+                                it.name = "NumericalSolverSumTime"

+                                it.value = (strategy.numericSolver.runtime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "NumericalSolverProblemFormingTime" it.value = (strategy.numericSolver.solverFormingProblem/1000000) as int

+                                it.name = "NumericalSolverProblemFormingTime"

+                                it.value = (strategy.numericSolver.solverFormingProblem / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "NumericalSolverSolvingTime" it.value = (strategy.numericSolver.solverSolvingProblem/1000000) as int

+                                it.name = "NumericalSolverSolvingTime"

+                                it.value = (strategy.numericSolver.solverSolvingProblem / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "NumericalSolverInterpretingSolution" it.value = (strategy.numericSolver.solverSolution/1000000) as int

+                                it.name = "NumericalSolverInterpretingSolution"

+                                it.value = (strategy.numericSolver.solverSolution / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int

+                                it.name = "NumericalSolverCachingTime"

+                                it.value = (strategy.numericSolver.cachingTime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls

+                                it.name = "NumericalSolverCallNumber"

+                                it.value = strategy.numericSolver.numberOfSolverCalls

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls

+                                it.name = "NumericalSolverCachedAnswerNumber"

+                                it.value = strategy.numericSolver.numberOfCachedSolverCalls

                         ]

-                        if(diversityChecker.active) {

+                        if (diversityChecker.active) {

                                 it.entries += createIntStatisticEntry => [

                                         it.name = "SolutionDiversityCheckTime"

                                         it.value = (diversityChecker.totalRuntime / 1000000) as int

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index a2ed6016..fbe6da9d 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -4,7 +4,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration

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

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

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

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

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

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

@@ -12,6 +11,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy

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

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostObjectiveHint

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold

 import java.util.LinkedList

@@ -114,9 +114,11 @@ class CostObjectiveConfiguration {
         public var ObjectiveKind kind

         public var ObjectiveThreshold threshold

         public var boolean findExtremum

+        public var CostObjectiveHint hint

 }

 

 class CostObjectiveElementConfiguration {

         public var String patternQualifiedName

         public var int weight

 }

+

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
index 4800f71d..4b7cead1 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
@@ -28,8 +28,6 @@ import org.eclipse.viatra.dse.objectives.Fitness;
 import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper;

 import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler;

 import org.eclipse.viatra.dse.solutionstore.SolutionStore;

-import org.eclipse.viatra.query.runtime.api.IPatternMatch;

-import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher;

 

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;

@@ -37,12 +35,11 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod;

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;

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

-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder;

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation;

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser;

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod;

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration;

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

 

@@ -301,7 +298,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                 return activationIds;

         }

 

-        private void checkForSolution(final Fitness fittness) {

+        private void checkForSolution(final Fitness fitness) {

                 solutionStore.newSolution(context);

         }

         

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
index 066040a0..70e8e9c2 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -1,13 +1,13 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

 import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator

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

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

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

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

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

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

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

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod

 import java.math.BigDecimal

 import java.util.HashMap

 import java.util.LinkedHashMap

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
index cfd11816..b48d0831 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
@@ -22,12 +22,13 @@ import java.util.List
 import java.util.Map

 import java.util.TreeSet

 import org.eclipse.emf.ecore.EObject

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

 import org.eclipse.xtext.xbase.lib.Functions.Function1

 

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

 

 class PartialModelAsLogicInterpretation implements LogicModelInterpretation{

-        val PartialInterpretation partialInterpretation

+        @Accessors val PartialInterpretation partialInterpretation

         val Map<EObject, EObject> trace;

         val Map<TypeDeclaration,PartialComplexTypeInterpretation> type2Interpretation

         val Map<RelationDeclaration,PartialRelationInterpretation> relation2Interpretation

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
index 38c8f5a1..33b69436 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
@@ -26,16 +26,12 @@ class CopiedSolution {
  * using the supplied {@link NumericSolver}.
  */
 class SolutionCopier {
-        val NumericSolver numericSolver
         val copiedSolutions = new LinkedHashMap<Object, CopiedSolution>
 
+        @Accessors NumericSolver numericSolver
         long startTime = System.nanoTime
         @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0
 
-        new(NumericSolver numericSolver) {
-                this.numericSolver = numericSolver
-        }
-
         def void copySolution(ThreadContext context, Object solutionId) {
                 val existingCopy = copiedSolutions.get(solutionId)
                 if (existingCopy === null) {
@@ -47,7 +43,7 @@ class SolutionCopier {
                         totalCopierRuntime += System.nanoTime - copyStart
                         val copierRuntime = System.nanoTime - startTime
                         val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime)
-                        numericSolver.fillSolutionCopy(copiedSolution.trace)
+                        numericSolver?.fillSolutionCopy(copiedSolution.trace)
                         copiedSolutions.put(solutionId, copiedSolution)
                 } else {
                         existingCopy.current = true
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
index c0b5008c..e00f76ff 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
@@ -1,5 +1,9 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
 
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.DirectionalThresholdObjective
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IObjectiveBoundsProvider
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
 import java.util.HashMap
 import java.util.Map
 import org.eclipse.viatra.dse.api.DSEException
@@ -18,24 +22,32 @@ import org.eclipse.xtend.lib.annotations.Accessors
  * Will also automatically fill any missing numerical values in the saved solutions
  * using the supplied {@link NumericSolver}.
  */
-class ViatraReasonerSolutionSaver implements ISolutionSaver {
+class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsProvider {
+        static val TOLERANCE = 1e-10
+
         @Accessors val SolutionCopier solutionCopier
-        val NumericSolver numericSolver
         @Accessors val DiversityChecker diversityChecker
+        val IObjective[][] leveledExtremalObjectives
         val boolean hasExtremalObjectives
         val int numberOfRequiredSolutions
         val ObjectiveComparatorHelper comparatorHelper
         val Map<SolutionTrajectory, Fitness> trajectories = new HashMap
 
-        @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection
+        @Accessors var NumericSolver numericSolver
+        @Accessors var Map<Object, Solution> solutionsCollection
 
-        new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker, NumericSolver numericSolver) {
+        new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) {
                 this.diversityChecker = diversityChecker
                 comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives)
+                this.leveledExtremalObjectives = leveledExtremalObjectives
                 hasExtremalObjectives = leveledExtremalObjectives.exists[!empty]
                 this.numberOfRequiredSolutions = numberOfRequiredSolutions
-                this.solutionCopier = new SolutionCopier(numericSolver)
+                this.solutionCopier = new SolutionCopier
+        }
+        
+        def setNumericSolver(NumericSolver numericSolver) {
                 this.numericSolver = numericSolver
+                solutionCopier.numericSolver = numericSolver
         }
 
         override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
@@ -51,6 +63,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
                 if (!shouldSaveSolution(fitness, context)) {
                         return false
                 }
+                println("Found: " + fitness)
                 val dominatedTrajectories = newArrayList
                 for (entry : trajectories.entrySet) {
                         val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value)
@@ -99,7 +112,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
         }
 
         private def shouldSaveSolution(Fitness fitness, ThreadContext context) {
-                return fitness.satisifiesHardObjectives && numericSolver.currentSatisfiable
+                fitness.satisifiesHardObjectives && (numericSolver === null || numericSolver.currentSatisfiable)
         }
 
         private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory,
@@ -145,8 +158,93 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
                 }
                 solutionsCollection.size < numberOfRequiredSolutions
         }
-        
+
         def getTotalCopierRuntime() {
                 solutionCopier.totalCopierRuntime
         }
+
+        override computeRequiredBounds(IObjective objective, Bounds bounds) {
+                if (!hasExtremalObjectives) {
+                        return
+                }
+                if (objective instanceof DirectionalThresholdObjective) {
+                        switch (threshold : objective.threshold) {
+                                case ObjectiveThreshold.NO_THRESHOLD: {
+                                        // No threshold to set.
+                                }
+                                ObjectiveThreshold.Exclusive: {
+                                        switch (kind : objective.kind) {
+                                                case HIGHER_IS_BETTER:
+                                                        bounds.tightenLowerBound(Math.floor(threshold.threshold + 1) as int)
+                                                case LOWER_IS_BETTER:
+                                                        bounds.tightenUpperBound(Math.ceil(threshold.threshold - 1) as int)
+                                                default:
+                                                        throw new IllegalArgumentException("Unknown objective kind" + kind)
+                                        }
+                                        if (threshold.clampToThreshold) {
+                                                return
+                                        }
+                                }
+                                ObjectiveThreshold.Inclusive: {
+                                        switch (kind : objective.kind) {
+                                                case HIGHER_IS_BETTER:
+                                                        bounds.tightenLowerBound(Math.ceil(threshold.threshold) as int)
+                                                case LOWER_IS_BETTER:
+                                                        bounds.tightenUpperBound(Math.floor(threshold.threshold) as int)
+                                                default:
+                                                        throw new IllegalArgumentException("Unknown objective kind" + kind)
+                                        }
+                                        if (threshold.clampToThreshold) {
+                                                return
+                                        }
+                                }
+                                default:
+                                        throw new IllegalArgumentException("Unknown threshold: " + threshold)
+                        }
+                        for (level : leveledExtremalObjectives) {
+                                switch (level.size) {
+                                        case 0: {
+                                                // Nothing to do, wait for the next level.
+                                        }
+                                        case 1: {
+                                                val primaryObjective = level.get(0)
+                                                if (primaryObjective != objective) {
+                                                        // There are no worst-case bounds for secondary objectives.
+                                                        return
+                                                }
+                                        }
+                                        default:
+                                                // There are no worst-case bounds for Pareto front calculation.
+                                                return
+                                }
+                        }
+                        val fitnessIterator = trajectories.values.iterator
+                        if (!fitnessIterator.hasNext) {
+                                return
+                        }
+                        val fitness = fitnessIterator.next.get(objective.name)
+                        while (fitnessIterator.hasNext) {
+                                val otherFitness = fitnessIterator.next.get(objective.name)
+                                if (Math.abs(fitness - otherFitness) > TOLERANCE) {
+                                        throw new IllegalStateException("Inconsistent fitness: " + objective.name)
+                                }
+                        }
+                        switch (kind : objective.kind) {
+                                case HIGHER_IS_BETTER:
+                                        if (needsMoreSolutionsWithSameFitness) {
+                                                bounds.tightenLowerBound(Math.floor(fitness) as int)
+                                        } else {
+                                                bounds.tightenLowerBound(Math.floor(fitness + 1) as int)
+                                        }
+                                case LOWER_IS_BETTER:
+                                        if (needsMoreSolutionsWithSameFitness) {
+                                                bounds.tightenUpperBound(Math.ceil(fitness) as int)
+                                        } else {
+                                                bounds.tightenUpperBound(Math.ceil(fitness - 1) as int)
+                                        }
+                                default:
+                                        throw new IllegalArgumentException("Unknown objective kind" + kind)
+                        }
+                }
+        }
 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend
new file mode 100644
index 00000000..885b14e8
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend
@@ -0,0 +1,137 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import com.google.common.collect.ImmutableList
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
+import java.util.List
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+import org.eclipse.xtend.lib.annotations.Data
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+
+@FunctionalInterface
+interface ParameterScopeBound {
+        def double getUpperBound()
+}
+
+@Data
+class CostElementMatch {
+        val IPatternMatch match
+        val boolean must
+
+        def isMulti() {
+                CostElementMatchers.isMultiMatch(match)
+        }
+}
+
+@Data
+class CostElementMatchers {
+        val ViatraQueryMatcher<? extends IPatternMatch> currentMatcher
+        val ViatraQueryMatcher<? extends IPatternMatch> mayMatcher
+        val ViatraQueryMatcher<? extends IPatternMatch> mustMatcher
+        val List<ParameterScopeBound> parameterScopeBounds
+        val int weight
+
+        def getCurrentNumberOfMatches() {
+                currentMatcher.countMatches
+        }
+
+        def getMinimumNumberOfMatches() {
+                mustMatcher.countMatches
+        }
+
+        def getMaximumNumberOfMatches() {
+                var double sum = 0
+                val iterator = mayMatcher.streamAllMatches.iterator
+                while (iterator.hasNext) {
+                        val match = iterator.next
+                        var double product = 1
+                        val numberOfParameters = parameterScopeBounds.size
+                        for (var int i = 0; i < numberOfParameters; i++) {
+                                if (isMulti(match.get(i + 2))) {
+                                        val scopeBound = parameterScopeBounds.get(i)
+                                        product *= scopeBound.upperBound
+                                }
+
+                        }
+                        sum += product
+                }
+                sum
+        }
+
+        def getMatches() {
+                ImmutableList.copyOf(mayMatcher.streamAllMatches.iterator.map [ match |
+                        new CostElementMatch(match, mustMatcher.isMatch(match))
+                ])
+        }
+        
+        def projectMayMatch(IPatternMatch match, int... indices) {
+                mayMatcher.projectMatch(match, indices)
+        }
+        
+        private static def <T extends IPatternMatch> projectMatch(ViatraQueryMatcher<T> matcher, IPatternMatch match, int... indices) {
+                checkMatch(match)
+                val n = matcher.specification.parameters.length - 2
+                if (indices.length != n) {
+                        throw new IllegalArgumentException("Invalid number of projection indices")
+                }
+                val newMatch = matcher.newEmptyMatch
+                newMatch.set(0, match.get(0))
+                newMatch.set(1, match.get(1))
+                for (var int i = 0; i < n; i++) {
+                        newMatch.set(i + 2, match.get(indices.get(i)))
+                }
+                if (!matcher.hasMatch(newMatch)) {
+                        throw new IllegalArgumentException("Projected match does not exist")
+                }
+                return newMatch
+        }
+
+        private static def <T extends IPatternMatch> isMatch(ViatraQueryMatcher<T> matcher, IPatternMatch match) {
+                val n = matcher.specification.parameters.length
+                if (n != match.specification.parameters.length) {
+                        throw new IllegalArgumentException("Invalid number of match arguments")
+                }
+                val newMatch = matcher.newEmptyMatch
+                for (var int i = 0; i < n; i++) {
+                        newMatch.set(i, match.get(i))
+                }
+                return matcher.hasMatch(newMatch)
+        }
+
+        static def isMulti(Object o) {
+                if (o instanceof EObject) {
+                        switch (feature : o.eContainmentFeature) {
+                                case LogicproblemPackage.eINSTANCE.logicProblem_Elements,
+                                case PartialinterpretationPackage.eINSTANCE.partialInterpretation_NewElements:
+                                        false
+                                case PartialinterpretationPackage.eINSTANCE.partialInterpretation_OpenWorldElements:
+                                        true
+                                default:
+                                        throw new IllegalStateException("Unknown containment feature for element: " + feature)
+                        }
+                } else {
+                        false
+                }
+        }
+
+        static def isMultiMatch(IPatternMatch match) {
+                checkMatch(match)
+                val n = match.specification.parameters.length
+                for (var int i = 2; i < n; i++) {
+                        if (isMulti(match.get(i))) {
+                                return true
+                        }
+                }
+                false
+        }
+        
+        private static def checkMatch(IPatternMatch match) {
+                val n = match.specification.parameters.length
+                if (n < 2 || !(match.get(0) instanceof LogicProblem) || !(match.get(1) instanceof PartialInterpretation)) {
+                        throw new IllegalArgumentException("Match is not from the partial interpretation")
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend
new file mode 100644
index 00000000..2434073d
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend
@@ -0,0 +1,68 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedLinearExpressionBuilder
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
+import java.util.Map
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
+import org.eclipse.xtend.lib.annotations.Accessors
+
+abstract class CostObjectiveHint implements LinearTypeConstraintHint, BoundSaturationListener {
+        @Accessors ThreeValuedCostObjective objective
+        @Accessors IObjectiveBoundsProvider boundsProvider
+        
+        Integer bestUpper = null
+
+        override getAdditionalPatterns(PatternGenerator patternGenerator, Map<String, PQuery> fqnToPQuery) {
+                ''''''
+        }
+
+        override createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) {
+                null
+        }
+        
+        def isExact() {
+                false
+        }
+
+        def PolyhedronExtensionOperator createPolyhedronExtensionOperator(
+                Map<String, CostElementMatchers> costElementMatchers) {
+                null
+        }
+        
+        def setObjective(ThreeValuedCostObjective objective) {
+                if (this.objective !== null) {
+                        throw new IllegalStateException("Objective was already set")
+                }
+                this.objective = objective
+        }
+        
+        def setBoundsProvider(IObjectiveBoundsProvider boundsProvider) {
+                if (this.boundsProvider !== null) {
+                        throw new IllegalStateException("Objective bounds provider was already set")
+                }
+                this.boundsProvider = boundsProvider
+        }
+        
+        protected def buildWithBounds(ExtendedLinearExpressionBuilder builder) {
+                val bounds = builder.build(this)
+                if (objective !== null && boundsProvider !== null) {
+                        boundsProvider.computeRequiredBounds(objective, bounds)
+                }
+                if (exact && bestUpper !== null) {
+                        bounds.tightenLowerBound(bestUpper)
+                }
+                bounds
+        }
+        
+        override boundsSaturated(Integer lower, Integer upper) {
+                if (upper !== null && (bestUpper === null || bestUpper < upper)) {
+                        bestUpper = upper
+                }
+                objective?.boundsSaturated(lower, upper)
+        }
+        
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend
new file mode 100644
index 00000000..3c4d36a5
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend
@@ -0,0 +1,8 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds
+import org.eclipse.viatra.dse.objectives.IObjective
+
+interface IObjectiveBoundsProvider {
+        def void computeRequiredBounds(IObjective objective, Bounds bounds)
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend
index 0a6fd55b..9b1a7e9f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend
@@ -1,85 +1,80 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
 
-import com.google.common.collect.ImmutableList
-import java.util.Collection
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener
+import java.util.Map
 import org.eclipse.viatra.dse.base.ThreadContext
-import org.eclipse.viatra.query.runtime.api.IPatternMatch
-import org.eclipse.viatra.query.runtime.api.IQuerySpecification
-import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
-import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.xtend.lib.annotations.Accessors
 
-@Data
-class ThreeValuedCostElement {
-        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentMatchQuery
-        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayMatchQuery
-        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustMatchQuery
-        val int weight
-}
-
-class ThreeValuedCostObjective extends AbstractThreeValuedObjective {
-        val Collection<ThreeValuedCostElement> costElements
-        Collection<CostElementMatchers> matchers
+class ThreeValuedCostObjective extends AbstractThreeValuedObjective implements BoundSaturationListener {
+        @Accessors val Map<String, CostElementMatchers> matchers
+        double lowerBoundHint = Double.NEGATIVE_INFINITY
+        double upperBoundHint = Double.POSITIVE_INFINITY
 
-        new(String name, Collection<ThreeValuedCostElement> costElements, ObjectiveKind kind, ObjectiveThreshold threshold,
+        new(String name, Map<String, CostElementMatchers> matchers, ObjectiveKind kind, ObjectiveThreshold threshold,
                 int level) {
                 super(name, kind, threshold, level)
-                this.costElements = costElements
+                this.matchers = matchers
         }
 
         override createNew() {
-                new ThreeValuedCostObjective(name, costElements, kind, threshold, level)
+                // new ThreeValuedCostObjective(name, matchers, kind, threshold, level)
+                throw new UnsupportedOperationException("ThreeValuedCostObjective can only be used from a single thread")
         }
 
         override init(ThreadContext context) {
-                val queryEngine = context.queryEngine
-                matchers = ImmutableList.copyOf(costElements.map [ element |
-                        new CostElementMatchers(
-                                queryEngine.getMatcher(element.currentMatchQuery),
-                                queryEngine.getMatcher(element.mayMatchQuery),
-                                queryEngine.getMatcher(element.mustMatchQuery),
-                                element.weight
-                        )
-                ])
         }
 
         override getRawFitness(ThreadContext context) {
-                var int cost = 0
-                for (matcher : matchers) {
-                        cost += matcher.weight * matcher.currentMatcher.countMatches
+                var double cost = 0
+                for (matcher : matchers.values) {
+                        cost += matcher.weight * matcher.currentNumberOfMatches
                 }
-                cost as double
+                cost
         }
 
         override getLowestPossibleFitness(ThreadContext threadContext) {
-                var int cost = 0
-                for (matcher : matchers) {
+                var double cost = 0
+                for (matcher : matchers.values) {
                         if (matcher.weight >= 0) {
-                                cost += matcher.weight * matcher.mustMatcher.countMatches
-                        } else if (matcher.mayMatcher.countMatches > 0) {
-                                // TODO Count may matches.
-                                return Double.NEGATIVE_INFINITY
+                                cost += matcher.weight * matcher.minimumNumberOfMatches
+                        } else {
+                                cost += matcher.weight * matcher.maximumNumberOfMatches
                         }
                 }
-                cost as double
+                val boundWithHint = Math.max(lowerBoundHint, cost)
+                if (boundWithHint > upperBoundHint) {
+                        throw new IllegalStateException("Inconsistent cost bounds")
+                }
+                boundWithHint
         }
 
         override getHighestPossibleFitness(ThreadContext threadContext) {
-                var int cost = 0
-                for (matcher : matchers) {
+                var double cost = 0
+                for (matcher : matchers.values) {
                         if (matcher.weight <= 0) {
-                                cost += matcher.weight * matcher.mustMatcher.countMatches
-                        } else if (matcher.mayMatcher.countMatches > 0) {
-                                return Double.POSITIVE_INFINITY
+                                cost += matcher.weight * matcher.minimumNumberOfMatches
+                        } else {
+                                cost += matcher.weight * matcher.maximumNumberOfMatches
                         }
                 }
-                cost as double
+                val boundWithHint = Math.min(upperBoundHint, cost)
+                if (boundWithHint < lowerBoundHint) {
+                        throw new IllegalStateException("Inconsistent cost bounds")
+                }
+                boundWithHint
         }
 
-        @Data
-        private static class CostElementMatchers {
-                val ViatraQueryMatcher<? extends IPatternMatch> currentMatcher
-                val ViatraQueryMatcher<? extends IPatternMatch> mayMatcher
-                val ViatraQueryMatcher<? extends IPatternMatch> mustMatcher
-                val int weight
+        override boundsSaturated(Integer lower, Integer upper) {
+                lowerBoundHint = if (lower === null) {
+                        Double.NEGATIVE_INFINITY
+                } else {
+                        lower
+                }
+                upperBoundHint = if (upper === null) {
+                        Double.POSITIVE_INFINITY
+                } else {
+                        upper
+                }
+                println('''Bounds saturated: «lower»..«upper»''')
         }
 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend
new file mode 100644
index 00000000..c2750acd
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend
@@ -0,0 +1,205 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import com.google.common.collect.ImmutableList
+import com.google.common.collect.ImmutableMap
+import com.google.common.collect.Lists
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
+import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration
+import java.util.Collection
+import java.util.Map
+import org.eclipse.viatra.dse.objectives.IObjective
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.xtend.lib.annotations.Data
+
+@Data
+class ThreeValuedCostObjectiveProviderResult {
+        val Collection<IObjective> objectives
+        val Collection<CostObjectiveHint> hints
+        val Collection<PolyhedronExtensionOperator> extensionOperators
+        val IObjective[][] leveledExtremalObjectives
+        val boolean optimizationProblem
+}
+
+class ThreeValuedCostObjectiveProvider {
+        static val COST_OBJECTIVE_LEVEL = 3
+
+        val ViatraQueryEngine queryEngine
+        val Map<String, ModalPatternQueries> modalRelationQueries
+        val Map<String, Relation> qualifiedNameToRelationMap
+        val ParameterScopeBound defaultBounds
+        val ParameterScopeBound booleanBounds
+        val ParameterScopeBound integerBounds
+        val ParameterScopeBound realBounds
+        val ParameterScopeBound stringBounds
+        val Map<TypeDeclaration, ParameterScopeBound> typeDeclarationToBoundsMap
+
+        new(ViatraQueryEngine queryEngine, PartialInterpretation interpretation,
+                Map<String, ModalPatternQueries> modalRelationQueries) {
+                this.queryEngine = queryEngine
+                this.modalRelationQueries = modalRelationQueries
+                qualifiedNameToRelationMap = ImmutableMap.copyOf(
+                        interpretation.problem.annotations.filter(TransfomedViatraQuery).
+                                toMap([patternFullyQualifiedName], [target]))
+                defaultBounds = new PartialInterpretationBasedParameterScopeBound(interpretation)
+                var ParameterScopeBound booleanBounds = null
+                var ParameterScopeBound integerBounds = null
+                var ParameterScopeBound realBounds = null
+                var ParameterScopeBound stringBounds = null
+                val typeDeclarationToBoundsMapBuilder = ImmutableMap.builder
+                for (scope : interpretation.scopes) {
+                        val bounds = new ScopeBasedParameterScopeBound(scope)
+                        switch (typeInterpretation : scope.targetTypeInterpretation) {
+                                PartialBooleanInterpretation:
+                                        if (booleanBounds === null) {
+                                                booleanBounds = bounds
+                                        } else {
+                                                throw new IllegalStateException("Duplicate partial boolean interpretation")
+                                        }
+                                PartialIntegerInterpretation:
+                                        if (integerBounds === null) {
+                                                integerBounds = bounds
+                                        } else {
+                                                throw new IllegalStateException("Duplicate partial integer interpretation")
+                                        }
+                                PartialRealInterpretation:
+                                        if (realBounds === null) {
+                                                realBounds = bounds
+                                        } else {
+                                                throw new IllegalStateException("Duplicate partial real interpretation")
+                                        }
+                                PartialStringInterpretation:
+                                        if (stringBounds === null) {
+                                                stringBounds = bounds
+                                        } else {
+                                                throw new IllegalStateException("Duplicate partial string interpretation")
+                                        }
+                                PartialComplexTypeInterpretation:
+                                        typeDeclarationToBoundsMapBuilder.put(typeInterpretation.interpretationOf, bounds)
+                        }
+                }
+                this.booleanBounds = booleanBounds ?: defaultBounds
+                this.integerBounds = integerBounds ?: defaultBounds
+                this.realBounds = realBounds ?: defaultBounds
+                this.stringBounds = stringBounds ?: defaultBounds
+                typeDeclarationToBoundsMap = typeDeclarationToBoundsMapBuilder.build
+        }
+
+        def getCostObjectives(Collection<CostObjectiveConfiguration> costObjectives) {
+                val objectives = ImmutableList.<IObjective>builder
+                val hints = ImmutableList.<CostObjectiveHint>builder
+                val extensionOperators = ImmutableList.<PolyhedronExtensionOperator>builder
+                val extremalObjectives = Lists.newArrayListWithExpectedSize(costObjectives.size)
+                for (entry : costObjectives.indexed) {
+                        val objectiveName = '''costObjective«entry.key»'''
+                        val objectiveConfig = entry.value
+                        val costObjective = transformCostObjective(objectiveConfig, objectiveName)
+                        objectives.add(costObjective)
+                        if (objectiveConfig.findExtremum) {
+                                extremalObjectives += costObjective
+                        }
+                        val hint = objectiveConfig.hint
+                        if (hint !== null) {
+                                hints.add(hint)
+                                hint.objective = costObjective
+                                val extensionOperator = hint.createPolyhedronExtensionOperator(costObjective.matchers)
+                                if (extensionOperator !== null) {
+                                        extensionOperators.add(extensionOperator)
+                                }
+                        }
+                }
+                new ThreeValuedCostObjectiveProviderResult(
+                        objectives.build,
+                        hints.build,
+                        extensionOperators.build,
+                        newArrayList(extremalObjectives),
+                        !extremalObjectives.empty
+                )
+        }
+
+        private def transformCostObjective(CostObjectiveConfiguration configuration, String name) {
+                val costElements = ImmutableMap.copyOf(configuration.elements.toMap([patternQualifiedName], [
+                        transformCostElement
+                ]))
+                new ThreeValuedCostObjective(name, costElements, configuration.kind, configuration.threshold,
+                        COST_OBJECTIVE_LEVEL)
+        }
+
+        private def transformCostElement(CostObjectiveElementConfiguration elementConfig) {
+                val relationName = elementConfig.patternQualifiedName
+                val modalQueries = modalRelationQueries.get(relationName)
+                if (modalQueries === null) {
+                        throw new IllegalArgumentException("Unknown relation queries: " + relationName)
+                }
+                val relation = qualifiedNameToRelationMap.get(relationName)
+                if (relation === null) {
+                        throw new IllegalArgumentException("Unknown transformed relation: " + relationName)
+                }
+                val parameterBounds = ImmutableList.copyOf(relation.parameters.map[parameterBound])
+                new CostElementMatchers(
+                        queryEngine.getMatcher(modalQueries.currentQuery),
+                        queryEngine.getMatcher(modalQueries.mayQuery),
+                        queryEngine.getMatcher(modalQueries.mustQuery),
+                        parameterBounds,
+                        elementConfig.weight
+                )
+        }
+
+        private def getParameterBound(TypeReference typeReference) {
+                switch (typeReference) {
+                        BoolTypeReference: booleanBounds
+                        IntTypeReference: integerBounds
+                        RealTypeReference: realBounds
+                        StringTypeReference: stringBounds
+                        ComplexTypeReference: typeDeclarationToBoundsMap.getOrDefault(typeReference.referred, defaultBounds)
+                }
+        }
+
+        private static abstract class AbstractParameterScopeBound implements ParameterScopeBound {
+                override getUpperBound() {
+                        val rawValue = rawUpperBound
+                        if (rawValue < 0) {
+                                Double.POSITIVE_INFINITY
+                        } else {
+                                rawValue
+                        }
+                }
+
+                protected def int getRawUpperBound()
+        }
+
+        @Data
+        private static class ScopeBasedParameterScopeBound extends AbstractParameterScopeBound {
+                val Scope scope
+
+                override protected getRawUpperBound() {
+                        scope.maxNewElements
+                }
+        }
+
+        @Data
+        private static class PartialInterpretationBasedParameterScopeBound extends AbstractParameterScopeBound {
+                val PartialInterpretation interpretation
+
+                override protected getRawUpperBound() {
+                        interpretation.maxNewElements
+                }
+        }
+}