23 files changed, 1974 insertions, 780 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend
new file mode 100644
index 00000000..65f9814c
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend
@@ -0,0 +1,24 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import java.util.ArrayList
+import java.util.Collection
+import java.util.Random
+abstract class ActivationSelector {
+        long runtime = 0
+        protected val Random r
+        new(Random r) {
+                this.r = r
+        }
+        
+        def randomizeActivationIDs(Collection<Object> activationIDs) {
+                val startTime = System.nanoTime
+                val res = internalRandomizationOfActivationIDs(activationIDs)
+                runtime+= System.nanoTime-startTime
+                return res
+        }
+        def protected ArrayList<Object> internalRandomizationOfActivationIDs(Collection<Object> activationIDs);
+        def getRuntime(){
+                return runtime
+        }
+}
+\ 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/BalancedActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend
new file mode 100644
index 00000000..2df9957b
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend
@@ -0,0 +1,51 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import java.util.Collection
+import java.util.HashMap
+import java.util.Map
+import java.util.List
+import java.util.Random
+import java.util.ArrayList
+import java.util.LinkedList
+import java.util.Collections
+class BalancedActivationSelector extends ActivationSelector{
+        val Random r = new Random
+        
+        new(Random r) {
+                super(r)
+        }
+        
+        override protected internalRandomizationOfActivationIDs(Collection<Object> activationIDs) {
+                val Map<String,List<Object>> urns = new HashMap
+                val res = new ArrayList(activationIDs.size)
+                for(activationID : activationIDs) {
+                        val pair = activationID as Pair<String,? extends Object>
+                        val name = pair.key
+                        val selectedUrn = urns.get(name)
+                        if(selectedUrn!==null) {
+                                selectedUrn.add(activationID)
+                        } else {
+                                val collection = new LinkedList
+                                collection.add(activationID)
+                                urns.put(name,collection)
+                        }
+                }
+                
+                for(list:urns.values) {
+                        Collections.shuffle(list,r)
+                }
+                
+                while(!urns.empty) {
+                        val randomEntry = urns.entrySet.get(r.nextInt(urns.size))
+                        val list = randomEntry.value
+                        val removedLast = list.remove(list.size-1)
+                        res.add(removedLast)
+                        if(list.empty) {
+                                urns.remove(randomEntry.key)
+                        }
+                }
+                return res
+        }
+        
+}
+\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/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 d9a1e54c..2940d12d 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
@@ -9,9 +9,7 @@
 *******************************************************************************/
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse;
-import java.util.ArrayList;
 import java.util.Arrays;
-import java.util.Collection;
 import java.util.Collections;
 import java.util.Comparator;
 import java.util.Iterator;
@@ -22,17 +20,16 @@ import java.util.Random;
 import org.apache.log4j.Level;
 import org.apache.log4j.Logger;
+import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.util.EcoreUtil;
+import org.eclipse.viatra.dse.api.SolutionTrajectory;
 import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;
 import org.eclipse.viatra.dse.base.ThreadContext;
 import org.eclipse.viatra.dse.objectives.Fitness;
 import org.eclipse.viatra.dse.objectives.IObjective;
 import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper;
+import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler;
 import org.eclipse.viatra.dse.solutionstore.SolutionStore;
-import org.eclipse.viatra.query.runtime.api.IPatternMatch;
-import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
-import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;
-import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher;
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
@@ -40,11 +37,11 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser;
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration;
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
@@ -77,54 +74,72 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
        // Running
        private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore;
        private SolutionStore solutionStore;
-        private SolutionStoreWithCopy solutionStoreWithCopy;
-        private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor;
        private volatile boolean isInterrupted = false;
        private ModelResult modelResultByInternalSolver = null;
        private Random random = new Random();
-        private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;
+//      private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;
-        
+        public ActivationSelector activationSelector = new EvenActivationSelector(random);
+        public ViatraReasonerSolutionSaver solutionSaver;
+        public NumericSolver numericSolver;
        // Statistics
        private int numberOfStatecoderFail = 0;
        private int numberOfPrintedModel = 0;
        private int numberOfSolverCalls = 0;
+        public long globalConstraintEvaluationTime = 0;
+        public long fitnessCalculationTime = 0;
+        
+        public long explorationStarted = 0;
        public BestFirstStrategyForModelGeneration(
                        ReasonerWorkspace workspace,
                        ViatraReasonerConfiguration configuration,
-                        ModelGenerationMethod method)
+                        ModelGenerationMethod method,
-        {
+                        ViatraReasonerSolutionSaver solutionSaver,
+                        NumericSolver numericSolver) {
                this.workspace = workspace;
                this.configuration = configuration;
                this.method = method;
+                this.solutionSaver = solutionSaver;
+                this.numericSolver = numericSolver;
+//              logger.setLevel(Level.DEBUG);
        }
        
-        public SolutionStoreWithCopy getSolutionStoreWithCopy() {
-                return solutionStoreWithCopy;
-        }
-        public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
-                return solutionStoreWithDiversityDescriptor;
-        }
        public int getNumberOfStatecoderFail() {
                return numberOfStatecoderFail;
        }
+        public long getForwardTime() {
+                return context.getDesignSpaceManager().getForwardTime();
+        }
+        public long getBacktrackingTime() {
+                return context.getDesignSpaceManager().getBacktrackingTime();
+        }
        @Override
        public void initStrategy(ThreadContext context) {
                this.context = context;
                this.solutionStore = context.getGlobalContext().getSolutionStore();
-                ViatraQueryEngine engine = context.getQueryEngine();
+                solutionStore.registerSolutionFoundHandler(new ISolutionFoundHandler() {
-//              // TODO: visualisation
+                        
-                matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
+                        @Override
-                for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {
+                        public void solutionTriedToSave(ThreadContext context, SolutionTrajectory trajectory) {
-                        //System.out.println(p.getSimpleName());
+                                // Ignore.
-                        ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);
+                        }
-                        matchers.add(matcher);
+                        
-                }
+                        @Override
+                        public void solutionFound(ThreadContext context, SolutionTrajectory trajectory) {
+                                configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions);
+                                saveTimes();
+                                logger.debug("Found a solution.");
+                        }
+                });
+                numericSolver.init(context);
                
-                this.solutionStoreWithCopy = new SolutionStoreWithCopy();
+//              ViatraQueryEngine engine = context.getQueryEngine();
-                this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
+//              matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
+//              for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {
+//                              ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);
+//              }
+//              
                final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
                this.comparator = new Comparator<TrajectoryWithFitness>() {
                        @Override
@@ -138,23 +153,26 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
        @Override
        public void explore() {
-                if (!context.checkGlobalConstraints()) {
+                this.explorationStarted=System.nanoTime();
+                if (!checkGlobalConstraints()) {
                        logger.info("Global contraint is not satisifed in the first state. Terminate.");
                        return;
+                } else if(!numericSolver.maySatisfiable()) {
+                        logger.info("Numeric contraints are not satisifed in the first state. Terminate.");
+                        return;
                }
                if (configuration.searchSpaceConstraints.maxDepth == 0) {
                        logger.info("Maximal depth is reached in the initial solution. Terminate.");
                        return;
                }
                
-                final Fitness firstFittness = context.calculateFitness();
+                final Fitness firstFitness = calculateFitness();
-                checkForSolution(firstFittness);
+                checkForSolution(firstFitness);
                
                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();
 //              for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
@@ -168,22 +186,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;
 //                      }
@@ -193,32 +211,30 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                        while (!isInterrupted && !configuration.progressMonitor.isCancelled() && iterator.hasNext()) {
                                final Object nextActivation = iterator.next();
-//                              if (!iterator.hasNext()) {
-//                                      logger.debug("Last untraversed activation of the state.");
-//                                      trajectoiresToExplore.remove(currentTrajectoryWithFittness);
-//                              }
                                logger.debug("Executing new activation: " + nextActivation);
                                context.executeAcitvationId(nextActivation);
+                                method.getStatistics().incrementDecisionCount();
                                visualiseCurrentState();
 //                              for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
-//                                      System.out.println(matcher.getPatternName());
+//                                      int c = matcher.countMatches();
-//                                      System.out.println("---------");
+//                                      if(c>=1) {
-//                                      for(IPatternMatch m : matcher.getAllMatches()) {
+//                                              System.out.println(c+ " " +matcher.getPatternName());
-//                                              System.out.println(m);
+//                                      }       
-//                                      }
-//                                      System.out.println("---------");
 //                              }
                                
-                                boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);
+                                boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness);
                                if(consistencyCheckResult == true) { continue mainLoop; }
                                if (context.isCurrentStateAlreadyTraversed()) {
                                        logger.info("The new state is already visited.");
                                        context.backtrack();
-                                } else if (!context.checkGlobalConstraints()) {
+                                } else if (!checkGlobalConstraints()) {
                                        logger.debug("Global contraint is not satisifed.");
                                        context.backtrack();
+                                } else if (!numericSolver.maySatisfiable()) {
+                                        logger.debug("Numeric constraints are not satisifed.");
+                                        context.backtrack();
                                } else {
                                        final Fitness nextFitness = context.calculateFitness();
                                        checkForSolution(nextFitness);
@@ -228,59 +244,89 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                                                continue;
                                        }
-                                        TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness(
+                                        TrajectoryWithFitness nextTrajectoryWithfitness = new TrajectoryWithFitness(
                                                        context.getTrajectory().toArray(), nextFitness);
-                                        trajectoiresToExplore.add(nextTrajectoryWithFittness);
+                                        trajectoiresToExplore.add(nextTrajectoryWithfitness);
-                                        int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness,
+                                        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.");
        }
+        private boolean checkGlobalConstraints() {
+                long start = System.nanoTime();
+                boolean result = context.checkGlobalConstraints();
+                globalConstraintEvaluationTime += System.nanoTime() - start;
+                return result;
+        }
+        
+        private Fitness calculateFitness() {
+                long start = System.nanoTime();
+                Fitness fitness = context.calculateFitness(); 
+                fitnessCalculationTime += System.nanoTime() - start;
+                return fitness;
+        }
+        
        private List<Object> selectActivation() {
                List<Object> activationIds;
                try {
-                        activationIds = new ArrayList<Object>(context.getUntraversedActivationIds());
+                        activationIds = this.activationSelector.randomizeActivationIDs(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) {
+        private void checkForSolution(final Fitness fitness) {
-                if (fittness.isSatisifiesHardObjectives()) {
+                solutionStore.newSolution(context);
-                        if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
+        }
-                                solutionStoreWithCopy.newSolution(context);
+        
-                                solutionStoreWithDiversityDescriptor.newSolution(context);
+        public List<String> times = new LinkedList<String>();
-                                solutionStore.newSolution(context);
+        private void saveTimes() {
-                                configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
+                long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000;
+                long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000;
-                                logger.debug("Found a solution.");
+                long activationSelection = this.activationSelector.getRuntime()/1000000;
-                        }
+                long solutionCopierTime = this.solutionSaver.getTotalCopierRuntime()/1000000;
-                }
+                long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000;
+                long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000;
+                long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000;
+                long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000;
+                this.times.add(
+                        "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+
+                        "|ForwardTime:"+forwardTime+
+                        "|Backtrackingtime:"+backtrackingTime+
+                        "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+
+                        "|FitnessCalculationTime:"+(fitnessCalculationTime/1000000)+
+                        "|ActivationSelectionTime:"+activationSelection+
+                        "|SolutionCopyTime:"+solutionCopierTime+
+                        "|NumericalSolverSumTime:"+numericalSolverSumTime+
+                        "|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+
+                        "|NumericalSolverSolvingTime:"+numericalSolverSolving+
+                        "|NumericalSolverInterpretingSolution:"+numericalSolverInterpreting+")");
+                
        }
        @Override
@@ -309,7 +355,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                } else {
                        return trajectoiresToExplore.element();
                }
-        }       
+        }
 //      private void logCurrentStateMetric() {
 //      if(this.configuration.documentationLevel != DocumentationLevel.NONE || workspace == null) {
@@ -322,13 +368,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/EvenActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend
new file mode 100644
index 00000000..82a5f32d
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend
@@ -0,0 +1,20 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import java.util.Random
+import java.util.Collection
+import java.util.Collections
+import java.util.ArrayList
+class EvenActivationSelector extends ActivationSelector {
+        
+        new(Random r) {
+                super(r)
+        }
+        
+        override protected internalRandomizationOfActivationIDs(Collection<Object> activationIDs) {
+                val toShuffle = new ArrayList<Object>(activationIDs);
+                Collections.shuffle(toShuffle);
+                return toShuffle
+        }
+        
+}
+\ 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/HillClimbingOnRealisticMetricStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/HillClimbingOnRealisticMetricStrategyForModelGeneration.java
index eb7df089..d9f84b36 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/HillClimbingOnRealisticMetricStrategyForModelGeneration.java
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/HillClimbingOnRealisticMetricStrategyForModelGeneration.java
@@ -16,6 +16,7 @@ import java.util.Random;
 import java.util.Set;
 import org.apache.log4j.Logger;
+import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.util.EcoreUtil;
 import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;
 import org.eclipse.viatra.dse.base.ThreadContext;
@@ -35,480 +36,540 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser;
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.RealisticGuidance;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration;
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
 public class HillClimbingOnRealisticMetricStrategyForModelGeneration implements IStrategy {
        // Services and Configuration
-                private ThreadContext context;
+        private ThreadContext context;
-                private ReasonerWorkspace workspace;
+        private ReasonerWorkspace workspace;
-                private ViatraReasonerConfiguration configuration;
+        private ViatraReasonerConfiguration configuration;
-                private ModelGenerationMethod method;
+        private ModelGenerationMethod method;
-                private PartialInterpretation2Logic partialInterpretation2Logic = new PartialInterpretation2Logic();
+        private PartialInterpretation2Logic partialInterpretation2Logic = new PartialInterpretation2Logic();
-                private Comparator<TrajectoryWithFitness> comparator;
+        private Comparator<TrajectoryWithFitness> comparator;
-                private Logger logger = Logger.getLogger(IStrategy.class);
+        private Logger logger = Logger.getLogger(IStrategy.class);
+        public NumericSolver numericSolver = null;
+        // 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();
+        
+        // matchers for detecting the number of violations
+        private Collection<ViatraQueryMatcher<? extends IPatternMatch>> mustMatchers;
+        private Collection<ViatraQueryMatcher<? extends IPatternMatch>> mayMatchers;
+        // Encode the used activations of a particular state
+        private Map<Object, List<Object>> stateAndActivations;
+        private boolean allowMustViolation;
+        private Domain domain;
+        int targetSize;
+        public ActivationSelector activationSelector = new EvenActivationSelector(random);
+        // Statistics
+        private int numberOfStatecoderFail = 0;
+        private int numberOfPrintedModel = 0;
+        private int numberOfSolverCalls = 0;
+        private PartialInterpretationMetricDistance metricDistance; 
+        private double currentStateValue = Double.MAX_VALUE;
+        private double currentNodeTypeDistance = 1;
+        private int numNodesToGenerate = 0;
+        public long explorationStarted = 0;
+        public long globalConstraintEvaluationTime = 0;
+        public long fitnessCalculationTime = 0;
+        
+        public HillClimbingOnRealisticMetricStrategyForModelGeneration(
+                        ReasonerWorkspace workspace,
+                        ViatraReasonerConfiguration configuration,
+                        ModelGenerationMethod method)
+        {
+                this.workspace = workspace;
+                this.configuration = configuration;
+                this.method = method;
+        }
+        
+        public SolutionStoreWithCopy getSolutionStoreWithCopy() {
+                return solutionStoreWithCopy;
+        }
+        public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
+                return solutionStoreWithDiversityDescriptor;
+        }
+        public int getNumberOfStatecoderFail() {
+                return numberOfStatecoderFail;
+        }
+        
+        public long getForwardTime() {
+                return context.getDesignSpaceManager().getForwardTime();
+        }
+        public long getBacktrackingTime() {
+                return context.getDesignSpaceManager().getBacktrackingTime();
+        }
+        @Override
+        public void initStrategy(ThreadContext context) {
+                this.context = context;
+                this.solutionStore = context.getGlobalContext().getSolutionStore();
+                domain = Domain.valueOf(configuration.domain);
+                ViatraQueryEngine engine = context.getQueryEngine();
+//                      // TODO: visualisation
+                mustMatchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
+                mayMatchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
                
-                // Running
+                // manully restict the number of super types of one class
-                private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore;
+                this.method.getInvalidWF().forEach(a ->{ 
-                private SolutionStore solutionStore;
+                        ViatraQueryMatcher<? extends IPatternMatch> matcher = a.getMatcher(engine);
-                private SolutionStoreWithCopy solutionStoreWithCopy;
+                        mustMatchers.add(matcher);
-                private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor;
+                });
-                private volatile boolean isInterrupted = false;
-                private ModelResult modelResultByInternalSolver = null;
-                private Random random = new Random();
                
-                // matchers for detecting the number of violations
+                this.method.getUnfinishedWF().forEach(a ->{ 
-                private Collection<ViatraQueryMatcher<? extends IPatternMatch>> mustMatchers;
+                        ViatraQueryMatcher<? extends IPatternMatch> matcher = a.getMatcher(engine);
-                private Collection<ViatraQueryMatcher<? extends IPatternMatch>> mayMatchers;
+                        mayMatchers.add(matcher);
+                });
        
-                // Encode the used activations of a particular state
-                private Map<Object, List<Object>> stateAndActivations;
-                private boolean allowMustViolation;
-                private Domain domain;
-                int targetSize;
-                // Statistics
-                private int numberOfStatecoderFail = 0;
-                private int numberOfPrintedModel = 0;
-                private int numberOfSolverCalls = 0;
-                private PartialInterpretationMetricDistance metricDistance; 
-                private double currentStateValue = Double.MAX_VALUE;
-                private double currentNodeTypeDistance = 1;
-                private int numNodesToGenerate = 0;
                
-                public HillClimbingOnRealisticMetricStrategyForModelGeneration(
+                //set up comparator
-                                ReasonerWorkspace workspace,
+                final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
-                                ViatraReasonerConfiguration configuration,
+                this.comparator = new Comparator<TrajectoryWithFitness>() {
-                                ModelGenerationMethod method)
+                        @Override
-                {
+                        public int compare(TrajectoryWithFitness o1, TrajectoryWithFitness o2) {
-                        this.workspace = workspace;
+                                return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);
-                        this.configuration = configuration;
+                        }
-                        this.method = method;
+                };
-                }
                
-                public SolutionStoreWithCopy getSolutionStoreWithCopy() {
+                this.solutionStoreWithCopy = new SolutionStoreWithCopy();
-                        return solutionStoreWithCopy;
+                this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
-                }
+                
-                public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
+                trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);
-                        return solutionStoreWithDiversityDescriptor;
+                stateAndActivations = new HashMap<Object, List<Object>>();
+                metricDistance = new PartialInterpretationMetricDistance(domain);
+                
+                //set whether allows must violations during the realistic generation
+                allowMustViolation = configuration.allowMustViolations;
+                targetSize = configuration.typeScopes.maxNewElements + 2;
+                //this.numericSolver = new NumericSolver(method, this.configuration.runIntermediateNumericalConsistencyChecks, false);
+        }
+        @Override
+        public void explore() {
+                this.explorationStarted=System.nanoTime();
+                if (!checkGlobalConstraints()) {
+                        logger.info("Global contraint is not satisifed in the first state. Terminate.");
+                        return;
                }
-                public int getNumberOfStatecoderFail() {
+                if (configuration.searchSpaceConstraints.maxDepth == 0) {
-                        return numberOfStatecoderFail;
+                        logger.info("Maximal depth is reached in the initial solution. Terminate.");
+                        return;
                }
-                @Override
-                public void initStrategy(ThreadContext context) {
-                        this.context = context;
-                        this.solutionStore = context.getGlobalContext().getSolutionStore();
-                        domain = Domain.valueOf(configuration.domain);
-                        ViatraQueryEngine engine = context.getQueryEngine();
-//                      // TODO: visualisation
-                        mustMatchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
-                        mayMatchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
-                        
-                        // manully restict the number of super types of one class
-                        this.method.getInvalidWF().forEach(a ->{ 
-                                ViatraQueryMatcher<? extends IPatternMatch> matcher = a.getMatcher(engine);
-                                mustMatchers.add(matcher);
-                        });
-                        
-                        this.method.getUnfinishedWF().forEach(a ->{ 
-                                ViatraQueryMatcher<? extends IPatternMatch> matcher = a.getMatcher(engine);
-                                mayMatchers.add(matcher);
-                        });
                
-                        
+                final Fitness firstFittness = context.calculateFitness();
-                        //set up comparator
+                
-                        final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
+                //final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
-                        this.comparator = new Comparator<TrajectoryWithFitness>() {
+                final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
-                                @Override
+                TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness);
-                                public int compare(TrajectoryWithFitness o1, TrajectoryWithFitness o2) {
+                trajectoiresToExplore.add(currentTrajectoryWithFittness);
-                                        return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);
+                Object lastState = null;
+                
+                //if(configuration)
+                visualiseCurrentState();
+                // the two is the True and False node generated at the beginning of the generation
+                int count = 0;
+                mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) {
+                        if (currentTrajectoryWithFittness == null) {
+                                if (trajectoiresToExplore.isEmpty()) {
+                                        logger.debug("State space is fully traversed.");
+                                        return;
+                                } else {
+                                        currentTrajectoryWithFittness = selectState();
+                                        if (logger.isDebugEnabled()) {
+                                                logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
+                                                logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness);
+                                        }
+                                        context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory);
+                                        
+                                        // reset the regression for this trajectory
+                                        metricDistance.getLinearModel().resetRegression(context.getCurrentStateId());
                                }
-                        };
+                        }
                        
-                        this.solutionStoreWithCopy = new SolutionStoreWithCopy();
+                        List<Object> activationIds = selectActivation();
-                        this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
+                        PartialInterpretation model = (PartialInterpretation) context.getModel();
+                        System.out.println(model.getNewElements().size());
+                        System.out.println("# violations: " + getNumberOfViolations(mayMatchers));
                        
-                        trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);
+                        Map<Object, Double> valueMap = new HashMap<Object,Double>();
-                        stateAndActivations = new HashMap<Object, List<Object>>();
-                        metricDistance = new PartialInterpretationMetricDistance(domain);
                        
-                        //set whether allows must violations during the realistic generation
+                        //init epsilon and draw
-                        allowMustViolation = configuration.allowMustViolations;
+                        MetricDistanceGroup heuristics =  metricDistance.calculateMetricDistanceKS(model);
-                        targetSize = configuration.typeScopes.maxNewElements + 2;
-                }
-                @Override
+                        if(!stateAndActivations.containsKey(context.getCurrentStateId())) {
-                public void explore() {
+                                stateAndActivations.put(context.getCurrentStateId(), new ArrayList<Object>());
-                        if (!context.checkGlobalConstraints()) {
-                                logger.info("Global contraint is not satisifed in the first state. Terminate.");
-                                return;
-                        }
-                        if (configuration.searchSpaceConstraints.maxDepth == 0) {
-                                logger.info("Maximal depth is reached in the initial solution. Terminate.");
-                                return;
                        }
                        
-                        final Fitness firstFittness = context.calculateFitness();
+                        // calculate values for epsilon greedy
-                        
+                        double epsilon = 1.0/count;
-                        //final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
+                        double draw = Math.random();
-                        final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
+                        count++;
-                        TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness);
+                        this.currentNodeTypeDistance = heuristics.getNodeTypeDistance();
-                        trajectoiresToExplore.add(currentTrajectoryWithFittness);
+                        numNodesToGenerate = model.getMaxNewElements();
-                        Object lastState = null;
+                        System.out.println("NA distance: " + heuristics.getNADistance());       
-                        
+                        System.out.println("MPC distance: " + heuristics.getMPCDistance());     
-                        //if(configuration)
+                        System.out.println("Out degree distance:" + heuristics.getOutDegreeDistance()); 
-                        visualiseCurrentState();
+                        System.out.println("NodeType :" + currentNodeTypeDistance);     
-                        // the two is the True and False node generated at the beginning of the generation
-                        int count = 0;
-                        mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) {
-                                if (currentTrajectoryWithFittness == null) {
-                                        if (trajectoiresToExplore.isEmpty()) {
-                                                logger.debug("State space is fully traversed.");
-                                                return;
-                                        } else {
-                                                currentTrajectoryWithFittness = selectState();
-                                                if (logger.isDebugEnabled()) {
-                                                        logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
-                                                        logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness);
-                                                }
-                                                context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory);
-                                                
-                                                // reset the regression for this trajectory
-                                                metricDistance.getLinearModel().resetRegression(context.getCurrentStateId());
-                                        }
-                                }
-                                
-                                List<Object> activationIds = selectActivation();
-                                PartialInterpretation model = (PartialInterpretation) context.getModel();
-//                              System.out.println(model.getNewElements().size());
-//                              System.out.println("# violations: " + getNumberOfViolations(mayMatchers));
-                                
-                                Map<Object, Double> valueMap = new HashMap<Object,Double>();
-                                
-                                //init epsilon and draw
-                                MetricDistanceGroup heuristics =  metricDistance.calculateMetricDistanceKS(model);
-                                if(!stateAndActivations.containsKey(context.getCurrentStateId())) {
+                        //TODO: the number of activations to be checked should be configurasble
-                                        stateAndActivations.put(context.getCurrentStateId(), new ArrayList<Object>());
+                        if(activationIds.size() > 50) {
-                                }
+                                activationIds = activationIds.subList(0, 50);
+                        }
+                        
+                        valueMap = sortWithWeight(activationIds);
+                        lastState = context.getCurrentStateId();
+                        while (!isInterrupted && !configuration.progressMonitor.isCancelled() && activationIds.size() > 0) {
+                                final Object nextActivation = drawWithEpsilonProbabilty(activationIds, valueMap, epsilon, draw);
+                                                                        
+                                stateAndActivations.get(context.getCurrentStateId()).add(nextActivation);
+                                logger.debug("Executing new activation: " + nextActivation);
+                                context.executeAcitvationId(nextActivation);
+                                visualiseCurrentState();
+                                boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);
+                                if(consistencyCheckResult == true) { continue mainLoop; }
                                
-                                // calculate values for epsilon greedy
+//                              if (context.isCurrentStateAlreadyTraversed()) {
-                                double epsilon = 1.0/count;
+//                                      logger.info("The new state is already visited.");
-                                double draw = Math.random();
+//                                      context.backtrack();
-                                count++;
+//                              } else if (!checkGlobalConstraints()) {
-                                this.currentNodeTypeDistance = heuristics.getNodeTypeDistance();
+//                                      logger.debug("Global contraint is not satisifed.");
-                                numNodesToGenerate = model.getMaxNewElements();
+//                                      context.backtrack();
-//                              System.out.println("NA distance: " + heuristics.getNADistance());       
+//                              } 
-//                              System.out.println("MPC distance: " + heuristics.getMPCDistance());     
-//                              System.out.println("Out degree distance:" + heuristics.getOutDegreeDistance()); 
-//                              System.out.println("NodeType :" + currentNodeTypeDistance);     
-                                //TODO: the number of activations to be checked should be configurasble
-                                if(activationIds.size() > 50) {
-                                        activationIds = activationIds.subList(0, 50);
-                                }
                                
-                                valueMap = sortWithWeight(activationIds);
+                                int currentSize = model.getNewElements().size();
-                                lastState = context.getCurrentStateId();
+                                int targetDiff = targetSize - currentSize;
-                                while (!isInterrupted && !configuration.progressMonitor.isCancelled() && activationIds.size() > 0) {
+                                boolean shouldFinish = currentSize >= targetSize;
-                                        final Object nextActivation = drawWithEpsilonProbabilty(activationIds, valueMap, epsilon, draw);
+                                
-                                                                                
+                                // does not allow must violations
-                                        stateAndActivations.get(context.getCurrentStateId()).add(nextActivation);
+                                if((getNumberOfViolations(mustMatchers) > 0|| getNumberOfViolations(mayMatchers) > targetDiff) && !allowMustViolation && !shouldFinish) {
-                                        logger.debug("Executing new activation: " + nextActivation);
+                                        context.backtrack();
-                                        context.executeAcitvationId(nextActivation);
+                                }else {
-                                        visualiseCurrentState();
+                                        final Fitness nextFitness = context.calculateFitness();
-                                        boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);
-                                        if(consistencyCheckResult == true) { continue mainLoop; }
-                                        
-                                        int currentSize = model.getNewElements().size();
-                                        int targetDiff = targetSize - currentSize;
-                                        boolean shouldFinish = currentSize >= targetSize;
                                        
-                                        // does not allow must violations
+                                        // the only hard objectives are configured in the config file
-                                        if((getNumberOfViolations(mustMatchers) > 0|| getNumberOfViolations(mayMatchers) > targetDiff) && !allowMustViolation && !shouldFinish) {
+                                        checkForSolution(nextFitness);
+                        
+                                        if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) {
+                                                logger.debug("Reached max depth.");
                                                context.backtrack();
-                                        }else {
+                                                continue;
-                                                final Fitness nextFitness = context.calculateFitness();
-                                                
-                                                // the only hard objectives are configured in the config file
-                                                checkForSolution(nextFitness);
-                                
-                                                if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) {
-                                                        logger.debug("Reached max depth.");
-                                                        context.backtrack();
-                                                        continue;
-                                                }
-                                                
-                                                //Record value for current trajectory
-                                                TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness(
-                                                                context.getTrajectory().toArray(), nextFitness);
-                                                int nodeSize = ((PartialInterpretation) context.getModel()).getNewElements().size();
-                                                int violation = getNumberOfViolations(mayMatchers);
-                                                double currentValue = calculateCurrentStateValue(nodeSize, violation);
-                                                metricDistance.getLinearModel().feedData(context.getCurrentStateId(), metricDistance.calculateFeature(nodeSize, violation), currentValue, lastState);
-                                                trajectoiresToExplore.add(nextTrajectoryWithFittness);
-                                                currentStateValue = currentValue;
-                                                //Currently, just go to the next state without considering the value of trajectory
-                                                currentTrajectoryWithFittness = nextTrajectoryWithFittness;
-                                                continue mainLoop;
                                        }
+                                        
+                                        //Record value for current trajectory
+                                        TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness(
+                                                        context.getTrajectory().toArray(), nextFitness);
+                                        int nodeSize = ((PartialInterpretation) context.getModel()).getNewElements().size();
+                                        int violation = getNumberOfViolations(mayMatchers);
+                                        double currentValue = calculateCurrentStateValue(nodeSize, violation);
+                                        metricDistance.getLinearModel().feedData(context.getCurrentStateId(), metricDistance.calculateFeature(nodeSize, violation), currentValue, lastState);
+                                        trajectoiresToExplore.add(nextTrajectoryWithFittness);
+                                        currentStateValue = currentValue;
+                                        //Currently, just go to the next state without considering the value of trajectory
+                                        currentTrajectoryWithFittness = nextTrajectoryWithFittness;
+                                        continue mainLoop;
                                }
-                                logger.debug("State is fully traversed.");
-                                trajectoiresToExplore.remove(currentTrajectoryWithFittness);
-                                currentTrajectoryWithFittness = null;
-                                context.backtrack();
                        }
-                        logger.info("Interrupted.");
+                        logger.debug("State is fully traversed.");
+                        trajectoiresToExplore.remove(currentTrajectoryWithFittness);
+                        currentTrajectoryWithFittness = null;
+                        context.backtrack();
                }
+                logger.info("Interrupted.");
+        }
-                /**
+        private boolean checkGlobalConstraints() {
-                 *
+                long start = System.nanoTime();
-                 * @param activationIds
+                boolean result = context.checkGlobalConstraints();
-                 * @return: activation to value map
+                globalConstraintEvaluationTime += System.nanoTime() - start;
-                 */
+                return result;
-                private Map<Object, Double> sortWithWeight(List<Object> activationIds){
+        }
-                        Map<Object, Double> valueMap = new HashMap<Object, Double>();
+        
-                        Object currentId = context.getCurrentStateId();
+        private Fitness calculateFitness() {
-                        // check for next states
+                long start = System.nanoTime();
-                        for(Object id : activationIds) {
+                Fitness fitness = context.calculateFitness(); 
-                                context.executeAcitvationId(id);
+                fitnessCalculationTime += System.nanoTime() - start;
-                                int violation = getNumberOfViolations(mayMatchers);
+                return fitness;
+        }
+        
+        /**
+         *
+         * @param activationIds
+         * @return: activation to value map
+         */
+        private Map<Object, Double> sortWithWeight(List<Object> activationIds){
+                Map<Object, Double> valueMap = new HashMap<Object, Double>();
+                Object currentId = context.getCurrentStateId();
+                // check for next states
+                for(Object id : activationIds) {
+                        context.executeAcitvationId(id);
+                        int violation = getNumberOfViolations(mayMatchers);
-                                if(!allowMustViolation && getNumberOfViolations(mustMatchers) > 0) {
+                        if(!allowMustViolation && getNumberOfViolations(mustMatchers) > 0) {
-                                        valueMap.put(id, Double.MAX_VALUE);
+                                valueMap.put(id, Double.MAX_VALUE);
-                                        stateAndActivations.get(currentId).add(id);
+                                stateAndActivations.get(currentId).add(id);
-                                }else {
+                        }else {
-                                        valueMap.put(id, calculateFutureStateValue(violation));
+                                valueMap.put(id, calculateFutureStateValue(violation));
-                                }
-                                        
-                                
-                                
-                                context.backtrack();
                        }
+                                
+                        
                        
-                        //remove all the elements having large distance
+                        context.backtrack();
-                        Collections.sort(activationIds, Comparator.comparing(li -> valueMap.get(li)));
-                        return valueMap;
                }
                
-                private double calculateFutureStateValue(int violation) {
+                //remove all the elements having large distance
-                        long start = System.nanoTime();
+                Collections.sort(activationIds, Comparator.comparing(li -> valueMap.get(li)));
-                        int nodeSize = ((PartialInterpretation) context.getModel()).getNewElements().size();
+                return valueMap;
-                        double currentValue = calculateCurrentStateValue(nodeSize,violation);
+        }
-                        double[] toPredict = metricDistance.calculateFeature(100, violation);
+        
-                        if(Math.abs(currentValue - currentStateValue) < 0.001) {
+        private double calculateFutureStateValue(int violation) {
-                                this.method.getStatistics().addMetricCalculationTime(System.nanoTime() - start);
+                long start = System.nanoTime();
-                                return Double.MAX_VALUE;
+                int nodeSize = ((PartialInterpretation) context.getModel()).getNewElements().size();
-                        }
+                double currentValue = calculateCurrentStateValue(nodeSize,violation);
-                        try {
+                double[] toPredict = metricDistance.calculateFeature(100, violation);
-                                this.method.getStatistics().addMetricCalculationTime(System.nanoTime() - start);
+                if(Math.abs(currentValue - currentStateValue) < 0.001) {
-                                return metricDistance.getLinearModel().getPredictionForNextDataSample(metricDistance.calculateFeature(nodeSize, violation), currentValue, toPredict);
+                        this.method.getStatistics().addMetricCalculationTime(System.nanoTime() - start);
-                        }catch(IllegalArgumentException e) {
+                        return Double.MAX_VALUE;
-                                this.method.getStatistics().addMetricCalculationTime(System.nanoTime() - start);
+                }
-                                return currentValue;
+                try {
-                        }
+                        this.method.getStatistics().addMetricCalculationTime(System.nanoTime() - start);
+                        return metricDistance.getLinearModel().getPredictionForNextDataSample(metricDistance.calculateFeature(nodeSize, violation), currentValue, toPredict);
+                }catch(IllegalArgumentException e) {
+                        this.method.getStatistics().addMetricCalculationTime(System.nanoTime() - start);
+                        return currentValue;
                }
-                private double calculateCurrentStateValue(int factor, int violation) {
-                        PartialInterpretation model = (PartialInterpretation) context.getModel();
-                        MetricDistanceGroup g = metricDistance.calculateMetricDistanceKS(model);
-                        if(configuration.realisticGuidance == RealisticGuidance.MPC) {
-                                return g.getMPCDistance();
-                        }else if(configuration.realisticGuidance == RealisticGuidance.NodeActivity) {
-                                return g.getNADistance();
-                        }else if(configuration.realisticGuidance == RealisticGuidance.OutDegree) {
-                                return g.getOutDegreeDistance();
-                        }else if(configuration.realisticGuidance == RealisticGuidance.NodeType) {
-                                return g.getNodeTypeDistance();
-                        }else if(configuration.realisticGuidance == RealisticGuidance.Composite) {
-                                double consistenceWeights = 5 * factor / (configuration.typeScopes.maxNewElements + 2) * (1- 1.0/(1+violation));
-                                if(domain == Domain.Yakindumm) {
-                                        double unfinishFactor = 50 * (1 - (double)factor / targetSize);
-                                        double nodeTypeFactor = g.getNodeTypeDistance();
-                                        double normalFactor = 5;
-                                        if(currentNodeTypeDistance <= 0.05 || numNodesToGenerate == 1) {
-                                                nodeTypeFactor = 0;
-                                                normalFactor = 100;
-                                                unfinishFactor = 0; 
-                                        }
-                                        
-                                        return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + g.getMPCDistance() + 2*g.getOutDegreeDistance()) + normalFactor / 5*consistenceWeights + unfinishFactor;
-                                }else if (domain == Domain.Ecore) {
-                                        double unfinishFactor = 100 * (1 - (double)factor / targetSize);
-                                        double nodeTypeFactor = g.getNodeTypeDistance();
-                                        double normalFactor = 5;
-                                        if(currentNodeTypeDistance <= 0.12 || numNodesToGenerate == 1) {
-                                                nodeTypeFactor = 0;
-                                                normalFactor = 100;
-                                                unfinishFactor *= 0.5; 
-                                        }
-                                        
-                                        return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + g.getMPCDistance() + 2*g.getOutDegreeDistance()) + normalFactor / 5*consistenceWeights + unfinishFactor;
-                                }else {
-                                        double unfinishFactor = context.calculateFitness().get("CompositeUnfinishednessObjective");
-                                        double nodeTypeFactor = g.getNodeTypeDistance();
-                                        double normalFactor = 5;
-                                        if(currentNodeTypeDistance <= 0.05 || numNodesToGenerate == 1) {
-                                                nodeTypeFactor = 0;
-                                                normalFactor = 100;
-                                                //unfinishFactor *= 0.5; 
-                                        }
-                                        
-                                        return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + 2*g.getMPCDistance() + 2*g.getOutDegreeDistance()) + normalFactor / 5*consistenceWeights + unfinishFactor;
-                                }
-                        }else if(configuration.realisticGuidance == RealisticGuidance.Composite_Without_Violations) {
+        }
-                                if(domain == Domain.Yakindumm) {
+        private double calculateCurrentStateValue(int factor, int violation) {
-                                        double unfinishFactor = 50 * (1 - (double)factor / targetSize);
+                PartialInterpretation model = (PartialInterpretation) context.getModel();
-                                        double nodeTypeFactor = g.getNodeTypeDistance();
+                MetricDistanceGroup g = metricDistance.calculateMetricDistanceKS(model);
-                                        double normalFactor = 5;
+                if(configuration.realisticGuidance == RealisticGuidance.MPC) {
-                                        if(currentNodeTypeDistance <= 0.05 || numNodesToGenerate == 1) {
+                        return g.getMPCDistance();
-                                                nodeTypeFactor = 0;
+                }else if(configuration.realisticGuidance == RealisticGuidance.NodeActivity) {
-                                                normalFactor = 100;
+                        return g.getNADistance();
-                                                unfinishFactor = 0; 
+                }else if(configuration.realisticGuidance == RealisticGuidance.OutDegree) {
-                                        }
+                        return g.getOutDegreeDistance();
-                                        
+                }else if(configuration.realisticGuidance == RealisticGuidance.NodeType) {
-                                        return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + g.getMPCDistance() + 2*g.getOutDegreeDistance()) + unfinishFactor;
+                        return g.getNodeTypeDistance();
-                                }else if (domain == Domain.Github) {
+                }else if(configuration.realisticGuidance == RealisticGuidance.Composite) {
-                                        double unfinishFactor = 100 * (1 - (double)factor / targetSize);
+                        double consistenceWeights = 5 * factor / (configuration.typeScopes.maxNewElements + 2) * (1- 1.0/(1+violation));
-                                        double nodeTypeFactor = g.getNodeTypeDistance();
+                        if(domain == Domain.Yakindumm) {
-                                        double normalFactor = 5;
+                                double unfinishFactor = 50 * (1 - (double)factor / targetSize);
-                                        if(currentNodeTypeDistance <= 0.12 || numNodesToGenerate == 1) {
+                                double nodeTypeFactor = g.getNodeTypeDistance();
-                                                nodeTypeFactor = 0;
+                                double normalFactor = 5;
-                                                normalFactor = 100;
+                                if(currentNodeTypeDistance <= 0.05 || numNodesToGenerate == 1) {
-                                                unfinishFactor *= 0.5; 
+                                        nodeTypeFactor = 0;
-                                        }
+                                        normalFactor = 100;
-                                        
+                                        unfinishFactor = 0; 
-                                        return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + g.getMPCDistance() + 2*g.getOutDegreeDistance()) + unfinishFactor;
-                                } else {
-                                        double unfinishFactor = 100 * (1 - (double)factor / targetSize);
-                                        double nodeTypeFactor = g.getNodeTypeDistance();
-                                        double normalFactor = 5;
-                                        if(currentNodeTypeDistance <= 0.20 || numNodesToGenerate == 1) {
-                                                nodeTypeFactor = 0;
-                                                normalFactor = 100;
-                                                unfinishFactor *= 0.5; 
-                                        }
-                                        
-                                        return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + g.getMPCDistance() + 2*g.getOutDegreeDistance()) + unfinishFactor;
                                }
+                                
+                                return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + g.getMPCDistance() + 2*g.getOutDegreeDistance()) + normalFactor / 5*consistenceWeights + unfinishFactor;
+                        }else if (domain == Domain.Ecore) {
+                                double unfinishFactor = 100 * (1 - (double)factor / targetSize);
+                                double nodeTypeFactor = g.getNodeTypeDistance();
+                                double normalFactor = 5;
+                                if(currentNodeTypeDistance <= 0.12 || numNodesToGenerate == 1) {
+                                        nodeTypeFactor = 0;
+                                        normalFactor = 100;
+                                        unfinishFactor *= 0.5; 
+                                }
+                                
+                                return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + g.getMPCDistance() + 2*g.getOutDegreeDistance()) + normalFactor / 5*consistenceWeights + unfinishFactor;
                        }else {
-                                return violation;
+                                double unfinishFactor = context.calculateFitness().get("CompositeUnfinishednessObjective");
-                        }
+                                double nodeTypeFactor = g.getNodeTypeDistance();
-                }
+                                double normalFactor = 5;
-                
+                                if(currentNodeTypeDistance <= 0.05 || numNodesToGenerate == 1) {
-                private int getNumberOfViolations(Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers) {
+                                        nodeTypeFactor = 0;
-                        int violations = matchers.stream().mapToInt(m -> m.countMatches()).sum();
+                                        normalFactor = 100;
-                        
+                                        //unfinishFactor *= 0.5; 
-                        return violations;
+                                }
-                }
+                                
-                
+                                return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + 2*g.getMPCDistance() + 2*g.getOutDegreeDistance()) + normalFactor / 5*consistenceWeights + unfinishFactor;
-                // Modified epsilon greedy choose for action based on value function
-                // with probability epsilon, choose the state with probability based on the weight
-                // with probability 1 - epsilon, choose the best state
-                // epsilon should decay w.r.t. time
-                private Object drawWithEpsilonProbabilty(List<Object> activationIds, Map<Object, Double> valueMap, double epsilon, double currentDraw) {
-                        if(activationIds.size() <= 0) {
-                                return null;
                        }
-                        
-                        // if epsilon is smaller than current draw, return greedy choice 
+                }else if(configuration.realisticGuidance == RealisticGuidance.Composite_Without_Violations) {
-                        if(epsilon < currentDraw) {
+                        if(domain == Domain.Yakindumm) {
-                                return activationIds.remove(0);
+                                double unfinishFactor = 50 * (1 - (double)factor / targetSize);
-                        }else {
+                                double nodeTypeFactor = g.getNodeTypeDistance();
-                                //else return draw with probability of the weights
+                                double normalFactor = 5;
-                                //find the sum of all 1-weights: the smaller the better
+                                if(currentNodeTypeDistance <= 0.05 || numNodesToGenerate == 1) {
-                                double sum = valueMap.values().stream().mapToDouble(d->1).sum();
+                                        nodeTypeFactor = 0;
-                                double rand = Math.random() * sum;
+                                        normalFactor = 100;
-                                double iterator = 0.0;
+                                        unfinishFactor = 0; 
-                                Object idToReturn = null;
+                                }
                                
-                                // draw an item with probability
+                                return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + g.getMPCDistance() + 2*g.getOutDegreeDistance()) + unfinishFactor;
-                                for(Object o : valueMap.keySet()) {
+                        }else if (domain == Domain.Github) {
-                                        iterator += (1);
+                                double unfinishFactor = 100 * (1 - (double)factor / targetSize);
-                                        if(rand < iterator) {
+                                double nodeTypeFactor = g.getNodeTypeDistance();
-                                                idToReturn = o;
+                                double normalFactor = 5;
-                                                break;
+                                if(currentNodeTypeDistance <= 0.12 || numNodesToGenerate == 1) {
-                                        }
+                                        nodeTypeFactor = 0;
+                                        normalFactor = 100;
+                                        unfinishFactor *= 0.5; 
+                                }
+                                
+                                return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + g.getMPCDistance() + 2*g.getOutDegreeDistance()) + unfinishFactor;
+                        } else {
+                                double unfinishFactor = 100 * (1 - (double)factor / targetSize);
+                                double nodeTypeFactor = g.getNodeTypeDistance();
+                                double normalFactor = 5;
+                                if(currentNodeTypeDistance <= 0.20 || numNodesToGenerate == 1) {
+                                        nodeTypeFactor = 0;
+                                        normalFactor = 100;
+                                        unfinishFactor *= 0.5; 
                                }
                                
-                                //delete the item from the list
+                                return 100*(nodeTypeFactor) + normalFactor*(2*g.getNADistance() + g.getMPCDistance() + 2*g.getOutDegreeDistance()) + unfinishFactor;
-                                activationIds.remove(idToReturn);
-                                valueMap.remove(idToReturn);
-                                return idToReturn;
                        }
+                }else {
+                        return violation;
                }
+        }
+        
+        private int getNumberOfViolations(Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers) {
+                int violations = matchers.stream().mapToInt(m -> m.countMatches()).sum();
                
-                private List<Object> selectActivation() {
+                return violations;
-                        List<Object> activationIds;
+        }
-                        try {
+        
-                                activationIds = new ArrayList<Object>(context.getCurrentActivationIds());
+        // Modified epsilon greedy choose for action based on value function
-                                if(stateAndActivations.containsKey(context.getCurrentStateId())) {
+        // with probability epsilon, choose the state with probability based on the weight
-                                        activationIds.removeAll(stateAndActivations.get(context.getCurrentStateId()));
+        // with probability 1 - epsilon, choose the best state
+        // epsilon should decay w.r.t. time
+        private Object drawWithEpsilonProbabilty(List<Object> activationIds, Map<Object, Double> valueMap, double epsilon, double currentDraw) {
+                if(activationIds.size() <= 0) {
+                        return null;
+                }
+                
+                // if epsilon is smaller than current draw, return greedy choice 
+                if(epsilon < currentDraw) {
+                        return activationIds.remove(0);
+                }else {
+                        //else return draw with probability of the weights
+                        //find the sum of all 1-weights: the smaller the better
+                        double sum = valueMap.values().stream().mapToDouble(d->1).sum();
+                        double rand = Math.random() * sum;
+                        double iterator = 0.0;
+                        Object idToReturn = null;
+                        
+                        // draw an item with probability
+                        for(Object o : valueMap.keySet()) {
+                                iterator += (1);
+                                if(rand < iterator) {
+                                        idToReturn = o;
+                                        break;
                                }
-                                Collections.shuffle(activationIds);
-                        } catch (NullPointerException e) {
-                                numberOfStatecoderFail++;
-                                activationIds = Collections.emptyList();
                        }
-                        return activationIds;
+                        
+                        //delete the item from the list
+                        activationIds.remove(idToReturn);
+                        valueMap.remove(idToReturn);
+                        return idToReturn;
                }
+        }
+        
+        private List<Object> selectActivation() {
+                List<Object> activationIds;
+                try {
+                        activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds());
+                } catch (NullPointerException e) {
+                        numberOfStatecoderFail++;
+                        activationIds = Collections.emptyList();
+                }
+                return activationIds;
+        }
-                private void checkForSolution(final Fitness fittness) {
+        private void checkForSolution(final Fitness fittness) {
-                        if (fittness.isSatisifiesHardObjectives()) {
+                if (fittness.isSatisifiesHardObjectives()) {
-                                logger.debug("Solution Found!!");
+                        logger.debug("Solution Found!!");
-                                logger.debug("# violations: " + (getNumberOfViolations(mustMatchers)));
+                        logger.debug("# violations: " + (getNumberOfViolations(mustMatchers)));
-                                if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
+                        if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
-                                        solutionStoreWithCopy.newSolution(context);
+                                solutionStoreWithCopy.newSolution(context);
-                                        solutionStoreWithDiversityDescriptor.newSolution(context);
+                                solutionStoreWithDiversityDescriptor.newSolution(context);
-                                        solutionStore.newSolution(context);
+                                solutionStore.newSolution(context);
-                                        configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
+                                configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions);
-                                        logger.debug("Found a solution.");
+                                logger.debug("Found a solution.");
-                                }
                        }
                }
+        }
+        
+        public List<String> times = new LinkedList<String>();
+        private void saveTimes() {
+                long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000;
+                long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000;
+                long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder)this.context.getStateCoder()).getStatecoderRuntime()/1000000;
+                long solutionCopy = solutionStoreWithCopy.getSumRuntime()/1000000;
+                long activationSelection = this.activationSelector.getRuntime()/1000000;
+//              long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000;
+//              long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000;
+//              long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000;
+//              long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000;
+                long metricCalculationTime = this.method.getStatistics().metricCalculationTime / 1000000;
+                this.times.add(
+                        "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ 
+                        "|ForwardTime:"+forwardTime+
+                        "|Backtrackingtime:"+backtrackingTime+
+                        "|StateCoderTime:"+statecoderTime+
+                        "|SolutionCopyTime:"+solutionCopy+
+                        "|ActivationSelectionTime:"+activationSelection+
+                        //"|NumericalSolverSumTime:"+numericalSolverSumTime+
+                        //"|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+
+                        //"|NumericalSolverSolvingTime:"+numericalSolverSolving+
+                        //"|NumericalSolverInterpretingSolution:"+numericalSolverInterpreting+
+                        "|MetricCalculationTime:"+metricCalculationTime + ")"
+                        );
+                
+        }
-                @Override
+        @Override
-                public void interruptStrategy() {
+        public void interruptStrategy() {
-                        isInterrupted = true;
+                isInterrupted = true;
-                }
+        }
-                private TrajectoryWithFitness selectState() {
+        private TrajectoryWithFitness selectState() {
-                        int randomNumber = random.nextInt(configuration.randomBacktrackChance);
+                int randomNumber = random.nextInt(configuration.randomBacktrackChance);
-                        if (randomNumber == 0) {
+                if (randomNumber == 0) {
-                                int elements = trajectoiresToExplore.size();
+                        int elements = trajectoiresToExplore.size();
-                                int randomElementIndex = random.nextInt(elements);
+                        int randomElementIndex = random.nextInt(elements);
-                                logger.debug("Randomly backtract to the " + randomElementIndex + " best solution...");
+                        logger.debug("Randomly backtract to the " + randomElementIndex + " best solution...");
-                                Iterator<TrajectoryWithFitness> iterator = trajectoiresToExplore.iterator();
+                        Iterator<TrajectoryWithFitness> iterator = trajectoiresToExplore.iterator();
-                                while (randomElementIndex != 0) {
+                        while (randomElementIndex != 0) {
-                                        iterator.next();
+                                iterator.next();
-                                        randomElementIndex--;
+                                randomElementIndex--;
-                                }
+                        }
-                                TrajectoryWithFitness res = iterator.next();
+                        TrajectoryWithFitness res = iterator.next();
-                                if (res == null) {
+                        if (res == null) {
-                                        return trajectoiresToExplore.element();
-                                } else {
-                                        return res;
-                                }
-                        } else {
                                return trajectoiresToExplore.element();
+                        } else {
+                                return res;
                        }
-                }       
+                } else {
-                
+                        return trajectoiresToExplore.element();
+                }
+        }       
+        
 //              private void logCurrentStateMetric() {
 //                      if(this.configuration.documentationLevel != DocumentationLevel.NONE || workspace == null) {
 //                              return;
@@ -518,77 +579,80 @@ public class HillClimbingOnRealisticMetricStrategyForModelGeneration implements
 //                      PartialInterpretationMetric.calculateMetric(interpretation, "debug/metric/" + context.getModel().hashCode(), context.getCurrentStateId().toString());           
 //              }
-                public void visualiseCurrentState() {
+        public void visualiseCurrentState() {
-                        PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser;
+                PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser;
-                        if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) {
+                if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) {
-                                PartialInterpretation p = (PartialInterpretation) (context.getModel());
+                        PartialInterpretation p = (PartialInterpretation) (context.getModel());
-                                int id = ++numberOfPrintedModel;
+                        int id = ++numberOfPrintedModel;
-                                if (id % configuration.debugCongiguration.partalInterpretationVisualisationFrequency == 0) {
+                        if (id % configuration.debugConfiguration.partalInterpretationVisualisationFrequency == 0) {
-                                        PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p);
+                                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");
                        }
                }
+        }
-                protected boolean checkConsistency(TrajectoryWithFitness t) {
+        protected boolean checkConsistency(TrajectoryWithFitness t) {
-                        LogicReasoner internalIncosnsitencyDetector = configuration.internalConsistencyCheckerConfiguration.internalIncosnsitencyDetector;
+                LogicReasoner internalIncosnsitencyDetector = configuration.internalConsistencyCheckerConfiguration.internalIncosnsitencyDetector;
-                        if (internalIncosnsitencyDetector!= null) {
+                if (internalIncosnsitencyDetector!= null) {
-                                int id = ++numberOfSolverCalls;
+                        int id = ++numberOfSolverCalls;
-                                if (id % configuration.internalConsistencyCheckerConfiguration.incternalConsistencyCheckingFrequency == 0) {
+                        if (id % configuration.internalConsistencyCheckerConfiguration.incternalConsistencyCheckingFrequency == 0) {
-                                        try {
+                                try {
-                                                PartialInterpretation interpretation = (PartialInterpretation) (context.getModel());
+                                        PartialInterpretation interpretation = (PartialInterpretation) (context.getModel());
-                                                PartialInterpretation copied = EcoreUtil.copy(interpretation);
+                                        PartialInterpretation copied = EcoreUtil.copy(interpretation);
-                                                this.partialInterpretation2Logic.transformPartialIntepretation2Logic(copied.getProblem(), copied);
+                                        this.partialInterpretation2Logic.transformPartialIntepretation2Logic(copied.getProblem(), copied);
-                                                LogicProblem newProblem = copied.getProblem();
+                                        LogicProblem newProblem = copied.getProblem();
-                                                this.configuration.typeScopes.maxNewElements = interpretation.getMaxNewElements();
+                                        this.configuration.typeScopes.maxNewElements = interpretation.getMaxNewElements();
-                                                this.configuration.typeScopes.minNewElements = interpretation.getMinNewElements();
+                                        this.configuration.typeScopes.minNewElements = interpretation.getMinNewElements();
-                                                LogicResult result = internalIncosnsitencyDetector.solve(newProblem, configuration, workspace);
+                                        LogicResult result = internalIncosnsitencyDetector.solve(newProblem, configuration, workspace);
-                                                if (result instanceof InconsistencyResult) {
+                                        if (result instanceof InconsistencyResult) {
-                                                        logger.debug("Solver found an Inconsistency!");
+                                                logger.debug("Solver found an Inconsistency!");
-                                                        removeSubtreeFromQueue(t);
+                                                removeSubtreeFromQueue(t);
-                                                        return true;
+                                                return true;
-                                                } else if (result instanceof ModelResult) {
+                                        } else if (result instanceof ModelResult) {
-                                                        logger.debug("Solver found a model!");
+                                                logger.debug("Solver found a model!");
-                                                        solutionStore.newSolution(context);
+                                                solutionStore.newSolution(context);
-                                                        this.modelResultByInternalSolver = (ModelResult) result;
+                                                this.modelResultByInternalSolver = (ModelResult) result;
-                                                        return true;
+                                                return true;
-                                                } else {
+                                        } else {
-                                                        logger.debug("Failed consistency check.");
+                                                logger.debug("Failed consistency check.");
-                                                        return false;
-                                                }
-                                        } catch (Exception e) {
-                                                logger.debug("Problem with internal consistency checking: "+e.getMessage());
-                                                e.printStackTrace();
                                                return false;
                                        }
+                                } catch (Exception e) {
+                                        logger.debug("Problem with internal consistency checking: "+e.getMessage());
+                                        e.printStackTrace();
+                                        return false;
                                }
                        }
-                        return false;
-                }
-                protected void removeSubtreeFromQueue(TrajectoryWithFitness t) {
-                        PriorityQueue<TrajectoryWithFitness> previous = this.trajectoiresToExplore;
-                        this.trajectoiresToExplore = new PriorityQueue<>(this.comparator);
-                        for (TrajectoryWithFitness trajectoryWithFitness : previous) {
-                                if (!containsAsSubstring(trajectoryWithFitness.trajectory, t.trajectory)) {
-                                        this.trajectoiresToExplore.add(trajectoryWithFitness);
-                                } else {
-                                        logger.debug("State has been excluded due to inherent inconsistency");
-                                }
-                        }
                }
+                return false;
+        }
-                private boolean containsAsSubstring(Object[] full, Object[] substring) {
+        protected void removeSubtreeFromQueue(TrajectoryWithFitness t) {
-                        if (substring.length > full.length) {
+                PriorityQueue<TrajectoryWithFitness> previous = this.trajectoiresToExplore;
-                                return false;
+                this.trajectoiresToExplore = new PriorityQueue<>(this.comparator);
-                        } else if (substring.length == full.length) {
+                for (TrajectoryWithFitness trajectoryWithFitness : previous) {
-                                return Arrays.equals(full, substring);
+                        if (!containsAsSubstring(trajectoryWithFitness.trajectory, t.trajectory)) {
+                                this.trajectoiresToExplore.add(trajectoryWithFitness);
                        } else {
-                                Object[] part = Arrays.copyOfRange(full, 0, substring.length);
+                                logger.debug("State has been excluded due to inherent inconsistency");
-                                return Arrays.equals(part, substring);
                        }
                }
+        }
+        private boolean containsAsSubstring(Object[] full, Object[] substring) {
+                if (substring.length > full.length) {
+                        return false;
+                } else if (substring.length == full.length) {
+                        return Arrays.equals(full, substring);
+                } else {
+                        Object[] part = Arrays.copyOfRange(full, 0, substring.length);
+                        return Arrays.equals(part, substring);
+                }
+        }
 }
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 9fc6853c..27208cf4 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
@@ -1,99 +1,123 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import com.google.common.collect.ImmutableList
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective
 import java.util.Comparator
 import java.util.List
 import org.eclipse.viatra.dse.base.ThreadContext
 import org.eclipse.viatra.dse.objectives.Comparators
 import org.eclipse.viatra.dse.objectives.IObjective
-import org.eclipse.viatra.dse.objectives.impl.BaseObjective
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
-//class ViatraReasonerNumbers {
+class ModelGenerationCompositeObjective implements IThreeValuedObjective {
-//      public static val scopePriority = 2
+        val IObjective scopeObjective
-//      public static val unfinishedMultiplicityPriority = 2
-//      public static val unifinshedWFPriority = 2
-//      //public static val complexityPriority = 4
-//      
-//      public static val scopeWeigth = 1.0
-//      public static val unfinishedMultiplicityWeigth = 1.5
-//      public static val unfinishedWFWeigth = 1.5
-//      //public static val complexityWeigth = 0.1
-//      
-//      public static val useCompositeObjective = true
-//      public static val compositePriority = 2
-//}
-class ModelGenerationCompositeObjective implements IObjective{
-        val ScopeObjective scopeObjective
        val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives
        val UnfinishedWFObjective unfinishedWFObjective
-        var boolean isWFOptional = false;
+        var PartialInterpretation model = null
+        val int scopeWeight
+        val int conaintmentWeight
+        val int nonContainmentWeight
+        val int unfinishedWFWeight
        
-        public new(
+        new(
-                ScopeObjective scopeObjective,
+                IObjective scopeObjective,
+                List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
+                UnfinishedWFObjective unfinishedWFObjective,
+                ViatraReasonerConfiguration configuration)
+        {
+                this(
+                        scopeObjective, unfinishedMultiplicityObjectives, unfinishedWFObjective,
+                        configuration.scopeWeight, configuration.conaintmentWeight, configuration.nonContainmentWeight,
+                        configuration.unfinishedWFWeight
+                )
+        }
+        new(
+                IObjective scopeObjective,
                List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
                UnfinishedWFObjective unfinishedWFObjective,
-                boolean isWFOptional)
+                int scopeWeight, int conaintmentWeight, int nonContainmentWeight, int unfinishedWFWeight)
        {
                this.scopeObjective = scopeObjective
                this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives
                this.unfinishedWFObjective = unfinishedWFObjective
-                this.isWFOptional = isWFOptional;
+                
-        }
+                this.scopeWeight = scopeWeight
-        
+                this.conaintmentWeight = conaintmentWeight
-        def getIsWFOptional(){
+                this.nonContainmentWeight = nonContainmentWeight
-                return this.isWFOptional;
+                this.unfinishedWFWeight = unfinishedWFWeight
        }
        
        override init(ThreadContext context) {
+                model = context.model as PartialInterpretation
                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, this.isWFOptional)
+                        scopeObjective.createNew,
+                        ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew as UnfinishedMultiplicityObjective]),
+                        unfinishedWFObjective.createNew as UnfinishedWFObjective,
+                        scopeWeight, conaintmentWeight, nonContainmentWeight, unfinishedWFWeight
+                )
        }
-        
        override getComparator() { Comparators.LOWER_IS_BETTER }
        override getFitness(ThreadContext context) {
-                var sum = 0.0
+                
                val scopeFitnes = scopeObjective.getFitness(context)
-                //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]
+                val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)
                
-                sum+=scopeFitnes
+                var containmentMultiplicity = 0.0
-                var multiplicity = 0.0
+                var nonContainmentMultiplicity = 0.0
                for(multiplicityObjective : unfinishedMultiplicityObjectives) {
-                        multiplicity+=multiplicityObjective.getFitness(context)//*0.5
+                        val multiplicity = multiplicityObjective.getFitness(context)
+//                      println(multiplicityObjective.name + "=" + multiplicity)
+                        if(multiplicityObjective.containment) {
+                                containmentMultiplicity+=multiplicity
+                        } else {
+                                nonContainmentMultiplicity+=multiplicity
+                        }
+                        
                }
-                sum+=multiplicity
                
-                // the WF can be optional when generating realistic models
+                var sum = 0.0
-                if(!isWFOptional){
+                sum += scopeFitnes*scopeWeight
-                        val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)
+                sum += containmentMultiplicity*conaintmentWeight
-                        sum += unfinishedWFsFitness//*0.5
+                sum += nonContainmentMultiplicity*nonContainmentWeight
-                }
+                sum += unfinishedWFsFitness*unfinishedWFWeight
                
-                //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
+//              println('''scope=«scopeFitnes», containment=«containmentMultiplicity», nonContainment=«nonContainmentMultiplicity», wf=«unfinishedWFsFitness», sum=«sum»''')
                
                return sum
        }
        
-        override getLevel() { 2 }
+        override getWorstPossibleFitness(ThreadContext threadContext) {
-        override getName() { "CompositeUnfinishednessObjective"}
+                Double.POSITIVE_INFINITY
-        def getObjective(){
-                return this.unfinishedMultiplicityObjectives;
        }
        
+        override getBestPossibleFitness(ThreadContext threadContext) {
+                0.0
+        }
+        override getLevel() { 2 }
+        override getName() { "CompositeUnfinishednessObjective" }
        override isHardObjective() { true }
-        override satisifiesHardObjective(Double fitness) { fitness <= 0.001 }
-        
+        override satisifiesHardObjective(Double fitness) { fitness < 0.01 }
-        
        override setComparator(Comparator<Double> comparator) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+                throw new UnsupportedOperationException("Model generation objective comparator cannot be set.")
        }
        override setLevel(int level) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+                throw new UnsupportedOperationException("Model generation objective level cannot be set.")
        }
-        
+}
-}
-\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
new file mode 100644
index 00000000..70e8e9c2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -0,0 +1,192 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod
+import java.math.BigDecimal
+import java.util.HashMap
+import java.util.LinkedHashMap
+import java.util.LinkedHashSet
+import java.util.List
+import java.util.Map
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
+class NumericSolver {
+        val ModelGenerationMethod method
+        var ThreadContext threadContext
+        val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
+        val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
+        NumericTranslator t = new NumericTranslator
+        
+        val boolean intermediateConsistencyCheck
+        val boolean caching;
+        Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap
+        
+        var long runtime = 0
+        var long cachingTime = 0 
+        var int numberOfSolverCalls = 0
+        var int numberOfCachedSolverCalls = 0
+        
+        new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) {
+                this.method = method
+                this.intermediateConsistencyCheck = intermediateConsistencyCheck
+                this.caching = caching
+        }
+        
+        def init(ThreadContext context) {
+                // This makes the NumericSolver single-threaded,
+                // but that's not a problem, because we only use the solver on a single thread anyways.
+                this.threadContext = context
+                val engine = threadContext.queryEngine
+                for(entry : method.mustUnitPropagationPreconditions.entrySet) {
+                        val constraint = entry.key
+                        val querySpec = entry.value
+                        val matcher = querySpec.getMatcher(engine);
+                        constraint2MustUnitPropagationPrecondition.put(constraint,matcher)
+                }
+                for(entry : method.currentUnitPropagationPreconditions.entrySet) {
+                        val constraint = entry.key
+                        val querySpec = entry.value
+                        val matcher = querySpec.getMatcher(engine);
+                        constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher)
+                }
+        }
+        
+        def getRuntime(){runtime}
+        def getCachingTime(){cachingTime}
+        def getNumberOfSolverCalls(){numberOfSolverCalls}
+        def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls}
+        def getSolverFormingProblem(){this.t.formingProblemTime}
+        def getSolverSolvingProblem(){this.t.solvingProblemTime}
+        def getSolverSolution(){this.t.formingSolutionTime}
+        
+        def boolean maySatisfiable() {
+                if(intermediateConsistencyCheck) {
+                        return isSatisfiable(this.constraint2MustUnitPropagationPrecondition)
+                } else {
+                        return true
+                }
+        }
+        def boolean currentSatisfiable() {
+                isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition)
+        }
+        
+        private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) {
+                val start = System.nanoTime
+                var boolean finalResult 
+                if(matches.empty){
+                        finalResult=true
+                } else {
+                        val propagatedConstraints = new HashMap
+                        for(entry : matches.entrySet) {
+                                val constraint = entry.key
+                                //println(constraint)
+                                val allMatches = entry.value.allMatches.map[it.toArray]
+                                //println(allMatches.toList)
+                                propagatedConstraints.put(constraint,allMatches)
+                        }
+                        if(propagatedConstraints.values.forall[empty]) {
+                                finalResult=true
+                        } else {
+                                if(caching) {
+                                        val code = getCode(propagatedConstraints)
+                                        val cachedResult = satisfiabilityCache.get(code)
+                                        if(cachedResult === null) {
+        //                                      println('''new problem, call solver''')
+        //                                      for(entry : code.entrySet) {
+        //                                              println('''«entry.key» -> «entry.value»''')
+        //                                      }
+                                                //println(code.hashCode)
+                                                this.numberOfSolverCalls++
+                                                val res = t.delegateIsSatisfiable(propagatedConstraints)
+                                                satisfiabilityCache.put(code,res)
+                                                finalResult=res
+                                        } else {
+                                                //println('''similar problem, answer from cache''')
+                                                finalResult=cachedResult
+                                                this.numberOfCachedSolverCalls++
+                                        }
+                                } else {
+                                        finalResult= t.delegateIsSatisfiable(propagatedConstraints)
+                                        this.numberOfSolverCalls++
+                                }
+                        }
+                }       
+                this.runtime+=System.nanoTime-start
+                return finalResult
+        }
+        
+        def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) {
+                val start = System.nanoTime
+                val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList
+                val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]])
+                this.cachingTime += System.nanoTime-start
+                return res
+        }
+        
+        def fillSolutionCopy(Map<EObject, EObject> trace) {
+                val model = threadContext.getModel as PartialInterpretation
+                val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
+                if(constraint2CurrentUnitPropagationPrecondition.empty) {
+                        fillWithDefaultValues(dataObjects,trace)
+                } else {
+                        val propagatedConstraints = new HashMap
+                        for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) {
+                                val constraint = entry.key
+                                val allMatches = entry.value.allMatches.map[it.toArray]
+                                propagatedConstraints.put(constraint,allMatches)
+                        }
+                        
+                        if(propagatedConstraints.values.forall[empty]) {
+                                fillWithDefaultValues(dataObjects,trace)
+                        } else {
+                                val solution = t.delegateGetSolution(dataObjects,propagatedConstraints)
+                                fillWithSolutions(dataObjects,solution,trace)
+                        }
+                }
+        }
+        
+        def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) {
+                for(element : elements) {
+                        if(element.valueSet==false) {
+                                val value = getDefaultValue(element)
+                                val target = trace.get(element) as PrimitiveElement
+                                target.fillWithValue(value)
+                        }
+                }
+        }
+        
+        def protected dispatch getDefaultValue(BooleanElement e) {false}
+        def protected dispatch getDefaultValue(IntegerElement e) {0}
+        def protected dispatch getDefaultValue(RealElement e) {0.0}
+        def protected dispatch getDefaultValue(StringElement e) {""}
+        
+        def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) {
+                for(element : elements) {
+                        if(element.valueSet==false) {
+                                if(solution.containsKey(element)) {
+                                        val value = solution.get(element)
+                                        val target = trace.get(element) as PrimitiveElement
+                                        target.fillWithValue(value)
+                                } else {
+                                        val target = trace.get(element) as PrimitiveElement
+                                        target.fillWithValue(target.defaultValue)
+                                }
+                        }
+                }
+        }
+        
+        def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean}
+        def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer}
+        def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=BigDecimal.valueOf(value as Double) }
+        def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}
+}
+\ 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..b48d0831 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
@@ -22,12 +22,13 @@ import java.util.List
 import java.util.Map
 import java.util.TreeSet
 import org.eclipse.emf.ecore.EObject
+import org.eclipse.xtend.lib.annotations.Accessors
 import org.eclipse.xtext.xbase.lib.Functions.Function1
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 class PartialModelAsLogicInterpretation implements LogicModelInterpretation{
-        val PartialInterpretation partialInterpretation
+        @Accessors val PartialInterpretation partialInterpretation
        val Map<EObject, EObject> trace;
        val Map<TypeDeclaration,PartialComplexTypeInterpretation> type2Interpretation
        val Map<RelationDeclaration,PartialRelationInterpretation> relation2Interpretation
@@ -153,14 +154,70 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{
        }
        
        override getAllIntegersInStructure() {
-                new TreeSet(this.integerForwardTrace.keySet)
+                new TreeSet(allIntegersWithInterpretation.values)
+        }
+        
+        override getAllIntegersWithInterpretation() {
+                val builder = new HashMap
+                for (entry : integerForwardTrace.entrySet) {
+                        builder.put(entry.value, entry.key)
+                }
+                for (element : partialInterpretation.newElements) {
+                        if (element instanceof IntegerElement) {
+                                builder.put(element, element.value)
+                        }
+                }
+                builder
        }
        
        override getAllRealsInStructure() {
-                new TreeSet(this.realForwardTrace.keySet)
+                new TreeSet(allRealsWithInterpretation.values)
+        }
+        
+        override getAllRealsWithInterpretation() {
+                val builder = new HashMap
+                for (entry : realForwardTrace.entrySet) {
+                        builder.put(entry.value, entry.key)
+                }
+                for (element : partialInterpretation.newElements) {
+                        if (element instanceof RealElement) {
+                                builder.put(element, element.value)
+                        }
+                }
+                builder
        }
        
        override getAllStringsInStructure() {
-                new TreeSet(this.stringForwardTrace.keySet)
+                new TreeSet(allStringsWithInterpretation.values)
+        }
+        
+        override getAllStringsWithInterpretation() {
+                val builder = new HashMap
+                for (entry : stringForwardTrace.entrySet) {
+                        builder.put(entry.value, entry.key)
+                }
+                for (element : partialInterpretation.newElements) {
+                        if (element instanceof StringElement) {
+                                builder.put(element, element.value)
+                        }
+                }
+                builder
+        }
+        
+        override getAllBooleansInStructure() {
+                new TreeSet(allBooleansWithInterpretation.values)
+        }
+        
+        override getAllBooleansWithInterpretation() {
+                val builder = new HashMap
+                for (entry : booleanForwardTrace.entrySet) {
+                        builder.put(entry.value, entry.key)
+                }
+                for (element : partialInterpretation.newElements) {
+                        if (element instanceof BooleanElement) {
+                                builder.put(element, element.value)
+                        }
+                }
+                builder
        }
-}
-\ No newline at end of file
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PunishSizeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PunishSizeObjective.xtend
new file mode 100644
index 00000000..bad8e4d1
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PunishSizeObjective.xtend
@@ -0,0 +1,52 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.AbstractThreeValuedObjective
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
+import org.eclipse.viatra.dse.base.ThreadContext
+class PunishSizeObjective extends AbstractThreeValuedObjective {
+        static val NAME = typeof(PunishSizeObjective).name
+        
+        new(ObjectiveKind kind, int level) {
+                super(NAME, kind, ObjectiveThreshold.NO_THRESHOLD, level)
+        }
+        
+        override createNew() {
+                new PunishSizeObjective(kind, level)
+        }
+        
+        override init(ThreadContext context) {
+                // Nothing to initialize.
+        }
+        
+        override getRawFitness(ThreadContext threadContext) {
+                val model = threadContext.model
+                if (model instanceof PartialInterpretation) {
+                        val size = model.newObjectCount
+//                      println('''size=«size»''')
+                        size as double
+                } else {
+                        throw new IllegalArgumentException("notifier must be a PartialInterpretation")
+                }
+        }
+        
+        override getLowestPossibleFitness(ThreadContext threadContext) {
+                getRawFitness(threadContext)
+        }
+        
+        override getHighestPossibleFitness(ThreadContext threadContext) {
+                val model = threadContext.model
+                if (model instanceof PartialInterpretation) {
+                        (model.newObjectCount + model.maxNewElements) as double
+                } else {
+                        throw new IllegalArgumentException("notifier must be a PartialInterpretation")
+                }
+        }
+        
+        private def getNewObjectCount(PartialInterpretation interpretation) {
+                interpretation.newElements.reject[it instanceof PrimitiveElement].size
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
index 69efe0d7..b61bd20b 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
@@ -23,9 +23,9 @@ class ScopeObjective implements IObjective{
        
        override getFitness(ThreadContext context) {
                val interpretation = context.model as PartialInterpretation
-                var res = interpretation.minNewElements.doubleValue
+                var res = interpretation.minNewElementsHeuristic.doubleValue
                for(scope : interpretation.scopes) {
-                        res += scope.minNewElements*2
+                        res += scope.minNewElementsHeuristic * 2
                }
                return res
        }
@@ -41,4 +41,4 @@ class ScopeObjective implements IObjective{
                throw new UnsupportedOperationException("TODO: auto-generated method stub")
        }
        override getLevel() { 2 }
-}
-\ No newline at end of file
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
new file mode 100644
index 00000000..888eda18
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
@@ -0,0 +1,82 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import com.google.common.collect.ImmutableList
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import java.util.LinkedHashMap
+import java.util.List
+import java.util.Map
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.emf.ecore.util.EcoreUtil
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+@FinalFieldsConstructor
+class CopiedSolution {
+        @Accessors val PartialInterpretation partialInterpretations
+        @Accessors val Map<EObject, EObject> trace
+        @Accessors val long copierRuntime
+        @Accessors var boolean current = true
+}
+/**
+ * Based on {@link SolutionStore.BestSolutionSaver}.
+ * 
+ * Will also automatically fill any missing numerical values in the saved solutions
+ * using the supplied {@link NumericSolver}.
+ */
+class SolutionCopier {
+        val copiedSolutions = new LinkedHashMap<Object, CopiedSolution>
+        @Accessors NumericSolver numericSolver
+        long startTime = System.nanoTime
+        @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0
+        def void copySolution(ThreadContext context, Object solutionId) {
+                val existingCopy = copiedSolutions.get(solutionId)
+                if (existingCopy === null) {
+                        val copyStart = System.nanoTime
+                        val solution = context.model as PartialInterpretation
+                        val copier = new EcoreUtil.Copier
+                        val copiedPartialInterpretation = copier.copy(solution) as PartialInterpretation
+                        copier.copyReferences
+                        totalCopierRuntime += System.nanoTime - copyStart
+                        val copierRuntime = System.nanoTime - startTime
+                        val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime)
+                        //numericSolver?.fillSolutionCopy(copiedSolution.trace)
+                        copiedSolutions.put(solutionId, copiedSolution)
+                } else {
+                        existingCopy.current = true
+                }
+        }
+        def void markAsObsolete(Object solutionId) {
+                val copiedSolution = copiedSolutions.get(solutionId)
+                if (copiedSolution === null) {
+                        throw new IllegalStateException("No solution to mark as obsolete for state code: " + solutionId)
+                }
+                copiedSolution.current = false
+        }
+        def List<PartialInterpretation> getPartialInterpretations(boolean currentOnly) {
+                getListOfCopiedSolutions(currentOnly).map[partialInterpretations]
+        }
+        def List<Map<EObject, EObject>> getTraces(boolean currentOnly) {
+                getListOfCopiedSolutions(currentOnly).map[trace]
+        }
+        def List<Long> getAllCopierRuntimes(boolean currentOnly) {
+                getListOfCopiedSolutions(currentOnly).map[copierRuntime]
+        }
+        def List<CopiedSolution> getListOfCopiedSolutions(boolean currentOnly) {
+                val values = copiedSolutions.values
+                val filteredSolutions = if (currentOnly) {
+                                values.filter[current]
+                        } else {
+                                values
+                        }
+                ImmutableList.copyOf(filteredSolutions)
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
index a8b7301e..4bd2c349 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
@@ -1,14 +1,12 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
-import java.util.List
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
 import java.util.LinkedList
-import org.eclipse.emf.ecore.EObject
+import java.util.List
 import java.util.Map
+import org.eclipse.emf.ecore.EObject
 import org.eclipse.emf.ecore.util.EcoreUtil
 import org.eclipse.viatra.dse.base.ThreadContext
-import java.util.TreeMap
-import java.util.SortedMap
 class SolutionStoreWithCopy {
        
@@ -25,7 +23,7 @@ class SolutionStoreWithCopy {
                newSolution(context)
        }*/
        
-        def newSolution(ThreadContext context) {
+        def Map<EObject,EObject> newSolution(ThreadContext context) {
                //print(System.nanoTime-initTime + ";")
                val copyStart = System.nanoTime
                val solution = context.model as PartialInterpretation
@@ -36,6 +34,7 @@ class SolutionStoreWithCopy {
                copyTraces.add(copier)
                runtime += System.nanoTime - copyStart
                solutionTimes.add(System.nanoTime-sartTime)
+                return copier
        }
        def getSumRuntime() {
                return runtime
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..e1582d3b 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
@@ -1,15 +1,15 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator
 import java.util.Comparator
 import org.eclipse.viatra.dse.base.ThreadContext
-import org.eclipse.viatra.dse.objectives.IObjective
 import org.eclipse.viatra.dse.objectives.Comparators
+import org.eclipse.viatra.dse.objectives.IObjective
 class UnfinishedMultiplicityObjective implements IObjective {
-        val MultiplicityGoalConstraintCalculator unfinishedMultiplicity;
+        val MultiplicityGoalConstraintCalculator unfinishedMultiplicity
        
-        public new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {
+        new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {
                this.unfinishedMultiplicity = unfinishedMultiplicity
        }
        
@@ -29,9 +29,13 @@ class UnfinishedMultiplicityObjective implements IObjective {
        override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }
        
        override setComparator(Comparator<Double> comparator) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+                throw new UnsupportedOperationException
        }
        override setLevel(int level) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+                throw new UnsupportedOperationException
+        }
+        def isContainment() {
+                return this.unfinishedMultiplicity.containment
        }
-}
-\ No newline at end of file
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
index e0111cf6..1b61ffa5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
@@ -1,56 +1,64 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
-import org.eclipse.viatra.dse.objectives.IObjective
+import 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..e00f76ff
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
@@ -0,0 +1,250 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.DirectionalThresholdObjective
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IObjectiveBoundsProvider
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
+import java.util.HashMap
+import java.util.Map
+import org.eclipse.viatra.dse.api.DSEException
+import org.eclipse.viatra.dse.api.Solution
+import org.eclipse.viatra.dse.api.SolutionTrajectory
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.dse.objectives.Fitness
+import org.eclipse.viatra.dse.objectives.IObjective
+import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper
+import org.eclipse.viatra.dse.solutionstore.SolutionStore.ISolutionSaver
+import org.eclipse.xtend.lib.annotations.Accessors
+/**
+ * Based on {@link SolutionStore.BestSolutionSaver}.
+ * 
+ * Will also automatically fill any missing numerical values in the saved solutions
+ * using the supplied {@link NumericSolver}.
+ */
+class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsProvider {
+        static val TOLERANCE = 1e-10
+        @Accessors val SolutionCopier solutionCopier
+        @Accessors val DiversityChecker diversityChecker
+        val IObjective[][] leveledExtremalObjectives
+        val boolean hasExtremalObjectives
+        val int numberOfRequiredSolutions
+        val ObjectiveComparatorHelper comparatorHelper
+        val Map<SolutionTrajectory, Fitness> trajectories = new HashMap
+        @Accessors var NumericSolver numericSolver
+        @Accessors var Map<Object, Solution> solutionsCollection
+        new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) {
+                this.diversityChecker = diversityChecker
+                comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives)
+                this.leveledExtremalObjectives = leveledExtremalObjectives
+                hasExtremalObjectives = leveledExtremalObjectives.exists[!empty]
+                this.numberOfRequiredSolutions = numberOfRequiredSolutions
+                this.solutionCopier = new SolutionCopier
+        }
+        
+        def setNumericSolver(NumericSolver numericSolver) {
+                this.numericSolver = numericSolver
+                solutionCopier.numericSolver = numericSolver
+        }
+        override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
+                if (hasExtremalObjectives) {
+                        saveBestSolutionOnly(context, id, solutionTrajectory)
+                } else {
+                        saveAnyDiverseSolution(context, id, solutionTrajectory)
+                }
+        }
+        private def saveBestSolutionOnly(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
+                val fitness = context.lastFitness
+                if (!shouldSaveSolution(fitness, context)) {
+                        return false
+                }
+                println("Found: " + fitness)
+                val dominatedTrajectories = newArrayList
+                for (entry : trajectories.entrySet) {
+                        val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value)
+                        if (isLastFitnessBetter < 0) {
+                                // Found a trajectory that dominates the current one, no need to save
+                                return false
+                        }
+                        if (isLastFitnessBetter > 0) {
+                                dominatedTrajectories += entry.key
+                        }
+                }
+                if (dominatedTrajectories.size == 0 && !needsMoreSolutionsWithSameFitness) {
+                        return false
+                }
+                if (!diversityChecker.newSolution(context, id, dominatedTrajectories.map[solution.stateCode])) {
+                        return false
+                }
+                // We must save the new trajectory before removing dominated trajectories
+                // to avoid removing the current solution when it is reachable only via dominated trajectories.
+                val solutionSaved = basicSaveSolution(context, id, solutionTrajectory, fitness)
+                for (dominatedTrajectory : dominatedTrajectories) {
+                        trajectories -= dominatedTrajectory
+                        val dominatedSolution = dominatedTrajectory.solution
+                        if (!dominatedSolution.trajectories.remove(dominatedTrajectory)) {
+                                throw new DSEException(
+                                        "Dominated solution is not reachable from dominated trajectory. This should never happen!")
+                        }
+                        if (dominatedSolution.trajectories.empty) {
+                                val dominatedSolutionId = dominatedSolution.stateCode
+                                solutionCopier.markAsObsolete(dominatedSolutionId)
+                                solutionsCollection -= dominatedSolutionId
+                        }
+                }
+                solutionSaved
+        }
+        private def saveAnyDiverseSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
+                val fitness = context.lastFitness
+                if (!shouldSaveSolution(fitness, context)) {
+                        return false
+                }
+                if (!diversityChecker.newSolution(context, id, emptyList)) {
+                        return false
+                }
+                basicSaveSolution(context, id, solutionTrajectory, fitness)
+        }
+        private def shouldSaveSolution(Fitness fitness, ThreadContext context) {
+                fitness.satisifiesHardObjectives && (numericSolver === null || numericSolver.currentSatisfiable)
+        }
+        private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory,
+                Fitness fitness) {
+                var boolean solutionSaved = false
+                var dseSolution = solutionsCollection.get(id)
+                if (dseSolution === null) {
+                        solutionCopier.copySolution(context, id)
+                        dseSolution = new Solution(id, solutionTrajectory)
+                        solutionsCollection.put(id, dseSolution)
+                        solutionSaved = true
+                } else {
+                        solutionSaved = dseSolution.trajectories.add(solutionTrajectory)
+                }
+                if (solutionSaved) {
+                        solutionTrajectory.solution = dseSolution
+                        trajectories.put(solutionTrajectory, fitness)
+                }
+                solutionSaved
+        }
+        def fitnessMayBeSaved(Fitness fitness) {
+                if (!hasExtremalObjectives) {
+                        return true
+                }
+                var boolean mayDominate
+                for (existingFitness : trajectories.values) {
+                        val isNewFitnessBetter = comparatorHelper.compare(fitness, existingFitness)
+                        if (isNewFitnessBetter < 0) {
+                                return false
+                        }
+                        if (isNewFitnessBetter > 0) {
+                                mayDominate = true
+                        }
+                }
+                mayDominate || needsMoreSolutionsWithSameFitness
+        }
+        private def boolean needsMoreSolutionsWithSameFitness() {
+                if (solutionsCollection === null) {
+                        // The solutions collection will only be initialized upon saving the first solution.
+                        return true
+                }
+                solutionsCollection.size < numberOfRequiredSolutions
+        }
+        def getTotalCopierRuntime() {
+                solutionCopier.totalCopierRuntime
+        }
+        override computeRequiredBounds(IObjective objective, Bounds bounds) {
+                if (!hasExtremalObjectives) {
+                        return
+                }
+                if (objective instanceof DirectionalThresholdObjective) {
+                        switch (threshold : objective.threshold) {
+                                case ObjectiveThreshold.NO_THRESHOLD: {
+                                        // No threshold to set.
+                                }
+                                ObjectiveThreshold.Exclusive: {
+                                        switch (kind : objective.kind) {
+                                                case HIGHER_IS_BETTER:
+                                                        bounds.tightenLowerBound(Math.floor(threshold.threshold + 1) as int)
+                                                case LOWER_IS_BETTER:
+                                                        bounds.tightenUpperBound(Math.ceil(threshold.threshold - 1) as int)
+                                                default:
+                                                        throw new IllegalArgumentException("Unknown objective kind" + kind)
+                                        }
+                                        if (threshold.clampToThreshold) {
+                                                return
+                                        }
+                                }
+                                ObjectiveThreshold.Inclusive: {
+                                        switch (kind : objective.kind) {
+                                                case HIGHER_IS_BETTER:
+                                                        bounds.tightenLowerBound(Math.ceil(threshold.threshold) as int)
+                                                case LOWER_IS_BETTER:
+                                                        bounds.tightenUpperBound(Math.floor(threshold.threshold) as int)
+                                                default:
+                                                        throw new IllegalArgumentException("Unknown objective kind" + kind)
+                                        }
+                                        if (threshold.clampToThreshold) {
+                                                return
+                                        }
+                                }
+                                default:
+                                        throw new IllegalArgumentException("Unknown threshold: " + threshold)
+                        }
+                        for (level : leveledExtremalObjectives) {
+                                switch (level.size) {
+                                        case 0: {
+                                                // Nothing to do, wait for the next level.
+                                        }
+                                        case 1: {
+                                                val primaryObjective = level.get(0)
+                                                if (primaryObjective != objective) {
+                                                        // There are no worst-case bounds for secondary objectives.
+                                                        return
+                                                }
+                                        }
+                                        default:
+                                                // There are no worst-case bounds for Pareto front calculation.
+                                                return
+                                }
+                        }
+                        val fitnessIterator = trajectories.values.iterator
+                        if (!fitnessIterator.hasNext) {
+                                return
+                        }
+                        val fitness = fitnessIterator.next.get(objective.name)
+                        while (fitnessIterator.hasNext) {
+                                val otherFitness = fitnessIterator.next.get(objective.name)
+                                if (Math.abs(fitness - otherFitness) > TOLERANCE) {
+                                        throw new IllegalStateException("Inconsistent fitness: " + objective.name)
+                                }
+                        }
+                        switch (kind : objective.kind) {
+                                case HIGHER_IS_BETTER:
+                                        if (needsMoreSolutionsWithSameFitness) {
+                                                bounds.tightenLowerBound(Math.floor(fitness) as int)
+                                        } else {
+                                                bounds.tightenLowerBound(Math.floor(fitness + 1) as int)
+                                        }
+                                case LOWER_IS_BETTER:
+                                        if (needsMoreSolutionsWithSameFitness) {
+                                                bounds.tightenUpperBound(Math.ceil(fitness) as int)
+                                        } else {
+                                                bounds.tightenUpperBound(Math.ceil(fitness - 1) as int)
+                                        }
+                                default:
+                                        throw new IllegalArgumentException("Unknown objective kind" + kind)
+                        }
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
index 5a528a9e..6d772f32 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
@@ -1,5 +1,6 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import com.google.common.collect.ImmutableList
 import java.util.ArrayList
 import java.util.Collection
 import org.eclipse.viatra.dse.objectives.Comparators
@@ -12,25 +13,33 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification
 import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 class WF2ObjectiveConverter {
-        
+        static val INVALIDATED_WFS_NAME = "invalidatedWFs"
        def createCompletenessObjective(
-                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF)
+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) {
-        {
+                new UnfinishedWFObjective(unfinishedWF)
-                val res = new ConstraintsObjective('''unfinishedWFs''',
+        }
-                        unfinishedWF.map[
-                                new QueryConstraint(it.fullyQualifiedName,it,2.0)
+        def createInvalidationObjective(
-                        ].toList
+                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
+}