38 files changed, 2171 insertions, 501 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
index e45ec1c8..6fbbc779 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
@@ -27,6 +27,7 @@ import java.util.Set
 import org.eclipse.viatra.query.runtime.api.IPatternMatch
 import org.eclipse.viatra.query.runtime.api.IQuerySpecification
 import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
 import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
 import org.eclipse.xtend.lib.annotations.Data
@@ -83,6 +84,9 @@ class ModelGenerationStatistics {
        Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
+        Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions
+        Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions
        Map<String, ModalPatternQueries> modalRelationQueries
        Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
@@ -120,12 +124,13 @@ class ModelGenerationMethodProvider {
                        workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles)
                val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics)
                scopePropagator.propagateAllScopeConstraints
-                val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator,
+                val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution,
-                        nameNewElements, statistics)
+                        queries, scopePropagator, nameNewElements, statistics)
                val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator,
                        statistics)
-                val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries)
+                val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries)
                val unfinishedWF = queries.getUnfinishedWFQueries.values
                val modalRelationQueriesBuilder = ImmutableMap.builder
@@ -138,6 +143,9 @@ class ModelGenerationMethodProvider {
                val modalRelationQueries = modalRelationQueriesBuilder.build
                val invalidWF = queries.getInvalidWFQueries.values
+                
+                val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns
+                val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns
                return new ModelGenerationMethod(
                        statistics,
@@ -146,6 +154,8 @@ class ModelGenerationMethodProvider {
                        unfinishedMultiplicities,
                        unfinishedWF,
                        invalidWF,
+                        mustUnitPropagationPreconditions,
+                        currentUnitPropagationPreconditions,
                        modalRelationQueries,
                        queries.allQueries
                )
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java
new file mode 100644
index 00000000..2288ad7e
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java
@@ -0,0 +1,8 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra;
+public enum PropagationModality {
+        /**The value was originally ? and set to 1 */
+        UP, 
+        /**The value was originally ? and set to 0 */
+        DOWN
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
index 86a59aa1..034420d6 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
@@ -7,26 +7,39 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 import org.eclipse.viatra.query.runtime.emf.EMFScope
 class MultiplicityGoalConstraintCalculator {
-        val String targetRelationName;
+        val String targetRelationName
-        val IQuerySpecification<?> querySpecification;
+        val IQuerySpecification<?> querySpecification
-        var ViatraQueryMatcher<?> matcher;
+        var ViatraQueryMatcher<?> matcher
+        val int minValue
+        val boolean containment
+        val int cost
                
-        new(String targetRelationName, IQuerySpecification<?> querySpecification) {
+        public new(String targetRelationName, IQuerySpecification<?> querySpecification, int minValue, boolean containment, int cost) {
                this.targetRelationName = targetRelationName
                this.querySpecification = querySpecification
                this.matcher = null
+                this.minValue = minValue
+                this.containment = containment
+                this.cost = cost
        }
        
        new(MultiplicityGoalConstraintCalculator other) {
                this.targetRelationName = other.targetRelationName
                this.querySpecification = other.querySpecification
                this.matcher = null
+                this.minValue = other.minValue
+                this.containment = other.containment
+                this.cost = other.cost
        }
        
        def getName() {
                targetRelationName
        }
        
+        def isContainment() {
+                return containment
+        }
        def init(Notifier notifier) {
                val engine = ViatraQueryEngine.on(new EMFScope(notifier))
                matcher = querySpecification.getMatcher(engine)
@@ -36,11 +49,17 @@ class MultiplicityGoalConstraintCalculator {
                var res = 0
                val allMatches = this.matcher.allMatches
                for(match : allMatches) {
-                        //println(targetRelationName+ " missing multiplicity: "+match.get(3))
+                        val existingMultiplicity = match.get(4) as Integer
-                        val missingMultiplicity = match.get(2) as Integer
+                        if(existingMultiplicity < this.minValue) {
-                        res += missingMultiplicity
+                                val missingMultiplicity = this.minValue-existingMultiplicity
+                                res += missingMultiplicity
+                        }
+//                      if(missingMultiplicity!=0) {
+//                              println(targetRelationName+ " missing multiplicity: "+missingMultiplicity)
+//                      }
                }
-                //println(targetRelationName+ " all missing multiplicities: "+res)
+//              if(res>0)
-                return res
+//              println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost)
+                return res*cost
        }
 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
index 51dba244..120fb18a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
@@ -187,16 +187,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                if (bounds.upperBound !== null && bounds.upperBound < 0) {
                        throw new IllegalArgumentException("Negative upper bound: " + bounds)
                }
-        }
+        } 
-        private def setScopesInvalid() {
-                partialInterpretation.minNewElements = Integer.MAX_VALUE
-                partialInterpretation.maxNewElements = 0
-                for (scope : partialInterpretation.scopes) {
-                        scope.minNewElements = Integer.MAX_VALUE
-                        scope.maxNewElements = 0
-                }
-        }
        private static def <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> matcher,
                PartialInterpretation p) {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
index 2376fb38..8f3a5bb0 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
@@ -79,7 +79,7 @@ class ScopePropagator {
                // Nothing to propagate.
        }
-        def propagateAdditionToType(PartialTypeInterpratation t) {
+        def decrementTypeScope(PartialTypeInterpratation t) {
 //              println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
                val targetScope = type2Scope.get(t)
                if (targetScope !== null) {
@@ -96,15 +96,23 @@ class ScopePropagator {
                if (this.partialInterpretation.maxNewElements > 0) {
                        this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1
                } else if (this.partialInterpretation.maxNewElements === 0) {
-                        throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''')
+                        setScopesInvalid()
                }
-                propagateAllScopeConstraints
 //              println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''')
 //              println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''')
 //              this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]
 //              println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
        }
+        
+        protected def setScopesInvalid() {
+                partialInterpretation.minNewElements = Integer.MAX_VALUE
+                partialInterpretation.maxNewElements = 0
+                for (scope : partialInterpretation.scopes) {
+                        scope.minNewElements = Integer.MAX_VALUE
+                        scope.maxNewElements = 0
+                }
+        }
        def void propagateAdditionToRelation(Relation r) {
                // Nothing to propagate.
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
index e511a961..fd4374f5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
@@ -11,7 +11,5 @@ import org.eclipse.xtend.lib.annotations.Data
 class CanonisedFormulae {
        CharSequence viatraCode
        Map<Assertion,String> assertion2ConstraintPattern
-        Map<ConstantDefinition,String> constant2ValuePattern
        Map<RelationDefinition,String> relation2ValuePattern
-        Map<FunctionDefinition,String> function2ValuePattern
 }
 \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
index 0af0b36a..182f3a3a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
@@ -5,17 +5,35 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
 import java.util.List
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
 /**
- * Translates a set of assertions and definitions to viatra patterns.
+ * Translates a Terms into format
+ * <P(x1,...,xn)> := Bodies(x1,...,xn)
+ * <Bodies(x1,...,xn)> := <Body(x1,...,xn)> | <Body(x1,...,xn)> or <Bodies(x1,...,xn)>
+ * <Body(x1,...,xn)> := Exists y1,...,ym : <Constraints(x1,...,xn,y1,....,ym)>
+ * <Constraints(x1,...,xn)> := Constraint(x1,...xn) | Constraint(x1,...,xn) and <Constraints(x1,...,xn)>   
 */
 class FormulaCanoniser {
-        def canonise(
+//      def canonise(
-                List<Assertion> assertions,
+//              List<Assertion> assertions,
-                List<RelationDefinition> relations,
+//              List<RelationDefinition> relations)
-                List<ConstantDefinition> constants,
+//      {
-                List<FunctionDefinition> functions)
+//              
-        {
+//      }
-                
+//      
-        }
+//      
+//      def canoniseToConstraintBlock(Term predicate, List<Variable> variables) {
+//              val 
+//      }
+//      
+//      def freeVariables(Term t) {
+//              val subterms = #[t]+t.eAllContents.toList
+//              val variables = subterms.filter(Variable).toSet
+//              val variableReferences = subterms.filter(SymbolicValue).filter[it.symbolicReference instanceof Variable]
+//              val freeVariables = variableReferences.filter[!variables.contains(it.symbolicReference)]
+//              return freeVariables.map
+//      }
 }
 \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
new file mode 100644
index 00000000..dd5cade1
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
@@ -0,0 +1,275 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
+import hu.bme.mit.inf.dslreasoner.viatra2logic.XExpressionExtractor
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
+import org.eclipse.emf.ecore.EAttribute
+import org.eclipse.emf.ecore.EEnumLiteral
+import org.eclipse.emf.ecore.EReference
+import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
+import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
+import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
+import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
+import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.VariableMapping
+import java.util.List
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
+import java.util.Map
+class PConstraintTransformer {
+        val extension RelationDefinitionIndexer relationDefinitionIndexer;
+        val expressionExtractor = new XExpressionExtractor
+        val expressionGenerator = new PExpressionGenerator
+        
+        new(RelationDefinitionIndexer relationDefinitionIndexer) {
+                this.relationDefinitionIndexer = relationDefinitionIndexer
+        }
+        
+        dispatch def transformConstraint(TypeConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
+                val touple = constraint.variablesTuple
+                if(touple.size == 1) {
+                        val inputKey = constraint.equivalentJudgement.inputKey
+                        if(inputKey instanceof EClassTransitiveInstancesKey) {
+                                return relationDefinitionIndexer.base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
+                                        constraint.getVariableInTuple(0).canonizeName)
+                        } else if(inputKey instanceof EDataTypeInSlotsKey){
+                                return '''// type constraint is enforced by construction'''
+                        }
+                        
+                } else if(touple.size == 2){
+                        val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
+                        if(key instanceof EReference) {
+                                return base.referRelationByName(
+                                        key,
+                                        constraint.getVariableInTuple(0).canonizeName,
+                                        constraint.getVariableInTuple(1).canonizeName,
+                                        modality.toMustMay)
+                        } else if (key instanceof EAttribute) {
+                                return base.referAttributeByName(key,
+                                        constraint.getVariableInTuple(0).canonizeName,
+                                        constraint.getVariableInTuple(1).canonizeName,
+                                        modality.toMustMay)
+                        } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
+                } else {
+                        throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
+                }
+        }
+        dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
+                val touple = constraint.variablesTuple
+                if(touple.size == 1) {
+                        val inputKey = constraint.equivalentJudgement.inputKey
+                        if(inputKey instanceof EClassTransitiveInstancesKey) {
+                                return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
+                                        (constraint.getVariablesTuple.get(0) as PVariable).canonizeName)
+                        } else if(inputKey instanceof EDataTypeInSlotsKey){
+                                return '''// type constraint is enforced by construction'''
+                        }
+                        
+                } else if(touple.size == 2){
+                        val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
+                        if(key instanceof EReference) {
+                                return base.referRelationByName(
+                                        key,
+                                        (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
+                                        (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
+                                        modality.toMustMay)
+                        } else if (key instanceof EAttribute) {
+                                return base.referAttributeByName(key,
+                                        (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
+                                        (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
+                                        modality.toMustMay)
+                        } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
+                } else {
+                        throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
+                }
+        }
+        
+        dispatch def transformConstraint(Equality equality, Modality modality, List<VariableMapping> variableMapping) {
+                val a = equality.who
+                val b = equality.withWhom
+                transformEquality(modality.toMustMay, a, b)
+        }
+        
+        private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) {
+                if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
+                else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
+        }       
+        
+        dispatch def transformConstraint(Inequality inequality, Modality modality, List<VariableMapping> variableMapping) {
+                val a = inequality.who
+                val b = inequality.withWhom
+                if(modality.isCurrent) {
+                        return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
+                } else if(modality.isMust) {
+                        return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
+                } else { // modality.isMay
+                        return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
+                }
+        }
+        
+        dispatch def transformConstraint(NegativePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
+                val params = (0..<pcall.actualParametersTuple.size).map[index | 
+                        val variable = pcall.actualParametersTuple.get(index) as PVariable
+                        return variable.canonizeName
+                ]
+                return referPattern(pcall.referredQuery,params,modality.dual,false,false)
+        }
+        
+        dispatch def transformConstraint(PositivePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
+                val params = (0..<pcall.variablesTuple.size).map[index | 
+                        val variable = pcall.variablesTuple.get(index) as PVariable
+                        return variable.canonizeName
+                ]
+                return referPattern(pcall.referredQuery,params,modality,true,false)
+        }
+        dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality, List<VariableMapping> variableMapping) {
+                val params = (0..1).map[index | 
+                        val variable = pcall.getVariableInTuple(index) as PVariable
+                        return variable.canonizeName
+                ]
+                return referPattern(pcall.referredQuery,params,modality,true,true)
+        }
+        dispatch def transformConstraint(ExportedParameter e, Modality modality, List<VariableMapping> variableMapping) {
+                val v1 = '''var_«e.parameterName»'''
+                val v2 = e.parameterVariable.canonizeName
+                if(v1.compareTo(v2) == 0) {
+                        return '''// «v1» exported'''
+                } else {
+                        return '''«v1» == «v2»;'''
+                }
+        }
+        dispatch def transformConstraint(ConstantValue c, Modality modality, List<VariableMapping> variableMapping) {
+                val target = c.supplierKey
+                
+                var String targetString;
+                var String additionalDefinition;
+                if(target instanceof EEnumLiteral) {
+                        targetString = '''const_«target.name»_«target.EEnum.name»'''
+                        additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»");  //LogicProblem.elements(problem,«targetString»);'''
+                } else if(target instanceof Integer) {
+                        targetString = '''const_«target»_Integer'''
+                        additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); IntegerElement.value(«targetString»,«target»);'''
+                } else if(target instanceof Boolean) {
+                        targetString = '''const_«target»_Boolean'''
+                        additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); BooleanElement.value(«targetString»,«target»);'''
+                } else if(target instanceof String) {
+                        targetString = '''const_«target»_String'''
+                        additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); StringElement.value(«targetString»,"«target»");'''
+                } else if(target instanceof Double) {
+                        targetString = '''const_«target»_Real'''
+                        additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
+                } else if(target instanceof Float) {
+                        targetString = '''const_«target»_Real'''
+                        additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
+                } else {
+                        throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')
+                }
+                
+                val source = c.variablesTuple
+                var String sourceName
+                if(source.size == 1)
+                        sourceName = (source.get(0) as PVariable).canonizeName
+                else throw new UnsupportedOperationException("unknown source")
+                return '''«sourceName» == «targetString»;«additionalDefinition»''';
+        }
+        
+        protected def valueVariable(PVariable v) {
+                "value_"+v.canonizeName
+        }
+        protected def valueSetted(PVariable v) {
+                "setted_"+v.canonizeName
+        }
+        def hasValue(PVariable v, String target, Modality m, List<VariableMapping> variableMapping) {
+                val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference
+                if(m.isMay) {
+                        '''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpressionByRef(typeReference,v,v.valueVariable)»
+«««                  check(!«v.valueSetted»||«v.valueVariable»==«target»));
+'''
+                } else { // Must or current
+                        '''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpressionByRef(typeReference,v,target)»'''
+                }
+        }
+        
+        private def hasValueExpression(List<VariableMapping> variableMapping, PVariable v, String target) {
+                val mapping = variableMapping.filter[
+                        val v2 = (it.sourcePVariable as PVariable)
+                        v2 === v
+                ].head
+                val range = mapping.targetLogicVariable.range
+                hasValueExpressionByRef(
+                        range,
+                        v,
+                        target
+                )
+        }
+        private def dispatch hasValueExpressionByRef(BoolTypeReference typeReference, PVariable v, String target)       '''BooleanElement.value(«v.canonizeName»,«target»);'''
+        private def dispatch hasValueExpressionByRef(IntTypeReference typeReference, PVariable v, String target)                '''IntegerElement.value(«v.canonizeName»,«target»);'''
+        private def dispatch hasValueExpressionByRef(RealTypeReference typeReference, PVariable v, String target)       '''RealElement.value(«v.canonizeName»,«target»);'''
+        private def dispatch hasValueExpressionByRef(StringTypeReference typeReference, PVariable v, String target)     '''StringElement.value(«v.canonizeName»,«target»);'''
+        private def dispatch hasValueExpressionByRef(TypeReference typeReference, PVariable v, String target) {
+                throw new UnsupportedOperationException('''Unsupported primitive type reference: «typeReference.class»''')
+        }
+        
+        dispatch def transformConstraint(ExpressionEvaluation e, Modality modality, List<VariableMapping> variableMapping) {
+                if(e.outputVariable!==null) {
+                        throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''')
+                } else {
+                        val expression = expressionExtractor.extractExpression(e.evaluator)
+                        val Map<PVariable, PrimitiveTypeReference> variable2Type = e.affectedVariables.toInvertedMap[v|variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference]
+                        if(modality.isMay) {
+                                return '''
+                                        «FOR variable: e.affectedVariables»
+                                                PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
+                                        «ENDFOR»
+«««                                  check(
+«««                                          «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»
+«««                                          «IF variable2Type.values.filter(RealTypeReference).empty»
+«««                                          ||
+«««                                          («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»)
+«««                                          «ENDIF»
+«««                                  );
+                                '''
+                        } else { // Must or Current
+                                return '''
+                                        «FOR variable: e.affectedVariables»
+                                                PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
+                                        «ENDFOR»
+«««                                  «IF variable2Type.values.filter(RealTypeReference).empty»
+«««                                          check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»);
+«««                                  «ENDIF»
+                                '''
+                        }
+                }
+        }
+        dispatch def transformConstraint(PConstraint c, Modality modality, List<VariableMapping> variableMapping) {
+                throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
+        }
+        
+        dispatch def transformConstraintUnset(ExpressionEvaluation e, List<VariableMapping> variableMapping) {
+                return '''
+                        «FOR variable: e.affectedVariables»
+                                PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
+                        «ENDFOR»
+«««                  check(«FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»);
+                '''
+        }
+        
+        dispatch def transformConstraintUnset(PConstraint c, List<VariableMapping> variableMapping) {
+                throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
new file mode 100644
index 00000000..62ff92b2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
@@ -0,0 +1,116 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
+import java.util.Map
+import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
+import org.eclipse.xtext.xbase.XBinaryOperation
+import org.eclipse.xtext.xbase.XExpression
+import org.eclipse.xtext.xbase.XFeatureCall
+import org.eclipse.xtext.xbase.XMemberFeatureCall
+import org.eclipse.xtext.xbase.XNumberLiteral
+import org.eclipse.xtext.xbase.XUnaryOperation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
+class PExpressionGenerator {
+        static val N_Base = "org.eclipse.xtext.xbase.lib."
+        
+        static val N_PLUS1 = "operator_plus"
+        static val N_MINUS1 = "operator_minus"
+        
+        static val N_MINUS2 = "operator_minus"
+        static val N_PLUS2 = "operator_plus"
+        static val N_POWER = "operator_power"
+        static val N_MULTIPLY = "operator_multiply"
+        static val N_DIVIDE = "operator_divide"
+        static val N_MODULO = "operator_modulo"
+        static val N_LESSTHAN = "operator_lessThan"
+        static val N_LESSEQUALSTHAN = "operator_lessEqualsThan"
+        static val N_GREATERTHAN = "operator_greaterThan"
+        static val N_GREATEREQUALTHAN = "operator_greaterEqualsThan"
+        static val N_EQUALS = "operator_equals"
+        static val N_NOTEQUALS = "operator_notEquals"
+        static val N_EQUALS3 = "operator_tripleEquals"
+        static val N_NOTEQUALS3 = "operator_tripleNotEquals"
+        
+        protected def isN(String name, String s) {
+                val res = name.startsWith(N_Base) && name.endsWith(s)
+                //println('''[«res»] «name» ?= «N_Base»*«s»''')
+                return res
+        }
+        
+        static val N_POWER2 = "java.lang.Math.pow"
+        
+        def dispatch CharSequence translateExpression(XBinaryOperation e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
+                val left = e.leftOperand.translateExpression(valueName,variable2Type)
+                val right = e.rightOperand.translateExpression(valueName,variable2Type)
+                val feature = e.feature.qualifiedName
+                     if(feature.isN(N_MINUS2)) { return '''(«left»-«right»)'''}
+                else if(feature.isN(N_PLUS2)) { return '''(«left»+«right»)''' }
+                else if(feature.isN(N_POWER)) { return '''(«left»^«right»)'''  }
+                else if(feature.isN(N_MULTIPLY)) { return '''(«left»*«right»)''' }
+                else if(feature.isN(N_DIVIDE)) { return '''(«left»/«right»)''' }
+                else if(feature.isN(N_MODULO)) { return '''(«left»%«right»)''' }
+                else if(feature.isN(N_LESSTHAN)) { return '''(«left»<«right»)''' }
+                else if(feature.isN(N_LESSEQUALSTHAN)) { return '''(«left»<=«right»)''' }
+                else if(feature.isN(N_GREATERTHAN)) { return '''(«left»>«right»)''' }
+                else if(feature.isN(N_GREATEREQUALTHAN)) { return '''(«left»>=«right»)''' }
+                else if(feature.isN(N_EQUALS)) { return '''(«left»==«right»)''' }
+                else if(feature.isN(N_NOTEQUALS)) { return '''(«left»!=«right»)''' }
+                else if(feature.isN(N_EQUALS3)) { return '''(«left»===«right»)''' }
+                else if(feature.isN(N_NOTEQUALS3)) { return '''(«left»!==«right»)''' }
+                else {
+                        println("-> " + e.feature+","+e.class)
+                        println("-> " + e.leftOperand)
+                        println("-> " + e.rightOperand)
+                        println("-> " + e.feature.qualifiedName)
+                        throw new UnsupportedOperationException('''Unsupported binary operator feature: "«e.feature.class.simpleName»" - «e»''')
+                }
+        }
+        
+        def dispatch CharSequence translateExpression(XUnaryOperation e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
+                val operand = e.operand.translateExpression(valueName,variable2Type)
+                val feature = e.feature.qualifiedName
+                if(feature.isN(N_MINUS1)) { return '''(-«operand»)'''}
+                else if(feature.isN(N_PLUS1)) { return '''(+«operand»)'''}
+                else{
+                        println("-> " + e.feature+","+e.class)
+                        println("-> " + e.operand)
+                        println("-> " + e.feature.qualifiedName)
+                        throw new UnsupportedOperationException('''Unsupported unary operator feature: "«e.feature.class.simpleName»" - «e»''')
+                }
+        }
+        
+        def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
+                val transformedArguments = e.actualArguments.map[translateExpression(valueName,variable2Type)]
+                val feature = e.feature.qualifiedName
+                if(feature == N_POWER2) {
+                        return '''Math.pow(«transformedArguments.get(0)»,«transformedArguments.get(1)»)'''
+                }else {
+                        println(e.feature+","+e.class)
+                        println(e.actualArguments.join(", "))
+                        println(e.feature.qualifiedName)
+                        throw new UnsupportedOperationException('''Unsupported feature call: "«e.feature.qualifiedName»" - «e»''')
+                }
+        }
+        
+        def dispatch CharSequence translateExpression(XFeatureCall e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
+                val featureName = e.feature.qualifiedName
+                val type = variable2Type.entrySet.filter[it.key.name===featureName].head.value
+                val entryWithName = valueName.entrySet.filter[it.key.name == featureName].head
+                if(entryWithName !== null) {
+                        if(type instanceof RealTypeReference) {
+                                return '''(«entryWithName.value».doubleValue)'''
+                        } else {
+                                return entryWithName.value
+                        }
+                } else {
+                        throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''')
+                }
+        }
+        
+        def dispatch CharSequence translateExpression(XNumberLiteral l, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) '''«l.value»'''
+        
+        def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
+                throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''')
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
index 5c35fb54..f3125b80 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
@@ -29,6 +29,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
 import org.eclipse.xtend.lib.annotations.Accessors
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
+@Data class PatternGeneratorResult {
+        CharSequence patternText
+        HashMap<PConstraint,String> constraint2MustPreconditionName
+        HashMap<PConstraint,String> constraint2CurrentPreconditionName
+}
 class PatternGenerator {
        @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this)
@@ -39,12 +47,12 @@ class PatternGenerator {
        @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this)
        @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this)
        @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer
-        @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator // = new RefinementGenerator(this)
+        @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this)
-        @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(
+        @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this)
-                this)
+        @Accessors(PUBLIC_GETTER) val UnitPropagationPreconditionGenerator unitPropagationPreconditionGenerator = new UnitPropagationPreconditionGenerator(this)
+        
-        new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) {
+        public new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) {
-                if (typeInferenceMethod == TypeInferenceMethod.Generic) {
+                if(typeInferenceMethod == TypeInferenceMethod.Generic) {
                        this.typeIndexer = new GenericTypeIndexer(this)
                        this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this)
                } else if (typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) {
@@ -151,8 +159,8 @@ class PatternGenerator {
                RelationConstraints constraints,
                Collection<LinearTypeConstraintHint> hints
        ) {
+                val first = 
-                return '''
+                 '''
                        import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage"
                        import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"
                        import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
@@ -167,6 +175,7 @@ class PatternGenerator {
                        /////////////////////////
                        // 0.1 Existence
                        /////////////////////////
+                        /** [[exist(element)]]=1 */
                        private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
                                find interpretation(problem,interpretation);
                                LogicProblem.elements(problem,element);
@@ -175,6 +184,7 @@ class PatternGenerator {
                                PartialInterpretation.newElements(interpretation,element);
                        }
                        
+                        /** [[exist(element)]]>=1/2 */
                        private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
                            find mustExist(problem,interpretation,element);
                        } or {
@@ -195,57 +205,108 @@ class PatternGenerator {
                        ////////////////////////
                        // 0.2 Equivalence
                        ////////////////////////
-                        pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
+                        pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement)
+                        // For non-primitive type. Boolean types always must equivalent or cannot equivalent
+                        {
                                find mayExist(problem,interpretation,a);
                                find mayExist(problem,interpretation,b);
                                a == b;
+«««                  } or {
+«««                          find mayExist(problem,interpretation,a);
+«««                          find mayExist(problem,interpretation,b);
+«««                          IntegerElement(a);
+«««                          IntegerElement(b);
+«««                          PrimitiveElement.valueSet(a,false);
+«««                  } or {
+«««                          find mayExist(problem,interpretation,a);
+«««                          find mayExist(problem,interpretation,b);
+«««                          IntegerElement(a);
+«««                          IntegerElement(b);
+«««                          PrimitiveElement.valueSet(b,false);
+«««                  } or {
+«««                          find mayExist(problem,interpretation,a);
+«««                          find mayExist(problem,interpretation,b);
+«««                          RealElement(a);
+«««                          RealElement(b);
+«««                          PrimitiveElement.valueSet(a,false);
+«««                  } or {
+«««                          find mayExist(problem,interpretation,a);
+«««                          find mayExist(problem,interpretation,b);
+«««                          RealElement(a);
+«««                          RealElement(b);
+«««                          PrimitiveElement.valueSet(b,false);
+«««                  } or {
+«««                          find mayExist(problem,interpretation,a);
+«««                          find mayExist(problem,interpretation,b);
+«««                          StringElement(a);
+«««                          StringElement(b);
+«««                          PrimitiveElement.valueSet(a,false);
+«««                  } or {
+«««                          find mayExist(problem,interpretation,a);
+«««                          find mayExist(problem,interpretation,b);
+«««                          StringElement(a);
+«««                          StringElement(b);
+«««                          PrimitiveElement.valueSet(b,false);
                        }
+                        
                        pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
+                        // For non-primitive and Boolean primitive type
                                find mustExist(problem,interpretation,a);
                                find mustExist(problem,interpretation,b);
                                a == b;
+«««                  } or {
+«««                          find mustExist(problem,interpretation,a);
+«««                          find mustExist(problem,interpretation,b);
+«««                          PrimitiveElement.valueSet(a,true);
+«««                          PrimitiveElement.valueSet(b,true);
+«««                          IntegerElement.value(a,value);
+«««                          IntegerElement.value(b,value);
+«««                  } or {
+«««                          find mustExist(problem,interpretation,a);
+«««                          find mustExist(problem,interpretation,b);
+«««                          PrimitiveElement.valueSet(a,true);
+«««                          PrimitiveElement.valueSet(b,true);
+«««                          RealElement.value(a,value);
+«««                          RealElement.value(b,value);
+«««                  } or {
+«««                          find mustExist(problem,interpretation,a);
+«««                          find mustExist(problem,interpretation,b);
+«««                          PrimitiveElement.valueSet(a,true);
+«««                          PrimitiveElement.valueSet(b,true);
+«««                          StringElement.value(a,value);
+«««                          StringElement.value(b,value);
                        }
                        
-                        ////////////////////////
-                        // 0.3 Required Patterns by TypeIndexer
-                        ////////////////////////
-                        «typeIndexer.requiredQueries»
-                        
                        //////////
                        // 1. Problem-Specific Base Indexers
                        //////////
                        // 1.1 Type Indexers
                        //////////
-                        // 1.1.1 primitive Type Indexers
+                        // 1.1.1 Required Patterns by TypeIndexer
                        //////////
-                        «««                  pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
-«««                          find interpretation(problem,interpretation);
+                        «typeIndexer.requiredQueries»
-«««                          PartialInterpretation.booleanelements(interpretation,element);
+                        
-«««                  }
+                        //////////
-«««                  pattern instanceofInteger(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+                        // 1.1.2 primitive Type Indexers
-«««                          find interpretation(problem,interpretation);
+                        //////////
-«««                          PartialInterpretation.integerelements(interpretation,element);
+                        // Currently unused. Refer primitive types as:
-«««                  } or {
+                        // > PrimitiveElement(element)
-«««                          find interpretation(problem,interpretation);
+                        // specific types are referred as:
-«««                          PartialInterpretation.newIntegers(interpetation,element);
+                        // > BooleanElement(variableName)
-«««                  }
+                        // > IntegerElement(variableName)
-«««                  pattern instanceofReal(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+                        // > RealElement(variableName)
-«««                          find interpretation(problem,interpretation);
+                        // > StringElement(variableName)
-«««                          PartialInterpretation.realelements(interpretation,element);
+                        // And their value as
-«««                  } or {
+                        // > BooleanElement.value(variableName,value)
-«««                          find interpretation(problem,interpretation);
+                        // > IntegerElement.value(variableName,value)
-«««                          PartialInterpretation.newReals(interpetation,element);
+                        // > RealElement.value(variableName,value)
-«««                  }
+                        // > StringElement.value(variableName,value)
-«««                  pattern instanceofString(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+                        // Whether a value is set is defined by:
-«««                          find interpretation(problem,interpretation);
+                        // > PrimitiveElement.valueSet(variableName,isFilled);
-«««                          PartialInterpretation.stringelements(interpretation,element);
-«««                  } or {
-«««                          find interpretation(problem,interpretation);
-«««                          PartialInterpretation.newStrings(interpetation,element);
-«««                  }
                        
                        //////////
-                        // 1.1.2 domain-specific Type Indexers
+                        // 1.1.3 domain-specific Type Indexers
                        //////////
                        «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)»
                        
@@ -306,6 +367,13 @@ class PatternGenerator {
                        «FOR hint : hints»
                                «hint.getAdditionalPatterns(this)»
                        «ENDFOR»
-                '''
+                        
+                        //////////
+                        // 6 Unit Propagations
+                        //////////
+                        '''
+                val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)
+                val second = up.definitions
+                return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName)
        }
 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
index f5c85524..ac4a0855 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
@@ -10,6 +10,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStati
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
@@ -17,27 +18,28 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
 import java.util.Collection
+import java.util.HashMap
 import java.util.Map
 import java.util.Set
 import org.eclipse.viatra.query.runtime.api.IPatternMatch
 import org.eclipse.viatra.query.runtime.api.IQuerySpecification
 import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
 import org.eclipse.xtend.lib.annotations.Data
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
-@Data
+@Data class GeneratedPatterns {
-class GeneratedPatterns {
        public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries
        public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries
        public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries
        public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery
-        public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedMulticiplicityQueries
+        public Map<ObjectCreationPrecondition,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries
-        public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries
        public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries
-        public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries
+        public Map<Pair<RelationDeclaration, Relation>,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries
+        public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns
+        public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns
        public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries
        public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries
 }
@@ -76,14 +78,15 @@ class PatternProvider {
                        } else {
                                null
                        }
-                val baseIndexerFile = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query,
+                val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query,
                        typeAnalysisResult, relationConstraints, hints)
                if (writeToFile) {
-                        workspace.writeText('''generated3valued.vql_deactivated''', baseIndexerFile)
+                        workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText)
                }
                val ParseUtil parseUtil = new ParseUtil
-                val generatedQueries = parseUtil.parse(baseIndexerFile)
+                val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText)
                val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult,
+                        patternGeneratorResult.constraint2MustPreconditionName, patternGeneratorResult.constraint2CurrentPreconditionName,
                        relationConstraints, generatedQueries)
                return runtimeQueries
        }
@@ -93,32 +96,36 @@ class PatternProvider {
                LogicProblem problem,
                PartialInterpretation emptySolution,
                TypeAnalysisResult typeAnalysisResult,
+                HashMap<PConstraint, String> mustUnitPropagationTrace,
+                HashMap<PConstraint, String> currentUnitPropagationTrace,
                RelationConstraints relationConstraints,
                Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries
        ) {
-                val invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues [
+                val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
-                        it.lookup(queries)
+                        invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]
-                ]
+                val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
-                val unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues [
+                        unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)]
-                        it.lookup(queries)
+                        
-                ]
+                val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints)
-                val multiplicityConstraintQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(
+                val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [
-                        relationConstraints.multiplicityConstraints).mapValues [
                        new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries),
                                unrepairableMultiplicityQueryName?.lookup(queries),
                                remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries))
                ]
                val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup(
                        queries)
-                val unfinishedMultiplicityQueries = multiplicityConstraintQueries.entrySet.filter [
-                        value.unfinishedMultiplicityQuery !== null
+                val Map<ObjectCreationPrecondition,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
-                ].toMap([key.relation], [value.unfinishedMultiplicityQuery])
+                        refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]
-                val refineObjectsQueries = patternGenerator.typeRefinementGenerator.
+                val Map<? extends Type,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
-                        getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues[it.lookup(queries)]
+                        refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]
-                val refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution,
+                val Map<Pair<RelationDeclaration, Relation>,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
-                        typeAnalysisResult).mapValues[it.lookup(queries)]
+                        refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]
-                val refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).
+                val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 
-                        mapValues[it.lookup(queries)]
+                        mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)]
+                val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 
+                        currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)]
                val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition |
                        val indexer = patternGenerator.relationDefinitionIndexer
                        new ModalPatternQueries(
@@ -127,15 +134,17 @@ class PatternProvider {
                                indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries)
                        )
                ])
+                
                return new GeneratedPatterns(
                        invalidWFQueries,
                        unfinishedWFQueries,
                        multiplicityConstraintQueries,
                        hasElementInContainmentQuery,
-                        unfinishedMultiplicityQueries,
                        refineObjectsQueries,
                        refineTypeQueries,
                        refineRelationQueries,
+                        mustUnitPropagationPreconditionPatterns,
+                        currentUnitPropagationPreconditionPatterns,
                        modalRelationQueries,
                        queries.values
                )
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
index f384cd50..cef707c5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
@@ -90,13 +90,13 @@ class RelationDeclarationIndexer {
                                // There are "numberOfExistingReferences" currently existing instances of the reference from the source,
                                // the upper bound of the multiplicity should be considered.
                                numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)»
-                                check(numberOfExistingReferences < «upperMultiplicities.get(relation)»);
+                                numberOfExistingReferences != «upperMultiplicities.get(relation)»;
                        «ENDIF»
                        «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))»
                                // There are "numberOfExistingReferences" currently existing instances of the reference to the target,
                                // the upper bound of the opposite reference multiplicity should be considered.
                                numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)»
-                                check(numberOfExistingOppositeReferences < «upperMultiplicities.get(inverseRelations.get(relation))»);
+                                numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»;
                        «ENDIF»
                        «IF containments.contains(relation)»
                                // The reference is containment, then a new reference cannot be create if:
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
index 0ae28b66..338a9af2 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
@@ -5,39 +5,27 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
 import java.util.Map
-import org.eclipse.emf.common.util.Enumerator
-import org.eclipse.emf.ecore.EAttribute
-import org.eclipse.emf.ecore.EEnumLiteral
-import org.eclipse.emf.ecore.EReference
-import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
-import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
-import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
-import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
 import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
-import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
-import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
-import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
-import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
-import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
 import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
-import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
-import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
-import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 class RelationDefinitionIndexer {
-        val PatternGenerator base;
+        public val PatternGenerator base;
+        val PConstraintTransformer constraintTransformer;
        
        new(PatternGenerator base) {
                this.base = base
+                this.constraintTransformer = new PConstraintTransformer(this);
        }
        
        def generateRelationDefinitions(
                LogicProblem problem,
                Iterable<RelationDefinition> relations,
-                Map<String,PQuery> fqn2PQuery) {
+                Map<String,PQuery> fqn2PQuery)
+        {
                val relation2PQuery = relations.toInvertedMap[
                        annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery)
                ]
@@ -75,20 +63,21 @@ class RelationDefinitionIndexer {
        def String relationDefinitionName(RelationDefinition relation, Modality modality)
                '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»'''
        
-        private def canonizeName(PVariable v) {
+        def canonizeName(PVariable v) {
                return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»'''
        }
        
        private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) {
                try {
+                val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
                return '''
                        private pattern «relationDefinitionName(relation,modality)»(
                                problem:LogicProblem, interpretation:PartialInterpretation,
                                «FOR param : p.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»)
-                        «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{
+                        «FOR body : bodies SEPARATOR "or"»{
                                find interpretation(problem,interpretation);
                                «FOR constraint : body.constraints»
-                                        «constraint.transformConstraint(modality)»
+                                        «this.constraintTransformer.transformConstraint(constraint,modality,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
                                «ENDFOR»
                        }«ENDFOR»
                '''
@@ -105,7 +94,7 @@ class RelationDefinitionIndexer {
                '''
        }
        
-        private def toMustMay(Modality modality) {
+        def toMustMay(Modality modality) {
                if(modality == Modality::MAY) return Modality::MAY
                else return Modality::MUST
        } 
@@ -113,154 +102,4 @@ class RelationDefinitionIndexer {
        def referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) '''
                «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»);
        '''
-        
-        private dispatch def transformConstraint(TypeConstraint constraint, Modality modality) {
-                val touple = constraint.variablesTuple
-                if(touple.size == 1) {
-                        val inputKey = constraint.equivalentJudgement.inputKey
-                        if(inputKey instanceof EClassTransitiveInstancesKey) {
-                                return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
-                                        constraint.getVariableInTuple(0).canonizeName)
-                        } else if(inputKey instanceof EDataTypeInSlotsKey){
-                                return '''// type constraint is enforced by construction'''
-                        }
-                        
-                } else if(touple.size == 2){
-                        val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
-                        if(key instanceof EReference) {
-                                return base.referRelationByName(
-                                        key,
-                                        constraint.getVariableInTuple(0).canonizeName,
-                                        constraint.getVariableInTuple(1).canonizeName,
-                                        modality.toMustMay)
-                        } else if (key instanceof EAttribute) {
-                                return base.referAttributeByName(key,
-                                        constraint.getVariableInTuple(0).canonizeName,
-                                        constraint.getVariableInTuple(1).canonizeName,
-                                        modality.toMustMay)
-                        } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
-                } else {
-                        throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
-                }
-        }
-        private dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) {
-                val touple = constraint.variablesTuple
-                if(touple.size == 1) {
-                        val inputKey = constraint.equivalentJudgement.inputKey
-                        if(inputKey instanceof EClassTransitiveInstancesKey) {
-                                return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
-                                        (constraint.getVariablesTuple.get(0) as PVariable).canonizeName)
-                        } else if(inputKey instanceof EDataTypeInSlotsKey){
-                                return '''// type constraint is enforced by construction'''
-                        }
-                        
-                } else if(touple.size == 2){
-                        val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
-                        if(key instanceof EReference) {
-                                return base.referRelationByName(
-                                        key,
-                                        (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
-                                        (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
-                                        modality.toMustMay)
-                        } else if (key instanceof EAttribute) {
-                                return base.referAttributeByName(key,
-                                        (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
-                                        (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
-                                        modality.toMustMay)
-                        } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
-                } else {
-                        throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
-                }
-        }
-        
-        private dispatch def transformConstraint(Equality equality, Modality modality) {
-                val a = equality.who
-                val b = equality.withWhom
-                transformEquality(modality.toMustMay, a, b)
-        }
-        
-        private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) {
-                if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
-                else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
-        }       
-        
-        private dispatch def transformConstraint(Inequality inequality, Modality modality) {
-                val a = inequality.who
-                val b = inequality.withWhom
-                if(modality.isCurrent) {
-                        return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
-                } else if(modality.isMust) {
-                        return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
-                } else { // modality.isMay
-                        return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
-                }
-        }
-        
-        private dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) {
-                val params = (0..<pcall.actualParametersTuple.size).map[index | 
-                        val variable = pcall.actualParametersTuple.get(index) as PVariable
-                        return variable.canonizeName
-                ]
-                return referPattern(pcall.referredQuery,params,modality.dual,false,false)
-        }
-        
-        private dispatch def transformConstraint(PositivePatternCall pcall, Modality modality) {
-                val params = (0..<pcall.variablesTuple.size).map[index | 
-                        val variable = pcall.variablesTuple.get(index) as PVariable
-                        return variable.canonizeName
-                ]
-                return referPattern(pcall.referredQuery,params,modality,true,false)
-        }
-        private dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality) {
-                val params = (0..1).map[index | 
-                        val variable = pcall.getVariableInTuple(index) as PVariable
-                        return variable.canonizeName
-                ]
-                return referPattern(pcall.referredQuery,params,modality,true,true)
-        }
-        private dispatch def transformConstraint(ExportedParameter e, Modality modality) {
-                return '''// «e.parameterName» is exported'''
-        }
-        private dispatch def transformConstraint(ConstantValue c, Modality modality) {
-                val target = c.supplierKey
-                
-                var String targetString;
-                var String additionalDefinition;
-                if(target instanceof EEnumLiteral) {
-                        targetString = '''const_«target.name»_«target.EEnum.name»'''
-                        additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» literal «target.EEnum.name»");  //LogicProblem.elements(problem,«targetString»);'''
-                } else if(target instanceof Enumerator) {
-                        // XXX We should get the corresponding EEnum name instead of the java class name.
-                        targetString = '''const_«target.name»_«target.class.simpleName»'''
-                        additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» literal «target.class.simpleName»");  //LogicProblem.elements(problem,«targetString»);'''
-                } else if(target instanceof Integer) {
-                        targetString = '''const_«target»_Integer'''
-                        additionalDefinition = '''IntegerElement.value(«targetString»,«target»);'''
-                } else if(target instanceof Boolean) {
-                        targetString = '''const_«target»_Boolean'''
-                        additionalDefinition = '''BooleanElement.value(«targetString»,«target»);'''
-                } else if(target instanceof String) {
-                        targetString = '''const_«target»_String'''
-                        additionalDefinition = '''StringElement.value(«targetString»,"«target»");'''
-                } else if(target instanceof Double) {
-                        targetString = '''const_«target»_Number'''
-                        additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''
-                } else if(target instanceof Float) {
-                        targetString = '''const_«target»_Number'''
-                        additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''
-                } else {
-                        throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')
-                }
-                
-                val source = c.variablesTuple
-                var String sourceName
-                if(source.size == 1)
-                        sourceName = (source.get(0) as PVariable).canonizeName
-                else throw new UnsupportedOperationException("unknown source")
-                return '''«sourceName» == «targetString»;«additionalDefinition»''';
-        }
-        
-        private dispatch def transformConstraint(PConstraint c, Modality modality) {
-                throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
-        }
 }
 \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend
index 7d687e99..e4e2aa30 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend
@@ -119,4 +119,8 @@ abstract class TypeIndexer {
                '''StringElement.value(«variableName»,"«value»");'''
        }
+        def CharSequence referPrimitiveFilled(String variableName, boolean isFilled) {
+                '''PrimitiveElement.valueSet(«variableName»,«isFilled»);'''
+        }
 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
new file mode 100644
index 00000000..400f47bc
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
@@ -0,0 +1,302 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.PropagationModality
+import java.util.Map
+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
+import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import java.util.LinkedList
+import java.util.List
+import org.eclipse.xtend.lib.annotations.Data
+import java.util.HashMap
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
+import java.util.Comparator
+import java.util.ArrayList
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
+import java.util.LinkedHashSet
+@Data class UnitPropagation {
+        val PQuery q
+        val PConstraint c
+        val PropagationModality pm
+        val Modality m3
+}
+@Data
+class UnitPropagationPreconditionGenerationResult {
+        List<CharSequence> definitions= new LinkedList
+        Map<UnitPropagation,String> unitPropagation2PatternName = new HashMap
+        Map<PConstraint,String> constraintOccurence2Name = new HashMap
+        
+        def registerQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3, String patternName, CharSequence definition) {
+                val key = new UnitPropagation(q,c,pm,m3)
+                definitions += definition
+                unitPropagation2PatternName.put(key,patternName)
+        }
+        def registerUnsatQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                val key = new UnitPropagation(q,c,pm,m3)
+                unitPropagation2PatternName.put(key,null)
+        }
+        def contains(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                val key = new UnitPropagation(q,c,pm,m3)
+                return unitPropagation2PatternName.containsKey(key)
+        }
+        def getName(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                val key = new UnitPropagation(q,c,pm,m3)
+                return key.lookup(unitPropagation2PatternName)
+        }
+        def isDefined(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                val key = new UnitPropagation(q,c,pm,m3)
+                return unitPropagation2PatternName.get(key) !== null
+        }
+}
+@Data
+class UnitPropagationPreconditionFinalResult {
+        CharSequence definitions
+        HashMap<PConstraint,String> constraint2MustPreconditionName
+        HashMap<PConstraint,String> constraint2CurrentPreconditionName
+}
+class UnitPropagationPreconditionGenerator {
+        val PatternGenerator base
+        val PConstraintTransformer constraintTransformer;
+        
+        new(PatternGenerator patternGenerator) {
+                this.base = patternGenerator
+                this.constraintTransformer = new PConstraintTransformer(base.relationDefinitionIndexer)
+        }
+        
+        def generateUnitPropagationRules(
+                LogicProblem problem,
+                Iterable<RelationDefinition> relations,
+                Map<String,PQuery> fqn2PQuery)
+        {
+                // Create an empty result
+                val res = new UnitPropagationPreconditionGenerationResult               
+                val wfs = base.wfQueries(problem)//.map[it.patternPQuery]
+                val Map<PConstraint,List<Pair<String,Integer>>> mainMustPropagationNames = new HashMap
+                val Map<PConstraint,List<Pair<String,Integer>>> mainCurrentPropagationNames = new HashMap
+                for(wf : wfs) {
+                        val query = wf.patternPQuery as PQuery
+                        val relation = wf.target
+                        val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation)
+                        
+                        for(referredCheck : allReferredChecks) {
+                                val mustPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST)
+                                val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT)
+                                if(!mainMustPropagationNames.containsKey(referredCheck)) {
+                                        mainMustPropagationNames.put(referredCheck,new LinkedList)
+                                }
+                                if(!mainCurrentPropagationNames.containsKey(referredCheck)) {
+                                        mainCurrentPropagationNames.put(referredCheck,new LinkedList)
+                                }
+                                if(mustPropagationPrecondition !== null) {
+                                        mainMustPropagationNames.get(referredCheck).add(mustPropagationPrecondition->query.parameterNames.size)
+                                }
+                                if(currentPropagationPrecondition !== null) {
+                                        mainCurrentPropagationNames.get(referredCheck).add(currentPropagationPrecondition->query.parameterNames.size)
+                                }
+                        }
+                }
+                val preconditions = new LinkedList
+                val constraint2MustPrecondition = new HashMap
+                val constraint2CurrentPrecondition = new HashMap
+                for(entry : mainMustPropagationNames.entrySet) {
+                        val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
+                        val def = '''
+                        pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
+                                «FOR propagation : entry.value SEPARATOR " or "»
+                                        { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
+                                «ENDFOR»'''
+                        preconditions+=def
+                        constraint2MustPrecondition.put(entry.key,name)
+                }
+                for(entry : mainCurrentPropagationNames.entrySet) {
+                        val name = '''UPCurrentPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
+                        val def = '''
+                        pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
+                                «FOR propagation : entry.value SEPARATOR " or "»
+                                        { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
+                                «ENDFOR»'''
+                        preconditions+=def
+                        constraint2CurrentPrecondition.put(entry.key,name)
+                }
+                
+                val definitions = '''
+                        «FOR def : res.definitions»
+                                «def»
+                        «ENDFOR»
+                        
+                        // Collected propagation preconditions:
+                        
+                        «FOR predondition : preconditions»
+                                «predondition»
+                        «ENDFOR»
+                '''
+                return new UnitPropagationPreconditionFinalResult(definitions,constraint2MustPrecondition,constraint2CurrentPrecondition)
+        }
+        def allReferredConstraints(Relation relation, PQuery query) {
+                val allReferredQueries = query.allReferredQueries
+                val problem = relation.eContainer as LogicProblem
+                val constraints = new LinkedHashSet
+                for(referredQuery: #[query]+allReferredQueries) {
+                        val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target
+                        val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
+                        constraints.addAll(bodies.map[getConstraints].flatten)
+                }
+                
+                return constraints
+        }
+        
+        def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                if(res.contains(q,c,pm,m3)) {
+                        return res.getName(q,c,pm,m3)
+                } else {
+                        res.generatePropagationRule(relation,q,c,pm,m3)
+                        return res.getName(q,c,pm,m3)
+                }
+        }
+        def getOrGenerateConstraintName(UnitPropagationPreconditionGenerationResult res, PConstraint c){
+                if(res.constraintOccurence2Name.containsKey(c)) {
+                        return res.constraintOccurence2Name.get(c)
+                } else {
+                        val constraintName = '''Constraint«res.constraintOccurence2Name.size»'''
+                        res.constraintOccurence2Name.put(c,constraintName)
+                        return constraintName
+                }
+        }
+        
+        def void generatePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                val name = relationDefinitionName(res,relation,q,c,pm,m3)
+                val constraintArity = c.arity
+                val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
+                val generatedBodies = new LinkedList
+                for(body : bodies) {
+                        if(body.constraints.contains(c)) {
+                                if(pm === PropagationModality::UP) {
+                                        generatedBodies += '''
+                                                // Original Constraints
+                                                «FOR constraint : body.constraints.filter[it !== c]»
+                                                        «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
+                                                «ENDFOR»
+                                                // Propagation for constraint
+                                                «this.constraintTransformer.transformConstraintUnset(c as ExpressionEvaluation,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
+                                                // Matching variables
+                                                «this.propagateVariables(c,pm)»
+                                        '''
+                                }
+                                // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied
+                        } else {
+                                val positives = body.constraints.filter(PositivePatternCall)
+                                for(positive: positives) {
+                                        val referredPQuery = positive.referredQuery
+                                        val referredRelation = (relation.eContainer as LogicProblem)
+                                                .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
+                                        if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
+                                                val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3)
+                                                if(referredName !== null) {
+                                                        generatedBodies += '''
+                                                                // Original Constraints
+                                                                «FOR constraint : body.constraints.filter[it !== positive]»
+                                                                        «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
+                                                                «ENDFOR»
+                                                                // Propagation for constraint referred indirectly from this pattern through «referredName»
+                                                                find «referredName»(problem, interpretation,
+                                                                        «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR»,
+                                                                        «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
+                                                        '''
+                                                }
+                                                // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either
+                                        }
+                                }
+                                
+                                val negatives = body.constraints.filter(NegativePatternCall)
+                                for(negative : negatives) {
+                                        val referredPQuery = negative.referredQuery
+                                        val referredRelation = (relation.eContainer as LogicProblem)
+                                                .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
+                                        if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
+                                                val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual)
+                                                if(referredName !== null) {
+                                                        generatedBodies += '''
+                                                                // Original Constraints
+                                                                «FOR constraint : body.constraints.filter[it !== negative]»
+                                                                        «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
+                                                                «ENDFOR»
+                                                                // Propagation for constraint referred indirectly from this pattern through «referredName»
+                                                                find «referredName»(problem, interpretation,
+                                                                        «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR»,
+                                                                        «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
+                                                        '''
+                                                } else {
+                                                        generatedBodies += '''
+                                                                // Original Constraints
+                                                                «FOR constraint : body.constraints.filter[it !== negative]»
+                                                                        «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
+                                                                «ENDFOR»
+                                                                // Propagation for constraint referred indirectly from this pattern through «referredName»,
+                                                                // which was unsatisfiable
+                                                        '''
+                                                }
+                                        }
+                                }
+                        }
+                }
+                
+                // Register the result
+                if(generatedBodies.empty) {
+                        res.registerUnsatQuery(q,c,pm,m3)
+                } else {
+                        val definition = '''
+                                private pattern «name»(
+                                        problem:LogicProblem, interpretation:PartialInterpretation,
+                                        «FOR param :  q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»,
+                                        «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR»)
+                                «FOR generatedBody: generatedBodies SEPARATOR " or "»{
+                                «generatedBody»
+                                }«ENDFOR»
+                        '''
+                        res.registerQuery(q,c,pm,m3,name,definition)
+                }
+        }
+        private def String relationDefinitionName(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3)
+                '''«pm.name»«m3.name»Propagate«res.getOrGenerateConstraintName(c)»_«base.canonizeName(relation.name)»'''
+        
+        def canonizeName(PVariable v) {
+                return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»'''
+        }
+        
+        def canonizeName(int index, PropagationModality m) {
+                return '''«m.name.toLowerCase»_«index»'''
+        }
+        
+        def dispatch propagateVariables(ExpressionEvaluation c, PropagationModality m) {
+                val comparator = new Comparator<PVariable>(){
+                        override compare(PVariable o1, PVariable o2) {
+                                o1.name.compareTo(o2.name)
+                        }
+                }
+                val variablesInOrder = new ArrayList(c.affectedVariables)
+                variablesInOrder.toList.sort(comparator)
+                return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»'''
+        }
+        def dispatch propagateVariables(PConstraint c, PropagationModality m) {
+                throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
+        }
+        
+        def dispatch arity(ExpressionEvaluation c) {
+                c.affectedVariables.size
+        }
+        def dispatch arity(PConstraint c) {
+                throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
index b6fdbe06..238ade5b 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
@@ -1,18 +1,26 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
 import java.util.ArrayList
 class GoalConstraintProvider {
-        def public getUnfinishedMultiplicityQueries(GeneratedPatterns patterns) {
+        
-                val multiplicityQueries = patterns.unfinishedMulticiplicityQueries
+        def getUnfinishedMultiplicityQueries(LogicProblem p, GeneratedPatterns patterns) {
-                val res = new ArrayList(multiplicityQueries.size)
+                val res = new ArrayList()
-                for(multiplicityQuery : multiplicityQueries.entrySet) {
+                for (entry : patterns.multiplicityConstraintQueries.entrySet) {
-                        val targetRelationName = multiplicityQuery.key.name
+                        val constraint = entry.key
-                        val query = multiplicityQuery.value
+                        if (constraint.constrainsUnfinished) {
-                        res += new MultiplicityGoalConstraintCalculator(targetRelationName,query);
+                                val queries = entry.value
+                                val targetRelationName = constraint.relation.name
+                                val query = queries.unfinishedMultiplicityQuery
+                                val minValue = constraint.lowerBound
+                                val containment = constraint.containment
+                                res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, minValue, containment, 1)
+                        }
                }
                return res
        }
 }
 \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
index 7891ebd8..0b8a9019 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
@@ -1,71 +1,93 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules
+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion
+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory
+import java.util.HashMap
 import java.util.LinkedHashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
 import org.eclipse.viatra.query.runtime.api.GenericPatternMatch
 import org.eclipse.viatra.query.runtime.api.IQuerySpecification
 import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
 import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory
+import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.xtext.xbase.lib.Functions.Function0
 class RefinementRuleProvider {
-        private extension BatchTransformationRuleFactory factory = new BatchTransformationRuleFactory
+        val extension BatchTransformationRuleFactory factory = new BatchTransformationRuleFactory
-        private extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE
+        val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE
-        private extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE
+        val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE
        
        def canonizeName(String name) {
                return name.replace(' ','_')
        }
        
-        def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> 
+        def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> createObjectRefinementRules(
-                createObjectRefinementRules(
+                        LogicProblem p,
+                        PartialInterpretation i,
                        GeneratedPatterns patterns,
                        ScopePropagator scopePropagator,
                        boolean nameNewElement,
                        ModelGenerationStatistics statistics
                )
-        {               
+        {
                val res = new LinkedHashMap
+                val recursiveObjectCreation = recursiveObjectCreation(p,i)
                for(LHSEntry: patterns.refineObjectQueries.entrySet) {
                        val containmentRelation = LHSEntry.key.containmentRelation
                        val inverseRelation = LHSEntry.key.inverseContainment
                        val type = LHSEntry.key.newType
                        val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>>
-                        val rule = createObjectCreationRule(containmentRelation,inverseRelation,type,lhs,nameNewElement,scopePropagator,statistics)
+                        val rule = createObjectCreationRule(p,containmentRelation,inverseRelation,type,recursiveObjectCreation.get(type),lhs,nameNewElement,scopePropagator,statistics)
                        res.put(LHSEntry.key,rule)
                }
                return res
        }
        
        def private createObjectCreationRule(
+                LogicProblem p,
                Relation containmentRelation,
                Relation inverseRelation,
                Type type,
+                List<ObjectCreationInterpretationData> recursiceObjectCreations,
                IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs,
                boolean nameNewElement,
                ScopePropagator scopePropagator,
                ModelGenerationStatistics statistics)
        {
                val name = '''addObject_«type.name.canonizeName»«
-                                        IF containmentRelation!=null»_by_«containmentRelation.name.canonizeName»«ENDIF»'''
+                                        IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»'''
-                //println("Rule created: " + name + "> " + lhs.fullyQualifiedName)
+                val ruleBuilder = factory.createRule(lhs)
-                val ruleBuilder = factory.createRule
                                .name(name)
-                                .precondition(lhs)
+                if(containmentRelation !== null) {
-                if(containmentRelation != null) {
+                        if(inverseRelation!== null) {
-                        if(inverseRelation!= null) {
                                ruleBuilder.action[match |
                                        statistics.incrementTransformationCount
 //                                      println(name)
@@ -77,33 +99,23 @@ class RefinementRuleProvider {
                                        val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation
                                        val container = match.get(5) as DefinedElement
                                        
-                                        val newElement = createDefinedElement
+                                        createObjectActionWithContainmentAndInverse(
-                                        if(nameNewElement) {
+                                                nameNewElement,
-                                                newElement.name = '''new «interpretation.newElements.size»'''
+                                                interpretation,
-                                        }
+                                                typeInterpretation,
-                                        
+                                                container,
-                                        // Existence
+                                                relationInterpretation,
-                                        interpretation.newElements+=newElement
+                                                inverseRelationInterpretation,
-                                        /*interpretation.maxNewElements=interpretation.maxNewElements-1
+                                                [createDefinedElement],
-                                        if(interpretation.minNewElements > 0) {
+                                                recursiceObjectCreations,
-                                                interpretation.minNewElements=interpretation.minNewElements-1
+                                                scopePropagator
-                                        }*/
+                                        )
-                                        
-                                        // Types
-                                        typeInterpretation.elements += newElement
-                                        typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
-                                        // ContainmentRelation
-                                        val newLink1 = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement]
-                                        relationInterpretation.relationlinks+=newLink1
-                                        // Inverse Containment
-                                        val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container]
-                                        inverseRelationInterpretation.relationlinks+=newLink2
                                        
                                        val propagatorStartTime = System.nanoTime
                                        statistics.addExecutionTime(propagatorStartTime-startTime)
                                        
                                        // Scope propagation
-                                        scopePropagator.propagateAdditionToType(typeInterpretation)
+                                        scopePropagator.propagateAllScopeConstraints()
                                        statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
                                ]
                        } else {
@@ -117,30 +129,22 @@ class RefinementRuleProvider {
                                        val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation
                                        val container = match.get(4) as DefinedElement
                                        
-                                        val newElement = createDefinedElement
+                                        createObjectActionWithContainment(
-                                        if(nameNewElement) {
+                                                nameNewElement,
-                                                newElement.name = '''new «interpretation.newElements.size»'''
+                                                interpretation,
-                                        }
+                                                typeInterpretation,
-                                        
+                                                container,
-                                        // Existence
+                                                relationInterpretation,
-                                        interpretation.newElements+=newElement
+                                                [createDefinedElement],
-                                        /*interpretation.maxNewElements=interpretation.maxNewElements-1
+                                                recursiceObjectCreations,
-                                        if(interpretation.minNewElements > 0) {
+                                                scopePropagator
-                                                interpretation.minNewElements=interpretation.minNewElements-1
+                                        )
-                                        }*/
-                                        
-                                        // Types
-                                        typeInterpretation.elements += newElement
-                                        typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
-                                        // ContainmentRelation
-                                        val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement]
-                                        relationInterpretation.relationlinks+=newLink
                                        
                                        val propagatorStartTime = System.nanoTime
                                        statistics.addExecutionTime(propagatorStartTime-startTime)
                                        
                                        // Scope propagation
-                                        scopePropagator.propagateAdditionToType(typeInterpretation)
+                                        scopePropagator.propagateAllScopeConstraints()
                                        statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
                                ]
                        }
@@ -148,40 +152,175 @@ class RefinementRuleProvider {
                        ruleBuilder.action[match |
                                statistics.incrementTransformationCount
 //                              println(name)
-                                
                                val startTime = System.nanoTime
                                //val problem = match.get(0) as LogicProblem
                                val interpretation = match.get(1) as PartialInterpretation
                                val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation
-                                
-                                val newElement = createDefinedElement
+                                createObjectAction(
-                                if(nameNewElement) {
+                                        nameNewElement,
-                                        newElement.name = '''new «interpretation.newElements.size»'''
+                                        interpretation,
-                                }
+                                        typeInterpretation,
-                                
+                                        [createDefinedElement],
-                                // Existence
+                                        recursiceObjectCreations,
-                                interpretation.newElements+=newElement
+                                        scopePropagator
-                                /*
+                                )
-                                interpretation.maxNewElements=interpretation.maxNewElements-1
-                                if(interpretation.minNewElements > 0) {
-                                        interpretation.minNewElements=interpretation.minNewElements-1
-                                }*/
-                                
-                                // Types
-                                typeInterpretation.elements += newElement
-                                typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
                                
                                val propagatorStartTime = System.nanoTime
                                statistics.addExecutionTime(propagatorStartTime-startTime)
                                
                                // Scope propagation
-                                scopePropagator.propagateAdditionToType(typeInterpretation)
+                                scopePropagator.propagateAllScopeConstraints()
                                statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
                        ]
                }
                return ruleBuilder.build
        }
        
+        def private recursiveObjectCreation(LogicProblem p, PartialInterpretation i) {
+                val Map<Type,List<ObjectCreationInterpretationData>> recursiveObjectCreation = new HashMap
+                for(type : p.types) {
+                        recursiveObjectCreation.put(type,new LinkedList)
+                }
+                
+                val containmentReferences = p.containmentHierarchies.head.containmentRelations
+                
+                for(relationInterpretation : i.partialrelationinterpretation) {
+                        val relation = relationInterpretation.interpretationOf
+                        val lowermultiplicities = p.annotations.filter(LowerMultiplicityAssertion).filter[it.relation === relation]
+                        if((!lowermultiplicities.empty)) {
+                                val number = lowermultiplicities.head.lower
+                                if(number > 0) {
+                                        val sourceTypeInterpretation = getTypeInterpretation(i, relation, 0) as PartialComplexTypeInterpretation
+                                        val subtypeInterpretations = i.partialtypeinterpratation.filter(PartialComplexTypeInterpretation).filter[
+                                                it === sourceTypeInterpretation ||
+                                                it.supertypeInterpretation.contains(sourceTypeInterpretation)
+                                        ]
+                                        
+                                        if(containmentReferences.contains(relation)) {
+                                                val targetTypeInterpretation = getTypeInterpretation(i, relation, 1)
+                                                val targetType = (targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf
+                                                if((!targetType.isIsAbstract) && (targetType.supertypes.empty)) {
+                                                        val inverseAnnotation = p.annotations.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation]
+                                                        if(!inverseAnnotation.empty) {
+                                                                val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) {
+                                                                        inverseAnnotation.head.inverseB
+                                                                } else {
+                                                                        inverseAnnotation.head.inverseA
+                                                                }
+                                                                val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head
+                                                                for(subTypeInterpretation : subtypeInterpretations) {
+                                                                        for(var times=0; times<number; times++) {
+                                                                                recursiveObjectCreation.get(subTypeInterpretation.interpretationOf) += 
+                                                                                        new ObjectCreationInterpretationData(
+                                                                                                i,
+                                                                                                targetTypeInterpretation,
+                                                                                                relationInterpretation,
+                                                                                                inverseRelationInterpretation,
+                                                                                                targetTypeInterpretation.getTypeConstructor
+                                                                                        )
+                                                                        }
+                                                                }
+                                                        } else {
+                                                                for(subTypeInterpretation : subtypeInterpretations) {
+                                                                        for(var times=0; times<number; times++) {
+                                                                                recursiveObjectCreation.get(subTypeInterpretation.interpretationOf) += 
+                                                                                        new ObjectCreationInterpretationData(
+                                                                                                i,
+                                                                                                targetTypeInterpretation,
+                                                                                                relationInterpretation,
+                                                                                                null,
+                                                                                                targetTypeInterpretation.getTypeConstructor
+                                                                                        )
+                                                                        }
+                                                                }
+                                                        }
+                                                }
+                                        } else if(relation.parameters.get(1) instanceof PrimitiveTypeReference) {
+                                                val targetTypeInterpretation = getTypeInterpretation(i, relation, 1)
+                                                for(subTypeInterpretation : subtypeInterpretations) {
+                                                        for(var times=0; times<number; times++) {
+                                                                recursiveObjectCreation.get(subTypeInterpretation.interpretationOf) += 
+                                                                        new ObjectCreationInterpretationData(
+                                                                                i,
+                                                                                targetTypeInterpretation,
+                                                                                relationInterpretation,
+                                                                                null,
+                                                                                targetTypeInterpretation.getTypeConstructor
+                                                                        )
+                                                        }
+                                                }
+                                        }
+                                }
+                        }
+                }
+                
+                // Doing the recursion
+                var objectCreations = new LinkedList(recursiveObjectCreation.values.flatten.toList)
+                for(objectCreation : objectCreations) {
+                        val newInterpretation = objectCreation.typeInterpretation
+                        if(newInterpretation instanceof PartialComplexTypeInterpretation) {
+                                val newlyCreatedType = newInterpretation.interpretationOf
+                                if(recursiveObjectCreation.containsKey(newlyCreatedType)) {
+                                        val actionsWhenTypeCreated = recursiveObjectCreation.get(newlyCreatedType)
+                                        objectCreation.recursiveConstructors+=actionsWhenTypeCreated
+                                }
+                        }
+                }
+                
+                // checking acyclicity
+                for(objectCreation : objectCreations) {
+                        var reachable = objectCreation.recursiveConstructors
+                        do {
+                                if(reachable.contains(objectCreation)) {
+                                        throw new IllegalArgumentException('''Cicrle in the containment!''')
+                                } else {
+                                        reachable = reachable.map[it.recursiveConstructors].flatten.toList
+                                }
+                        } while(!reachable.empty)
+                }       
+                
+                return recursiveObjectCreation
+        }
+        
+        private def getTypeInterpretation(PartialInterpretation i, RelationDeclaration relation, int index) {
+                val typeReference = relation.parameters.get(index)
+                return getTypeInterpretation(i,typeReference)
+                
+        }
+        private dispatch def getTypeInterpretation(PartialInterpretation i, ComplexTypeReference reference) {
+                return i.partialtypeinterpratation
+                                .filter(PartialComplexTypeInterpretation)
+                                .filter[it.getInterpretationOf == reference.referred]
+                                .head
+        }
+        private dispatch def getTypeInterpretation(PartialInterpretation i, BoolTypeReference reference) {
+                return i.partialtypeinterpratation
+                                .filter(PartialBooleanInterpretation)
+                                .head
+        }
+        private dispatch def getTypeInterpretation(PartialInterpretation i, IntTypeReference reference) {
+                return i.partialtypeinterpratation
+                                .filter(PartialIntegerInterpretation)
+                                .head
+        }
+        private dispatch def getTypeInterpretation(PartialInterpretation i, RealTypeReference reference) {
+                return i.partialtypeinterpratation
+                                .filter(PartialRealInterpretation)
+                                .head
+        }
+        private dispatch def getTypeInterpretation(PartialInterpretation i, StringTypeReference reference) {
+                return i.partialtypeinterpratation
+                                .filter(PartialStringInterpretation)
+                                .head
+        }
+        private dispatch def Function0<DefinedElement> getTypeConstructor(PartialComplexTypeInterpretation reference) { [createDefinedElement] }
+        private dispatch def Function0<DefinedElement> getTypeConstructor(PartialBooleanInterpretation reference) { [createBooleanElement] }
+        private dispatch def Function0<DefinedElement> getTypeConstructor(PartialIntegerInterpretation reference) { [createIntegerElement] }
+        private dispatch def Function0<DefinedElement> getTypeConstructor(PartialRealInterpretation reference) { [createRealElement] }
+        private dispatch def Function0<DefinedElement> getTypeConstructor(PartialStringInterpretation reference) { [createStringElement] }
+        
+        
        def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) {
                val res = new LinkedHashMap
                for(LHSEntry: patterns.refinerelationQueries.entrySet) {
@@ -197,11 +336,10 @@ class RefinementRuleProvider {
        def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>
                createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ScopePropagator scopePropagator, ModelGenerationStatistics statistics)
        {
-                val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation != null»_and_«inverseRelation.name.canonizeName»«ENDIF»'''
+                val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»'''
-                val ruleBuilder = factory.createRule
+                val ruleBuilder = factory.createRule(lhs)
                        .name(name)
-                        .precondition(lhs)
+                if (inverseRelation === null) {
-                if (inverseRelation == null) {
                        ruleBuilder.action [ match |
                                statistics.incrementTransformationCount
                            val startTime = System.nanoTime
@@ -211,8 +349,8 @@ class RefinementRuleProvider {
                                val relationInterpretation = match.get(2) as PartialRelationInterpretation
                                val src = match.get(3) as DefinedElement
                                val trg = match.get(4) as DefinedElement
-                                val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg]
+                                
-                                relationInterpretation.relationlinks += link
+                                createRelationLinkAction(src, trg, relationInterpretation)
                                
                                val propagatorStartTime = System.nanoTime
                                statistics.addExecutionTime(propagatorStartTime-startTime)
@@ -232,10 +370,8 @@ class RefinementRuleProvider {
                                val inverseInterpretation = match.get(3) as PartialRelationInterpretation
                                val src = match.get(4) as DefinedElement
                                val trg = match.get(5) as DefinedElement
-                                val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg]
-                                relationInterpretation.relationlinks += link
+                                createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation)
-                                val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src]
-                                inverseInterpretation.relationlinks += inverseLink
                                
                                val propagatorStartTime = System.nanoTime
                                statistics.addExecutionTime(propagatorStartTime-startTime)
@@ -248,4 +384,182 @@ class RefinementRuleProvider {
                return ruleBuilder.build
        }
+        
+        /////////////////////////
+        // Actions
+        /////////////////////////
+        
+        protected def void createObjectAction(boolean nameNewElement, ObjectCreationInterpretationData data, DefinedElement container, ScopePropagator scopePropagator) {
+                if(data.containerInterpretation !== null) {
+                        if(data.containerInverseInterpretation !== null) {
+                                createObjectActionWithContainmentAndInverse(
+                                        nameNewElement,
+                                        data.interpretation,
+                                        data.typeInterpretation,
+                                        container,
+                                        data.containerInterpretation,
+                                        data.containerInverseInterpretation,
+                                        data.constructor,
+                                        data.recursiveConstructors,
+                                        scopePropagator
+                                )
+                        } else {
+                                createObjectActionWithContainment(
+                                        nameNewElement,
+                                        data.interpretation,
+                                        data.typeInterpretation,
+                                        container,
+                                        data.containerInterpretation,
+                                        data.constructor,
+                                        data.recursiveConstructors,
+                                        scopePropagator
+                                )
+                        }
+                } else {
+                        createObjectAction(
+                                nameNewElement,
+                                data.interpretation,
+                                data.typeInterpretation,
+                                data.constructor,
+                                data.recursiveConstructors,
+                                scopePropagator
+                        )
+                }
+                
+        }
+        
+        protected def createObjectActionWithContainmentAndInverse(
+                boolean nameNewElement,
+                PartialInterpretation interpretation,
+                PartialTypeInterpratation typeInterpretation,
+                DefinedElement container,
+                PartialRelationInterpretation relationInterpretation,
+                PartialRelationInterpretation inverseRelationInterpretation,
+                Function0<DefinedElement> constructor,
+                List<ObjectCreationInterpretationData> recursiceObjectCreations,
+                ScopePropagator scopePropagator
+        ) {
+                val newElement = constructor.apply
+                if(nameNewElement) {
+                        newElement.name = '''new «interpretation.newElements.size»'''
+                }
+                
+                // Types
+                typeInterpretation.elements += newElement
+                if(typeInterpretation instanceof PartialComplexTypeInterpretation) {
+                        typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
+                }
+                // ContainmentRelation
+                val newLink1 = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement]
+                relationInterpretation.relationlinks+=newLink1
+                // Inverse Containment
+                val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container]
+                inverseRelationInterpretation.relationlinks+=newLink2
+                
+                // Scope propagation
+                scopePropagator.decrementTypeScope(typeInterpretation)
+                
+                // Existence
+                interpretation.newElements+=newElement
+                
+                // Do recursive object creation
+                for(newConstructor : recursiceObjectCreations) {
+                        createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator)
+                }
+                
+                return newElement
+        }
+        
+        protected def createObjectActionWithContainment(
+                boolean nameNewElement,
+                PartialInterpretation interpretation,
+                PartialTypeInterpratation typeInterpretation,
+                DefinedElement container,
+                PartialRelationInterpretation relationInterpretation,
+                Function0<DefinedElement> constructor,
+                List<ObjectCreationInterpretationData> recursiceObjectCreations,
+                ScopePropagator scopePropagator
+        ) {
+                val newElement = constructor.apply
+                if(nameNewElement) {
+                        newElement.name = '''new «interpretation.newElements.size»'''
+                }
+                
+                // Types
+                typeInterpretation.elements += newElement
+                if(typeInterpretation instanceof PartialComplexTypeInterpretation) {
+                        typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
+                }
+                // ContainmentRelation
+                val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement]
+                relationInterpretation.relationlinks+=newLink
+                
+                // Scope propagation
+                scopePropagator.decrementTypeScope(typeInterpretation)
+                
+                // Existence
+                interpretation.newElements+=newElement
+                
+                // Do recursive object creation
+                for(newConstructor : recursiceObjectCreations) {
+                        createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator)
+                }
+                
+                return newElement
+        }
+        
+        protected def createObjectAction(
+                boolean nameNewElement,
+                PartialInterpretation interpretation,
+                PartialTypeInterpratation typeInterpretation,
+                Function0<DefinedElement> constructor,
+                List<ObjectCreationInterpretationData> recursiceObjectCreations,
+                ScopePropagator scopePropagator)
+        {
+                val newElement = constructor.apply
+                if(nameNewElement) {
+                        newElement.name = '''new «interpretation.newElements.size»'''
+                }
+                
+                // Types
+                typeInterpretation.elements += newElement
+                if(typeInterpretation instanceof PartialComplexTypeInterpretation) {
+                        typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
+                }
+                
+                // Scope propagation
+                scopePropagator.decrementTypeScope(typeInterpretation)
+                
+                // Existence
+                interpretation.newElements+=newElement
+                
+                // Do recursive object creation
+                for(newConstructor : recursiceObjectCreations) {
+                        createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator)
+                }
+                
+                return newElement
+        }
+        
+        protected def boolean createRelationLinkAction(DefinedElement src, DefinedElement trg, PartialRelationInterpretation relationInterpretation) {
+                val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg]
+                relationInterpretation.relationlinks += link
+        }
+        
+        protected def boolean createRelationLinkWithInverse(DefinedElement src, DefinedElement trg, PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation) {
+                val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg]
+                relationInterpretation.relationlinks += link
+                val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src]
+                inverseInterpretation.relationlinks += inverseLink
+        }
+}
+@Data
+class ObjectCreationInterpretationData {
+        PartialInterpretation interpretation
+        PartialTypeInterpratation typeInterpretation
+        PartialRelationInterpretation containerInterpretation
+        PartialRelationInterpretation containerInverseInterpretation
+        Function0<DefinedElement> constructor
+        List<ObjectCreationInterpretationData> recursiveConstructors = new LinkedList
 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend
index 8e264488..26ec7091 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend
@@ -196,8 +196,20 @@ class ParseUtil {
 }
 class FixedMetamodelProvider implements IMetamodelProvider {
+        
+        static val EPACKAGE_TO_PLUGIN_MAP = #{
+                PartialinterpretationPackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage",
+                LogicproblemPackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.logic.model",
+                LogiclanguagePackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.logic.model"
+        }
+        
+        static val EPACKAGE_TO_JAVA_PACKAGE_MAP = #{
+                PartialinterpretationPackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation",
+                LogicproblemPackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.logic.model.logicproblem",
+                LogiclanguagePackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage"
+        }
-        protected val List<EPackage> packages = new LinkedList
+        val List<EPackage> packages = new LinkedList
        new() {
                packages += PartialinterpretationPackage.eINSTANCE
@@ -213,15 +225,24 @@ class FixedMetamodelProvider implements IMetamodelProvider {
        }
        override boolean isGeneratedCodeAvailable(EPackage ePackage, ResourceSet set) {
-                true
+                EPACKAGE_TO_PLUGIN_MAP.containsKey(ePackage)
        }
        override String getModelPluginId(EPackage ePackage, ResourceSet set) {
-                return "hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage"
+                EPACKAGE_TO_PLUGIN_MAP.get(ePackage)
        }
        override String getQualifiedClassName(EClassifier classifier, EObject context) {
-                classifier.name
+                val instanceClassName = classifier.instanceClassName
+                if (instanceClassName !== null) {
+                        return instanceClassName
+                }
+                val javaPackage = EPACKAGE_TO_JAVA_PACKAGE_MAP.get(classifier.EPackage)
+                if (javaPackage !== null) {
+                        javaPackage + "." + classifier.name
+                } else {
+                        null
+                }
        }
        override loadEPackage(String uri, ResourceSet resourceSet) {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
index f7a1ce4f..d37acb6d 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
@@ -42,6 +42,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
 @Data class Problem2PartialInterpretationTrace {
        Map<TypeDeclaration, PartialComplexTypeInterpretation> type2Interpretation
@@ -233,7 +234,11 @@ class PartialInterpretationInitialiser {
        
        def private Map<RelationDeclaration, PartialRelationInterpretation> initRelations(PartialInterpretation interpretation, PrimitiveValueTrace trace) {
                val Map<RelationDeclaration, PartialRelationInterpretation> relation2Interpretation = new HashMap
-                for(relation : interpretation.problem.relations.filter(RelationDeclaration)) {
+                val definedRelationDeclarations = interpretation.problem.relations.filter(RelationDefinition).map[defines]
+                val undefinedRelationDeclarations = interpretation.problem.relations.filter(RelationDeclaration).filter[
+                        declared | !definedRelationDeclarations.exists[defined | defined === declared]
+                ]
+                for(relation : undefinedRelationDeclarations) {
                        val partialInterpretation = relation.initialisePartialRelationInterpretation
                        interpretation.partialrelationinterpretation += partialInterpretation
                        relation2Interpretation.put(relation,partialInterpretation)
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend
index 2b42a8b1..bdf402f3 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend
@@ -5,9 +5,13 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
+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.PartialComplexTypeInterpretation
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
 import java.util.HashMap
 import java.util.Map
 import java.util.Set
@@ -106,10 +110,38 @@ class PartialInterpretation2Gml {
                '''
        }
        
-        def protected transormTitle(DefinedElement object) {
+        def protected dispatch transormTitle(DefinedElement object) {
-                if(object.name!= null)object.name
+                if(object.name !== null) object.name.replace("\"", "")
                else "null"
        }
+        def protected dispatch transormTitle(BooleanElement object) {
+                if(object.valueSet) {
+                        object.value.toString
+                } else {
+                        "?"
+                }
+        }
+        def protected dispatch transormTitle(IntegerElement object) {
+                if(object.valueSet) {
+                        object.value.toString
+                } else {
+                        "?"
+                }
+        }
+        def protected dispatch transormTitle(RealElement object) {
+                if(object.valueSet) {
+                        object.value.toString
+                } else {
+                        "?"
+                }
+        }
+        def protected dispatch transormTitle(StringElement object) {
+                if(object.valueSet) {
+                        object.value.toString
+                } else {
+                        "?"
+                }
+        }
        
        def protected transformLink(
                PartialRelationInterpretation reference,
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)
        }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/GraphvizV8WithMemory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/GraphvizV8WithMemory.xtend
new file mode 100644
index 00000000..542289d4
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/GraphvizV8WithMemory.xtend
@@ -0,0 +1,16 @@
+package hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz
+import guru.nidi.graphviz.engine.GraphvizV8Engine
+class GraphvizV8WithMemory extends GraphvizV8Engine {
+        val int memory;
+        new(int memory) {
+                this.memory = memory
+                //this.
+        }
+        
+        override protected jsInitEnv() {
+                println super.jsInitEnv()
+                super.jsInitEnv()
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/PartialInterpretation2Graphviz.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/PartialInterpretation2Graphviz.xtend
index 78326207..cd0b3e00 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/PartialInterpretation2Graphviz.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/PartialInterpretation2Graphviz.xtend
@@ -30,6 +30,7 @@ import org.eclipse.xtext.xbase.lib.Functions.Function1
 import static guru.nidi.graphviz.model.Factory.*
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
 class GraphvizVisualiser implements PartialInterpretationVisualiser {
        
@@ -106,10 +107,10 @@ class GraphvizVisualiser implements PartialInterpretationVisualiser {
 //                      elements2Node.put(newElement,image)
 //              }
                
-                partialInterpretation.newElements.filter(BooleanElement).drawDataTypes([it.value.toString],elements2Node,elements2ID)
+                //partialInterpretation.newElements.filter(BooleanElement).drawDataTypes([it.value.toString],elements2Node,elements2ID)
-                partialInterpretation.newElements.filter(IntegerElement).drawDataTypes([it.value.toString],elements2Node,elements2ID)
+                //partialInterpretation.newElements.filter(IntegerElement).drawDataTypes([it.value.toString],elements2Node,elements2ID)
-                partialInterpretation.newElements.filter(StringElement).drawDataTypes(['''"«it.value.toString»"'''],elements2Node,elements2ID)
+                //partialInterpretation.newElements.filter(StringElement).drawDataTypes(['''"«it.value.toString»"'''],elements2Node,elements2ID)
-                partialInterpretation.newElements.filter(RealElement).drawDataTypes([it.value.toString],elements2Node,elements2ID)
+                //partialInterpretation.newElements.filter(RealElement).drawDataTypes([it.value.toString],elements2Node,elements2ID)
                
                // Drawing the edges
                val edges = new HashMap
@@ -135,35 +136,51 @@ class GraphvizVisualiser implements PartialInterpretationVisualiser {
                return new GraphvizVisualisation(graph)
        }
        
-        def protected <T extends DefinedElement> void drawDataTypes(Iterable<T> collection, Function1<T,String> namer, HashMap<DefinedElement, Node> elements2Node, HashMap<DefinedElement, String> elements2ID) {
+//      def protected <T extends DefinedElement> void drawDataTypes(Iterable<T> collection, Function1<T,String> namer, HashMap<DefinedElement, Node> elements2Node, HashMap<DefinedElement, String> elements2ID) {
-                for(booleanElementIndex: 0..<collection.size) {
+//              for(booleanElementIndex: 0..<collection.size) {
-                        val newElement = collection.get(booleanElementIndex)
+//                      val newElement = collection.get(booleanElementIndex)
-                        val id = namer.apply(newElement)
+//                      val name = namer.apply(newElement)
-                        val image = drawElement(newElement,id,false,emptySet,emptySet)
+//                      val image = drawElement(newElement,name,newElement.lookup(elements2ID),false,emptySet,emptySet)
-                        elements2ID.put(newElement,id)
+//                      elements2Node.put(newElement,image)
-                        elements2Node.put(newElement,image)
+//              }
-                }
+//      }
-        }
        
        def protected drawElement(DefinedElement element, String ID, boolean old, Set<Type> mustTypes, Set<Type> mayTypes) {
                var tableStyle =  ''' CELLSPACING="0" BORDER="2" CELLBORDER="0" CELLPADDING="1" STYLE="ROUNDED"'''
                if(typeColoringStyle==TypeColoringStyle::AVERAGE) {
                        tableStyle += ''' BGCOLOR="#«typePredicateColor(mustTypes).toBackgroundColorString»"'''
                }
-                val mainLabel = if(element.name !== null) {
+                val mainLabel = if(element instanceof PrimitiveElement) {
+                        if(element.isValueSet) {
+                                if(element instanceof BooleanElement) { element.value.toString }
+                                else if(element instanceof IntegerElement) { element.value.toString }
+                                else if(element instanceof RealElement) { element.value.toString }
+                                else if(element instanceof StringElement) { "\""+element.value.toString+"\"" }
+                        } else {
+                                "?"
+                        }
+                 }else if(element.name !== null) {
                        val parts = element.name.split("\\s+")
                        textWithSubSup(parts.getOrNull(0),parts.getOrNull(1),parts.getOrNull(2),null)
                } else {
                        val parts = ID.split("\\s+")
-                        textWithSubSup(parts.get(0),parts.get(1),parts.getOrNull(2),null)
+                        textWithSubSup(parts.getOrNull(0),parts.getOrNull(1),parts.getOrNull(2),null)
                }
-                val label = Label.html(
+                val hasNoCompexType = (mustTypes.empty) && (mayTypes.empty)
+                
+                val label = if(hasNoCompexType) {
+                        Label.html(
+                                '''<TABLE«tableStyle»>'''+
+                                '''<TR><TD COLSPAN="2">    «mainLabel»  </TD></TR>'''+
+                                '''</TABLE>''')
+                } else {
+                        Label.html(
                        '''<TABLE«tableStyle»>'''+
                        '''<TR><TD COLSPAN="2" BORDER="2" SIDES="B">«mainLabel»</TD></TR>'''+
                        '''«FOR mustTypeName : mustTypes.map[it.name].sort»«typePredicateDescription(mustTypeName,true)»«ENDFOR»'''+
                        '''«FOR mayTypeName : mayTypes.map[it.name].sort»«typePredicateDescription(mayTypeName,false)»«ENDFOR»'''+
                        '''</TABLE>''')
-                        
+                }
                val node = node(ID).with(label).with(
                        Shape.NONE
                        //,
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/VisualisationQueque.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/VisualisationQueque.xtend
index b067ba7d..6f003f80 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/VisualisationQueque.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/VisualisationQueque.xtend
@@ -3,15 +3,15 @@ package hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz
 import guru.nidi.graphviz.engine.Format
 import guru.nidi.graphviz.engine.Graphviz
 import guru.nidi.graphviz.engine.GraphvizEngine
-import guru.nidi.graphviz.engine.GraphvizV8Engine
 import guru.nidi.graphviz.model.Graph
 import java.io.File
 import java.io.IOException
 import java.util.concurrent.BlockingQueue
 import java.util.concurrent.CompletableFuture
 import java.util.concurrent.LinkedBlockingQueue
-import org.eclipse.xtend.lib.annotations.Data
 import java.util.function.Consumer
+import org.eclipse.xtend.lib.annotations.Data
+import guru.nidi.graphviz.engine.GraphvizV8Engine
 class VisualisationQueque {
        val BlockingQueue<VisualisationQueueEntry> taskQueue = new LinkedBlockingQueue
@@ -45,7 +45,7 @@ class VisualisationQueque {
                } else {
                        runnerThread = new Thread(new Runnable() {
                                override run() {
-                                        val engine = new GraphvizV8Engine()
+                                        val engine = new GraphvizV8Engine
                                        val nullConsumer = new Consumer<GraphvizEngine>() {
                                                override accept(GraphvizEngine t) {}
                                        }
@@ -69,7 +69,7 @@ class VisualisationQueque {
        private def execute(GraphvizEngine engine, Graph document, File targetFile, Format format) {
                Graphviz.useEngine(engine);
                try {
-                        Graphviz.fromGraph(document).render(format).toFile(targetFile)
+                        Graphviz.fromGraph(document).totalMemory(536870912).render(format).toFile(targetFile)
                        return null
                } catch(IOException e){
                        return e.message