28 files changed, 1527 insertions, 415 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
index 2a271acf..4ad61ccb 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
@@ -3,7 +3,8 @@ Bundle-ManifestVersion: 2
 Bundle-Name: Reasoner
 Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
 Bundle-Version: 1.0.0.qualifier
-Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
+Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner,
+ hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
 Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
 hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
 hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0",
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index 6639e5f3..aa02cd30 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -1,5 +1,7 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
+import com.google.common.collect.ImmutableList
+import com.google.common.collect.Lists
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
@@ -10,19 +12,28 @@ 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.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.BestFirstStrategyForModelGeneration
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler
 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective
 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation
 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.ViatraReasonerSolutionSaver
 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
 import java.util.List
 import java.util.Map
@@ -31,185 +42,263 @@ 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
-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,
-        override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
+                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 ||
-                val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output
+                        viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {
-                if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {
+                        workspace.writeModel(emptySolution, "init.partialmodel")
-                        workspace.writeModel(emptySolution,"init.partialmodel")
+                }
-                } 
                emptySolution.problemConainer = problem
-                
+                var BasicScopeGlobalConstraint basicScopeGlobalConstraint = null
-                val ScopePropagator scopePropagator = new ScopePropagator(emptySolution)
+                if (viatraConfig.scopePropagatorStrategy == ScopePropagatorStrategy.None) {
-                scopePropagator.propagateAllScopeConstraints            
+                        basicScopeGlobalConstraint = new BasicScopeGlobalConstraint(emptySolution)
-                
+                        emptySolution.scopes.clear
+                }
                val method = modelGenerationMethodProvider.createModelGenerationMethod(
                        problem,
                        emptySolution,
                        workspace,
                        viatraConfig.nameNewElements,
                        viatraConfig.typeInferenceMethod,
-                        scopePropagator,
+                        viatraConfig.scopePropagatorStrategy,
+                        viatraConfig.hints,
                        viatraConfig.documentationLevel
                )
-                
                dse.addObjective(new ModelGenerationCompositeObjective(
-                        new ScopeObjective,
+                        basicScopeGlobalConstraint ?: new ScopeObjective,
                        method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)],
-                        new UnfinishedWFObjective(method.unfinishedWF)
+                        wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF)
                ))
-                dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF))
+                val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size)
-                for(additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) {
+                for (entry : viatraConfig.costObjectives.indexed) {
+                        val objectiveName = '''costObjective«entry.key»'''
+                        val objectiveConfig = entry.value
+                        val elementsBuilder = ImmutableList.builder
+                        for (elementConfig : objectiveConfig.elements) {
+                                val relationName = elementConfig.patternQualifiedName
+                                val modalQueries = method.modalRelationQueries.get(relationName)
+                                if (modalQueries === null) {
+                                        throw new IllegalArgumentException("Unknown relation: " + relationName)
+                                }
+                                elementsBuilder.add(new ThreeValuedCostElement(
+                                        modalQueries.currentQuery,
+                                        modalQueries.mayQuery,
+                                        modalQueries.mustQuery,
+                                        elementConfig.weight
+                                ))
+                        }
+                        val costElements = elementsBuilder.build
+                        val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind,
+                                objectiveConfig.threshold, 3)
+                        dse.addObjective(costObjective)
+                        if (objectiveConfig.findExtremum) {
+                                extremalObjectives += costObjective
+                        }
+                }
+                val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions
+                val solutionStore = if (extremalObjectives.empty) {
+                                new SolutionStore(numberOfRequiredSolutions)
+                        } else {
+                                new SolutionStore()
+                        }
+                solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))
+                val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement)
+                val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions,
+                        diversityChecker)
+                val solutionCopier = solutionSaver.solutionCopier
+                solutionStore.withSolutionSaver(solutionSaver)
+                dse.solutionStore = solutionStore
+                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)
+                dse.setInitialModel(emptySolution, false)
-                
-                val IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) {
+                val IStateCoderFactory statecoder = switch (viatraConfig.stateCoderStrategy) {
-                        new NeighbourhoodBasedStateCoderFactory
+                        case Neighbourhood:
-                } else {
+                                new NeighbourhoodBasedHashStateCoderFactory
-                        new IdentifierBasedStateCoderFactory
+                        case PairwiseNeighbourhood:
+                                new PairwiseNeighbourhoodBasedStateCoderFactory
+                        default:
+                                new IdentifierBasedStateCoderFactory
                }
                dse.stateCoderFactory = statecoder
-                
                dse.maxNumberOfThreads = 1
-                
-                val solutionStore =  new SolutionStore(configuration.solutionScope.numberOfRequiredSolution)
+                for (rule : method.relationRefinementRules) {
-                dse.solutionStore = solutionStore
-                
-                for(rule : method.relationRefinementRules) {
                        dse.addTransformationRule(rule)
                }
-                for(rule : method.objectRefinementRules) {
+                for (rule : method.objectRefinementRules) {
                        dse.addTransformationRule(rule)
                }
-                
-                val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method)
+                val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method)
                viatraConfig.progressMonitor.workedForwardTransformation
-                
                val transformationTime = System.nanoTime - transformationStartTime
                val solverStartTime = System.nanoTime
-                
                var boolean stoppedByTimeout
-                var boolean stoppedByException
+                try {
-                try{
+                        stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000);
-                        stoppedByTimeout = dse.startExplorationWithTimeout(strategy,configuration.runtimeLimit*1000);
-                        stoppedByException = false
                } 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 = viatraConfig.runtimeLimit
-                        it.solverTime = (solverTime/1000000) as int
+                        it.solverTime = (solverTime / 1000000) as int
-                        it.transformationTime = (transformationTime/1000000) as int
+                        it.transformationTime = (transformationTime / 1000000) as int
-                        for(x : 0..<strategy.solutionStoreWithCopy.allRuntimes.size) {
+                        for (pair : solutionCopier.getAllCopierRuntimes(true).indexed) {
                                it.entries += createIntStatisticEntry => [
-                                        it.name = '''_Solution«x»FoundAt'''
+                                        it.name = '''_Solution«pair.key»FoundAt'''
-                                        it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int
+                                        it.value = (pair.value / 1000000) as int
                                ]
                        }
                        it.entries += createIntStatisticEntry => [
-                                it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int
+                                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 = "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 = "TypeAnalysisTime" it.value = (method.statistics.PreliminaryTypeAnalisisTime/1000000) as int
+                                it.name = "StateCoderFailCount"
+                                it.value = strategy.numberOfStatecoderFail
                        ]
                        it.entries += createIntStatisticEntry => [
-                                it.name = "StateCoderTime" it.value = (statecoder.runtime/1000000) as int
+                                it.name = "SolutionCopyTime"
+                                it.value = (solutionCopier.getTotalCopierRuntime / 1000000) as int
                        ]
                        it.entries += createIntStatisticEntry => [
-                                it.name = "StateCoderFailCount" it.value = strategy.numberOfStatecoderFail
+                                it.name = "States"
+                                it.value = dse.numberOfStates as int
                        ]
                        it.entries += createIntStatisticEntry => [
-                                it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int
+                                it.name = "Decisions"
+                                it.value = method.statistics.decisionsTried
                        ]
-                        if(strategy.solutionStoreWithDiversityDescriptor.isActive) {
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "Transformations"
+                                it.value = method.statistics.transformationInvocations
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "ScopePropagations"
+                                it.value = method.statistics.scopePropagatorInvocations
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "ScopePropagationsSolverCalls"
+                                it.value = method.statistics.scopePropagatorSolverInvocations
+                        ]
+                        if (diversityChecker.isActive) {
                                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) {
+                if (stoppedByTimeout) {
-                        return createInsuficientResourcesResult=>[
+                        return createInsuficientResourcesResult => [
                                it.problem = problem
-                                it.resourceName="time"
+                                it.resourceName = "time"
-                                it.representation += strategy.solutionStoreWithCopy.solutions
+                                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.trace = solutionCopier.getTraces(true)
-                                        it.representation += strategy.solutionStoreWithCopy.solutions
+                                        it.representation += solutionCopier.getPartialInterpretations(true)
                                        it.statistics = statistics
                                ]
                        }
                }
        }
-    private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) {
+        private def dispatch long runtime(AbstractNeighbourhoodBasedStateCoderFactory sc) {
-        sc.sumStatecoderRuntime
+                sc.sumStatecoderRuntime
-    }
+        }
-    private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) {
+        private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) {
-        sc.sumStatecoderRuntime
+                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 c4d7e231..6f38d261 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
@@ -6,19 +6,28 @@ 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.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.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
 import java.util.LinkedList
 import java.util.List
 import java.util.Set
 import org.eclipse.xtext.xbase.lib.Functions.Function1
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
-public enum StateCoderStrategy {
+enum StateCoderStrategy {
-        Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity
+        Neighbourhood,
+        PairwiseNeighbourhood,
+        NeighbourhoodWithEquivalence,
+        IDBased,
+        DefinedByDiversity
 }
-class ViatraReasonerConfiguration extends LogicSolverConfiguration{
+class ViatraReasonerConfiguration extends LogicSolverConfiguration {
-        //public var Iterable<PQuery> existingQueries
+        // public var Iterable<PQuery> existingQueries
-        
        public var nameNewElements = false
        public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood
        public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
@@ -26,7 +35,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,14 +49,21 @@ 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.
         */
-         public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint
+        public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint
+        public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(
+                PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)
+        
+        public var List<LinearTypeConstraintHint> hints = newArrayList
+        public var List<CostObjectiveConfiguration> costObjectives = newArrayList
 }
-public class DiversityDescriptor {
+class DiversityDescriptor {
        public var ensureDiversity = false
        public static val FixPointRange = -1
        public var int range = FixPointRange
@@ -57,20 +73,31 @@ public class DiversityDescriptor {
        public var Set<RelationDeclaration> relevantRelations = null
 }
-public class DebugConfiguration {
+class DebugConfiguration {
-        public var logging = false
+        public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null
-        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
-}
-\ 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
+}
+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 60f46033..081e48fa 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
@@ -21,6 +21,7 @@ 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.strategy.interfaces.IStrategy;
 import org.eclipse.viatra.dse.base.ThreadContext;
@@ -75,8 +76,6 @@ 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();
@@ -95,14 +94,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                this.workspace = workspace;
                this.configuration = configuration;
                this.method = method;
+                //logger.setLevel(Level.DEBUG);
        }
        
-        public SolutionStoreWithCopy getSolutionStoreWithCopy() {
-                return solutionStoreWithCopy;
-        }
-        public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
-                return solutionStoreWithDiversityDescriptor;
-        }
        public int getNumberOfStatecoderFail() {
                return numberOfStatecoderFail;
        }
@@ -121,9 +115,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                        matchers.add(matcher);
                }
                
-                this.solutionStoreWithCopy = new SolutionStoreWithCopy();
-                this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
                final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
                this.comparator = new Comparator<TrajectoryWithFitness>() {
                        @Override
@@ -146,13 +137,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                        return;
                }
                
-                final Fitness firstFittness = context.calculateFitness();
+                final Fitness firstfitness = context.calculateFitness();
-                checkForSolution(firstFittness);
+                solutionStore.newSolution(context);
                
                final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
                final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
-                TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness);
+                TrajectoryWithFitness currentTrajectoryWithfitness = new TrajectoryWithFitness(firstTrajectory, firstfitness);
-                trajectoiresToExplore.add(currentTrajectoryWithFittness);
+                trajectoiresToExplore.add(currentTrajectoryWithfitness);
                
                //if(configuration)
                visualiseCurrentState();
@@ -167,22 +158,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;
 //                      }
@@ -194,10 +185,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                                final Object nextActivation = iterator.next();
 //                              if (!iterator.hasNext()) {
 //                                      logger.debug("Last untraversed activation of the state.");
-//                                      trajectoiresToExplore.remove(currentTrajectoryWithFittness);
+//                                      trajectoiresToExplore.remove(currentTrajectoryWithfitness);
 //                              }
                                logger.debug("Executing new activation: " + nextActivation);
                                context.executeAcitvationId(nextActivation);
+                                method.getStatistics().incrementDecisionCount();
                                visualiseCurrentState();
 //                              for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
@@ -209,7 +201,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
 //                                      System.out.println("---------");
 //                              }
                                
-                                boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);
+                                boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
                                if(consistencyCheckResult == true) { continue mainLoop; }
                                if (context.isCurrentStateAlreadyTraversed()) {
@@ -220,38 +212,38 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                                        context.backtrack();
                                } else {
                                        final Fitness nextFitness = context.calculateFitness();
-                                        checkForSolution(nextFitness);
+                                        solutionStore.newSolution(context);
                                        if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) {
                                                logger.debug("Reached max depth.");
                                                context.backtrack();
                                                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,
+                                        int compare = objectiveComparatorHelper.compare(currentTrajectoryWithfitness.fitness,
-                                                        nextTrajectoryWithFittness.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);
+                        trajectoiresToExplore.remove(currentTrajectoryWithfitness);
-                        currentTrajectoryWithFittness = null;
+                        currentTrajectoryWithfitness = null;
                }
                logger.info("Interrupted.");
@@ -263,25 +255,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                        activationIds = new ArrayList<Object>(context.getUntraversedActivationIds());
                        Collections.shuffle(activationIds);
                } 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)) {
-                                solutionStoreWithCopy.newSolution(context);
-                                solutionStoreWithDiversityDescriptor.newSolution(context);
-                                solutionStore.newSolution(context);
-                                configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
-                                logger.debug("Found a solution.");
-                        }
-                }
-        }
        @Override
        public void interruptStrategy() {
                isInterrupted = true;
@@ -311,13 +291,16 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
        }       
        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/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 2489c751..2976bebe 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,11 +1,13 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import com.google.common.collect.ImmutableList
+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 org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
 //class ViatraReasonerNumbers {
 //      public static val scopePriority = 2
@@ -22,64 +24,66 @@ import org.eclipse.viatra.dse.objectives.impl.BaseObjective
 //      public static val compositePriority = 2
 //}
-class ModelGenerationCompositeObjective implements IObjective{
+@FinalFieldsConstructor
-        val ScopeObjective scopeObjective
+class ModelGenerationCompositeObjective implements IThreeValuedObjective {
-        val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives
+        val IObjective scopeObjective
-        val UnfinishedWFObjective unfinishedWFObjective
+        val List<IObjective> unfinishedMultiplicityObjectives
-        
+        val IObjective unfinishedWFObjective
-        public new(
-                ScopeObjective scopeObjective,
-                List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
-                UnfinishedWFObjective unfinishedWFObjective)
-        {
-                this.scopeObjective = scopeObjective
-                this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives
-                this.unfinishedWFObjective = unfinishedWFObjective
-        }
-        
        override init(ThreadContext context) {
                this.scopeObjective.init(context)
                this.unfinishedMultiplicityObjectives.forEach[it.init(context)]
                this.unfinishedWFObjective.init(context)
        }
-        
        override createNew() {
                return new ModelGenerationCompositeObjective(
-                        this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective)
+                        scopeObjective.createNew,
+                        ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew]),
+                        unfinishedWFObjective.createNew
+                )
        }
-        
        override getComparator() { Comparators.LOWER_IS_BETTER }
        override getFitness(ThreadContext context) {
                var sum = 0.0
                val scopeFitnes = scopeObjective.getFitness(context)
-                //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]
+                // val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]
                val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)
-                
-                sum+=scopeFitnes
+                sum += scopeFitnes
                var multiplicity = 0.0
-                for(multiplicityObjective : unfinishedMultiplicityObjectives) {
+                for (multiplicityObjective : unfinishedMultiplicityObjectives) {
-                        multiplicity+=multiplicityObjective.getFitness(context)//*0.5
+                        multiplicity += multiplicityObjective.getFitness(context) // *0.5
                }
-                sum+=multiplicity
+                sum += multiplicity
-                sum += unfinishedWFsFitness//*0.5
+                sum += unfinishedWFsFitness // *0.5
-                
+//              println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
-                //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
-                
                return sum
        }
        
-        override getLevel() { 2 }
+        override getWorstPossibleFitness(ThreadContext threadContext) {
-        override getName() { "CompositeUnfinishednessObjective"}
+                Double.POSITIVE_INFINITY
+        }
        
+        override getBestPossibleFitness(ThreadContext threadContext) {
+                0.0
+        }
+        override getLevel() { 2 }
+        override getName() { "CompositeUnfinishednessObjective" }
        override isHardObjective() { true }
        override satisifiesHardObjective(Double fitness) { fitness <= 0.001 }
-        
-        
        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/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 f61c7333..b63bfe8b 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
@@ -163,4 +163,4 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{
        override getAllStringsInStructure() {
                new TreeSet(this.stringForwardTrace.keySet)
        }
-}
-\ 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..69a734f8 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..d036257d
--- /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,74 @@
+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
+}
+class SolutionCopier {
+        val copiedSolutions = new LinkedHashMap<Object, CopiedSolution>
+        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)
+                        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
deleted file mode 100644
index a8b7301e..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
+++ /dev/null
@@ -1,52 +0,0 @@
-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.Map
-import org.eclipse.emf.ecore.util.EcoreUtil
-import org.eclipse.viatra.dse.base.ThreadContext
-import java.util.TreeMap
-import java.util.SortedMap
-class SolutionStoreWithCopy {
-        
-        long runtime = 0
-        List<PartialInterpretation> solutions = new LinkedList
-        //public List<SortedMap<String,Integer>> additionalMatches = new LinkedList
-        List<Map<EObject,EObject>> copyTraces = new LinkedList
-        
-        long sartTime = System.nanoTime
-        List<Long> solutionTimes = new LinkedList
-        
-        /*def newSolution(ThreadContext context, SortedMap<String,Integer> additonalMatch) {
-                additionalMatches+= additonalMatch
-                newSolution(context)
-        }*/
-        
-        def newSolution(ThreadContext context) {
-                //print(System.nanoTime-initTime + ";")
-                val copyStart = System.nanoTime
-                val solution = context.model as PartialInterpretation
-                val copier = new EcoreUtil.Copier
-                val solutionCopy = copier.copy(solution) as PartialInterpretation
-                copier.copyReferences
-                solutions.add(solutionCopy)
-                copyTraces.add(copier)
-                runtime += System.nanoTime - copyStart
-                solutionTimes.add(System.nanoTime-sartTime)
-        }
-        def getSumRuntime() {
-                return runtime
-        }
-        def getAllRuntimes() {
-                return solutionTimes
-        }
-        def getSolutions() {
-                solutions
-        }
-        def getCopyTraces() {
-                return copyTraces
-        }
-}
-\ 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/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 aad9a448..9f0c642f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
@@ -1,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;
        
-        public new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {
+        new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {
                this.unfinishedMultiplicity = unfinishedMultiplicity
        }
        
@@ -29,9 +29,9 @@ class UnfinishedMultiplicityObjective implements IObjective {
        override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }
        
        override setComparator(Comparator<Double> comparator) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+                throw new UnsupportedOperationException
        }
        override setLevel(int level) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+                throw new UnsupportedOperationException
        }
-}
-\ No newline at end of file
+}
diff --git a/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 java.util.ArrayList
-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.Collection
-import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import java.util.Comparator
-import org.eclipse.viatra.query.runtime.emf.EMFScope
-import org.eclipse.viatra.dse.base.ThreadContext
 import java.util.List
+import org.eclipse.viatra.dse.base.ThreadContext
 import org.eclipse.viatra.dse.objectives.Comparators
-import java.util.ArrayList
+import org.eclipse.viatra.dse.objectives.IObjective
-import java.util.Comparator
+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))
+                val engine = context.queryEngine // ViatraQueryEngine.on(new EMFScope(context.model))
-                for(unfinishedWF : unfinishedWFs) {
+                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»''')
+//                      if (number > 0) {
-                        sumOfMatches+=number
+//                              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..74500cc2
--- /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,142 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+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}.
+ */
+class ViatraReasonerSolutionSaver implements ISolutionSaver {
+        @Accessors val solutionCopier = new SolutionCopier
+        @Accessors val DiversityChecker diversityChecker
+        val boolean hasExtremalObjectives
+        val int numberOfRequiredSolutions
+        val ObjectiveComparatorHelper comparatorHelper
+        val Map<SolutionTrajectory, Fitness> trajectories = new HashMap
+        @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection
+        new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) {
+                this.diversityChecker = diversityChecker
+                comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives)
+                hasExtremalObjectives = leveledExtremalObjectives.exists[!empty]
+                this.numberOfRequiredSolutions = numberOfRequiredSolutions
+        }
+        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
+                }
+                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) {
+                return fitness.satisifiesHardObjectives
+        }
+        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
+        }
+}
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..63d78220 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,35 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification
 import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 class WF2ObjectiveConverter {
-        
+        static val UNFINISHED_WFS_NAME = "unfinishedWFs"
+        static val INVALIDATED_WFS_NAME = "invalidatedWFs"
        def createCompletenessObjective(
-                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF)
+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) {
-        {
+                // createConstraintObjective(UNFINISHED_WFS_NAME, unfinishedWF)
-                val res = new ConstraintsObjective('''unfinishedWFs''',
+                new UnfinishedWFObjective(unfinishedWF)
-                        unfinishedWF.map[
+        }
-                                new QueryConstraint(it.fullyQualifiedName,it,2.0)
-                        ].toList
+        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
+                res
-        }
-        
-        def IGlobalConstraint createInvalidationObjective(
-                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF)
-        {
-                return new ModelQueriesGlobalConstraint('''invalidatedWFs''',
-                        new ArrayList(invalidatedByWF)
-                )
        }
-}
-\ 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/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/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..0a6fd55b
--- /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,85 @@
+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 ThreeValuedCostElement {
+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentMatchQuery
+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayMatchQuery
+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustMatchQuery
+        val int weight
+}
+class ThreeValuedCostObjective extends AbstractThreeValuedObjective {
+        val Collection<ThreeValuedCostElement> costElements
+        Collection<CostElementMatchers> matchers
+        new(String name, Collection<ThreeValuedCostElement> costElements, ObjectiveKind kind, ObjectiveThreshold threshold,
+                int level) {
+                super(name, kind, threshold, level)
+                this.costElements = costElements
+        }
+        override createNew() {
+                new ThreeValuedCostObjective(name, costElements, kind, threshold, level)
+        }
+        override init(ThreadContext context) {
+                val queryEngine = context.queryEngine
+                matchers = ImmutableList.copyOf(costElements.map [ element |
+                        new CostElementMatchers(
+                                queryEngine.getMatcher(element.currentMatchQuery),
+                                queryEngine.getMatcher(element.mayMatchQuery),
+                                queryEngine.getMatcher(element.mustMatchQuery),
+                                element.weight
+                        )
+                ])
+        }
+        override getRawFitness(ThreadContext context) {
+                var int cost = 0
+                for (matcher : matchers) {
+                        cost += matcher.weight * matcher.currentMatcher.countMatches
+                }
+                cost as double
+        }
+        override getLowestPossibleFitness(ThreadContext threadContext) {
+                var int cost = 0
+                for (matcher : matchers) {
+                        if (matcher.weight >= 0) {
+                                cost += matcher.weight * matcher.mustMatcher.countMatches
+                        } else if (matcher.mayMatcher.countMatches > 0) {
+                                // TODO Count may matches.
+                                return Double.NEGATIVE_INFINITY
+                        }
+                }
+                cost as double
+        }
+        override getHighestPossibleFitness(ThreadContext threadContext) {
+                var int cost = 0
+                for (matcher : matchers) {
+                        if (matcher.weight <= 0) {
+                                cost += matcher.weight * matcher.mustMatcher.countMatches
+                        } else if (matcher.mayMatcher.countMatches > 0) {
+                                return Double.POSITIVE_INFINITY
+                        }
+                }
+                cost as double
+        }
+        @Data
+        private static class CostElementMatchers {
+                val ViatraQueryMatcher<? extends IPatternMatch> currentMatcher
+                val ViatraQueryMatcher<? extends IPatternMatch> mayMatcher
+                val ViatraQueryMatcher<? extends IPatternMatch> mustMatcher
+                val int weight
+        }
+}