15 files changed, 696 insertions, 104 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend
index 28cf986d..9ef5e091 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend
@@ -1,11 +1,11 @@
-package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
-import org.eclipse.viatra.dse.objectives.IGlobalConstraint
+import org.eclipse.viatra.dse.objectives.IGlobalConstraint
-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
-abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint {
+abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint {
-        val protected ModelGenerationMethod method
+        val protected ModelGenerationMethod method
-        new(ModelGenerationMethod method) {
+        new(ModelGenerationMethod method) {
-                this.method = method
+                this.method = method
-        }
+        }
-}
-\ 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/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index aa02cd30..3033eca7 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -42,6 +42,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer
 import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel
 import org.eclipse.viatra.dse.solutionstore.SolutionStore
 import org.eclipse.viatra.dse.statecode.IStateCoderFactory
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericSolver
 class ViatraReasoner extends LogicReasoner {
        val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()
@@ -66,12 +67,12 @@ class ViatraReasoner extends LogicReasoner {
                dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE)
                val transformationStartTime = System.nanoTime
                val emptySolution = initialiser.initialisePartialInterpretation(problem, viatraConfig.typeScopes).output
                if ((viatraConfig.documentationLevel == DocumentationLevel::FULL ||
                        viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {
                        workspace.writeModel(emptySolution, "init.partialmodel")
                }
                emptySolution.problemConainer = problem
                var BasicScopeGlobalConstraint basicScopeGlobalConstraint = null
                if (viatraConfig.scopePropagatorStrategy == ScopePropagatorStrategy.None) {
@@ -93,7 +94,8 @@ class ViatraReasoner extends LogicReasoner {
                dse.addObjective(new ModelGenerationCompositeObjective(
                        basicScopeGlobalConstraint ?: new ScopeObjective,
                        method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)],
-                        wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF)
+                        wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF),
+                        viatraConfig
                ))
                val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size)
@@ -131,8 +133,9 @@ class ViatraReasoner extends LogicReasoner {
                        }
                solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))
                val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement)
+                val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false)
                val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions,
-                        diversityChecker)
+                        diversityChecker, numericSolver)
                val solutionCopier = solutionSaver.solutionCopier
                solutionStore.withSolutionSaver(solutionSaver)
                dse.solutionStore = solutionStore
@@ -168,10 +171,10 @@ class ViatraReasoner extends LogicReasoner {
                        dse.addTransformationRule(rule)
                }
-                val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method)
+                val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, numericSolver)
                viatraConfig.progressMonitor.workedForwardTransformation
+                val transformationFinished = System.nanoTime
-                val transformationTime = System.nanoTime - transformationStartTime
+                val transformationTime = transformationFinished - transformationStartTime
                val solverStartTime = System.nanoTime
                var boolean stoppedByTimeout
@@ -194,6 +197,15 @@ class ViatraReasoner extends LogicReasoner {
                                        it.value = (pair.value / 1000000) as int
                                ]
                        }
+                        for(x: 0..<strategy.times.size) {
+                                it.entries += createStringStatisticEntry => [
+                                        it.name = '''Solution«x+1»DetailedStatistics'''
+                                        it.value = strategy.times.get(x)
+                                ]
+                        }
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int
+                        ]
                        it.entries += createIntStatisticEntry => [
                                it.name = "TransformationExecutionTime"
                                it.value = (method.statistics.transformationExecutionTime / 1000000) as int
@@ -223,6 +235,24 @@ class ViatraReasoner extends LogicReasoner {
                                it.value = dse.numberOfStates as int
                        ]
                        it.entries += createIntStatisticEntry => [
+                                it.name = "ForwardTime" it.value = (strategy.forwardTime/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "BacktrackingTime" it.value = (strategy.backtrackingTime/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "GlobalConstraintEvaluationTime" it.value = (strategy.globalConstraintEvaluationTime/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "FitnessCalculationTime" it.value = (strategy.fitnessCalculationTime/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "SolutionCopyTime" it.value = (solutionSaver.totalCopierRuntime/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
                                it.name = "Decisions"
                                it.value = method.statistics.decisionsTried
                        ]
@@ -238,7 +268,28 @@ class ViatraReasoner extends LogicReasoner {
                                it.name = "ScopePropagationsSolverCalls"
                                it.value = method.statistics.scopePropagatorSolverInvocations
                        ]
-                        if (diversityChecker.isActive) {
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "NumericalSolverSumTime" it.value = (strategy.numericSolver.runtime/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "NumericalSolverProblemFormingTime" it.value = (strategy.numericSolver.solverFormingProblem/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "NumericalSolverSolvingTime" it.value = (strategy.numericSolver.solverSolvingProblem/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "NumericalSolverInterpretingSolution" it.value = (strategy.numericSolver.solverSolution/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls
+                        ]
+                        it.entries += createIntStatisticEntry => [
+                                it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls
+                        ]
+                        if(diversityChecker.active) {
                                it.entries += createIntStatisticEntry => [
                                        it.name = "SolutionDiversityCheckTime"
                                        it.value = (diversityChecker.totalRuntime / 1000000) as int
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index c0a71c85..ddd25aac 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -54,8 +54,16 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
         * Configuration for cutting search space.
         */
        public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint
+         
-        public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.Polyhedral(
+        public var runIntermediateNumericalConsistencyChecks = true
+        
+        public var punishSize = true
+        public var scopeWeight = 1
+        public var conaintmentWeight = 2
+        public var nonContainmentWeight = 1
+        public var unfinishedWFWeight = 1
+        
+        public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(
                PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)
        
        public var List<LinearTypeConstraintHint> hints = newArrayList
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/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 081e48fa..e529892c 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;
@@ -23,15 +21,13 @@ import java.util.Random;
 import org.apache.log4j.Logger;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.util.EcoreUtil;
+import org.eclipse.viatra.dse.api.SolutionTrajectory;
 import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;
 import org.eclipse.viatra.dse.base.ThreadContext;
 import org.eclipse.viatra.dse.objectives.Fitness;
 import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper;
+import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler;
 import org.eclipse.viatra.dse.solutionstore.SolutionStore;
-import org.eclipse.viatra.query.runtime.api.IPatternMatch;
-import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
-import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;
-import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher;
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
@@ -42,6 +38,7 @@ 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.ViatraReasonerConfiguration;
@@ -79,41 +76,70 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
        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 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();
+                solutionStore.registerSolutionFoundHandler(new ISolutionFoundHandler() {
+                        
+                        @Override
+                        public void solutionTriedToSave(ThreadContext context, SolutionTrajectory trajectory) {
+                                // Ignore.
+                        }
+                        
+                        @Override
+                        public void solutionFound(ThreadContext context, SolutionTrajectory trajectory) {
+                                configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions);
+                                saveTimes();
+                                logger.debug("Found a solution.");
+                        }
+                });
+                numericSolver.init(context);
                
-                ViatraQueryEngine engine = context.getQueryEngine();
+//              ViatraQueryEngine engine = context.getQueryEngine();
-//              // TODO: visualisation
+//              matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
-                matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
+//              for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {
-                for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {
+//                      //System.out.println(p.getSimpleName());
-                        //System.out.println(p.getSimpleName());
+//                      ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);
-                        ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);
+//                      matchers.add(matcher);
-                        matchers.add(matcher);
+//              }
-                }
                
                final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
                this.comparator = new Comparator<TrajectoryWithFitness>() {
@@ -128,23 +154,33 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
        @Override
        public void explore() {
-                if (!context.checkGlobalConstraints()) {
+//              System.out.println("press enter");
+//              try {
+//                      new BufferedReader(new InputStreamReader(System.in)).readLine();
+//              } catch (IOException e) {
+//                      // TODO Auto-generated catch block
+//                      e.printStackTrace();
+//              }
+                this.explorationStarted=System.nanoTime();
+                if (!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 firstfitness = context.calculateFitness();
+                final Fitness firstFitness = calculateFitness();
-                solutionStore.newSolution(context);
+                checkForSolution(firstFitness);
                
                final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
                final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
-                TrajectoryWithFitness currentTrajectoryWithfitness = new TrajectoryWithFitness(firstTrajectory, firstfitness);
+                TrajectoryWithFitness currentTrajectoryWithFitness = new TrajectoryWithFitness(firstTrajectory, firstFitness);
-                trajectoiresToExplore.add(currentTrajectoryWithfitness);
+                trajectoiresToExplore.add(currentTrajectoryWithFitness);
-                
                //if(configuration)
                visualiseCurrentState();
 //              for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
@@ -158,17 +194,17 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                
                mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) {
-                        if (currentTrajectoryWithfitness == null) {
+                        if (currentTrajectoryWithFitness == null) {
                                if (trajectoiresToExplore.isEmpty()) {
                                        logger.debug("State space is fully traversed.");
                                        return;
                                } else {
-                                        currentTrajectoryWithfitness = selectState();
+                                        currentTrajectoryWithFitness = selectState();
                                        if (logger.isDebugEnabled()) {
                                                logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
-                                                logger.debug("New trajectory is chosen: " + currentTrajectoryWithfitness);
+                                                logger.debug("New trajectory is chosen: " + currentTrajectoryWithFitness);
                                        }
-                                        context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithfitness.trajectory);
+                                        context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFitness.trajectory);
                                }
                        }
                        
@@ -193,26 +229,28 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                                visualiseCurrentState();
 //                              for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
-//                                      System.out.println(matcher.getPatternName());
+//                                      int c = matcher.countMatches();
-//                                      System.out.println("---------");
+//                                      if(c>=100) {
-//                                      for(IPatternMatch m : matcher.getAllMatches()) {
+//                                              System.out.println(c+ " " +matcher.getPatternName());
-//                                              System.out.println(m);
 //                                      }
-//                                      System.out.println("---------");
+//                                      
 //                              }
                                
-                                boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
+                                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();
-                                        solutionStore.newSolution(context);
+                                        checkForSolution(nextFitness);
                                        if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) {
                                                logger.debug("Reached max depth.");
                                                context.backtrack();
@@ -223,37 +261,50 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                                                        context.getTrajectory().toArray(), nextFitness);
                                        trajectoiresToExplore.add(nextTrajectoryWithfitness);
-                                        int compare = objectiveComparatorHelper.compare(currentTrajectoryWithfitness.fitness,
+                                        int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFitness.fitness,
                                                        nextTrajectoryWithfitness.fitness);
                                        if (compare < 0) {
                                                logger.debug("Better fitness, moving on: " + nextFitness);
-                                                currentTrajectoryWithfitness = nextTrajectoryWithfitness;
+                                                currentTrajectoryWithFitness = nextTrajectoryWithfitness;
                                                continue mainLoop;
                                        } else if (compare == 0) {
                                                logger.debug("Equally good fitness, moving on: " + nextFitness);
-                                                currentTrajectoryWithfitness = nextTrajectoryWithfitness;
+                                                currentTrajectoryWithFitness = nextTrajectoryWithfitness;
                                                continue mainLoop;
                                        } else {
                                                logger.debug("Worse fitness.");
-                                                currentTrajectoryWithfitness = null;
+                                                currentTrajectoryWithFitness = null;
                                                continue mainLoop;
                                        }
                                }
                        }
                        logger.debug("State is fully traversed.");
-                        trajectoiresToExplore.remove(currentTrajectoryWithfitness);
+                        trajectoiresToExplore.remove(currentTrajectoryWithFitness);
-                        currentTrajectoryWithfitness = 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++;
@@ -262,6 +313,37 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                return activationIds;
        }
+        private void checkForSolution(final Fitness fittness) {
+                solutionStore.newSolution(context);
+        }
+        
+        public List<String> times = new LinkedList<String>();
+        private void saveTimes() {
+                long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder<?, ?>)this.context.getStateCoder()).getStatecoderRuntime()/1000000;
+                long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000;
+                long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000;
+                long activationSelection = this.activationSelector.getRuntime()/1000000;
+                long solutionCopierTime = this.solutionSaver.getTotalCopierRuntime()/1000000;
+                long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000;
+                long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000;
+                long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000;
+                long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000;
+                this.times.add(
+                        "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ 
+                        "|StateCoderTime:"+statecoderTime+
+                        "|ForwardTime:"+forwardTime+
+                        "|Backtrackingtime:"+backtrackingTime+
+                        "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+
+                        "|FitnessCalculationTime:"+(fitnessCalculationTime/1000000)+
+                        "|ActivationSelectionTime:"+activationSelection+
+                        "|SolutionCopyTime:"+solutionCopierTime+
+                        "|NumericalSolverSumTime:"+numericalSolverSumTime+
+                        "|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+
+                        "|NumericalSolverSolvingTime:"+numericalSolverSolving+
+                        "|NumericalSolverInterpretingSolution:"+numericalSolverInterpreting+")");
+                
+        }
        @Override
        public void interruptStrategy() {
                isInterrupted = true;
@@ -288,7 +370,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                } else {
                        return trajectoiresToExplore.element();
                }
-        }       
+        }
        public void visualiseCurrentState() {
                PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser;
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/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 2976bebe..d2faaa65 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,36 +1,58 @@
 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.xtend.lib.annotations.FinalFieldsConstructor
-//class ViatraReasonerNumbers {
-//      public static val scopePriority = 2
-//      public static val unfinishedMultiplicityPriority = 2
-//      public static val unifinshedWFPriority = 2
-//      //public static val complexityPriority = 4
-//      
-//      public static val scopeWeigth = 1.0
-//      public static val unfinishedMultiplicityWeigth = 1.5
-//      public static val unfinishedWFWeigth = 1.5
-//      //public static val complexityWeigth = 0.1
-//      
-//      public static val useCompositeObjective = true
-//      public static val compositePriority = 2
-//}
-@FinalFieldsConstructor
 class ModelGenerationCompositeObjective implements IThreeValuedObjective {
        val IObjective scopeObjective
-        val List<IObjective> unfinishedMultiplicityObjectives
+        val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives
-        val IObjective unfinishedWFObjective
+        val UnfinishedWFObjective unfinishedWFObjective
+        var PartialInterpretation model = null
+        val boolean punishSize
+        val int scopeWeight
+        val int conaintmentWeight
+        val int nonContainmentWeight
+        val int unfinishedWFWeight
+        
+        new(
+                IObjective scopeObjective,
+                List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
+                UnfinishedWFObjective unfinishedWFObjective,
+                ViatraReasonerConfiguration configuration)
+        {
+                this(
+                        scopeObjective, unfinishedMultiplicityObjectives, unfinishedWFObjective, configuration.punishSize,
+                        configuration.scopeWeight, configuration.conaintmentWeight, configuration.nonContainmentWeight,
+                        configuration.unfinishedWFWeight
+                )
+        }
+        new(
+                IObjective scopeObjective,
+                List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
+                UnfinishedWFObjective unfinishedWFObjective,
+                boolean punishSize, int scopeWeight, int conaintmentWeight, int nonContainmentWeight, int unfinishedWFWeight)
+        {
+                this.scopeObjective = scopeObjective
+                this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives
+                this.unfinishedWFObjective = unfinishedWFObjective
+                
+                this.punishSize = punishSize
+                this.scopeWeight = scopeWeight
+                this.conaintmentWeight = conaintmentWeight
+                this.nonContainmentWeight = nonContainmentWeight
+                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)
@@ -39,27 +61,40 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective {
        override createNew() {
                return new ModelGenerationCompositeObjective(
                        scopeObjective.createNew,
-                        ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew]),
+                        ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew as UnfinishedMultiplicityObjective]),
-                        unfinishedWFObjective.createNew
+                        unfinishedWFObjective.createNew as UnfinishedWFObjective,
+                        punishSize, 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) {
+                for(multiplicityObjective : unfinishedMultiplicityObjectives) {
-                        multiplicity += multiplicityObjective.getFitness(context) // *0.5
+                        if(multiplicityObjective.containment) {
+                                containmentMultiplicity+=multiplicityObjective.getFitness(context)
+                        } else {
+                                nonContainmentMultiplicity+=multiplicityObjective.getFitness(context)
+                        }
                }
-                sum += multiplicity
+                val size = if(punishSize) {
-                sum += unfinishedWFsFitness // *0.5
+                        0.9/model.newElements.size
-//              println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
+                } else {
+                        0
+                }
+                
+                var sum = 0.0
+                sum += scopeFitnes*scopeWeight
+                sum += containmentMultiplicity*conaintmentWeight
+                sum += nonContainmentMultiplicity*nonContainmentWeight
+                sum += unfinishedWFsFitness*unfinishedWFWeight
+                sum+=size
                return sum
        }
        
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..066040a0
--- /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.logic2viatra.ModelGenerationMethod
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
+import 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 b63bfe8b..cfd11816 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
@@ -153,14 +153,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
        }
 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
index d036257d..38c8f5a1 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
@@ -19,12 +19,23 @@ class CopiedSolution {
        @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 NumericSolver numericSolver
        val copiedSolutions = new LinkedHashMap<Object, CopiedSolution>
        long startTime = System.nanoTime
        @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0
+        new(NumericSolver numericSolver) {
+                this.numericSolver = numericSolver
+        }
        def void copySolution(ThreadContext context, Object solutionId) {
                val existingCopy = copiedSolutions.get(solutionId)
                if (existingCopy === null) {
@@ -36,6 +47,7 @@ class SolutionCopier {
                        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
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
new file mode 100644
index 00000000..4bd2c349
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
@@ -0,0 +1,51 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import java.util.LinkedList
+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
+class SolutionStoreWithCopy {
+        
+        long runtime = 0
+        List<PartialInterpretation> solutions = new LinkedList
+        //public List<SortedMap<String,Integer>> additionalMatches = new LinkedList
+        List<Map<EObject,EObject>> copyTraces = new LinkedList
+        
+        long sartTime = System.nanoTime
+        List<Long> solutionTimes = new LinkedList
+        
+        /*def newSolution(ThreadContext context, SortedMap<String,Integer> additonalMatch) {
+                additionalMatches+= additonalMatch
+                newSolution(context)
+        }*/
+        
+        def Map<EObject,EObject> newSolution(ThreadContext context) {
+                //print(System.nanoTime-initTime + ";")
+                val copyStart = System.nanoTime
+                val solution = context.model as PartialInterpretation
+                val copier = new EcoreUtil.Copier
+                val solutionCopy = copier.copy(solution) as PartialInterpretation
+                copier.copyReferences
+                solutions.add(solutionCopy)
+                copyTraces.add(copier)
+                runtime += System.nanoTime - copyStart
+                solutionTimes.add(System.nanoTime-sartTime)
+                return copier
+        }
+        def getSumRuntime() {
+                return runtime
+        }
+        def getAllRuntimes() {
+                return solutionTimes
+        }
+        def getSolutions() {
+                solutions
+        }
+        def getCopyTraces() {
+                return copyTraces
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/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 9f0c642f..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
@@ -7,7 +7,7 @@ import org.eclipse.viatra.dse.objectives.Comparators
 import org.eclipse.viatra.dse.objectives.IObjective
 class UnfinishedMultiplicityObjective implements IObjective {
-        val MultiplicityGoalConstraintCalculator unfinishedMultiplicity;
+        val MultiplicityGoalConstraintCalculator unfinishedMultiplicity
        
        new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {
                this.unfinishedMultiplicity = unfinishedMultiplicity
@@ -34,4 +34,8 @@ class UnfinishedMultiplicityObjective implements IObjective {
        override setLevel(int level) {
                throw new UnsupportedOperationException
        }
+        def isContainment() {
+                return this.unfinishedMultiplicity.containment
+        }
 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
index 74500cc2..d879d4cc 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
@@ -14,9 +14,12 @@ 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 {
-        @Accessors val solutionCopier = new SolutionCopier
+        @Accessors val SolutionCopier solutionCopier
        @Accessors val DiversityChecker diversityChecker
        val boolean hasExtremalObjectives
        val int numberOfRequiredSolutions
@@ -25,11 +28,12 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
        @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection
-        new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) {
+        new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker, NumericSolver numericSolver) {
                this.diversityChecker = diversityChecker
                comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives)
                hasExtremalObjectives = leveledExtremalObjectives.exists[!empty]
                this.numberOfRequiredSolutions = numberOfRequiredSolutions
+                this.solutionCopier = new SolutionCopier(numericSolver)
        }
        override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
@@ -139,4 +143,8 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
                }
                solutionsCollection.size < numberOfRequiredSolutions
        }
+        
+        def getTotalCopierRuntime() {
+                solutionCopier.totalCopierRuntime
+        }
 }
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 63d78220..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
@@ -13,12 +13,10 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification
 import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 class WF2ObjectiveConverter {
-        static val UNFINISHED_WFS_NAME = "unfinishedWFs"
        static val INVALIDATED_WFS_NAME = "invalidatedWFs"
        def createCompletenessObjective(
                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) {
-                // createConstraintObjective(UNFINISHED_WFS_NAME, unfinishedWF)
                new UnfinishedWFObjective(unfinishedWF)
        }