32 files changed, 1760 insertions, 668 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..f5eb5514 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",
@@ -24,9 +25,8 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
  org.eclipse.xtext;bundle-version="2.10.0",
  org.eclipse.viatra.transformation.runtime.emf;bundle-version="2.0.0",
  org.eclipse.xtext.xbase;bundle-version="2.10.0",
- com.microsoft.z3;bundle-version="4.8.5",
  hu.bme.mit.inf.dslreasoner.ilp.cbc;bundle-version="1.0.0",
- org.eclipse.viatra.query.runtime.rete;bundle-version="2.0.0"
-Bundle-RequiredExecutionEnvironment: JavaSE-1.8
+ org.eclipse.viatra.query.runtime.rete;bundle-version="2.0.0",
+ com.microsoft.z3
+Bundle-RequiredExecutionEnvironment: JavaSE-11
 Import-Package: org.apache.log4j
-Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery
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/LinearTypeConstraintHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend
index 8c21ca1d..31f98e36 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend
@@ -3,8 +3,10 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import java.util.Map
 import org.eclipse.viatra.query.runtime.api.IPatternMatch
 import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
 
 interface LinearTypeExpressionBuilderFactory {
         def ViatraQueryMatcher<? extends IPatternMatch> createMatcher(String queryName)
@@ -24,7 +26,7 @@ interface RelationConstraintUpdater {
 }
 
 interface LinearTypeConstraintHint {
-        def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator)
+        def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator, Map<String, PQuery> fqnToPQuery)
         
         def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory)
 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/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.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
index 93b83577..cacba3c6 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
@@ -19,6 +19,8 @@ class ScopePropagator {
         val Map<PartialTypeInterpratation, Scope> type2Scope

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

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

+        

+        @Accessors(PUBLIC_GETTER) var scopePropagationNeeded = false

 

         new(PartialInterpretation p, ModelGenerationStatistics statistics) {

                 partialInterpretation = p

@@ -64,7 +66,8 @@ class ScopePropagator {
                 copyScopeBoundsToHeuristic()

         }

 

-        def propagateAllScopeConstraints() {

+        def void propagateAllScopeConstraints() {

+                scopePropagationNeeded = false

                 if (!valid) {

                         return

                 }

@@ -93,6 +96,7 @@ class ScopePropagator {
                 if (isPrimitive) {

                         return

                 }

+                scopePropagationNeeded = true

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

                 val targetScope = type2Scope.get(t)

                 if (targetScope !== null) {

@@ -117,6 +121,12 @@ class ScopePropagator {
 //              this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]

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

         }

+        

+        def addedToRelation(Relation r) {

+                if (isPropagationNeededAfterAdditionToRelation(r)) {

+                        scopePropagationNeeded = true

+                }

+        }

 

         protected def setScopesInvalid() {

                 partialInterpretation.minNewElements = Integer.MAX_VALUE

@@ -127,7 +137,7 @@ class ScopePropagator {
                 }

         }

 

-        def isPropagationNeededAfterAdditionToRelation(Relation r) {

+        protected def isPropagationNeededAfterAdditionToRelation(Relation r) {

                 false

         }

         

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
index 80bc3844..edf92343 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
@@ -25,12 +25,13 @@ import java.util.HashMap
 import java.util.Map

 import org.eclipse.emf.ecore.EAttribute

 import org.eclipse.emf.ecore.EReference

+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint

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

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

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

+import org.eclipse.xtend2.lib.StringConcatenationClient

 

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

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

-import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint

 

 @Data class PatternGeneratorResult {

         CharSequence patternText

@@ -38,6 +39,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
         HashMap<PConstraint,String> constraint2CurrentPreconditionName

 }

 

+interface UnitPropagationPatternGenerator {

+        def Map<Relation, String> getMustPatterns()

+        

+        def Map<Relation, String> getMustNotPatterns()

+        

+        def StringConcatenationClient getAdditionalPatterns(PatternGenerator generator, Map<String, PQuery> fqn2PQuery)

+}

+

 class PatternGenerator {

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

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

@@ -157,7 +166,8 @@ class PatternGenerator {
                 Map<String, PQuery> fqn2PQuery,

                 TypeAnalysisResult typeAnalysisResult,

                 RelationConstraints constraints,

-                Collection<LinearTypeConstraintHint> hints

+                Collection<LinearTypeConstraintHint> hints,

+                Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators

         ) {

                 val first = 

                  '''

@@ -313,7 +323,7 @@ class PatternGenerator {
                         //////////

                         // 1.2 Relation Declaration Indexers

                         //////////

-                        «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),fqn2PQuery)»

+                        «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),unitPropagationPatternGenerators,fqn2PQuery)»

                         

                         //////////

                         // 1.3 Relation Definition Indexers

@@ -359,13 +369,16 @@ class PatternGenerator {
                         //////////

                         // 4.3 Relation refinement

                         //////////

-                        «relationRefinementGenerator.generateRefineReference(problem)»

+                        «relationRefinementGenerator.generateRefineReference(problem, unitPropagationPatternGenerators)»

                         

                         //////////

                         // 5 Hints

                         //////////

                         «FOR hint : hints»

-                                «hint.getAdditionalPatterns(this)»

+                                «hint.getAdditionalPatterns(this, fqn2PQuery)»

+                        «ENDFOR»

+                        «FOR generator : unitPropagationPatternGenerators»

+                                «generator.getAdditionalPatterns(this, fqn2PQuery)»

                         «ENDFOR»

                         

                         //////////

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
index d57705ce..2e786286 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
@@ -36,9 +36,10 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
         public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries

         public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries

         public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery

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

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

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

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

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

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

         public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns

         public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns

         public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries

@@ -56,7 +57,7 @@ class ModalPatternQueries {
 class UnifinishedMultiplicityQueries {

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

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

-        

+

         def Set<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> getAllQueries() {

                 val builder = ImmutableSet.builder

                 if (existingMultiplicityQuery !== null) {

@@ -70,13 +71,13 @@ class UnifinishedMultiplicityQueries {
 }

 

 class PatternProvider {

-

         val TypeAnalysis typeAnalysis = new TypeAnalysis

 

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

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

-                ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, 

-                Collection<LinearTypeConstraintHint> hints, boolean writeToFile) {

+                ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints,

+                Collection<LinearTypeConstraintHint> hints,

+                Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, boolean writeToFile) {

                 val fqn2Query = existingQueries.toMap[it.fullyQualifiedName]

                 val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy)

                 val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) {

@@ -89,15 +90,16 @@ class PatternProvider {
                                 null

                         }

                 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query,

-                        typeAnalysisResult, relationConstraints, hints)

+                        typeAnalysisResult, relationConstraints, hints, unitPropagationPatternGenerators)

                 if (writeToFile) {

                         workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText)

                 }

                 val ParseUtil parseUtil = new ParseUtil

                 val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText)

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

-                        patternGeneratorResult.constraint2MustPreconditionName, patternGeneratorResult.constraint2CurrentPreconditionName,

-                        relationConstraints, generatedQueries)

+                        patternGeneratorResult.constraint2MustPreconditionName,

+                        patternGeneratorResult.constraint2CurrentPreconditionName, relationConstraints,

+                        unitPropagationPatternGenerators, generatedQueries)

                 return runtimeQueries

         }

 

@@ -109,14 +111,16 @@ class PatternProvider {
                 HashMap<PConstraint, String> mustUnitPropagationTrace,

                 HashMap<PConstraint, String> currentUnitPropagationTrace,

                 RelationConstraints relationConstraints,

+                Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators,

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

         ) {

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

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

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

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

-                        

-                val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints)

+                val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries = patternGenerator.

+                        invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]

+                val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries = patternGenerator.

+                        unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)]

+

+                val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(

+                        relationConstraints.multiplicityConstraints)

                 val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [

                         new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries),

                                 existingInverseMultiplicityQueryName?.lookup(queries))

@@ -124,16 +128,22 @@ class PatternProvider {
                 val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup(

                         queries)

 

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

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

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

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

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

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

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

-                        mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)]

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

-                        currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)]

+                val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectsQueries = patternGenerator.

+                        typeRefinementGenerator.getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [

+                                it.lookup(queries)

+                        ]

+                val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries = patternGenerator.

+                        typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [

+                                it.lookup(queries)

+                        ]

+                val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineRelationQueries = patternGenerator.

+                        relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]

+                val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustRelationPropagationQueries = patternGenerator.

+                        relationRefinementGenerator.getMustPropagationQueries(problem, unitPropagationPatternGenerators).mapValues[it.lookup(queries)]

+                val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.

+                        mapValues[it.lookup(queries)]

+                val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.

+                        mapValues[it.lookup(queries)]

 

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

                         val indexer = patternGenerator.relationDefinitionIndexer

@@ -143,7 +153,7 @@ class PatternProvider {
                                 indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries)

                         )

                 ])

-                

+

                 return new GeneratedPatterns(

                         invalidWFQueries,

                         unfinishedWFQueries,

@@ -152,6 +162,7 @@ class PatternProvider {
                         refineObjectsQueries,

                         refineTypeQueries,

                         refineRelationQueries,

+                        mustRelationPropagationQueries,

                         mustUnitPropagationPreconditionPatterns,

                         currentUnitPropagationPreconditionPatterns,

                         modalRelationQueries,

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
index b4403979..23ba3cad 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
@@ -1,10 +1,13 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns

 

+import com.google.common.collect.ImmutableMap

+import com.google.common.collect.ImmutableSet

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

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

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

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

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

+import java.util.Collection

 import java.util.HashMap

 import java.util.List

 import java.util.Map

@@ -14,41 +17,40 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 

 class RelationDeclarationIndexer {

         val PatternGenerator base;

-        

+

         new(PatternGenerator base) {

                 this.base = base

         }

-        

-        def generateRelationIndexers(LogicProblem problem, Iterable<RelationDeclaration> relations, Map<String,PQuery> fqn2PQuery) {

+

+        def generateRelationIndexers(LogicProblem problem, Iterable<RelationDeclaration> relations,

+                Iterable<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, Map<String, PQuery> fqn2PQuery) {

                 val upperMultiplicities = new HashMap

-                problem.annotations.filter(UpperMultiplicityAssertion).forEach[

-                        upperMultiplicities.put(it.relation,it.upper)

+                problem.annotations.filter(UpperMultiplicityAssertion).forEach [

+                        upperMultiplicities.put(it.relation, it.upper)

                 ]

-                

+                val mustNotRelations = ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustNotPatterns.entrySet].

+                        groupBy[key].mapValues[ImmutableSet.copyOf(map[value])])

+

                 return '''

-                «FOR relation : relations»

-                        «IF base.isDerived(relation)»

-                                «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))»

-                                «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))»

-                        «ELSE»

-                                «generateMustRelation(problem,relation)»

-                                «generateMayRelation(problem,relation,upperMultiplicities,base.getContainments(problem),base.getInverseRelations(problem),fqn2PQuery)»

-                        «ENDIF»

-                «ENDFOR»

+                        «FOR relation : relations»

+                                «IF base.isDerived(relation)»

+                                        «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))»

+                                        «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))»

+                                «ELSE»

+                                        «generateMustRelation(problem, relation)»

+                                        «generateMayRelation(problem, relation, upperMultiplicities, base.getContainments(problem), base.getInverseRelations(problem), mustNotRelations.get(relation) ?: emptySet, fqn2PQuery)»

+                                «ENDIF»

+                        «ENDFOR»

                 '''

         }

-        

+

         def private patternName(RelationDeclaration r, Modality modality) {

                 '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»'''

         }

-        

-        def referRelation(

-                RelationDeclaration referred,

-                String sourceVariable,

-                String targetVariable,

-                Modality modality)

-        '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);'''

-        

+

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

+                Modality modality) '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);'''

+

         def generateMustRelation(LogicProblem problem, RelationDeclaration relation) '''

                 /**

                  * Matcher for detecting tuples t where []«relation.name»(source,target)

@@ -65,59 +67,64 @@ class RelationDeclarationIndexer {
                         BinaryElementRelationLink.param2(link,target);

                 }

         '''

+

         def generateMayRelation(LogicProblem problem, RelationDeclaration relation,

-                Map<Relation, Integer> upperMultiplicities,

-                List<Relation> containments,

-                HashMap<Relation, Relation> inverseRelations,

-                Map<String,PQuery> fqn2PQuery)

-        {

+                Map<Relation, Integer> upperMultiplicities, List<Relation> containments,

+                HashMap<Relation, Relation> inverseRelations, Collection<String> mustNotRelations,

+                Map<String, PQuery> fqn2PQuery) {

                 return '''

-                /**

-                 * Matcher for detecting tuples t where <>«relation.name»(source,target)

-                 */

-                private pattern «relation.patternName(Modality.MAY)»(

-                        problem:LogicProblem, interpretation:PartialInterpretation,

-                        source: DefinedElement, target:DefinedElement)

-                {

-                        find interpretation(problem,interpretation);

-                        // The two endpoint of the link have to exist

-                        find mayExist(problem, interpretation, source);

-                        find mayExist(problem, interpretation, target);

-                        // Type consistency

-                        «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")»

-                        «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")»

-                        «IF upperMultiplicities.containsKey(relation)»

-                                // There are "numberOfExistingReferences" currently existing instances of the reference from the source,

-                                // the upper bound of the multiplicity should be considered.

-                                numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)»

-                                numberOfExistingReferences != «upperMultiplicities.get(relation)»;

-                        «ENDIF»

-                        «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))»

-                                // There are "numberOfExistingReferences" currently existing instances of the reference to the target,

-                                // the upper bound of the opposite reference multiplicity should be considered.

-                                numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)»

-                                numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»;

-                        «ENDIF»

-                        «IF containments.contains(relation)»

-                                // The reference is containment, then a new reference cannot be create if:

-                                // 1. Multiple parents

-                                neg «base.containmentIndexer.referMustContaint("_","target")»

-                                // 2. Circle in the containment hierarchy

-                                neg «base.containmentIndexer.referTransitiveMustContains("target","source")»

-                        «ENDIF»

-                        «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))»

-                                // The eOpposite of the reference is containment, then a referene cannot be created if

-                                // 1. Multiple parents

-                                neg «base.containmentIndexer.referMustContaint("source","_")»

-                                // 2. Circle in the containment hierarchy

-                                neg «base.containmentIndexer.referTransitiveMustContains("source","target")»

-                        «ENDIF»

-                } or {

-                        «relation.referRelation("source","target",Modality.MUST)»

-                }

-        '''

+                        /**

+                         * Matcher for detecting tuples t where <>«relation.name»(source,target)

+                         */

+                        private pattern «relation.patternName(Modality.MAY)»(

+                                problem:LogicProblem, interpretation:PartialInterpretation,

+                                source: DefinedElement, target:DefinedElement)

+                        {

+                                find interpretation(problem,interpretation);

+                                // The two endpoint of the link have to exist

+                                find mayExist(problem, interpretation, source);

+                                find mayExist(problem, interpretation, target);

+                                // Type consistency

+                                «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")»

+                                «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")»

+                                «IF upperMultiplicities.containsKey(relation)»

+                                        // There are "numberOfExistingReferences" currently existing instances of the reference from the source,

+                                        // the upper bound of the multiplicity should be considered.

+                                        numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)»

+                                        numberOfExistingReferences != «upperMultiplicities.get(relation)»;

+                                «ENDIF»

+                                «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))»

+                                        // There are "numberOfExistingReferences" currently existing instances of the reference to the target,

+                                        // the upper bound of the opposite reference multiplicity should be considered.

+                                        numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)»

+                                        numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»;

+                                «ENDIF»

+                                «IF containments.contains(relation)»

+                                        // The reference is containment, then a new reference cannot be create if:

+                                        // 1. Multiple parents

+                                        neg «base.containmentIndexer.referMustContaint("_","target")»

+                                        // 2. Circle in the containment hierarchy

+                                        neg «base.containmentIndexer.referTransitiveMustContains("target","source")»

+                                «ENDIF»

+                                «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))»

+                                        // The eOpposite of the reference is containment, then a referene cannot be created if

+                                        // 1. Multiple parents

+                                        neg «base.containmentIndexer.referMustContaint("source","_")»

+                                        // 2. Circle in the containment hierarchy

+                                        neg «base.containmentIndexer.referTransitiveMustContains("source","target")»

+                                «ENDIF»

+                                «IF !mustNotRelations.empty»

+                                        // ![] unit propagation relations

+                                        «FOR mustNotRelation : mustNotRelations»

+                                                neg find «mustNotRelation»(problem, interpretation, source, target);

+                                        «ENDFOR»

+                                «ENDIF»

+                        } or {

+                                «relation.referRelation("source","target",Modality.MUST)»

+                        }

+                '''

         }

-        

+

         def generateDerivedMustRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) '''

                 /**

                  * Matcher for detecting tuples t where []«relation.name»(source,target)

@@ -129,6 +136,7 @@ class RelationDeclarationIndexer {
                         «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MUST,true,false)»

                  }

         '''

+

         def generateDerivedMayRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) '''

                 /**

                  * Matcher for detecting tuples t where []«relation.name»(source,target)

@@ -140,4 +148,4 @@ class RelationDeclarationIndexer {
                         «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)»

                  }

         '''

-}
\ No newline at end of file
+}

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
index 783cd36b..6f5f2402 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
@@ -1,10 +1,17 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns

 

+import com.google.common.collect.ImmutableList

+import com.google.common.collect.ImmutableMap

+import com.google.common.collect.ImmutableSet

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

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

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

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

+import java.util.Collection

 import java.util.LinkedList

+import java.util.Map

+import java.util.Set

+import org.eclipse.xtend2.lib.StringConcatenationClient

 

 class RelationRefinementGenerator {

         PatternGenerator base;

@@ -13,53 +20,61 @@ class RelationRefinementGenerator {
                 this.base = base

         }

 

-        def CharSequence generateRefineReference(LogicProblem p) '''

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

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

-                                problem:LogicProblem, interpretation:PartialInterpretation,

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

-                                from: DefinedElement, to: DefinedElement)

-                        {

-                                find interpretation(problem,interpretation);

-                                PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);

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

-                                «IF relationRefinement.value !== null»

-                                        PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);

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

+        def CharSequence generateRefineReference(LogicProblem p,

+                Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {

+                val mustRelations = getMustRelations(unitPropagationPatternGenerators)

+

+                '''

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

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

+                                        problem:LogicProblem, interpretation:PartialInterpretation,

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

+                                        from: DefinedElement, to: DefinedElement)

+                                {

+                                        find interpretation(problem,interpretation);

+                                        PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);

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

+                                        «IF relationRefinement.value !== null»

+                                                PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);

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

+                                        «ENDIF»

+                                        find mustExist(problem, interpretation, from);

+                                        find mustExist(problem, interpretation, to);

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

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

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

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

+                                }

+                                

+                                «IF isMustPropagationQueryNeeded(relationRefinement.key, relationRefinement.value, mustRelations)»

+                                        pattern «mustPropagationQueryName(relationRefinement.key)»(

+                                                problem:LogicProblem, interpretation:PartialInterpretation,

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

+                                                from: DefinedElement, to: DefinedElement)

+                                        «FOR body : getMustPropagationBodies(relationRefinement.key, relationRefinement.value, mustRelations) SEPARATOR " or "»

+                                                {

+                                                        «referRefinementQuery(relationRefinement.key, relationRefinement.value, "relationIterpretation", "oppositeInterpretation", "from", "to")»

+                                                        «body»

+                                                }

+                                        «ENDFOR»

                                 «ENDIF»

-                                find mustExist(problem, interpretation, from);

-                                find mustExist(problem, interpretation, to);

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

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

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

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

-                        }

-                «ENDFOR»

-        '''

+                        «ENDFOR»

+                '''

+        }

 

         def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) {

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

         }

 

+        def String mustPropagationQueryName(RelationDeclaration relation) {

+                '''mustPropagation_«base.canonizeName(relation.name)»'''

+        }

+

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

                 String inverseInterpretationName, String sourceName,

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

 

         def getRefineRelationQueries(LogicProblem p) {

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

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

-                /*

-                 * val res = new LinkedHashMap

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

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

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

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

-                 *      } else {

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

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

-                 *      }

-                 * }

-                 return res*/

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

         }

 

@@ -83,4 +98,54 @@ class RelationRefinementGenerator {
                 }

                 return list

         }

+

+        def getMustPropagationQueries(LogicProblem p,

+                Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {

+                val refinements = getRelationRefinements(p)

+                val mustRelations = getMustRelations(unitPropagationPatternGenerators)

+                refinements.filter[isMustPropagationQueryNeeded(key, value, mustRelations)].toInvertedMap [

+                        mustPropagationQueryName(key)

+                ]

+        }

+

+        private def getMustRelations(Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {

+                ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustPatterns.entrySet].groupBy[key].mapValues [

+                        ImmutableSet.copyOf(map[value])

+                ])

+        }

+

+        private def isMustPropagationQueryNeeded(Relation relation, Relation inverseRelation,

+                Map<Relation, ? extends Set<String>> mustRelations) {

+                val mustSet = mustRelations.get(relation)

+                if (mustSet !== null && !mustSet.empty) {

+                        return true

+                }

+                if (inverseRelation !== null) {

+                        val inverseMustSet = mustRelations.get(inverseRelation)

+                        if (inverseMustSet !== null && !inverseMustSet.empty) {

+                                return true

+                        }

+                }

+                false

+        }

+

+        private def getMustPropagationBodies(Relation relation, Relation inverseRelation,

+                Map<Relation, ? extends Set<String>> mustRelations) {

+                val builder = ImmutableList.<StringConcatenationClient>builder()

+                val mustSet = mustRelations.get(relation)

+                if (mustSet !== null) {

+                        for (refinementQuery : mustSet) {

+                                builder.add('''find «refinementQuery»(problem, interpretation, from, to);''')

+                        }

+                }

+                if (inverseRelation !== null && inverseRelation != relation) {

+                        val inverseMustSet = mustRelations.get(inverseRelation)

+                        if (inverseMustSet !== null) {

+                                for (refinementQuery : inverseMustSet) {

+                                        builder.add('''find «refinementQuery»(problem, interpretation, to, from);''')

+                                }

+                        }

+                }

+                builder.build

+        }

 }

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

 

+import com.google.common.collect.ImmutableList

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

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

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

@@ -29,12 +30,14 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory

 import java.lang.reflect.Field

 import java.util.HashMap

+import java.util.Iterator

 import java.util.LinkedHashMap

 import java.util.LinkedList

 import java.util.List

 import java.util.Map

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

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

+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

@@ -43,6 +46,7 @@ import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory
 import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule

 import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory

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

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

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

 

 class RefinementRuleProvider {

@@ -50,57 +54,55 @@ class RefinementRuleProvider {
         val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE

         val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE

 

-        var AdvancedViatraQueryEngine queryEngine

-        var Field delayMessageDelivery

-

         def canonizeName(String name) {

                 return name.replace(' ', '_')

         }

 

+        def createUnitPrulePropagator(LogicProblem p, PartialInterpretation i, GeneratedPatterns patterns,

+                ScopePropagator scopePropagator, ModelGenerationStatistics statistics) {

+                new UnitRulePropagator(p, i, this, scopePropagator, patterns.mustRelationPropagationQueries, statistics)

+        }

+

         def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> createObjectRefinementRules(

                 LogicProblem p,

                 PartialInterpretation i,

                 GeneratedPatterns patterns,

-                ScopePropagator scopePropagator,

+                UnitRulePropagator unitRulePropagator,

                 boolean nameNewElement,

                 ModelGenerationStatistics statistics

         ) {

                 val res = new LinkedHashMap

                 val recursiveObjectCreation = recursiveObjectCreation(p, i)

-                queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine

-                delayMessageDelivery = queryEngine.class.getDeclaredField("delayMessageDelivery")

-                delayMessageDelivery.accessible = true

                 for (LHSEntry : patterns.refineObjectQueries.entrySet) {

                         val containmentRelation = LHSEntry.key.containmentRelation

                         val inverseRelation = LHSEntry.key.inverseContainment

                         val type = LHSEntry.key.newType

                         val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>>

                         val rule = createObjectCreationRule(p, containmentRelation, inverseRelation, type,

-                                recursiveObjectCreation.get(type), lhs, nameNewElement, scopePropagator, statistics)

+                                recursiveObjectCreation.get(type), lhs, nameNewElement, unitRulePropagator, statistics)

                         res.put(LHSEntry.key, rule)

                 }

                 return res

         }

 

         def private createObjectCreationRule(LogicProblem p, Relation containmentRelation, Relation inverseRelation,

-                Type type, List<ObjectCreationInterpretationData> recursiceObjectCreations,

+                Type type, List<ObjectCreationInterpretationData> recursiveObjectCreations,

                 IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, boolean nameNewElement,

-                ScopePropagator scopePropagator, ModelGenerationStatistics statistics) {

+                UnitRulePropagator unitRulePropagator, ModelGenerationStatistics statistics) {

                 val name = '''addObject_«type.name.canonizeName»«IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»'''

                 val ruleBuilder = factory.createRule(lhs).name(name)

                 if (containmentRelation !== null) {

                         if (inverseRelation !== null) {

                                 ruleBuilder.action [ match |

                                         statistics.incrementTransformationCount

-//                                      println(name)                                           

+//                                      println(name)

+                                        val startTime = System.nanoTime

                                         // val problem = match.get(0) as LogicProblem

                                         val interpretation = match.get(1) as PartialInterpretation

                                         val relationInterpretation = match.get(2) as PartialRelationInterpretation

                                         val inverseRelationInterpretation = match.get(3) as PartialRelationInterpretation

                                         val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation

                                         val container = match.get(5) as DefinedElement

-

-                                        val startTime = System.nanoTime

                                         createObjectActionWithContainmentAndInverse(

                                                 nameNewElement,

                                                 interpretation,

@@ -109,29 +111,24 @@ class RefinementRuleProvider {
                                                 relationInterpretation,

                                                 inverseRelationInterpretation,

                                                 [createDefinedElement],

-                                                recursiceObjectCreations,

-                                                scopePropagator

+                                                recursiveObjectCreations,

+                                                unitRulePropagator

                                         )

                                         statistics.addExecutionTime(System.nanoTime - startTime)

 

-                                        flushQueryEngine(scopePropagator)

-

-                                        // Scope propagation

-                                        val propagatorStartTime = System.nanoTime

-                                        scopePropagator.propagateAllScopeConstraints()

-                                        statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime)

+                                        unitRulePropagator.propagate

                                 ]

                         } else {

                                 ruleBuilder.action [ match |

                                         statistics.incrementTransformationCount

 //                                      println(name)

+                                        val startTime = System.nanoTime

                                         // val problem = match.get(0) as LogicProblem

                                         val interpretation = match.get(1) as PartialInterpretation

                                         val relationInterpretation = match.get(2) as PartialRelationInterpretation

                                         val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation

                                         val container = match.get(4) as DefinedElement

 

-                                        val startTime = System.nanoTime

                                         createObjectActionWithContainment(

                                                 nameNewElement,

                                                 interpretation,

@@ -139,44 +136,34 @@ class RefinementRuleProvider {
                                                 container,

                                                 relationInterpretation,

                                                 [createDefinedElement],

-                                                recursiceObjectCreations,

-                                                scopePropagator

+                                                recursiveObjectCreations,

+                                                unitRulePropagator

                                         )

                                         statistics.addExecutionTime(System.nanoTime - startTime)

 

-                                        flushQueryEngine(scopePropagator)

-

-                                        // Scope propagation

-                                        val propagatorStartTime = System.nanoTime

-                                        scopePropagator.propagateAllScopeConstraints()

-                                        statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime)

+                                        unitRulePropagator.propagate

                                 ]

                         }

                 } else {

                         ruleBuilder.action [ match |

                                 statistics.incrementTransformationCount

 //                              println(name)

+                                val startTime = System.nanoTime

                                 // val problem = match.get(0) as LogicProblem

                                 val interpretation = match.get(1) as PartialInterpretation

                                 val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation

 

-                                val startTime = System.nanoTime

                                 createObjectAction(

                                         nameNewElement,

                                         interpretation,

                                         typeInterpretation,

                                         [createDefinedElement],

-                                        recursiceObjectCreations,

-                                        scopePropagator

+                                        recursiveObjectCreations,

+                                        unitRulePropagator

                                 )

                                 statistics.addExecutionTime(System.nanoTime - startTime)

 

-                                flushQueryEngine(scopePropagator)

-

-                                // Scope propagation

-                                val propagatorStartTime = System.nanoTime

-                                scopePropagator.propagateAllScopeConstraints()

-                                statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime)

+                                unitRulePropagator.propagate

                         ]

                 }

                 return ruleBuilder.build

@@ -342,14 +329,14 @@ class RefinementRuleProvider {
                 [createStringElement]

         }

 

-        def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator,

+        def createRelationRefinementRules(GeneratedPatterns patterns, UnitRulePropagator unitRulePropagator,

                 ModelGenerationStatistics statistics) {

                 val res = new LinkedHashMap

-                for (LHSEntry : patterns.refinerelationQueries.entrySet) {

+                for (LHSEntry : patterns.refineRelationQueries.entrySet) {

                         val declaration = LHSEntry.key.key

                         val inverseReference = LHSEntry.key.value

                         val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>>

-                        val rule = createRelationRefinementRule(declaration, inverseReference, lhs, scopePropagator, statistics)

+                        val rule = createRelationRefinementRule(declaration, inverseReference, lhs, unitRulePropagator, statistics)

                         res.put(LHSEntry.key, rule)

                 }

                 return res

@@ -357,59 +344,29 @@ class RefinementRuleProvider {
 

         def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>> createRelationRefinementRule(

                 RelationDeclaration declaration, Relation inverseRelation,

-                IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ScopePropagator scopePropagator,

+                IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, UnitRulePropagator unitRulePropagator,

                 ModelGenerationStatistics statistics) {

                 val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»'''

                 val ruleBuilder = factory.createRule(lhs).name(name)

                 if (inverseRelation === null) {

                         ruleBuilder.action [ match |

                                 statistics.incrementTransformationCount

-

 //                              println(name)

-                                // val problem = match.get(0) as LogicProblem

-                                // val interpretation = match.get(1) as PartialInterpretation

-                                val relationInterpretation = match.get(2) as PartialRelationInterpretation

-                                val src = match.get(3) as DefinedElement

-                                val trg = match.get(4) as DefinedElement

-

-                                queryEngine.delayUpdatePropagation [

-                                        val startTime = System.nanoTime

-                                        createRelationLinkAction(src, trg, relationInterpretation)

-                                        statistics.addExecutionTime(System.nanoTime - startTime)

-                                ]

+                                val startTime = System.nanoTime

+                                createRelationLinkAction(match, unitRulePropagator)

+                                statistics.addExecutionTime(System.nanoTime - startTime)

 

-                                // Scope propagation

-                                if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) {

-                                        queryEngine.delayUpdatePropagation [

-                                                val propagatorStartTime = System.nanoTime

-                                                scopePropagator.propagateAllScopeConstraints()

-                                                statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime)

-                                        ]

-                                }

+                                unitRulePropagator.propagate

                         ]

                 } else {

                         ruleBuilder.action [ match |

                                 statistics.incrementTransformationCount

 //                              println(name)

-                                // val problem = match.get(0) as LogicProblem

-                                // val interpretation = match.get(1) as PartialInterpretation

-                                val relationInterpretation = match.get(2) as PartialRelationInterpretation

-                                val inverseInterpretation = match.get(3) as PartialRelationInterpretation

-                                val src = match.get(4) as DefinedElement

-                                val trg = match.get(5) as DefinedElement

-

                                 val startTime = System.nanoTime

-                                createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation)

+                                createRelationLinkWithInverse(match, unitRulePropagator)

                                 statistics.addExecutionTime(System.nanoTime - startTime)

 

-                                // Scope propagation

-                                if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) {

-                                        flushQueryEngine(scopePropagator)

-

-                                        val propagatorStartTime = System.nanoTime

-                                        scopePropagator.propagateAllScopeConstraints()

-                                        statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime)

-                                }

+                                unitRulePropagator.propagate

                         ]

                 }

 

@@ -420,7 +377,7 @@ class RefinementRuleProvider {
         // Actions

         // ///////////////////////

         protected def void createObjectAction(boolean nameNewElement, ObjectCreationInterpretationData data,

-                DefinedElement container, ScopePropagator scopePropagator) {

+                DefinedElement container, UnitRulePropagator unitRulePropagator) {

                 if (data.containerInterpretation !== null) {

                         if (data.containerInverseInterpretation !== null) {

                                 createObjectActionWithContainmentAndInverse(

@@ -432,7 +389,7 @@ class RefinementRuleProvider {
                                         data.containerInverseInterpretation,

                                         data.constructor,

                                         data.recursiveConstructors,

-                                        scopePropagator

+                                        unitRulePropagator

                                 )

                         } else {

                                 createObjectActionWithContainment(

@@ -443,7 +400,7 @@ class RefinementRuleProvider {
                                         data.containerInterpretation,

                                         data.constructor,

                                         data.recursiveConstructors,

-                                        scopePropagator

+                                        unitRulePropagator

                                 )

                         }

                 } else {

@@ -453,7 +410,7 @@ class RefinementRuleProvider {
                                 data.typeInterpretation,

                                 data.constructor,

                                 data.recursiveConstructors,

-                                scopePropagator

+                                unitRulePropagator

                         )

                 }

 

@@ -468,7 +425,7 @@ class RefinementRuleProvider {
                 PartialRelationInterpretation inverseRelationInterpretation,

                 Function0<DefinedElement> constructor,

                 List<ObjectCreationInterpretationData> recursiceObjectCreations,

-                ScopePropagator scopePropagator

+                UnitRulePropagator unitRulePropagator

         ) {

                 val newElement = constructor.apply

                 if (nameNewElement) {

@@ -488,14 +445,16 @@ class RefinementRuleProvider {
                 inverseRelationInterpretation.relationlinks += newLink2

 

                 // Scope propagation

-                scopePropagator.decrementTypeScope(typeInterpretation)

+                unitRulePropagator.decrementTypeScope(typeInterpretation)

+                unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf)

+                unitRulePropagator.addedToRelation(inverseRelationInterpretation.interpretationOf)

 

                 // Existence

                 interpretation.newElements += newElement

 

                 // Do recursive object creation

                 for (newConstructor : recursiceObjectCreations) {

-                        createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator)

+                        createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator)

                 }

 

                 return newElement

@@ -509,7 +468,7 @@ class RefinementRuleProvider {
                 PartialRelationInterpretation relationInterpretation,

                 Function0<DefinedElement> constructor,

                 List<ObjectCreationInterpretationData> recursiceObjectCreations,

-                ScopePropagator scopePropagator

+                UnitRulePropagator unitRulePropagator

         ) {

                 val newElement = constructor.apply

                 if (nameNewElement) {

@@ -524,16 +483,17 @@ class RefinementRuleProvider {
                 // ContainmentRelation

                 val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement]

                 relationInterpretation.relationlinks += newLink

+                unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf)

 

                 // Scope propagation

-                scopePropagator.decrementTypeScope(typeInterpretation)

+                unitRulePropagator.decrementTypeScope(typeInterpretation)

 

                 // Existence

                 interpretation.newElements += newElement

 

                 // Do recursive object creation

                 for (newConstructor : recursiceObjectCreations) {

-                        createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator)

+                        createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator)

                 }

 

                 return newElement

@@ -541,7 +501,7 @@ class RefinementRuleProvider {
 

         protected def createObjectAction(boolean nameNewElement, PartialInterpretation interpretation,

                 PartialTypeInterpratation typeInterpretation, Function0<DefinedElement> constructor,

-                List<ObjectCreationInterpretationData> recursiceObjectCreations, ScopePropagator scopePropagator) {

+                List<ObjectCreationInterpretationData> recursiceObjectCreations, UnitRulePropagator unitRulePropagator) {

                 val newElement = constructor.apply

                 if (nameNewElement) {

                         newElement.name = '''new «interpretation.newElements.size»'''

@@ -554,38 +514,220 @@ class RefinementRuleProvider {
                 }

 

                 // Scope propagation

-                scopePropagator.decrementTypeScope(typeInterpretation)

+                unitRulePropagator.decrementTypeScope(typeInterpretation)

 

                 // Existence

                 interpretation.newElements += newElement

 

                 // Do recursive object creation

                 for (newConstructor : recursiceObjectCreations) {

-                        createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator)

+                        createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator)

                 }

 

                 return newElement

         }

 

-        protected def boolean createRelationLinkAction(DefinedElement src, DefinedElement trg,

-                PartialRelationInterpretation relationInterpretation) {

+        protected def createRelationLinkAction(IPatternMatch match, UnitRulePropagator unitRulePropagator) {

+                // val problem = match.get(0) as LogicProblem

+                // val interpretation = match.get(1) as PartialInterpretation

+                val relationInterpretation = match.get(2) as PartialRelationInterpretation

+                val src = match.get(3) as DefinedElement

+                val trg = match.get(4) as DefinedElement

+                createRelationLinkAction(src, trg, relationInterpretation, unitRulePropagator)

+        }

+

+        protected def void createRelationLinkAction(DefinedElement src, DefinedElement trg,

+                PartialRelationInterpretation relationInterpretation, UnitRulePropagator unitRulePropagator) {

                 val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg]

                 relationInterpretation.relationlinks += link

+                unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf)

         }

 

-        protected def boolean createRelationLinkWithInverse(DefinedElement src, DefinedElement trg,

-                PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation) {

+        protected def void createRelationLinkWithInverse(IPatternMatch match, UnitRulePropagator unitRulePropagator) {

+                // val problem = match.get(0) as LogicProblem

+                // val interpretation = match.get(1) as PartialInterpretation

+                val relationInterpretation = match.get(2) as PartialRelationInterpretation

+                val inverseInterpretation = match.get(3) as PartialRelationInterpretation

+                val src = match.get(4) as DefinedElement

+                val trg = match.get(5) as DefinedElement

+                createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation, unitRulePropagator)

+        }

+

+        protected def void createRelationLinkWithInverse(DefinedElement src, DefinedElement trg,

+                PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation,

+                UnitRulePropagator unitRulePropagator) {

                 val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg]

                 relationInterpretation.relationlinks += link

                 val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src]

                 inverseInterpretation.relationlinks += inverseLink

+                unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf)

+                unitRulePropagator.addedToRelation(inverseInterpretation.interpretationOf)

         }

 

-        protected def flushQueryEngine(ScopePropagator scopePropagator) {

-                if (scopePropagator.queryEngineFlushRequiredBeforePropagation && queryEngine.updatePropagationDelayed) {

-                        delayMessageDelivery.setBoolean(queryEngine, false)

-                        queryEngine.getQueryBackend(ReteBackendFactory.INSTANCE).flushUpdates

-                        delayMessageDelivery.setBoolean(queryEngine, true)

+        static class UnitRulePropagator {

+                val LogicProblem p

+                val PartialInterpretation i

+                val RefinementRuleProvider refinementRuleProvider

+                var AdvancedViatraQueryEngine queryEngine

+                var Field delayMessageDelivery

+                val ScopePropagator scopePropagator

+                val List<AbstractMustRelationPropagator<? extends IPatternMatch>> propagators

+                val ModelGenerationStatistics statistics

+

+                new(LogicProblem p, PartialInterpretation i, RefinementRuleProvider refinementRuleProvider,

+                        ScopePropagator scopePropagator,

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

+                        ModelGenerationStatistics statistics) {

+                        this.p = p

+                        this.i = i

+                        this.refinementRuleProvider = refinementRuleProvider

+                        queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine

+                        delayMessageDelivery = queryEngine.class.getDeclaredField("delayMessageDelivery")

+                        delayMessageDelivery.accessible = true

+                        this.scopePropagator = scopePropagator

+                        propagators = ImmutableList.copyOf(mustRelationPropagationQueries.entrySet.map [ entry |

+                                val matcher = queryEngine.getMatcher(entry.value)

+                                getPropagator(entry.key.key, entry.key.value, matcher)

+                        ])

+                        this.statistics = statistics

+                }

+

+                def decrementTypeScope(PartialTypeInterpratation partialTypeInterpratation) {

+                        scopePropagator.decrementTypeScope(partialTypeInterpratation)

+                }

+

+                def addedToRelation(Relation r) {

+                        scopePropagator.addedToRelation(r)

+                }

+

+                def propagate() {

+                        var boolean changed

+                        do {

+                                val scopeChanged = propagateScope()

+                                val mustChanged = propagateMustRelations()

+                                changed = scopeChanged || mustChanged

+                        } while (changed)

+                }

+

+                protected def flushQueryEngine() {

+                        if (queryEngine.updatePropagationDelayed) {

+                                delayMessageDelivery.setBoolean(queryEngine, false)

+                                queryEngine.getQueryBackend(ReteBackendFactory.INSTANCE).flushUpdates

+                                delayMessageDelivery.setBoolean(queryEngine, true)

+                        }

+                }

+

+                protected def propagateScope() {

+                        if (scopePropagator.scopePropagationNeeded) {

+                                if (scopePropagator.queryEngineFlushRequiredBeforePropagation) {

+                                        flushQueryEngine()

+                                }

+                                val propagatorStartTime = System.nanoTime

+                                scopePropagator.propagateAllScopeConstraints()

+                                statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime)

+                                true

+                        } else {

+                                false

+                        }

+                }

+

+                protected def propagateMustRelations() {

+                        if (propagators.empty) {

+                                return false

+                        }

+                        flushQueryEngine()

+                        val propagatorStartTime = System.nanoTime

+                        var changed = false

+                        for (propagator : propagators) {

+                                changed = propagator.propagate(p, i, refinementRuleProvider, this) || changed

+                        }

+                        statistics.addMustRelationPropagationTime(System.nanoTime - propagatorStartTime)

+                        changed

+                }

+

+                private static def <T extends IPatternMatch> getPropagator(Relation relation, Relation inverseRelation,

+                        ViatraQueryMatcher<T> matcher) {

+                        if (inverseRelation === null) {

+                                new MustRelationPropagator(matcher)

+                        } else if (relation == inverseRelation) {

+                                new MustRelationPropagatorWithSelfInverse(matcher)

+                        } else {

+                                new MustRelationPropagatorWithInverse(matcher)

+                        }

+                }

+

+                @FinalFieldsConstructor

+                private static abstract class AbstractMustRelationPropagator<T extends IPatternMatch> {

+                        val ViatraQueryMatcher<T> matcher

+

+                        def propagate(LogicProblem p, PartialInterpretation i, RefinementRuleProvider refinementRuleProvider,

+                                UnitRulePropagator unitRulePropagator) {

+                                val iterator = getIterator(p, i)

+                                if (!iterator.hasNext) {

+                                        return false

+                                }

+                                iterate(iterator, refinementRuleProvider, unitRulePropagator)

+                                true

+                        }

+

+                        def iterate(Iterator<T> iterator, RefinementRuleProvider refinementRuleProvider,

+                                UnitRulePropagator unitRulePropagator) {

+                                while (iterator.hasNext) {

+                                        doPropagate(iterator.next, refinementRuleProvider, unitRulePropagator)

+                                }

+                        }

+

+                        protected def getIterator(LogicProblem p, PartialInterpretation i) {

+                                val partialMatch = matcher.newEmptyMatch

+                                partialMatch.set(0, p)

+                                partialMatch.set(1, i)

+                                matcher.streamAllMatches(partialMatch).iterator

+                        }

+

+                        protected def void doPropagate(T match, RefinementRuleProvider refinementRuleProvider,

+                                UnitRulePropagator unitRulePropagator)

+                }

+

+                private static class MustRelationPropagator<T extends IPatternMatch> extends AbstractMustRelationPropagator<T> {

+                        new(ViatraQueryMatcher<T> matcher) {

+                                super(matcher)

+                        }

+

+                        override protected doPropagate(T match, RefinementRuleProvider refinementRuleProvider,

+                                UnitRulePropagator unitRulePropagator) {

+                                refinementRuleProvider.createRelationLinkAction(match, unitRulePropagator)

+                        }

+                }

+

+                private static class MustRelationPropagatorWithInverse<T extends IPatternMatch> extends AbstractMustRelationPropagator<T> {

+                        new(ViatraQueryMatcher<T> matcher) {

+                                super(matcher)

+                        }

+

+                        override protected doPropagate(T match, RefinementRuleProvider refinementRuleProvider,

+                                UnitRulePropagator unitRulePropagator) {

+                                refinementRuleProvider.createRelationLinkWithInverse(match, unitRulePropagator)

+                        }

+                }

+

+                private static class MustRelationPropagatorWithSelfInverse<T extends IPatternMatch> extends MustRelationPropagatorWithInverse<T> {

+                        new(ViatraQueryMatcher<T> matcher) {

+                                super(matcher)

+                        }

+

+                        override iterate(Iterator<T> iterator, RefinementRuleProvider refinementRuleProvider,

+                                UnitRulePropagator unitRulePropagator) {

+                                val pairs = newHashSet

+                                while (iterator.hasNext) {

+                                        val match = iterator.next

+                                        val src = match.get(4) as DefinedElement

+                                        val trg = match.get(5) as DefinedElement

+                                        if (!pairs.contains(trg -> src)) {

+                                                pairs.add(src -> trg)

+                                                doPropagate(match, refinementRuleProvider, unitRulePropagator)

+                                        }

+                                }

+                        }

                 }

         }

 }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend
index 26ec7091..69b54b8a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend
@@ -6,7 +6,6 @@ import com.google.inject.Inject
 import com.google.inject.Injector

 import com.google.inject.multibindings.Multibinder

 import com.google.inject.name.Names

-import com.google.inject.util.Modules

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

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

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

@@ -46,7 +45,6 @@ import org.eclipse.xtext.scoping.IScope
 import org.eclipse.xtext.scoping.IScopeProvider

 import org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider

 import org.eclipse.xtext.scoping.impl.SimpleScope

-import org.eclipse.xtext.service.AbstractGenericModule

 import org.eclipse.xtext.service.SingletonBinding

 import org.eclipse.xtext.workspace.IProjectConfigProvider

 

@@ -65,35 +63,32 @@ package class StandaloneParserWithFixedMetamodelProviderModule extends Standalon
                 Multibinder::newSetBinder(binder, IMetamodelProviderInstance);

         }

 

-}

-

-package class StandaloneParserOverridesModule extends AbstractGenericModule {

-

-        def Class<? extends IMetamodelProvider> bindIMetamodelProvider() {

+        @SingletonBinding

+        override IResourceServiceProvider.Registry bindIResourceServiceProvider$Registry() {

+                new VqlDeactivatedServiceProviderRegistry

+        }

+        

+        override Class<? extends IMetamodelProvider> bindIMetamodelProvider() {

                 FixedMetamodelProvider

         }

 

-        def Class<? extends IProjectConfigProvider> bindProjectConfigProvider() {

+        override Class<? extends IProjectConfigProvider> bindProjectConfigProvider() {

                 NullProjectConfigProvider

         }

 

         @SingletonBinding

-        def Class<? extends IResourceServiceProvider.Registry> bindIResourceServiceProvider$Registry() {

-                VqlDeactivatedServiceProviderRegistry

-        }

-

-        def EValidator.Registry bindEValidator$Registry() {

+        override EValidator.Registry bindEValidatorRegistry() {

                 // org.eclipse.xtext.validation.EValidatorRegistrar modifies EValidators already in the registry,

                 // so it is not safe to populate the registry from the EValidator.Registry.INSTANCE singleton.

                 // There is no need to execute any EValiator other than EMFPatternLanguageValidator,

                 // so we can start with a blank registry instead.

-                new EValidatorRegistryImpl()

+                new EValidatorRegistryImpl

         }

 

-        def EPackage.Registry bindEPackage$Registry() {

+        @SingletonBinding

+        override EPackage.Registry bindEPackageRegistry() {

                 new EPackageRegistryImpl(EPackage.Registry.INSTANCE)

         }

-

 }

 

 package class NullProjectConfigProvider implements IProjectConfigProvider {

@@ -136,10 +131,8 @@ class ParseUtil {
 

         def protected Injector internalCreateInjector() {

                 ensureViatraInitialized();

-                val runtimeModulemodule = new StandaloneParserWithFixedMetamodelProviderModule

-                val overridesModule = new StandaloneParserOverridesModule

-                val module = Modules.override(runtimeModulemodule).with(overridesModule)

-                val newInjector = Guice.createInjector(module)

+                val runtimeModule = new StandaloneParserWithFixedMetamodelProviderModule

+                val newInjector = Guice.createInjector(runtimeModule)

                 return newInjector

         }

 

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 56beacfa..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,215 +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.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 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,

-                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, writeFiles)

-

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

-                scopePropagator.propagateAllScopeConstraints

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

-                        queries, scopePropagator, nameNewElements, statistics)

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

-                        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 c333feca..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,12 +79,7 @@ class ViatraReasoner extends LogicReasoner {
                         problem,

                         emptySolution,

                         workspace,

-                        viatraConfig.nameNewElements,

-                        viatraConfig.typeInferenceMethod,

-                        viatraConfig.calculateObjectCreationCosts,

-                        viatraConfig.scopePropagatorStrategy,

-                        viatraConfig.hints,

-                        viatraConfig.documentationLevel

+                        viatraConfig

                 )

 

                 val compositeObjective = new ModelGenerationCompositeObjective(

@@ -111,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

 

@@ -184,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

@@ -210,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"

@@ -228,6 +194,10 @@ class ViatraReasoner extends LogicReasoner {
                                 it.value = (method.statistics.scopePropagationTime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

+                                it.name = "MustRelationPropagationTime"

+                                it.value = (method.statistics.mustRelationPropagationTime / 1000000) as int

+                        ]

+                        it.entries += createIntStatisticEntry => [

                                 it.name = "TypeAnalysisTime"

                                 it.value = (method.statistics.preliminaryTypeAnalisisTime / 1000000) as int

                         ]

@@ -248,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"

@@ -282,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 0173124c..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,19 +4,20 @@ 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

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

 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

 import java.util.List

 import java.util.Set

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

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

 

 enum StateCoderStrategy {

         Neighbourhood,

@@ -77,6 +78,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
         public var List<LinearTypeConstraintHint> hints = newArrayList

 

         public var List<CostObjectiveConfiguration> costObjectives = newArrayList

+        

+        public var List<UnitPropagationPatternGenerator> unitPropagationPatternGenerators = newArrayList

 }

 

 class DiversityDescriptor {

@@ -111,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 a2de1abc..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,13 +298,12 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                 return activationIds;

         }

 

-        private void checkForSolution(final Fitness fittness) {

+        private void checkForSolution(final Fitness fitness) {

                 solutionStore.newSolution(context);

         }

         

         public List<String> times = new LinkedList<String>();

         private void saveTimes() {

-                long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder<?, ?>)this.context.getStateCoder()).getStatecoderRuntime()/1000000;

                 long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000;

                 long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000;

                 long activationSelection = this.activationSelector.getRuntime()/1000000;

@@ -317,8 +313,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                 long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000;

                 long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000;

                 this.times.add(

-                        "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ 

-                        "|StateCoderTime:"+statecoderTime+

+                        "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+

                         "|ForwardTime:"+forwardTime+

                         "|Backtrackingtime:"+backtrackingTime+

                         "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+

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
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java
index 7e7a6e51..133ef948 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java
@@ -369,6 +369,7 @@ public class DesignSpaceManager implements IBacktrackListener {
                 } catch (InvocationTargetException e) {
                         throw new RuntimeException(e);
                 }
+                backtrackingTime += System.nanoTime() - start;
                 updateActivationCodes();
 
                 Object lastActivationId = trajectory.getLastActivationId();
@@ -382,7 +383,6 @@ public class DesignSpaceManager implements IBacktrackListener {
                 }
 
                 logger.debug("Backtrack.");
-                backtrackingTime += System.nanoTime() - start;
 
                 return true;
         }