merge with current master, comment numerical solver related logging

36 files changed, 2500 insertions, 484 deletions

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 28cf986d..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,11 +1,10 @@
-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

-        new(ModelGenerationMethod method) {

-                this.method = method

-        }

-}
\ No newline at end of file
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
+
+import org.eclipse.viatra.dse.objectives.IGlobalConstraint
+
+abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint {
+        val protected ModelGenerationMethod method
+        new(ModelGenerationMethod method) {
+                this.method = method
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend
new file mode 100644
index 00000000..25137eba
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend
@@ -0,0 +1,201 @@
+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 af7b071a..a6fa627d 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
@@ -9,246 +9,349 @@ 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.ScopePropagator

+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

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

+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.AbstractNeighbourhoodBasedStateCoderFactory

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory

-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory

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

+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedHashStateCoderFactory

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

+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

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericSolver

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

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

 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.workspace.ReasonerWorkspace

 import java.util.List

 import java.util.Map

 import org.eclipse.emf.ecore.EObject

+import org.eclipse.emf.ecore.util.EcoreUtil

 import org.eclipse.viatra.dse.api.DesignSpaceExplorer

 import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel

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

 import org.eclipse.viatra.dse.statecode.IStateCoderFactory

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

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

-import org.eclipse.emf.ecore.util.EcoreUtil

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

 

-class ViatraReasoner extends LogicReasoner{

+class ViatraReasoner extends LogicReasoner {

         val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()

         val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider

-        val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE 

+        val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE

         val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter

-        

-        

-        override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {

+

+        override solve(LogicProblem problem, LogicSolverConfiguration configuration,

+                ReasonerWorkspace workspace) throws LogicReasonerException {

                 val viatraConfig = configuration.asConfig

-                

-                if(viatraConfig.debugCongiguration.logging) {

+

+                if (viatraConfig.documentationLevel == DocumentationLevel.FULL) {

                         DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL)

                 } else {

                         DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN)

                 }

-                

+

                 val DesignSpaceExplorer dse = new DesignSpaceExplorer();

-                

+

                 dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE)

                 dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE)

                 dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE)

-                

+

                 val transformationStartTime = System.nanoTime

-                

-                

-                val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output

-                if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {

-                        workspace.writeModel(emptySolution,"init.partialmodel")

-                } 

+                val emptySolution = initialiser.initialisePartialInterpretation(problem, viatraConfig.typeScopes).output

+                if ((viatraConfig.documentationLevel == DocumentationLevel::FULL ||

+                        viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {

+                        workspace.writeModel(emptySolution, "init.partialmodel")

+                }

+

                 emptySolution.problemConainer = problem

                 val emptySolutionCopy = EcoreUtil.copy(emptySolution)

                 

                 val ScopePropagator scopePropagator = new ScopePropagator(emptySolution)

                 scopePropagator.propagateAllScopeConstraints            

                 

+                var BasicScopeGlobalConstraint basicScopeGlobalConstraint = null

+                if (viatraConfig.scopePropagatorStrategy == ScopePropagatorStrategy.None) {

+                        basicScopeGlobalConstraint = new BasicScopeGlobalConstraint(emptySolution)

+                        emptySolution.scopes.clear

+                }

+

                 val method = modelGenerationMethodProvider.createModelGenerationMethod(

                         problem,

                         emptySolution,

                         workspace,

-                        viatraConfig.nameNewElements,

-                        viatraConfig.typeInferenceMethod,

-                        scopePropagator,

-                        viatraConfig.documentationLevel,

-                        viatraConfig.calculateObjectCreationCosts

+                        viatraConfig

                 )

-                //println("parsed")

-                

-                dse.addObjective(new ModelGenerationCompositeObjective(

-                        new ScopeObjective,

+

+                val compositeObjective = new ModelGenerationCompositeObjective(

+                        basicScopeGlobalConstraint ?: new ScopeObjective,

                         method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)],

-                        new UnfinishedWFObjective(method.unfinishedWF),

+                        wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF),

                         viatraConfig

-                ))

+                )

+                dse.addObjective(compositeObjective)

+                if (viatraConfig.punishSize != PunishSizeStrategy.NONE) {

+                        val punishSizeStrategy = switch (viatraConfig.punishSize) {

+                                case SMALLER_IS_BETTER: ObjectiveKind.LOWER_IS_BETTER

+                                case LARGER_IS_BETTER: ObjectiveKind.HIGHER_IS_BETTER

+                                default: throw new IllegalArgumentException("Unknown PunishSizeStrategy: " + viatraConfig.punishSize)

+                        }

+                        val punishObjective = new PunishSizeObjective(punishSizeStrategy, compositeObjective.level + 1)

+                        dse.addObjective(punishObjective)

+                }

+

+                for (costObjective : method.costObjectives) {

+                        dse.addObjective(costObjective)

+                }

+                val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions

+                val solutionStore = if (method.optimizationProblem) {

+                                new SolutionStore()

+                        } else {

+                                new SolutionStore(numberOfRequiredSolutions)

+                        }

+                solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))

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

+                val solutionSaver = method.solutionSaver

+                solutionSaver.numericSolver = numericSolver

+                val solutionCopier = solutionSaver.solutionCopier

+                val diversityChecker = solutionSaver.diversityChecker

+                solutionStore.withSolutionSaver(solutionSaver)

+                dse.solutionStore = solutionStore

 

-                dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF))

-                for(additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) {

+                dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationGlobalConstraint(method.invalidWF))

+                dse.addGlobalConstraint(new SurelyViolatedObjectiveGlobalConstraint(solutionSaver))

+                dse.addGlobalConstraint(new InconsistentScopeGlobalConstraint)

+                if (basicScopeGlobalConstraint !== null) {

+                        dse.addGlobalConstraint(basicScopeGlobalConstraint)

+                }

+                for (additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) {

                         dse.addGlobalConstraint(additionalConstraint.apply(method))

                 }

-                

-                dse.setInitialModel(emptySolution,false)

-                

-                val IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) {

-                        new NeighbourhoodBasedStateCoderFactory

-                } else {

-                        new IdentifierBasedStateCoderFactory

+

+                dse.setInitialModel(emptySolution, false)

+

+                val IStateCoderFactory statecoder = switch (viatraConfig.stateCoderStrategy) {

+                        case Neighbourhood:

+                                new NeighbourhoodBasedHashStateCoderFactory

+                        case PairwiseNeighbourhood:

+                                new PairwiseNeighbourhoodBasedStateCoderFactory

+                        default:

+                                new IdentifierBasedStateCoderFactory

                 }

                 dse.stateCoderFactory = statecoder

-                

+

                 dse.maxNumberOfThreads = 1

-                

-                val solutionStore =  new SolutionStore(configuration.solutionScope.numberOfRequiredSolution)

-                dse.solutionStore = solutionStore

-                

-                for(rule : method.relationRefinementRules) {

+

+                for (rule : method.relationRefinementRules) {

                         dse.addTransformationRule(rule)

                 }

-                for(rule : method.objectRefinementRules) {

+                for (rule : method.objectRefinementRules) {

                         dse.addTransformationRule(rule)

                 }

                 

                 val strategy = new HillClimbingOnRealisticMetricStrategyForModelGeneration(workspace,viatraConfig,method)

                 viatraConfig.progressMonitor.workedForwardTransformation

-                val transformationFinished = System.nanoTime 

+                val transformationFinished = System.nanoTime

                 val transformationTime = transformationFinished - transformationStartTime

-                

                 val solverStartTime = System.nanoTime

-                

+

                 var boolean stoppedByTimeout

-                var boolean stoppedByException

-                try{

-                        stoppedByTimeout = dse.startExplorationWithTimeout(strategy,configuration.runtimeLimit*1000);

-                        stoppedByException = false

+                try {

+                        stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000);

                 } catch (NullPointerException npe) {

                         stoppedByTimeout = false

-                        stoppedByException = true

                 }

                 val solverTime = System.nanoTime - solverStartTime

                 viatraConfig.progressMonitor.workedSearchFinished

-                

-                //additionalMatches = strategy.solutionStoreWithCopy.additionalMatches

+

+                // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches

                 val statistics = createStatistics => [

-                        //it.solverTime = viatraConfig.runtimeLimit

-                        it.solverTime = (solverTime/1000000) as int

-                        it.transformationTime = (transformationTime/1000000) as int

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

+                        // it.solverTime = viatraConfig.runtimeLimit

+                        it.solverTime = (solverTime / 1000000) as int

+                        it.transformationTime = (transformationTime / 1000000) as int

+                        for (pair : solutionCopier.getAllCopierRuntimes(true).indexed) {

                                 it.entries += createIntStatisticEntry => [

-                                        it.name = '''Solution«x+1»FoundAt'''

-                                        it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int

+                                        it.name = '''Solution«pair.key»FoundAt'''

+                                        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"

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

+                        ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "ScopePropagationTime"

+                                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

+                        ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "StateCoderTime"

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

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int

+                                it.name = "StateCoderFailCount"

+                                it.value = strategy.numberOfStatecoderFail

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "TypeAnalysisTime" it.value = (method.statistics.PreliminaryTypeAnalisisTime/1000000) as int

+                                it.name = "SolutionCopyTime"

+                                it.value = (solutionCopier.getTotalCopierRuntime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "StateCoderTime" it.value = (statecoder.runtime/1000000) as int

+                                it.name = "States"

+                                it.value = dse.numberOfStates as int

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "StateCoderFailCount" it.value = strategy.numberOfStatecoderFail

+                                it.name = "ForwardTime"

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

                         ]

                         it.entries += createIntStatisticEntry => [

-                                it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int

+                                it.name = "BacktrackingTime"

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

                         ]

                         it.entries += createIntStatisticEntry => [

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

+                                it.name = "GlobalConstraintEvaluationTime"

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

                         ]

                         it.entries += createIntStatisticEntry => [

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

+                                it.name = "FitnessCalculationTime"

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

                         ]

                         it.entries += createIntStatisticEntry => [

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

+                                it.name = "SolutionCopyTime"

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

                         ]

                         it.entries += createIntStatisticEntry => [

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

+                                it.name = "ActivationSelectionTime"

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

                         ]

                         it.entries += createIntStatisticEntry => [

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

+                                it.name = "Decisions"

+                                it.value = method.statistics.decisionsTried

                         ]

                         it.entries += createIntStatisticEntry => [

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

+                                it.name = "Transformations"

+                                it.value = method.statistics.transformationInvocations

                         ]

                         it.entries += createIntStatisticEntry => [

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

+                                it.name = "ScopePropagations"

+                                it.value = method.statistics.scopePropagatorInvocations

                         ]

                         it.entries += createIntStatisticEntry => [

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

+                                it.name = "ScopePropagationsSolverCalls"

+                                it.value = method.statistics.scopePropagatorSolverInvocations

                         ]

-                        if(strategy.solutionStoreWithDiversityDescriptor.isActive) {

+//                      it.entries += createIntStatisticEntry => [

+//                              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.entries += createIntStatisticEntry => [

+//                              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.entries += createIntStatisticEntry => [

+//                              it.name = "NumericalSolverCachingTime"

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

+//                      ]

+//                      it.entries += createIntStatisticEntry => [

+//                              it.name = "NumericalSolverCallNumber"

+//                              it.value = strategy.numericSolver.numberOfSolverCalls

+//                      ]

+//                      it.entries += createIntStatisticEntry => [

+//                              it.name = "NumericalSolverCachedAnswerNumber"

+//                              it.value = strategy.numericSolver.numberOfCachedSolverCalls

+//                      ]

+                        if (diversityChecker.active) {

                                 it.entries += createIntStatisticEntry => [

-                                        it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int

+                                        it.name = "SolutionDiversityCheckTime"

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

                                 ]

                                 it.entries += createRealStatisticEntry => [

-                                        it.name = "SolutionDiversitySuccessRate" it.value = strategy.solutionStoreWithDiversityDescriptor.successRate

+                                        it.name = "SolutionDiversitySuccessRate"

+                                        it.value = diversityChecker.successRate

                                 ]

                         }

                 ]

-                

+

                 viatraConfig.progressMonitor.workedBackwardTransformationFinished

-                

-                if(stoppedByTimeout) {

-                        return createInsuficientResourcesResult=>[

+

+                if (stoppedByTimeout) {

+                        return createInsuficientResourcesResult => [

                                 it.problem = problem

-                                it.resourceName="time"

-                                it.representation += strategy.solutionStoreWithCopy.solutions

+                                it.resourceName = "time"

+                                it.representation += solutionCopier.getPartialInterpretations(true)

                                 it.statistics = statistics

                         ]

                 } else {

-                        if(solutionStore.solutions.empty) {

+                        if (solutionStore.solutions.empty) {

                                 return createInconsistencyResult => [

                                         it.problem = problem

-                                        it.representation += strategy.solutionStoreWithCopy.solutions

+                                        it.representation += solutionCopier.getPartialInterpretations(true)

                                         it.statistics = statistics

                                 ]

                         } else {

                                 return createModelResult => [

                                         it.problem = problem

-                                        it.trace = strategy.solutionStoreWithCopy.copyTraces

-                                        it.representation += strategy.solutionStoreWithCopy.solutions

+                                        it.trace = solutionCopier.getTraces(true)

+                                        it.representation += solutionCopier.getPartialInterpretations(true)

                                         it.statistics = statistics

                                 ]

                         }

                 }

         }

 

-    private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) {

-        sc.sumStatecoderRuntime

-    }

+        private def dispatch long runtime(AbstractNeighbourhoodBasedStateCoderFactory sc) {

+                sc.sumStatecoderRuntime

+        }

 

-    private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) {

-        sc.sumStatecoderRuntime

-    }

+        private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) {

+                sc.sumStatecoderRuntime

+        }

 

         override getInterpretations(ModelResult modelResult) {

-                val indexes = 0..<modelResult.representation.size

+                val indexes = 0 ..< modelResult.representation.size

                 val traces = modelResult.trace as List<Map<EObject, EObject>>;

-                val res = indexes.map[i | new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation,traces.get(i))].toList

+                val res = indexes.map [ i |

+                        new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation,

+                                traces.get(i))

+                ].toList

                 return res

         }

-        

+

         private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) {

-                if(configuration instanceof ViatraReasonerConfiguration) {

+                if (configuration instanceof ViatraReasonerConfiguration) {

                         return configuration

-                } else throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''')

+                } else

+                        throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''')

         }

 }

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 96bf014d..e73a52b6 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,21 +4,37 @@ 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

 

-public enum StateCoderStrategy {

-        Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity

+enum StateCoderStrategy {

+        Neighbourhood,

+        PairwiseNeighbourhood,

+        NeighbourhoodWithEquivalence,

+        IDBased,

+        DefinedByDiversity

 }

 

-class ViatraReasonerConfiguration extends LogicSolverConfiguration{

-        //public var Iterable<PQuery> existingQueries

-        

+enum PunishSizeStrategy {

+        NONE,

+        SMALLER_IS_BETTER,

+        LARGER_IS_BETTER

+}

+

+class ViatraReasonerConfiguration extends LogicSolverConfiguration {

+        // public var Iterable<PQuery> existingQueries

         public var nameNewElements = false

         public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood

         public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis

@@ -26,7 +42,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
          * Once per 1/randomBacktrackChance the search selects a random state.

          */

         public var int randomBacktrackChance = 20;

-        

+

         /**

          * Describes the required diversity between the solutions.

          * Null means that the solutions have to have different state codes only.

@@ -40,7 +56,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
         /**

          * Configuration for debugging support.

          */

-        public var DebugConfiguration debugCongiguration = new DebugConfiguration

+        public var DebugConfiguration debugConfiguration = new DebugConfiguration

         /**

          * Configuration for cutting search space.

          */

@@ -48,12 +64,11 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
          

         public var runIntermediateNumericalConsistencyChecks = true

         

-        public var punishSize = true

+        public var punishSize = PunishSizeStrategy.NONE

         public var scopeWeight = 1

         public var conaintmentWeight = 2

         public var nonContainmentWeight = 1

         public var unfinishedWFWeight = 1

-        

         public var calculateObjectCreationCosts = false

         

         public var RealisticGuidance realisticGuidance = RealisticGuidance.Composite;

@@ -63,9 +78,18 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
          public var allowMustViolations = false;

          

          public var String domain = '';

+        public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(

+                PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)

+//      public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.BasicTypeHierarchy

+        

+        public var List<LinearTypeConstraintHint> hints = newArrayList

+

+        public var List<CostObjectiveConfiguration> costObjectives = newArrayList

+        

+        public var List<UnitPropagationPatternGenerator> unitPropagationPatternGenerators = newArrayList

 }

 

-public class DiversityDescriptor {

+class DiversityDescriptor {

         public var ensureDiversity = false

         public static val FixPointRange = -1

         public var int range = FixPointRange

@@ -75,19 +99,18 @@ public class DiversityDescriptor {
         public var Set<RelationDeclaration> relevantRelations = null

 }

 

-public class DebugConfiguration {

-        public var logging = false

-        public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null;

+class DebugConfiguration {

+        public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null

         public var partalInterpretationVisualisationFrequency = 1

 }

 

-public class InternalConsistencyCheckerConfiguration {

+class InternalConsistencyCheckerConfiguration {

         public var LogicReasoner internalIncosnsitencyDetector = null

         public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null

         public var incternalConsistencyCheckingFrequency = 1

 }

 

-public class SearchSpaceConstraint {

+class SearchSpaceConstraint {

         public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE

         public var int maxDepth = UNLIMITED_MAXDEPTH

         public var List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList

@@ -101,4 +124,17 @@ public enum RealisticGuidance{
         Composite,

         Composite_Without_Violations,

         Violations

-}
\ No newline at end of file
+}

+class CostObjectiveConfiguration {

+        public var List<CostObjectiveElementConfiguration> elements = newArrayList

+        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/BasicScopeGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend
new file mode 100644
index 00000000..67f447ed
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend
@@ -0,0 +1,103 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+
+import com.google.common.collect.ImmutableList
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
+import java.util.Comparator
+import java.util.List
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.dse.objectives.Comparators
+import org.eclipse.viatra.dse.objectives.IGlobalConstraint
+import org.eclipse.viatra.dse.objectives.IObjective
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+class BasicScopeGlobalConstraint implements IGlobalConstraint, IObjective {
+        val PartialInterpretation p
+        val List<ScopeAssertion> assertions
+
+        new(PartialInterpretation p) {
+                this.p = p
+                assertions = ImmutableList.copyOf(p.scopes.map [
+                        val currentSize = targetTypeInterpretation.elements.size
+                        val minElements = minNewElements + currentSize
+                        val maxElements = if (maxNewElements < 0) {
+                                -1
+                        } else {
+                                maxNewElements + currentSize
+                        }
+                        new ScopeAssertion(minElements, maxElements, targetTypeInterpretation)
+                ])
+        }
+
+        override init(ThreadContext context) {
+                if (context.model != p) {
+                        throw new IllegalArgumentException(
+                                "Partial model must be passed to the constructor of BasicScopeGlobalConstraint")
+                }
+        }
+
+        override checkGlobalConstraint(ThreadContext context) {
+                assertions.forall[upperBoundSatisfied]
+        }
+
+        override getFitness(ThreadContext context) {
+                var double fitness = p.minNewElements
+                for (assertion : assertions) {
+                        if (!assertion.lowerBoundSatisfied) {
+                                fitness += 1
+                        }
+                }
+                fitness
+        }
+
+        override satisifiesHardObjective(Double fitness) {
+                fitness <= 0.01
+        }
+
+        override BasicScopeGlobalConstraint createNew() {
+                this
+        }
+
+        override getName() {
+                class.name
+        }
+
+        override getComparator() {
+                Comparators.LOWER_IS_BETTER
+        }
+
+        override getLevel() {
+                2
+        }
+
+        override isHardObjective() {
+                true
+        }
+
+        override setComparator(Comparator<Double> comparator) {
+                throw new UnsupportedOperationException
+        }
+
+        override setLevel(int level) {
+                throw new UnsupportedOperationException
+        }
+
+        @FinalFieldsConstructor
+        private static class ScopeAssertion {
+                val int lowerBound
+                val int upperBound
+                val PartialTypeInterpratation typeDefinitions
+
+                private def getCount() {
+                        typeDefinitions.elements.size
+                }
+
+                private def isLowerBoundSatisfied() {
+                        count >= lowerBound
+                }
+
+                private def isUpperBoundSatisfied() {
+                        upperBound < 0 || count <= upperBound
+                }
+        }
+}
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 e0f838a6..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
@@ -9,33 +9,25 @@
  *******************************************************************************/

 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse;

 

-import java.io.BufferedReader;

-import java.io.IOException;

-import java.io.InputStreamReader;

-import java.util.ArrayList;

 import java.util.Arrays;

-import java.util.Collection;

 import java.util.Collections;

 import java.util.Comparator;

 import java.util.Iterator;

 import java.util.LinkedList;

 import java.util.List;

-import java.util.Map;

 import java.util.PriorityQueue;

 import java.util.Random;

 

 import org.apache.log4j.Logger;

 import org.eclipse.emf.ecore.EObject;

 import org.eclipse.emf.ecore.util.EcoreUtil;

+import org.eclipse.viatra.dse.api.SolutionTrajectory;

 import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;

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

 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.IQuerySpecification;

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

-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;

@@ -43,13 +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.viatra2logic.NumericProblemSolver;

-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;

 

@@ -82,58 +72,72 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
         // Running

         private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore;

         private SolutionStore solutionStore;

-        private SolutionStoreWithCopy solutionStoreWithCopy;

-        private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor;

         private volatile boolean isInterrupted = false;

         private ModelResult modelResultByInternalSolver = null;

         private Random random = new Random();

-        //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;

+//      private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;

         public ActivationSelector activationSelector = new EvenActivationSelector(random);

-        public NumericSolver numericSolver = null;

+        public ViatraReasonerSolutionSaver solutionSaver;

+        public NumericSolver numericSolver;

         // Statistics

         private int numberOfStatecoderFail = 0;

         private int numberOfPrintedModel = 0;

         private int numberOfSolverCalls = 0;

+        public long globalConstraintEvaluationTime = 0;

+        public long fitnessCalculationTime = 0;

         

         public long explorationStarted = 0;

 

         public BestFirstStrategyForModelGeneration(

                         ReasonerWorkspace workspace,

                         ViatraReasonerConfiguration configuration,

-                        ModelGenerationMethod method)

-        {

+                        ModelGenerationMethod method,

+                        ViatraReasonerSolutionSaver solutionSaver,

+                        NumericSolver numericSolver) {

                 this.workspace = workspace;

                 this.configuration = configuration;

                 this.method = method;

+                this.solutionSaver = solutionSaver;

+                this.numericSolver = numericSolver;

+//              logger.setLevel(Level.DEBUG);

         }

         

-        public SolutionStoreWithCopy getSolutionStoreWithCopy() {

-                return solutionStoreWithCopy;

-        }

-        public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {

-                return solutionStoreWithDiversityDescriptor;

-        }

         public int getNumberOfStatecoderFail() {

                 return numberOfStatecoderFail;

         }

-        //LinkedList<ViatraQueryMatcher<? extends IPatternMatch>> matchers;

+        public long getForwardTime() {

+                return context.getDesignSpaceManager().getForwardTime();

+        }

+        public long getBacktrackingTime() {

+                return context.getDesignSpaceManager().getBacktrackingTime();

+        }

+

         @Override

         public void initStrategy(ThreadContext context) {

                 this.context = context;

                 this.solutionStore = context.getGlobalContext().getSolutionStore();

+                solutionStore.registerSolutionFoundHandler(new ISolutionFoundHandler() {

+                        

+                        @Override

+                        public void solutionTriedToSave(ThreadContext context, SolutionTrajectory trajectory) {

+                                // Ignore.

+                        }

+                        

+                        @Override

+                        public void solutionFound(ThreadContext context, SolutionTrajectory trajectory) {

+                                configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions);

+                                saveTimes();

+                                logger.debug("Found a solution.");

+                        }

+                });

+                numericSolver.init(context);

                 

 //              ViatraQueryEngine engine = context.getQueryEngine();

-//              // TODO: visualisation

 //              matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();

 //              for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {

-//                      //System.out.println(p.getSimpleName());

-//                      ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);

-//                      matchers.add(matcher);

+//                              ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);

 //              }

-                

-                this.solutionStoreWithCopy = new SolutionStoreWithCopy();

-                this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);

-

+//              

                 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();

                 this.comparator = new Comparator<TrajectoryWithFitness>() {

                         @Override

@@ -141,23 +145,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                                 return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);

                         }

                 };

-                

-                this.numericSolver = new NumericSolver(context, method, this.configuration.runIntermediateNumericalConsistencyChecks, false);

 

                 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);

         }

 

         @Override

         public void explore() {

-//              System.out.println("press enter");

-//              try {

-//                      new BufferedReader(new InputStreamReader(System.in)).readLine();

-//              } catch (IOException e) {

-//                      // TODO Auto-generated catch block

-//                      e.printStackTrace();

-//              }  

                 this.explorationStarted=System.nanoTime();

-                if (!context.checkGlobalConstraints()) {

+                if (!checkGlobalConstraints()) {

                         logger.info("Global contraint is not satisifed in the first state. Terminate.");

                         return;

                 } else if(!numericSolver.maySatisfiable()) {

@@ -169,14 +164,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                         return;

                 }

                 

-                final Fitness firstFittness = context.calculateFitness();

-                checkForSolution(firstFittness);

+                final Fitness firstFitness = calculateFitness();

+                checkForSolution(firstFitness);

                 

                 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();

                 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);

-                TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness);

-                trajectoiresToExplore.add(currentTrajectoryWithFittness);

-                

+                TrajectoryWithFitness currentTrajectoryWithFitness = new TrajectoryWithFitness(firstTrajectory, firstFitness);

+                trajectoiresToExplore.add(currentTrajectoryWithFitness);

                 //if(configuration)

                 visualiseCurrentState();

 //              for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {

@@ -190,22 +184,22 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                 

                 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) {

 

-                        if (currentTrajectoryWithFittness == null) {

+                        if (currentTrajectoryWithFitness == null) {

                                 if (trajectoiresToExplore.isEmpty()) {

                                         logger.debug("State space is fully traversed.");

                                         return;

                                 } else {

-                                        currentTrajectoryWithFittness = selectState();

+                                        currentTrajectoryWithFitness = selectState();

                                         if (logger.isDebugEnabled()) {

                                                 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));

-                                                logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness);

+                                                logger.debug("New trajectory is chosen: " + currentTrajectoryWithFitness);

                                         }

-                                        context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory);

+                                        context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFitness.trajectory);

                                 }

                         }

                         

 //                      visualiseCurrentState();

-//                      boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);

+//                      boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);

 //                      if(consistencyCheckResult == true) {

 //                              continue mainLoop;

 //                      }

@@ -215,29 +209,25 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
 

                         while (!isInterrupted && !configuration.progressMonitor.isCancelled() && iterator.hasNext()) {

                                 final Object nextActivation = iterator.next();

-//                              if (!iterator.hasNext()) {

-//                                      logger.debug("Last untraversed activation of the state.");

-//                                      trajectoiresToExplore.remove(currentTrajectoryWithFittness);

-//                              }

                                 logger.debug("Executing new activation: " + nextActivation);

                                 context.executeAcitvationId(nextActivation);

+                                method.getStatistics().incrementDecisionCount();

 

                                 visualiseCurrentState();

 //                              for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {

 //                                      int c = matcher.countMatches();

-//                                      if(c>=100) {

+//                                      if(c>=1) {

 //                                              System.out.println(c+ " " +matcher.getPatternName());

-//                                      }

-//                                      

+//                                      }       

 //                              }

                                 

-                                boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);

+                                boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness);

                                 if(consistencyCheckResult == true) { continue mainLoop; }

 

                                 if (context.isCurrentStateAlreadyTraversed()) {

                                         logger.info("The new state is already visited.");

                                         context.backtrack();

-                                } else if (!context.checkGlobalConstraints()) {

+                                } else if (!checkGlobalConstraints()) {

                                         logger.debug("Global contraint is not satisifed.");

                                         context.backtrack();

                                 } else if (!numericSolver.maySatisfiable()) {

@@ -252,76 +242,84 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                                                 continue;

                                         }

 

-                                        TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness(

+                                        TrajectoryWithFitness nextTrajectoryWithfitness = new TrajectoryWithFitness(

                                                         context.getTrajectory().toArray(), nextFitness);

-                                        trajectoiresToExplore.add(nextTrajectoryWithFittness);

+                                        trajectoiresToExplore.add(nextTrajectoryWithfitness);

 

-                                        int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness,

-                                                        nextTrajectoryWithFittness.fitness);

+                                        int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFitness.fitness,

+                                                        nextTrajectoryWithfitness.fitness);

                                         if (compare < 0) {

                                                 logger.debug("Better fitness, moving on: " + nextFitness);

-                                                currentTrajectoryWithFittness = nextTrajectoryWithFittness;

+                                                currentTrajectoryWithFitness = nextTrajectoryWithfitness;

                                                 continue mainLoop;

                                         } else if (compare == 0) {

                                                 logger.debug("Equally good fitness, moving on: " + nextFitness);

-                                                currentTrajectoryWithFittness = nextTrajectoryWithFittness;

+                                                currentTrajectoryWithFitness = nextTrajectoryWithfitness;

                                                 continue mainLoop;

                                         } else {

                                                 logger.debug("Worse fitness.");

-                                                currentTrajectoryWithFittness = null;

+                                                currentTrajectoryWithFitness = null;

                                                 continue mainLoop;

                                         }

                                 }

                         }

 

                         logger.debug("State is fully traversed.");

-                        trajectoiresToExplore.remove(currentTrajectoryWithFittness);

-                        currentTrajectoryWithFittness = null;

+                        trajectoiresToExplore.remove(currentTrajectoryWithFitness);

+                        currentTrajectoryWithFitness = null;

 

                 }

                 logger.info("Interrupted.");

         }

 

+        private boolean checkGlobalConstraints() {

+                long start = System.nanoTime();

+                boolean result = context.checkGlobalConstraints();

+                globalConstraintEvaluationTime += System.nanoTime() - start;

+                return result;

+        }

+        

+        private Fitness calculateFitness() {

+                long start = System.nanoTime();

+                Fitness fitness = context.calculateFitness(); 

+                fitnessCalculationTime += System.nanoTime() - start;

+                return fitness;

+        }

+        

         private List<Object> selectActivation() {

                 List<Object> activationIds;

                 try {

                         activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds());

                 } catch (NullPointerException e) {

+//                      logger.warn("Unexpected state code: " + context.getDesignSpaceManager().getCurrentState());

                         numberOfStatecoderFail++;

                         activationIds = Collections.emptyList();

                 }

                 return activationIds;

         }

 

-        private void checkForSolution(final Fitness fittness) {

-                if (fittness.isSatisifiesHardObjectives()) {

-                        if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {

-                                if(numericSolver.currentSatisfiable()) {

-                                        Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context);

-                                        numericSolver.fillSolutionCopy(trace);

-                                        solutionStoreWithDiversityDescriptor.newSolution(context);

-                                        solutionStore.newSolution(context);

-                                        configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);

-                                        saveTimes();

-                                        logger.debug("Found a solution.");

-                                }

-                        }

-                }

+        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 solutionCopy = solutionStoreWithCopy.getSumRuntime()/1000000;

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

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

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

+                long solutionCopierTime = this.solutionSaver.getTotalCopierRuntime()/1000000;

                 long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000;

                 long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000;

                 long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000;

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

                 this.times.add(

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

-                        "|StateCoderTime:"+statecoderTime+

-                        "|SolutionCopyTime:"+solutionCopy+

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

+                        "|ForwardTime:"+forwardTime+

+                        "|Backtrackingtime:"+backtrackingTime+

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

+                        "|FitnessCalculationTime:"+(fitnessCalculationTime/1000000)+

                         "|ActivationSelectionTime:"+activationSelection+

+                        "|SolutionCopyTime:"+solutionCopierTime+

                         "|NumericalSolverSumTime:"+numericalSolverSumTime+

                         "|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+

                         "|NumericalSolverSolvingTime:"+numericalSolverSolving+

@@ -355,16 +353,19 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                 } else {

                         return trajectoiresToExplore.element();

                 }

-        }       

+        }

 

         public void visualiseCurrentState() {

-                PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser;

+                PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser;

                 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) {

                         PartialInterpretation p = (PartialInterpretation) (context.getModel());

                         int id = ++numberOfPrintedModel;

-                        if (id % configuration.debugCongiguration.partalInterpretationVisualisationFrequency == 0) {

+                        if (id % configuration.debugConfiguration.partalInterpretationVisualisationFrequency == 0) {

                                 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p);

-                                visualisation.writeToFile(workspace, String.format("state%09d.png", id));

+                                logger.debug("Visualizing state: " + id + " (" + context.getDesignSpaceManager().getCurrentState() + ")");

+                                String name = String.format("state%09d", id);

+                                visualisation.writeToFile(workspace, name + ".png");

+                                workspace.writeModel((EObject) context.getModel(), name + ".xmi");

                         }

                 }

         }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend
new file mode 100644
index 00000000..fb1b2066
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend
@@ -0,0 +1,184 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

+

+import com.google.common.collect.HashMultiset

+import com.google.common.collect.ImmutableSet

+import com.google.common.collect.Multiset

+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor

+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.NeighbourhoodWithTraces

+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice

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

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

+import java.util.Collection

+import java.util.HashSet

+import java.util.Map

+import java.util.Set

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

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

+

+interface DiversityChecker {

+        public static val NO_DIVERSITY_CHECKER = new DiversityChecker {

+                override isActive() {

+                        false

+                }

+

+                override getTotalRuntime() {

+                        0

+                }

+

+                override getSuccessRate() {

+                        1.0

+                }

+

+                override newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) {

+                        true

+                }

+        }

+

+        def boolean isActive()

+

+        def long getTotalRuntime()

+

+        def double getSuccessRate()

+

+        def boolean newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds)

+

+        static def of(DiversityDescriptor descriptor) {

+                if (descriptor.ensureDiversity) {

+                        new NodewiseDiversityChecker(descriptor)

+                } else {

+                        NO_DIVERSITY_CHECKER

+                }

+        }

+}

+

+abstract class AbstractDiversityChecker implements DiversityChecker {

+        val DiversityDescriptor descriptor

+        val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice

+

+        @Accessors(PUBLIC_GETTER) var long totalRuntime = 0

+        var int allCheckCount = 0

+        var int successfulCheckCount = 0

+

+        protected new(DiversityDescriptor descriptor) {

+                if (!descriptor.ensureDiversity) {

+                        throw new IllegalArgumentException(

+                                "Diversity description should enforce diversity or NO_DIVERSITY_CHECKER should be used instead.")

+                }

+                this.descriptor = descriptor

+        }

+

+        override isActive() {

+                true

+        }

+

+        override getTotalRuntime() {

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

+        }

+

+        override getSuccessRate() {

+                (allCheckCount as double) / (successfulCheckCount as double)

+        }

+

+        override newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) {

+                val start = System.nanoTime

+                val model = threadContext.model as PartialInterpretation

+                val representation = solutionCoder.createRepresentation(model, descriptor.range, descriptor.parallels,

+                        descriptor.maxNumber, descriptor.relevantTypes, descriptor.relevantRelations)

+                val isDifferent = internalNewSolution(representation, solutionId, dominatedSolutionIds)

+                totalRuntime += System.nanoTime - start

+                allCheckCount++

+                if (isDifferent) {

+                        successfulCheckCount++

+                }

+                isDifferent

+        }

+

+        protected abstract def boolean internalNewSolution(

+                NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation,

+                Object solutionId, Collection<Object> dominatedSolutionIds)

+}

+

+class NodewiseDiversityChecker extends AbstractDiversityChecker {

+        var Multiset<Integer> nodeCodes = HashMultiset.create

+        val Map<Object, Set<Integer>> tracedNodeCodes = newHashMap

+

+        new(DiversityDescriptor descriptor) {

+                super(descriptor)

+        }

+

+        override protected internalNewSolution(

+                NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation,

+                Object solutionId, Collection<Object> dominatedSolutionIds) {

+                val nodeCodesInSolution = ImmutableSet.copyOf(representation.modelRepresentation.keySet.map[hashCode])

+                val remainingNodeCodes = if (dominatedSolutionIds.empty) {

+                                nodeCodes

+                        } else {

+                                getRemainingNodeCodes(dominatedSolutionIds)

+                        }

+                val hasNewCode = nodeCodesInSolution.exists[!remainingNodeCodes.contains(it)]

+                if (hasNewCode) {

+                        nodeCodes = remainingNodeCodes

+                        nodeCodes.addAll(nodeCodesInSolution)

+                        for (dominatedSolutionId : dominatedSolutionIds) {

+                                tracedNodeCodes.remove(dominatedSolutionId)

+                        }

+                        tracedNodeCodes.put(solutionId, nodeCodesInSolution)

+                }

+                hasNewCode

+        }

+

+        private def getRemainingNodeCodes(Collection<Object> dominatedSolutionIds) {

+                // TODO Optimize multiset operations.

+                val copyOfNodeCodes = HashMultiset.create(nodeCodes)

+                for (dominatedSolutionId : dominatedSolutionIds) {

+                        val dominatedModelCode = tracedNodeCodes.get(dominatedSolutionId)

+                        if (dominatedModelCode === null) {

+                                throw new IllegalArgumentException("Unknown dominated solution: " + dominatedSolutionId)

+                        }

+                        copyOfNodeCodes.removeAll(dominatedModelCode)

+                }

+                copyOfNodeCodes

+        }

+}

+

+class GraphwiseDiversityChecker extends AbstractDiversityChecker {

+        var Set<Integer> modelCodes = newHashSet

+        val Map<Object, Integer> tracedModelCodes = newHashMap

+

+        new(DiversityDescriptor descriptor) {

+                super(descriptor)

+        }

+

+        override protected internalNewSolution(

+                NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation,

+                Object solutionId, Collection<Object> dominatedSolutionIds) {

+                val modelCodeOfSolution = representation.modelRepresentation.hashCode

+                val remainingModelCodes = if (dominatedSolutionIds.empty) {

+                                modelCodes

+                        } else {

+                                getRemainingModelCodes(dominatedSolutionIds)

+                        }

+                val isNewCode = !remainingModelCodes.contains(modelCodeOfSolution)

+                if (isNewCode) {

+                        modelCodes = remainingModelCodes

+                        modelCodes += modelCodeOfSolution

+                        for (dominatedSolutionId : dominatedSolutionIds) {

+                                tracedModelCodes.remove(dominatedSolutionId)

+                        }

+                        tracedModelCodes.put(solutionId, modelCodeOfSolution)

+                }

+                isNewCode

+        }

+

+        private def getRemainingModelCodes(Collection<Object> dominatedSolutionIds) {

+                val copyOfModelCodes = new HashSet(modelCodes)

+                for (dominatedSolutionId : dominatedSolutionIds) {

+                        val dominatedModelCode = tracedModelCodes.get(dominatedSolutionId)

+                        if (dominatedModelCode === null) {

+                                throw new IllegalArgumentException("Unknown dominated solution: " + dominatedSolutionId)

+                        }

+                        copyOfModelCodes -= dominatedModelCode

+                }

+                copyOfModelCodes

+        }

+}

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend
new file mode 100644
index 00000000..3c2e3319
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend
@@ -0,0 +1,66 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.dse.objectives.Comparators
+import org.eclipse.viatra.dse.objectives.Fitness
+import org.eclipse.viatra.dse.objectives.IObjective
+
+final class DseUtils {
+        private new() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly.")
+        }
+
+        static def calculateFitness(ThreadContext it, (IObjective)=>Double getFitness) {
+                val result = new Fitness
+                var boolean satisifiesHardObjectives = true
+                for (objective : objectives) {
+                        val fitness = getFitness.apply(objective)
+                        result.put(objective.name, fitness)
+                        if (objective.isHardObjective() && !objective.satisifiesHardObjective(fitness)) {
+                                satisifiesHardObjectives = false
+                        }
+                }
+                result.satisifiesHardObjectives = satisifiesHardObjectives
+                result
+        }
+
+        static def caclulateBestPossibleFitness(ThreadContext threadContext) {
+                threadContext.calculateFitness [ objective |
+                        if (objective instanceof IThreeValuedObjective) {
+                                objective.getBestPossibleFitness(threadContext)
+                        } else {
+                                switch (objective.comparator) {
+                                        case Comparators.LOWER_IS_BETTER:
+                                                Double.NEGATIVE_INFINITY
+                                        case Comparators.HIGHER_IS_BETTER:
+                                                Double.POSITIVE_INFINITY
+                                        case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER:
+                                                0.0
+                                        default:
+                                                throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " +
+                                                        objective.name)
+                                }
+                        }
+                ]
+        }
+
+        static def caclulateWorstPossibleFitness(ThreadContext threadContext) {
+                threadContext.calculateFitness [ objective |
+                        if (objective instanceof IThreeValuedObjective) {
+                                objective.getWorstPossibleFitness(threadContext)
+                        } else {
+                                switch (objective.comparator) {
+                                        case Comparators.LOWER_IS_BETTER,
+                                        case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER:
+                                                Double.POSITIVE_INFINITY
+                                        case Comparators.HIGHER_IS_BETTER:
+                                                Double.NEGATIVE_INFINITY
+                                        default:
+                                                throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " +
+                                                        objective.name)
+                                }
+                        }
+                ]
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/HillClimbingOnRealisticMetricStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/HillClimbingOnRealisticMetricStrategyForModelGeneration.java
index f1bf96b6..d9f84b36 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/HillClimbingOnRealisticMetricStrategyForModelGeneration.java
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/HillClimbingOnRealisticMetricStrategyForModelGeneration.java
@@ -16,6 +16,7 @@ import java.util.Random;
 import java.util.Set;
 
 import org.apache.log4j.Logger;
+import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.util.EcoreUtil;
 import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;
 import org.eclipse.viatra.dse.base.ThreadContext;
@@ -35,12 +36,12 @@ 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.RealisticGuidance;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration;
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
@@ -84,6 +85,8 @@ public class HillClimbingOnRealisticMetricStrategyForModelGeneration implements
         private double currentNodeTypeDistance = 1;
         private int numNodesToGenerate = 0;
         public long explorationStarted = 0;
+        public long globalConstraintEvaluationTime = 0;
+        public long fitnessCalculationTime = 0;
         
         public HillClimbingOnRealisticMetricStrategyForModelGeneration(
                         ReasonerWorkspace workspace,
@@ -104,6 +107,13 @@ public class HillClimbingOnRealisticMetricStrategyForModelGeneration implements
         public int getNumberOfStatecoderFail() {
                 return numberOfStatecoderFail;
         }
+        
+        public long getForwardTime() {
+                return context.getDesignSpaceManager().getForwardTime();
+        }
+        public long getBacktrackingTime() {
+                return context.getDesignSpaceManager().getBacktrackingTime();
+        }
 
         @Override
         public void initStrategy(ThreadContext context) {
@@ -147,13 +157,13 @@ public class HillClimbingOnRealisticMetricStrategyForModelGeneration implements
                 //set whether allows must violations during the realistic generation
                 allowMustViolation = configuration.allowMustViolations;
                 targetSize = configuration.typeScopes.maxNewElements + 2;
-                this.numericSolver = new NumericSolver(context, method, this.configuration.runIntermediateNumericalConsistencyChecks, false);
+                //this.numericSolver = new NumericSolver(method, this.configuration.runIntermediateNumericalConsistencyChecks, false);
         }
 
         @Override
         public void explore() {
                 this.explorationStarted=System.nanoTime();
-                if (!context.checkGlobalConstraints()) {
+                if (!checkGlobalConstraints()) {
                         logger.info("Global contraint is not satisifed in the first state. Terminate.");
                         return;
                 }
@@ -236,6 +246,14 @@ public class HillClimbingOnRealisticMetricStrategyForModelGeneration implements
                                 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);
                                 if(consistencyCheckResult == true) { continue mainLoop; }
                                 
+//                              if (context.isCurrentStateAlreadyTraversed()) {
+//                                      logger.info("The new state is already visited.");
+//                                      context.backtrack();
+//                              } else if (!checkGlobalConstraints()) {
+//                                      logger.debug("Global contraint is not satisifed.");
+//                                      context.backtrack();
+//                              } 
+                                
                                 int currentSize = model.getNewElements().size();
                                 int targetDiff = targetSize - currentSize;
                                 boolean shouldFinish = currentSize >= targetSize;
@@ -278,6 +296,20 @@ public class HillClimbingOnRealisticMetricStrategyForModelGeneration implements
                 logger.info("Interrupted.");
         }
 
+        private boolean checkGlobalConstraints() {
+                long start = System.nanoTime();
+                boolean result = context.checkGlobalConstraints();
+                globalConstraintEvaluationTime += System.nanoTime() - start;
+                return result;
+        }
+        
+        private Fitness calculateFitness() {
+                long start = System.nanoTime();
+                Fitness fitness = context.calculateFitness(); 
+                fitnessCalculationTime += System.nanoTime() - start;
+                return fitness;
+        }
+        
         /**
          *
          * @param activationIds
@@ -475,7 +507,7 @@ public class HillClimbingOnRealisticMetricStrategyForModelGeneration implements
                                 solutionStoreWithCopy.newSolution(context);
                                 solutionStoreWithDiversityDescriptor.newSolution(context);
                                 solutionStore.newSolution(context);
-                                configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
+                                configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions);
 
                                 logger.debug("Found a solution.");
                         }
@@ -484,23 +516,27 @@ public class HillClimbingOnRealisticMetricStrategyForModelGeneration implements
         
         public List<String> times = new LinkedList<String>();
         private void saveTimes() {
+                long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000;
+                long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000;
                 long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder)this.context.getStateCoder()).getStatecoderRuntime()/1000000;
                 long solutionCopy = solutionStoreWithCopy.getSumRuntime()/1000000;
                 long activationSelection = this.activationSelector.getRuntime()/1000000;
-                long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000;
-                long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000;
-                long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000;
-                long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000;
+//              long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000;
+//              long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000;
+//              long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000;
+//              long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000;
                 long metricCalculationTime = this.method.getStatistics().metricCalculationTime / 1000000;
                 this.times.add(
                         "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ 
+                        "|ForwardTime:"+forwardTime+
+                        "|Backtrackingtime:"+backtrackingTime+
                         "|StateCoderTime:"+statecoderTime+
                         "|SolutionCopyTime:"+solutionCopy+
                         "|ActivationSelectionTime:"+activationSelection+
-                        "|NumericalSolverSumTime:"+numericalSolverSumTime+
-                        "|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+
-                        "|NumericalSolverSolvingTime:"+numericalSolverSolving+
-                        "|NumericalSolverInterpretingSolution:"+numericalSolverInterpreting+
+                        //"|NumericalSolverSumTime:"+numericalSolverSumTime+
+                        //"|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+
+                        //"|NumericalSolverSolvingTime:"+numericalSolverSolving+
+                        //"|NumericalSolverInterpretingSolution:"+numericalSolverInterpreting+
                         "|MetricCalculationTime:"+metricCalculationTime + ")"
                         );
                 
@@ -544,13 +580,16 @@ public class HillClimbingOnRealisticMetricStrategyForModelGeneration implements
 //              }
 
         public void visualiseCurrentState() {
-                PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser;
+                PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser;
                 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) {
                         PartialInterpretation p = (PartialInterpretation) (context.getModel());
                         int id = ++numberOfPrintedModel;
-                        if (id % configuration.debugCongiguration.partalInterpretationVisualisationFrequency == 0) {
+                        if (id % configuration.debugConfiguration.partalInterpretationVisualisationFrequency == 0) {
                                 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p);
-                                visualisation.writeToFile(workspace, String.format("state%09d.png", id));
+                                logger.debug("Visualizing state: " + id + " (" + context.getDesignSpaceManager().getCurrentState() + ")");
+                                String name = String.format("state%09d", id);
+                                visualisation.writeToFile(workspace, name + ".png");
+                                workspace.writeModel((EObject) context.getModel(), name + ".xmi");
                         }
                 }
         }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend
new file mode 100644
index 00000000..2e039ca2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend
@@ -0,0 +1,25 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+
+import org.eclipse.viatra.dse.objectives.IGlobalConstraint
+import org.eclipse.viatra.dse.base.ThreadContext
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+
+class InconsistentScopeGlobalConstraint implements IGlobalConstraint {
+
+        override init(ThreadContext context) {
+                // Nothing to initialize.
+        }
+
+        override createNew() {
+                this
+        }
+
+        override getName() {
+                class.name
+        }
+
+        override checkGlobalConstraint(ThreadContext context) {
+                val partialModel = context.model as PartialInterpretation
+                partialModel.minNewElements <= partialModel.maxNewElements || partialModel.maxNewElements < 0
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend
new file mode 100644
index 00000000..39ef5f9a
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend
@@ -0,0 +1,24 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
+import org.apache.log4j.Logger
+import org.eclipse.viatra.dse.api.SolutionTrajectory
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+@FinalFieldsConstructor
+class LoggerSolutionFoundHandler implements ISolutionFoundHandler {
+        val ViatraReasonerConfiguration configuration
+
+        val logger = Logger.getLogger(SolutionCopier)
+
+        override solutionFound(ThreadContext context, SolutionTrajectory trajectory) {
+                configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions)
+                logger.debug("Found a solution.")
+        }
+
+        override solutionTriedToSave(ThreadContext context, SolutionTrajectory trajectory) {
+                // We are not interested in invalid solutions, ignore.
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
index a10530c7..27208cf4 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
@@ -1,67 +1,49 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

+import com.google.common.collect.ImmutableList

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

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

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

 import java.util.Comparator

 import java.util.List

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

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

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

-import org.eclipse.viatra.dse.objectives.impl.BaseObjective

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

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

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

 

-//class ViatraReasonerNumbers {

-//      public static val scopePriority = 2

-//      public static val unfinishedMultiplicityPriority = 2

-//      public static val unifinshedWFPriority = 2

-//      //public static val complexityPriority = 4

-//      

-//      public static val scopeWeigth = 1.0

-//      public static val unfinishedMultiplicityWeigth = 1.5

-//      public static val unfinishedWFWeigth = 1.5

-//      //public static val complexityWeigth = 0.1

-//      

-//      public static val useCompositeObjective = true

-//      public static val compositePriority = 2

-//}

-

-class ModelGenerationCompositeObjective implements IObjective{

-        val ScopeObjective scopeObjective

+class ModelGenerationCompositeObjective implements IThreeValuedObjective {

+        val IObjective scopeObjective

         val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives

         val UnfinishedWFObjective unfinishedWFObjective

-        var PartialInterpretation model=null;

-        val boolean punishSize

+        var PartialInterpretation model = null

         val int scopeWeight

         val int conaintmentWeight

         val int nonContainmentWeight

         val int unfinishedWFWeight

         

         new(

-                ScopeObjective scopeObjective,

+                IObjective scopeObjective,

                 List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,

                 UnfinishedWFObjective unfinishedWFObjective,

                 ViatraReasonerConfiguration configuration)

         {

-                this.scopeObjective = scopeObjective

-                this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives

-                this.unfinishedWFObjective = unfinishedWFObjective

-                

-                this.punishSize = configuration.punishSize

-                this.scopeWeight = configuration.scopeWeight

-                this.conaintmentWeight = configuration.conaintmentWeight

-                this.nonContainmentWeight = configuration.nonContainmentWeight

-                this.unfinishedWFWeight = configuration.unfinishedWFWeight

+                this(

+                        scopeObjective, unfinishedMultiplicityObjectives, unfinishedWFObjective,

+                        configuration.scopeWeight, configuration.conaintmentWeight, configuration.nonContainmentWeight,

+                        configuration.unfinishedWFWeight

+                )

         }

+

         new(

-                ScopeObjective scopeObjective,

+                IObjective scopeObjective,

                 List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,

                 UnfinishedWFObjective unfinishedWFObjective,

-                boolean punishSize, int scopeWeight, int conaintmentWeight, int nonContainmentWeight, int unfinishedWFWeight)

+                int scopeWeight, int conaintmentWeight, int nonContainmentWeight, int unfinishedWFWeight)

         {

                 this.scopeObjective = scopeObjective

                 this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives

                 this.unfinishedWFObjective = unfinishedWFObjective

                 

-                this.punishSize = punishSize

                 this.scopeWeight = scopeWeight

                 this.conaintmentWeight = conaintmentWeight

                 this.nonContainmentWeight = nonContainmentWeight

@@ -74,33 +56,34 @@ class ModelGenerationCompositeObjective implements IObjective{
                 this.unfinishedMultiplicityObjectives.forEach[it.init(context)]

                 this.unfinishedWFObjective.init(context)

         }

-        

+

         override createNew() {

                 return new ModelGenerationCompositeObjective(

-                        this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective,

-                        this.punishSize, this.scopeWeight, this.conaintmentWeight, this.nonContainmentWeight, this.unfinishedWFWeight)

+                        scopeObjective.createNew,

+                        ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew as UnfinishedMultiplicityObjective]),

+                        unfinishedWFObjective.createNew as UnfinishedWFObjective,

+                        scopeWeight, conaintmentWeight, nonContainmentWeight, unfinishedWFWeight

+                )

         }

-        

+

         override getComparator() { Comparators.LOWER_IS_BETTER }

+

         override getFitness(ThreadContext context) {

                 

                 val scopeFitnes = scopeObjective.getFitness(context)

-                //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]

                 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)

                 

                 var containmentMultiplicity = 0.0

                 var nonContainmentMultiplicity = 0.0

                 for(multiplicityObjective : unfinishedMultiplicityObjectives) {

+                        val multiplicity = multiplicityObjective.getFitness(context)

+//                      println(multiplicityObjective.name + "=" + multiplicity)

                         if(multiplicityObjective.containment) {

-                                containmentMultiplicity+=multiplicityObjective.getFitness(context)

+                                containmentMultiplicity+=multiplicity

                         } else {

-                                nonContainmentMultiplicity+=multiplicityObjective.getFitness(context)

+                                nonContainmentMultiplicity+=multiplicity

                         }

-                }

-                val size = if(punishSize) {

-                        0.9/model.newElements.size

-                } else {

-                        0

+                        

                 }

                 

                 var sum = 0.0

@@ -108,25 +91,33 @@ class ModelGenerationCompositeObjective implements IObjective{
                 sum += containmentMultiplicity*conaintmentWeight

                 sum += nonContainmentMultiplicity*nonContainmentWeight

                 sum += unfinishedWFsFitness*unfinishedWFWeight

-                sum+=size

                 

-                //println('''Sum=«sum»|Scope=«scopeFitnes»|ContainmentMultiplicity=«containmentMultiplicity»|NonContainmentMultiplicity=«nonContainmentMultiplicity»|WFs=«unfinishedWFsFitness»''')

+//              println('''scope=«scopeFitnes», containment=«containmentMultiplicity», nonContainment=«nonContainmentMultiplicity», wf=«unfinishedWFsFitness», sum=«sum»''')

                 

                 return sum

         }

         

-        override getLevel() { 2 }

-        override getName() { "CompositeUnfinishednessObjective"}

+        override getWorstPossibleFitness(ThreadContext threadContext) {

+                Double.POSITIVE_INFINITY

+        }

         

+        override getBestPossibleFitness(ThreadContext threadContext) {

+                0.0

+        }

+

+        override getLevel() { 2 }

+

+        override getName() { "CompositeUnfinishednessObjective" }

+

         override isHardObjective() { true }

-        override satisifiesHardObjective(Double fitness) { fitness < 0.95 }

-        

-        

+

+        override satisifiesHardObjective(Double fitness) { fitness < 0.01 }

+

         override setComparator(Comparator<Double> comparator) {

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

+                throw new UnsupportedOperationException("Model generation objective comparator cannot be set.")

         }

+

         override setLevel(int level) {

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

+                throw new UnsupportedOperationException("Model generation objective level cannot be set.")

         }

-        

-}
\ No newline at end of file
+}

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 0b0feb1a..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

@@ -21,7 +21,8 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint

 

 class NumericSolver {

-        val ThreadContext threadContext;

+        val ModelGenerationMethod method

+        var ThreadContext threadContext

         val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

         val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

         NumericTranslator t = new NumericTranslator

@@ -35,8 +36,16 @@ class NumericSolver {
         var int numberOfSolverCalls = 0

         var int numberOfCachedSolverCalls = 0

         

-        new(ThreadContext threadContext, ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) {

-                this.threadContext = threadContext

+        new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) {

+                this.method = method

+                this.intermediateConsistencyCheck = intermediateConsistencyCheck

+                this.caching = caching

+        }

+        

+        def init(ThreadContext context) {

+                // This makes the NumericSolver single-threaded,

+                // but that's not a problem, because we only use the solver on a single thread anyways.

+                this.threadContext = context

                 val engine = threadContext.queryEngine

                 for(entry : method.mustUnitPropagationPreconditions.entrySet) {

                         val constraint = entry.key

@@ -50,8 +59,6 @@ class NumericSolver {
                         val matcher = querySpec.getMatcher(engine);

                         constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher)

                 }

-                this.intermediateConsistencyCheck = intermediateConsistencyCheck

-                this.caching = caching

         }

         

         def getRuntime(){runtime}

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 efc2ef36..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

@@ -219,4 +220,4 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{
                 }

                 builder

         }

-}
\ No newline at end of file
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PunishSizeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PunishSizeObjective.xtend
new file mode 100644
index 00000000..bad8e4d1
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PunishSizeObjective.xtend
@@ -0,0 +1,52 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+
+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.reasoner.optimization.AbstractThreeValuedObjective
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
+import org.eclipse.viatra.dse.base.ThreadContext
+
+class PunishSizeObjective extends AbstractThreeValuedObjective {
+        static val NAME = typeof(PunishSizeObjective).name
+        
+        new(ObjectiveKind kind, int level) {
+                super(NAME, kind, ObjectiveThreshold.NO_THRESHOLD, level)
+        }
+        
+        override createNew() {
+                new PunishSizeObjective(kind, level)
+        }
+        
+        override init(ThreadContext context) {
+                // Nothing to initialize.
+        }
+        
+        override getRawFitness(ThreadContext threadContext) {
+                val model = threadContext.model
+                if (model instanceof PartialInterpretation) {
+                        val size = model.newObjectCount
+//                      println('''size=«size»''')
+                        size as double
+                } else {
+                        throw new IllegalArgumentException("notifier must be a PartialInterpretation")
+                }
+        }
+        
+        override getLowestPossibleFitness(ThreadContext threadContext) {
+                getRawFitness(threadContext)
+        }
+        
+        override getHighestPossibleFitness(ThreadContext threadContext) {
+                val model = threadContext.model
+                if (model instanceof PartialInterpretation) {
+                        (model.newObjectCount + model.maxNewElements) as double
+                } else {
+                        throw new IllegalArgumentException("notifier must be a PartialInterpretation")
+                }
+        }
+        
+        private def getNewObjectCount(PartialInterpretation interpretation) {
+                interpretation.newElements.reject[it instanceof PrimitiveElement].size
+        }
+}
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
index 69efe0d7..b61bd20b 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
@@ -23,9 +23,9 @@ class ScopeObjective implements IObjective{
         

         override getFitness(ThreadContext context) {

                 val interpretation = context.model as PartialInterpretation

-                var res = interpretation.minNewElements.doubleValue

+                var res = interpretation.minNewElementsHeuristic.doubleValue

                 for(scope : interpretation.scopes) {

-                        res += scope.minNewElements*2

+                        res += scope.minNewElementsHeuristic * 2

                 }

                 return res

         }

@@ -41,4 +41,4 @@ class ScopeObjective implements IObjective{
                 throw new UnsupportedOperationException("TODO: auto-generated method stub")

         }

         override getLevel() { 2 }

-}
\ No newline at end of file
+}
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
new file mode 100644
index 00000000..888eda18
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
@@ -0,0 +1,82 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+
+import com.google.common.collect.ImmutableList
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import java.util.LinkedHashMap
+import java.util.List
+import java.util.Map
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.emf.ecore.util.EcoreUtil
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+@FinalFieldsConstructor
+class CopiedSolution {
+        @Accessors val PartialInterpretation partialInterpretations
+        @Accessors val Map<EObject, EObject> trace
+        @Accessors val long copierRuntime
+        @Accessors var boolean current = true
+}
+
+/**
+ * Based on {@link SolutionStore.BestSolutionSaver}.
+ * 
+ * Will also automatically fill any missing numerical values in the saved solutions
+ * using the supplied {@link NumericSolver}.
+ */
+class SolutionCopier {
+        val copiedSolutions = new LinkedHashMap<Object, CopiedSolution>
+
+        @Accessors NumericSolver numericSolver
+        long startTime = System.nanoTime
+        @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0
+
+        def void copySolution(ThreadContext context, Object solutionId) {
+                val existingCopy = copiedSolutions.get(solutionId)
+                if (existingCopy === null) {
+                        val copyStart = System.nanoTime
+                        val solution = context.model as PartialInterpretation
+                        val copier = new EcoreUtil.Copier
+                        val copiedPartialInterpretation = copier.copy(solution) as PartialInterpretation
+                        copier.copyReferences
+                        totalCopierRuntime += System.nanoTime - copyStart
+                        val copierRuntime = System.nanoTime - startTime
+                        val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime)
+                        //numericSolver?.fillSolutionCopy(copiedSolution.trace)
+                        copiedSolutions.put(solutionId, copiedSolution)
+                } else {
+                        existingCopy.current = true
+                }
+        }
+
+        def void markAsObsolete(Object solutionId) {
+                val copiedSolution = copiedSolutions.get(solutionId)
+                if (copiedSolution === null) {
+                        throw new IllegalStateException("No solution to mark as obsolete for state code: " + solutionId)
+                }
+                copiedSolution.current = false
+        }
+
+        def List<PartialInterpretation> getPartialInterpretations(boolean currentOnly) {
+                getListOfCopiedSolutions(currentOnly).map[partialInterpretations]
+        }
+
+        def List<Map<EObject, EObject>> getTraces(boolean currentOnly) {
+                getListOfCopiedSolutions(currentOnly).map[trace]
+        }
+
+        def List<Long> getAllCopierRuntimes(boolean currentOnly) {
+                getListOfCopiedSolutions(currentOnly).map[copierRuntime]
+        }
+
+        def List<CopiedSolution> getListOfCopiedSolutions(boolean currentOnly) {
+                val values = copiedSolutions.values
+                val filteredSolutions = if (currentOnly) {
+                                values.filter[current]
+                        } else {
+                                values
+                        }
+                ImmutableList.copyOf(filteredSolutions)
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
index 21867a4e..4bd2c349 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
@@ -1,14 +1,12 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

-import java.util.List

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

 import java.util.LinkedList

-import org.eclipse.emf.ecore.EObject

+import java.util.List

 import java.util.Map

+import org.eclipse.emf.ecore.EObject

 import org.eclipse.emf.ecore.util.EcoreUtil

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

-import java.util.TreeMap

-import java.util.SortedMap

 

 class SolutionStoreWithCopy {

         

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend
deleted file mode 100644
index 1e7f18a8..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend
+++ /dev/null
@@ -1,120 +0,0 @@
-package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

-

-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice

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

-import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor

-import java.util.LinkedList

-import java.util.List

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

-import java.util.HashSet

-import java.util.Set

-

-enum DiversityGranularity {

-        Nodewise, Graphwise

-}

-

-class SolutionStoreWithDiversityDescriptor {

-        val DiversityDescriptor descriptor

-        DiversityGranularity granularity

-        val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice

-        val Set<Integer> solutionCodeList = new HashSet

-        

-        var long runtime

-        var int allCheck

-        var int successfulCheck

-        

-        new(DiversityDescriptor descriptor) {

-                if(descriptor.ensureDiversity) {

-                        this.descriptor = descriptor

-                        this.granularity = DiversityGranularity::Nodewise

-                } else {

-                        this.descriptor = null

-                        this.granularity = DiversityGranularity::Nodewise

-                }

-        }

-        

-        def public isActive() {

-                descriptor!==null

-        }

-        

-        def getSumRuntime() {

-                return runtime

-        }

-        def getSuccessRate() {

-                return successfulCheck as double / allCheck

-        }

-        

-        def isDifferent(ThreadContext context) {

-                if(active) {

-                        val start = System.nanoTime

-                        val model = context.model as PartialInterpretation

-                        var boolean isDifferent

-                        if(this.granularity == DiversityGranularity::Graphwise) {

-                                val code = solutionCoder.createRepresentation(model,

-                                descriptor.range,

-                                descriptor.parallels,

-                                descriptor.maxNumber,

-                                descriptor.relevantTypes,

-                                descriptor.relevantRelations).modelRepresentation.hashCode

-                        

-                                isDifferent = !solutionCodeList.contains(code)

-                        } else if(this.granularity == DiversityGranularity::Nodewise){

-                                val codes = solutionCoder.createRepresentation(model,

-                                descriptor.range,

-                                descriptor.parallels,

-                                descriptor.maxNumber,

-                                descriptor.relevantTypes,

-                                descriptor.relevantRelations).modelRepresentation.keySet.map[hashCode].toList

-                                val differentCodes = codes.filter[!solutionCodeList.contains(it)]

-                                //println(differentCodes.size)

-                                

-                                isDifferent = differentCodes.size>=1

-                        } else {

-                                throw new UnsupportedOperationException('''Unsupported diversity type: «this.granularity»''')

-                        }

-                        

-                        runtime += System.nanoTime - start

-                        allCheck++

-                        if(isDifferent) { successfulCheck++ }

-                        return isDifferent

-                } else {

-                        allCheck++

-                        successfulCheck++

-                        return true

-                }

-        }

-        

-        def canBeDifferent(ThreadContext context) {

-                return true

-        }

-        

-        def newSolution(ThreadContext context) {

-                if(active) {

-                        val start = System.nanoTime

-                        val model = context.model as PartialInterpretation

-                        if(this.granularity == DiversityGranularity::Graphwise) {

-                                val code = solutionCoder.createRepresentation(model,

-                                descriptor.range,

-                                descriptor.parallels,

-                                descriptor.maxNumber,

-                                descriptor.relevantTypes,

-                                descriptor.relevantRelations).modelRepresentation.hashCode

-                        

-                                solutionCodeList += code.hashCode

-                        } else if(this.granularity == DiversityGranularity::Nodewise){

-                                val codes = solutionCoder.createRepresentation(model,

-                                descriptor.range,

-                                descriptor.parallels,

-                                descriptor.maxNumber,

-                                descriptor.relevantTypes,

-                                descriptor.relevantRelations).modelRepresentation.keySet.map[hashCode].toList

-                                

-                                solutionCodeList += codes.map[it.hashCode]

-                        } else {

-                                throw new UnsupportedOperationException('''Unsupported diversity type: «this.granularity»''')

-                        }

-                        

-                        runtime += System.nanoTime - start

-                }

-        }

-}
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend
new file mode 100644
index 00000000..8ed3e912
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend
@@ -0,0 +1,27 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.dse.objectives.IGlobalConstraint
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+@FinalFieldsConstructor
+class SurelyViolatedObjectiveGlobalConstraint implements IGlobalConstraint {
+        val ViatraReasonerSolutionSaver solutionSaver
+
+        override init(ThreadContext context) {
+                // Nothing to initialize.
+        }
+
+        override createNew() {
+                this
+        }
+
+        override getName() {
+                class.name
+        }
+
+        override checkGlobalConstraint(ThreadContext context) {
+                val bestFitness = DseUtils.caclulateBestPossibleFitness(context)
+                bestFitness.satisifiesHardObjectives && solutionSaver.fitnessMayBeSaved(bestFitness)
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
index 2b0807d6..e1582d3b 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
@@ -1,15 +1,15 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

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

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

 import java.util.Comparator

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

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

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

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

 

 class UnfinishedMultiplicityObjective implements IObjective {

-        val MultiplicityGoalConstraintCalculator unfinishedMultiplicity;

+        val MultiplicityGoalConstraintCalculator unfinishedMultiplicity

         

-        public new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {

+        new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {

                 this.unfinishedMultiplicity = unfinishedMultiplicity

         }

         

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

         

         override setComparator(Comparator<Double> comparator) {

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

+                throw new UnsupportedOperationException

         }

         override setLevel(int level) {

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

+                throw new UnsupportedOperationException

         }

+

         def isContainment() {

                 return this.unfinishedMultiplicity.containment

         }

-}
\ No newline at end of file
+}

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
index e0111cf6..1b61ffa5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
@@ -1,56 +1,64 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

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

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

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

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

+import java.util.ArrayList

 import java.util.Collection

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

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

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

+import java.util.Comparator

 import java.util.List

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

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

-import java.util.ArrayList

-import java.util.Comparator

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

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

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

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

 

 class UnfinishedWFObjective implements IObjective {

         Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs

         val List<ViatraQueryMatcher<?>> matchers

-        

-        public new(Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) {

+

+        new(

+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) {

                 this.unfinishedWFs = unfinishedWFs

                 matchers = new ArrayList(unfinishedWFs.size)

         }

+

         override getName() '''unfinishedWFs'''

+

         override createNew() {

                 return new UnfinishedWFObjective(unfinishedWFs)

         }

+

         override init(ThreadContext context) {

-                val engine = context.queryEngine//ViatraQueryEngine.on(new EMFScope(context.model))

-                for(unfinishedWF : unfinishedWFs) {

+                val engine = context.queryEngine // ViatraQueryEngine.on(new EMFScope(context.model))

+                for (unfinishedWF : unfinishedWFs) {

                         matchers += unfinishedWF.getMatcher(engine)

                 }

         }

-        

+

         override getComparator() { Comparators.LOWER_IS_BETTER }

+

         override getFitness(ThreadContext context) {

                 var sumOfMatches = 0

-                for(matcher : matchers) {

+                for (matcher : matchers) {

                         val number = matcher.countMatches

-                        //println('''«matcher.patternName» = «number»''')

-                        sumOfMatches+=number

+//                      if (number > 0) {

+//                              println('''«matcher.patternName» = «number»''')

+//                      }

+                        sumOfMatches += number

                 }

                 return sumOfMatches.doubleValue

         }

-        

+

         override getLevel() { 2 }

+

         override isHardObjective() { true }

-        override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }

-        

+

+        override satisifiesHardObjective(Double fitness) { return fitness <= 0.01 }

+

         override setComparator(Comparator<Double> comparator) {

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

+                throw new UnsupportedOperationException()

         }

+

         override setLevel(int level) {

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

+                throw new UnsupportedOperationException()

         }

-}
\ No newline at end of file
+}

diff --git a/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
new file mode 100644
index 00000000..e00f76ff
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
@@ -0,0 +1,250 @@
+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
+import org.eclipse.viatra.dse.api.Solution
+import org.eclipse.viatra.dse.api.SolutionTrajectory
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.dse.objectives.Fitness
+import org.eclipse.viatra.dse.objectives.IObjective
+import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper
+import org.eclipse.viatra.dse.solutionstore.SolutionStore.ISolutionSaver
+import org.eclipse.xtend.lib.annotations.Accessors
+
+/**
+ * Based on {@link SolutionStore.BestSolutionSaver}.
+ * 
+ * Will also automatically fill any missing numerical values in the saved solutions
+ * using the supplied {@link NumericSolver}.
+ */
+class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsProvider {
+        static val TOLERANCE = 1e-10
+
+        @Accessors val SolutionCopier solutionCopier
+        @Accessors val DiversityChecker diversityChecker
+        val IObjective[][] leveledExtremalObjectives
+        val boolean hasExtremalObjectives
+        val int numberOfRequiredSolutions
+        val ObjectiveComparatorHelper comparatorHelper
+        val Map<SolutionTrajectory, Fitness> trajectories = new HashMap
+
+        @Accessors var NumericSolver numericSolver
+        @Accessors var Map<Object, Solution> solutionsCollection
+
+        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
+        }
+        
+        def setNumericSolver(NumericSolver numericSolver) {
+                this.numericSolver = numericSolver
+                solutionCopier.numericSolver = numericSolver
+        }
+
+        override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
+                if (hasExtremalObjectives) {
+                        saveBestSolutionOnly(context, id, solutionTrajectory)
+                } else {
+                        saveAnyDiverseSolution(context, id, solutionTrajectory)
+                }
+        }
+
+        private def saveBestSolutionOnly(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
+                val fitness = context.lastFitness
+                if (!shouldSaveSolution(fitness, context)) {
+                        return false
+                }
+                println("Found: " + fitness)
+                val dominatedTrajectories = newArrayList
+                for (entry : trajectories.entrySet) {
+                        val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value)
+                        if (isLastFitnessBetter < 0) {
+                                // Found a trajectory that dominates the current one, no need to save
+                                return false
+                        }
+                        if (isLastFitnessBetter > 0) {
+                                dominatedTrajectories += entry.key
+                        }
+                }
+                if (dominatedTrajectories.size == 0 && !needsMoreSolutionsWithSameFitness) {
+                        return false
+                }
+                if (!diversityChecker.newSolution(context, id, dominatedTrajectories.map[solution.stateCode])) {
+                        return false
+                }
+                // We must save the new trajectory before removing dominated trajectories
+                // to avoid removing the current solution when it is reachable only via dominated trajectories.
+                val solutionSaved = basicSaveSolution(context, id, solutionTrajectory, fitness)
+                for (dominatedTrajectory : dominatedTrajectories) {
+                        trajectories -= dominatedTrajectory
+                        val dominatedSolution = dominatedTrajectory.solution
+                        if (!dominatedSolution.trajectories.remove(dominatedTrajectory)) {
+                                throw new DSEException(
+                                        "Dominated solution is not reachable from dominated trajectory. This should never happen!")
+                        }
+                        if (dominatedSolution.trajectories.empty) {
+                                val dominatedSolutionId = dominatedSolution.stateCode
+                                solutionCopier.markAsObsolete(dominatedSolutionId)
+                                solutionsCollection -= dominatedSolutionId
+                        }
+                }
+                solutionSaved
+        }
+
+        private def saveAnyDiverseSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
+                val fitness = context.lastFitness
+                if (!shouldSaveSolution(fitness, context)) {
+                        return false
+                }
+                if (!diversityChecker.newSolution(context, id, emptyList)) {
+                        return false
+                }
+                basicSaveSolution(context, id, solutionTrajectory, fitness)
+        }
+
+        private def shouldSaveSolution(Fitness fitness, ThreadContext context) {
+                fitness.satisifiesHardObjectives && (numericSolver === null || numericSolver.currentSatisfiable)
+        }
+
+        private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory,
+                Fitness fitness) {
+                var boolean solutionSaved = false
+                var dseSolution = solutionsCollection.get(id)
+                if (dseSolution === null) {
+                        solutionCopier.copySolution(context, id)
+                        dseSolution = new Solution(id, solutionTrajectory)
+                        solutionsCollection.put(id, dseSolution)
+                        solutionSaved = true
+                } else {
+                        solutionSaved = dseSolution.trajectories.add(solutionTrajectory)
+                }
+                if (solutionSaved) {
+                        solutionTrajectory.solution = dseSolution
+                        trajectories.put(solutionTrajectory, fitness)
+                }
+                solutionSaved
+        }
+
+        def fitnessMayBeSaved(Fitness fitness) {
+                if (!hasExtremalObjectives) {
+                        return true
+                }
+                var boolean mayDominate
+                for (existingFitness : trajectories.values) {
+                        val isNewFitnessBetter = comparatorHelper.compare(fitness, existingFitness)
+                        if (isNewFitnessBetter < 0) {
+                                return false
+                        }
+                        if (isNewFitnessBetter > 0) {
+                                mayDominate = true
+                        }
+                }
+                mayDominate || needsMoreSolutionsWithSameFitness
+        }
+
+        private def boolean needsMoreSolutionsWithSameFitness() {
+                if (solutionsCollection === null) {
+                        // The solutions collection will only be initialized upon saving the first solution.
+                        return true
+                }
+                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/dse/WF2ObjectiveConverter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
index 5a528a9e..6d772f32 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
@@ -1,5 +1,6 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

+import com.google.common.collect.ImmutableList

 import java.util.ArrayList

 import java.util.Collection

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

@@ -12,25 +13,33 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification
 import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher

 

 class WF2ObjectiveConverter {

-        

+        static val INVALIDATED_WFS_NAME = "invalidatedWFs"

+

         def createCompletenessObjective(

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

-        {

-                val res = new ConstraintsObjective('''unfinishedWFs''',

-                        unfinishedWF.map[

-                                new QueryConstraint(it.fullyQualifiedName,it,2.0)

-                        ].toList

+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) {

+                new UnfinishedWFObjective(unfinishedWF)

+        }

+

+        def createInvalidationObjective(

+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {

+                createConstraintObjective(INVALIDATED_WFS_NAME, invalidatedByWF)

+        }

+

+        def IGlobalConstraint createInvalidationGlobalConstraint(

+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {

+                new ModelQueriesGlobalConstraint(INVALIDATED_WFS_NAME, new ArrayList(invalidatedByWF))

+        }

+

+        private def createConstraintObjective(String name,

+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries) {

+                val res = new ConstraintsObjective(

+                        name,

+                        ImmutableList.copyOf(queries.map [

+                                new QueryConstraint(it.fullyQualifiedName, it, 1.0)

+                        ])

                 )

                 res.withComparator(Comparators.LOWER_IS_BETTER)

                 res.level = 2

-                return res

-        }

-        

-        def IGlobalConstraint createInvalidationObjective(

-                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF)

-        {

-                return new ModelQueriesGlobalConstraint('''invalidatedWFs''',

-                        new ArrayList(invalidatedByWF)

-                )

+                res

         }

-}
\ No newline at end of file
+}

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend
new file mode 100644
index 00000000..cd911ab5
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend
@@ -0,0 +1,35 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import org.eclipse.viatra.dse.base.ThreadContext
+
+abstract class AbstractThreeValuedObjective extends DirectionalThresholdObjective implements IThreeValuedObjective {
+        protected new(String name, ObjectiveKind kind, ObjectiveThreshold threshold, int level) {
+                super(name, kind, threshold, level)
+        }
+
+        abstract def double getLowestPossibleFitness(ThreadContext threadContext)
+
+        abstract def double getHighestPossibleFitness(ThreadContext threadContext)
+
+        override getWorstPossibleFitness(ThreadContext threadContext) {
+                switch (kind) {
+                        case LOWER_IS_BETTER:
+                                getHighestPossibleFitness(threadContext)
+                        case HIGHER_IS_BETTER:
+                                getLowestPossibleFitness(threadContext)
+                        default:
+                                throw new IllegalStateException("Unknown three valued objective kind: " + kind)
+                }
+        }
+
+        override getBestPossibleFitness(ThreadContext threadContext) {
+                switch (kind) {
+                        case LOWER_IS_BETTER:
+                                getLowestPossibleFitness(threadContext)
+                        case HIGHER_IS_BETTER:
+                                getHighestPossibleFitness(threadContext)
+                        default:
+                                throw new IllegalStateException("Unknown three valued 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/CompositeDirectionalThresholdObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CompositeDirectionalThresholdObjective.xtend
new file mode 100644
index 00000000..0aa442f5
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CompositeDirectionalThresholdObjective.xtend
@@ -0,0 +1,62 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import com.google.common.collect.ImmutableList
+import java.util.Collection
+import org.eclipse.viatra.dse.base.ThreadContext
+
+class CompositeDirectionalThresholdObjective extends DirectionalThresholdObjective {
+        val Collection<DirectionalThresholdObjective> objectives
+
+        new(String name, Collection<DirectionalThresholdObjective> objectives) {
+                this(name, objectives, getKind(objectives), getThreshold(objectives), getLevel(objectives))
+        }
+
+        new(String name, DirectionalThresholdObjective... objectives) {
+                this(name, objectives as Collection<DirectionalThresholdObjective>)
+        }
+
+        protected new(String name, Iterable<DirectionalThresholdObjective> objectives, ObjectiveKind kind,
+                ObjectiveThreshold threshold, int level) {
+                super(name, kind, threshold, level)
+                this.objectives = ImmutableList.copyOf(objectives)
+        }
+
+        override createNew() {
+                new CompositeDirectionalThresholdObjective(name, objectives.map[createNew as DirectionalThresholdObjective],
+                        kind, threshold, level)
+        }
+
+        override init(ThreadContext context) {
+                for (objective : objectives) {
+                        objective.init(context)
+                }
+        }
+
+        override protected getRawFitness(ThreadContext context) {
+                var double fitness = 0
+                for (objective : objectives) {
+                        fitness += objective.getFitness(context)
+                }
+                fitness
+        }
+
+        private static def getKind(Collection<DirectionalThresholdObjective> objectives) {
+                val kinds = objectives.map[kind].toSet
+                if (kinds.size != 1) {
+                        throw new IllegalArgumentException("Passed objectives must have the same kind")
+                }
+                kinds.head
+        }
+
+        private static def getThreshold(Collection<DirectionalThresholdObjective> objectives) {
+                objectives.map[threshold].reduce[a, b|a.merge(b)]
+        }
+
+        private static def int getLevel(Collection<DirectionalThresholdObjective> objectives) {
+                val levels = objectives.map[level].toSet
+                if (levels.size != 1) {
+                        throw new IllegalArgumentException("Passed objectives must have the same level")
+                }
+                levels.head
+        }
+}
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/DirectionalThresholdObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/DirectionalThresholdObjective.xtend
new file mode 100644
index 00000000..376e3d1a
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/DirectionalThresholdObjective.xtend
@@ -0,0 +1,164 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import java.util.Comparator
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.dse.objectives.IObjective
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+abstract class ObjectiveThreshold {
+        public static val NO_THRESHOLD = new ObjectiveThreshold {
+                override isHard() {
+                        false
+                }
+
+                override satisfiesThreshold(double cost, Comparator<Double> comparator) {
+                        true
+                }
+
+                override protected postProcessSatisfactoryCost(double cost, ObjectiveKind kind) {
+                        cost
+                }
+
+                override ObjectiveThreshold merge(ObjectiveThreshold other) {
+                        if (other == NO_THRESHOLD) {
+                                NO_THRESHOLD
+                        } else {
+                                throw new IllegalArgumentException("Merged thresholds must have the same type")
+                        }
+                }
+        }
+
+        private new() {
+        }
+
+        def boolean isHard() {
+                true
+        }
+
+        def boolean satisfiesThreshold(double cost, ObjectiveKind kind) {
+                satisfiesThreshold(cost, kind.comparator)
+        }
+
+        def boolean satisfiesThreshold(double cost, Comparator<Double> comparator)
+
+        def double postProcessCost(double cost, ObjectiveKind kind) {
+                if (satisfiesThreshold(cost, kind)) {
+                        postProcessSatisfactoryCost(cost, kind)
+                } else {
+                        cost
+                }
+        }
+
+        protected def double postProcessSatisfactoryCost(double cost, ObjectiveKind kind)
+
+        def ObjectiveThreshold merge(ObjectiveThreshold other)
+
+        @Data
+        static class Exclusive extends ObjectiveThreshold {
+                static val EPSILON = 0.1
+
+                val double threshold
+                val boolean clampToThreshold
+
+                @FinalFieldsConstructor
+                new() {
+                }
+
+                new(double threshold) {
+                        this(threshold, true)
+                }
+
+                override satisfiesThreshold(double cost, Comparator<Double> comparator) {
+                        comparator.compare(threshold, cost) < 0
+                }
+
+                override protected postProcessSatisfactoryCost(double cost, ObjectiveKind kind) {
+                        if (clampToThreshold) {
+                                threshold + Math.signum(kind.satisfiedValue) * EPSILON
+                        } else {
+                                cost
+                        }
+                }
+
+                override ObjectiveThreshold merge(ObjectiveThreshold other) {
+                        if (other instanceof Exclusive) {
+                                new Exclusive(threshold + other.threshold)
+                        } else {
+                                throw new IllegalArgumentException("Merged thresholds must have the same type")
+                        }
+                }
+        }
+
+        @Data
+        static class Inclusive extends ObjectiveThreshold {
+                val double threshold
+                val boolean clampToThreshold
+
+                @FinalFieldsConstructor
+                new() {
+                }
+
+                new(double threshold) {
+                        this(threshold, true)
+                }
+
+                override satisfiesThreshold(double cost, Comparator<Double> comparator) {
+                        comparator.compare(threshold, cost) <= 0
+                }
+
+                override protected postProcessSatisfactoryCost(double cost, ObjectiveKind kind) {
+                        if (clampToThreshold) {
+                                threshold
+                        } else {
+                                cost
+                        }
+                }
+                
+                override ObjectiveThreshold merge(ObjectiveThreshold other) {
+                        if (other instanceof Inclusive) {
+                                new Inclusive(threshold + other.threshold)
+                        } else {
+                                throw new IllegalArgumentException("Merged thresholds must have the same type")
+                        }
+                }
+        }
+}
+
+abstract class DirectionalThresholdObjective implements IObjective {
+        @Accessors val String name
+        @Accessors ObjectiveKind kind
+        @Accessors ObjectiveThreshold threshold
+        @Accessors int level
+
+        protected new(String name, ObjectiveKind kind, ObjectiveThreshold threshold, int level) {
+                this.name = name
+                this.kind = kind
+                this.threshold = threshold
+                this.level = level
+        }
+
+        override isHardObjective() {
+                threshold.hard
+        }
+
+        override satisifiesHardObjective(Double fitness) {
+                threshold.satisfiesThreshold(fitness, comparator)
+        }
+
+        override getComparator() {
+                kind.comparator
+        }
+
+        override setComparator(Comparator<Double> comparator) {
+                kind = ObjectiveKind.fromComparator(comparator)
+        }
+
+        override getFitness(ThreadContext context) {
+                val fitness = getRawFitness(context)
+                threshold.postProcessCost(fitness, kind)
+        }
+
+        protected def double getRawFitness(ThreadContext context)
+}
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/IThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend
new file mode 100644
index 00000000..4a870a3e
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend
@@ -0,0 +1,10 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.dse.objectives.IObjective
+
+interface IThreeValuedObjective extends IObjective {
+        def Double getWorstPossibleFitness(ThreadContext threadContext)
+        
+        def Double getBestPossibleFitness(ThreadContext threadContext)
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/MatchCostObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/MatchCostObjective.xtend
new file mode 100644
index 00000000..a0c6a2c1
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/MatchCostObjective.xtend
@@ -0,0 +1,52 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import com.google.common.collect.ImmutableList
+import java.util.Collection
+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
+
+@Data
+class MatchCostElement {
+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> querySpecification
+        val double weight
+}
+
+class MatchCostObjective extends DirectionalThresholdObjective {
+        val Collection<MatchCostElement> costElements
+        Collection<CostElementMatcher> matchers
+
+        new(String name, Collection<MatchCostElement> costElements, ObjectiveKind kind, ObjectiveThreshold threshold,
+                int level) {
+                super(name, kind, threshold, level)
+                this.costElements = costElements
+        }
+
+        override createNew() {
+                new MatchCostObjective(name, costElements, kind, threshold, level)
+        }
+
+        override init(ThreadContext context) {
+                val queryEngine = context.queryEngine
+                matchers = ImmutableList.copyOf(costElements.map [
+                        val matcher = querySpecification.getMatcher(queryEngine)
+                        new CostElementMatcher(matcher, weight)
+                ])
+        }
+
+        override protected getRawFitness(ThreadContext context) {
+                var double cost = 0
+                for (it : matchers) {
+                        cost += weight * matcher.countMatches
+                }
+                cost
+        }
+
+        @Data
+        private static class CostElementMatcher {
+                val ViatraQueryMatcher<? extends IPatternMatch> matcher
+                val double weight
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java
new file mode 100644
index 00000000..cbbaaafd
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java
@@ -0,0 +1,60 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization;
+
+import java.util.Comparator;
+
+import org.eclipse.viatra.dse.objectives.Comparators;
+
+public enum ObjectiveKind {
+        LOWER_IS_BETTER {
+
+                @Override
+                public Comparator<Double> getComparator() {
+                        return Comparators.LOWER_IS_BETTER;
+                }
+
+                @Override
+                public double getInvalidValue() {
+                        return Double.POSITIVE_INFINITY;
+                }
+
+                @Override
+                public double getSatisfiedValue() {
+                        return Double.NEGATIVE_INFINITY;
+                }
+
+        },
+        HIGHER_IS_BETTER {
+
+                @Override
+                public Comparator<Double> getComparator() {
+                        return Comparators.HIGHER_IS_BETTER;
+                }
+
+                @Override
+                public double getInvalidValue() {
+                        return Double.NEGATIVE_INFINITY;
+                }
+
+                @Override
+                public double getSatisfiedValue() {
+                        return Double.POSITIVE_INFINITY;
+                }
+
+        };
+
+        public abstract Comparator<Double> getComparator();
+
+        public abstract double getInvalidValue();
+
+        public abstract double getSatisfiedValue();
+
+        public static ObjectiveKind fromComparator(Comparator<Double> comparator) {
+                if (Comparators.LOWER_IS_BETTER.equals(comparator)) {
+                        return ObjectiveKind.LOWER_IS_BETTER;
+                } else if (Comparators.HIGHER_IS_BETTER.equals(comparator)) {
+                        return ObjectiveKind.HIGHER_IS_BETTER;
+                } else {
+                        throw new IllegalStateException("Only LOWER_IS_BETTER and HIGHER_IS_BETTER comparators are supported.");
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/QueryBasedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/QueryBasedObjective.xtend
new file mode 100644
index 00000000..d355f5be
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/QueryBasedObjective.xtend
@@ -0,0 +1,48 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+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
+
+class QueryBasedObjective extends DirectionalThresholdObjective {
+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> querySpecification
+        ViatraQueryMatcher<? extends IPatternMatch> matcher
+
+        new(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> querySpecification,
+                ObjectiveKind kind, ObjectiveThreshold threshold, int level) {
+                super(querySpecification.simpleName + " objective", kind, threshold, level)
+                if (querySpecification.parameters.size != 1) {
+                        throw new IllegalArgumentException("Objective query must have a single parameter")
+                }
+                this.querySpecification = querySpecification
+        }
+
+        override createNew() {
+                new QueryBasedObjective(querySpecification, kind, threshold, level)
+        }
+
+        override init(ThreadContext context) {
+                matcher = querySpecification.getMatcher(context.queryEngine)
+        }
+
+        override protected getRawFitness(ThreadContext context) {
+                val iterator = matcher.allMatches.iterator
+                if (!iterator.hasNext) {
+                        return invalidValue
+                }
+                val value = iterator.next.get(0)
+                if (iterator.hasNext) {
+                        throw new IllegalStateException("Multiple matches for objective query")
+                }
+                if (value instanceof Number) {
+                        value.doubleValue
+                } else {
+                        throw new IllegalStateException("Objective value is not an instance of Number")
+                }
+        }
+
+        private def getInvalidValue() {
+                kind.invalidValue
+        }
+}
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
new file mode 100644
index 00000000..9b1a7e9f
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend
@@ -0,0 +1,80 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener
+import java.util.Map
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.xtend.lib.annotations.Accessors
+
+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, Map<String, CostElementMatchers> matchers, ObjectiveKind kind, ObjectiveThreshold threshold,
+                int level) {
+                super(name, kind, threshold, level)
+                this.matchers = matchers
+        }
+
+        override createNew() {
+                // new ThreeValuedCostObjective(name, matchers, kind, threshold, level)
+                throw new UnsupportedOperationException("ThreeValuedCostObjective can only be used from a single thread")
+        }
+
+        override init(ThreadContext context) {
+        }
+
+        override getRawFitness(ThreadContext context) {
+                var double cost = 0
+                for (matcher : matchers.values) {
+                        cost += matcher.weight * matcher.currentNumberOfMatches
+                }
+                cost
+        }
+
+        override getLowestPossibleFitness(ThreadContext threadContext) {
+                var double cost = 0
+                for (matcher : matchers.values) {
+                        if (matcher.weight >= 0) {
+                                cost += matcher.weight * matcher.minimumNumberOfMatches
+                        } else {
+                                cost += matcher.weight * matcher.maximumNumberOfMatches
+                        }
+                }
+                val boundWithHint = Math.max(lowerBoundHint, cost)
+                if (boundWithHint > upperBoundHint) {
+                        throw new IllegalStateException("Inconsistent cost bounds")
+                }
+                boundWithHint
+        }
+
+        override getHighestPossibleFitness(ThreadContext threadContext) {
+                var double cost = 0
+                for (matcher : matchers.values) {
+                        if (matcher.weight <= 0) {
+                                cost += matcher.weight * matcher.minimumNumberOfMatches
+                        } else {
+                                cost += matcher.weight * matcher.maximumNumberOfMatches
+                        }
+                }
+                val boundWithHint = Math.min(upperBoundHint, cost)
+                if (boundWithHint < lowerBoundHint) {
+                        throw new IllegalStateException("Inconsistent cost bounds")
+                }
+                boundWithHint
+        }
+
+        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
+                }
+        }
+}