Measurements WIP

14 files changed, 329 insertions, 74 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 23632d4d..e45ec1c8 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
@@ -5,6 +5,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem

 import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver

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

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

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator

@@ -46,16 +47,28 @@ class ModelGenerationStatistics {
         public var long preliminaryTypeAnalisisTime = 0

 

         public var int decisionsTried = 0

-        

+

         synchronized def incrementDecisionCount() {

                 decisionsTried++

         }

+

+        public var int transformationInvocations

         

+        synchronized def incrementTransformationCount() {

+                transformationInvocations++

+        }

+

         public var int scopePropagatorInvocations

-        

+

         synchronized def incrementScopePropagationCount() {

                 scopePropagatorInvocations++

         }

+        

+        public var int scopePropagatorSolverInvocations

+

+        synchronized def incrementScopePropagationSolverCount() {

+                scopePropagatorSolverInvocations++

+        }

 }

 

 @Data class ModelGenerationMethod {

@@ -93,6 +106,7 @@ class ModelGenerationMethodProvider {
                 boolean nameNewElements,

                 TypeInferenceMethod typeInferenceMethod,

                 ScopePropagatorStrategy scopePropagatorStrategy,

+                Collection<LinearTypeConstraintHint> hints,

                 DocumentationLevel debugLevel

         ) {

                 val statistics = new ModelGenerationStatistics

@@ -103,8 +117,8 @@ class ModelGenerationMethodProvider {
 

                 val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem)

                 val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries,

-                        workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles)

-                val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries, statistics)

+                        workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles)

+                val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics)

                 scopePropagator.propagateAllScopeConstraints

                 val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator,

                         nameNewElements, statistics)

@@ -138,14 +152,20 @@ class ModelGenerationMethodProvider {
         }

 

         private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy,

-                PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) {

+                PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, GeneratedPatterns queries,

+                ModelGenerationStatistics statistics) {

+                if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) {

+                        throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.")

+                }

                 switch (scopePropagatorStrategy) {

-                        case ScopePropagatorStrategy.Count:

+                        case ScopePropagatorStrategy.None,

+                        case ScopePropagatorStrategy.Basic:

                                 new ScopePropagator(emptySolution, statistics)

                         case ScopePropagatorStrategy.BasicTypeHierarchy:

                                 new TypeHierarchyScopePropagator(emptySolution, statistics)

                         ScopePropagatorStrategy.Polyhedral: {

                                 val types = queries.refineObjectQueries.keySet.map[newType].toSet

+                                val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName]

                                 val solver = switch (scopePropagatorStrategy.solver) {

                                         case Z3Integer:

                                                 new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds)

@@ -160,7 +180,8 @@ class ModelGenerationMethodProvider {
                                                         scopePropagatorStrategy.solver)

                                 }

                                 new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries,

-                                        queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing)

+                                        queries.hasElementInContainmentQuery, allPatternsByName, hints, solver,

+                                        scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic)

                         }

                         default:

                                 throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy)

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend
new file mode 100644
index 00000000..8c21ca1d
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend
@@ -0,0 +1,30 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+
+interface LinearTypeExpressionBuilderFactory {
+        def ViatraQueryMatcher<? extends IPatternMatch> createMatcher(String queryName)
+        
+        def LinearTypeExpressionBuilder createBuilder()
+}
+
+interface LinearTypeExpressionBuilder {
+        def LinearTypeExpressionBuilder add(int scale, Type type)
+
+        def LinearBoundedExpression build()
+}
+
+@FunctionalInterface
+interface RelationConstraintUpdater {
+        def void update(PartialInterpretation p)
+}
+
+interface LinearTypeConstraintHint {
+        def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator)
+        
+        def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory)
+}
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 7c05e818..51dba244 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
@@ -1,5 +1,7 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
 
+import com.google.common.cache.Cache
+import com.google.common.cache.CacheBuilder
 import com.google.common.collect.ImmutableList
 import com.google.common.collect.ImmutableMap
 import com.google.common.collect.ImmutableSet
@@ -15,6 +17,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
 import java.util.ArrayDeque
 import java.util.ArrayList
+import java.util.Collection
 import java.util.HashMap
 import java.util.HashSet
 import java.util.List
@@ -29,26 +32,33 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope
 import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
 
 class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
+        static val CACHE_SIZE = 10000
+        
+        val boolean updateHeuristic
         val Map<Scope, LinearBoundedExpression> scopeBounds
         val LinearBoundedExpression topLevelBounds
         val Polyhedron polyhedron
         val PolyhedronSaturationOperator operator
         val Set<Relation> relevantRelations
+        val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build
         List<RelationConstraintUpdater> updaters = emptyList
 
         new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes,
                 Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries,
                 IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery,
-                PolyhedronSolver solver, boolean propagateRelations) {
+                Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName,
+                Collection<LinearTypeConstraintHint> hints, PolyhedronSolver solver, boolean propagateRelations,
+                boolean updateHeuristic) {
                 super(p, statistics)
+                this.updateHeuristic = updateHeuristic
                 val builder = new PolyhedronBuilder(p)
                 builder.buildPolyhedron(possibleNewDynamicTypes)
                 scopeBounds = builder.scopeBounds
                 topLevelBounds = builder.topLevelBounds
                 polyhedron = builder.polyhedron
                 operator = solver.createSaturationOperator(polyhedron)
+                propagateAllScopeConstraints()
                 if (propagateRelations) {
-                        propagateAllScopeConstraints()
                         val maximumNumberOfNewNodes = topLevelBounds.upperBound
                         if (maximumNumberOfNewNodes === null) {
                                 throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded")
@@ -57,7 +67,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                                 throw new IllegalStateException("Maximum number of new nodes is not positive")
                         }
                         builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery,
-                                maximumNumberOfNewNodes)
+                                allPatternsByName, hints, maximumNumberOfNewNodes)
                         relevantRelations = builder.relevantRelations
                         updaters = builder.updaters
                 } else {
@@ -66,21 +76,40 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
         }
 
         override void doPropagateAllScopeConstraints() {
+                super.doPropagateAllScopeConstraints()
                 resetBounds()
                 populatePolyhedronFromScope()
 //              println(polyhedron)
-                val result = operator.saturate()
-//              println(polyhedron)
-                if (result == PolyhedronSaturationResult.EMPTY) {
-                        setScopesInvalid()
-                } else {
-                        populateScopesFromPolyhedron()
-                        if (result != PolyhedronSaturationResult.SATURATED) {
-                                super.propagateAllScopeConstraints()
+                val signature = polyhedron.createSignature
+                val cachedSignature = cache.getIfPresent(signature)
+                switch (cachedSignature) {
+                        case null: {
+                                statistics.incrementScopePropagationSolverCount
+                                val result = operator.saturate()
+                                if (result == PolyhedronSaturationResult.EMPTY) {
+                                        cache.put(signature, PolyhedronSignature.EMPTY)
+                                        setScopesInvalid()
+                                } else {
+                                        val resultSignature = polyhedron.createSignature
+                                        cache.put(signature, resultSignature)
+                                        populateScopesFromPolyhedron()
+                                }
                         }
+                        case PolyhedronSignature.EMPTY:
+                                setScopesInvalid()
+                        PolyhedronSignature.Bounds: {
+                                polyhedron.applySignature(signature)
+                                populateScopesFromPolyhedron()
+                        }
+                        default:
+                                throw new IllegalStateException("Unknown polyhedron signature: " + signature)
+                }
+//              println(polyhedron)
+                if (updateHeuristic) {
+                        copyScopeBoundsToHeuristic()
                 }
         }
-        
+
         override propagateAdditionToRelation(Relation r) {
                 super.propagateAdditionToRelation(r)
                 if (relevantRelations.contains(r)) {
@@ -186,7 +215,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
         }
 
         @FinalFieldsConstructor
-        private static class PolyhedronBuilder {
+        private static class PolyhedronBuilder implements LinearTypeExpressionBuilderFactory {
                 static val INFINITY_SCALE = 10
 
                 val PartialInterpretation p
@@ -197,6 +226,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                 Map<Type, LinearBoundedExpression> typeBounds
                 int infinity
                 ViatraQueryEngine queryEngine
+                Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName
                 ImmutableList.Builder<RelationConstraintUpdater> updatersBuilder
 
                 Map<Scope, LinearBoundedExpression> scopeBounds
@@ -222,9 +252,11 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                 def buildMultiplicityConstraints(
                         Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> constraints,
                         IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery,
-                        int maximumNuberOfNewNodes) {
+                        Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName,
+                        Collection<LinearTypeConstraintHint> hints, int maximumNuberOfNewNodes) {
                         infinity = maximumNuberOfNewNodes * INFINITY_SCALE
                         queryEngine = ViatraQueryEngine.on(new EMFScope(p))
+                        this.allPatternsByName = allPatternsByName
                         updatersBuilder = ImmutableList.builder
                         val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType]
                         for (pair : containmentConstraints.entrySet) {
@@ -238,10 +270,13 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                                 }
                         }
                         buildRelevantRelations(constraints.keySet)
+                        for (hint : hints) {
+                                updatersBuilder.add(hint.createConstraintUpdater(this))
+                        }
                         updaters = updatersBuilder.build
                         addCachedConstraintsToPolyhedron()
                 }
-                
+
                 private def buildRelevantRelations(Set<RelationMultiplicityConstraint> constraints) {
                         val builder = ImmutableSet.builder
                         for (constraint : constraints) {
@@ -345,7 +380,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                         }
                 }
 
-                private def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) {
+                private static def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) {
                         for (pair : a.entrySet) {
                                 val dimension = pair.key
                                 val currentValue = accumulator.get(pair.key) ?: 0
@@ -411,14 +446,41 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                         }
                         scopeBoundsBuilder.build
                 }
+
+                override createMatcher(String queryName) {
+                        val querySpecification = allPatternsByName.get(queryName)
+                        if (querySpecification === null) {
+                                throw new IllegalArgumentException("Unknown pattern: " + queryName)
+                        }
+                        querySpecification.getMatcher(queryEngine)
+                }
+
+                override createBuilder() {
+                        new PolyhedronBuilderLinearTypeExpressionBuilder(this)
+                }
         }
 
-        private static interface RelationConstraintUpdater {
-                def void update(PartialInterpretation p)
+        @FinalFieldsConstructor
+        private static class PolyhedronBuilderLinearTypeExpressionBuilder implements LinearTypeExpressionBuilder {
+                val PolyhedronBuilder polyhedronBuilder
+                val Map<Dimension, Integer> coefficients = new HashMap
+
+                override add(int scale, Type type) {
+                        val typeCoefficients = polyhedronBuilder.subtypeDimensions.get(type)
+                        if (typeCoefficients === null) {
+                                throw new IllegalArgumentException("Unknown type: " + type)
+                        }
+                        PolyhedronBuilder.addCoefficients(coefficients, scale, typeCoefficients)
+                        this
+                }
+
+                override build() {
+                        polyhedronBuilder.toExpression(coefficients)
+                }
         }
 
         @FinalFieldsConstructor
-        static class ContainmentConstraintUpdater implements RelationConstraintUpdater {
+        private static class ContainmentConstraintUpdater implements RelationConstraintUpdater {
                 val String name
                 val LinearBoundedExpression orphansLowerBound
                 val LinearBoundedExpression orphansUpperBound
@@ -460,7 +522,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
         }
 
         @FinalFieldsConstructor
-        static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater {
+        private static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater {
                 val LinearBoundedExpression typeCardinality
                 val ViatraQueryMatcher<? extends IPatternMatch> hasElementInContainmentMatcher
 
@@ -479,7 +541,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
         }
 
         @FinalFieldsConstructor
-        static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater {
+        private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater {
                 val String name
                 val LinearBoundedExpression availableMultiplicityExpression
                 val ViatraQueryMatcher<? extends IPatternMatch> unfinishedMultiplicityMatcher
@@ -500,7 +562,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
         }
 
         @FinalFieldsConstructor
-        static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater {
+        private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater {
                 val String name
                 val LinearBoundedExpression targetCardinalityExpression
                 val ViatraQueryMatcher<? extends IPatternMatch> unrepairableMultiplicityMatcher
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend
index 9c6cb82e..4e046190 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend
@@ -3,6 +3,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
 import java.util.List
 import java.util.Map
 import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.Data
 import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
 
 interface PolyhedronSolver {
@@ -52,16 +53,66 @@ class Polyhedron {
         val List<LinearBoundedExpression> expressionsToSaturate
 
         override toString() '''
-        Dimensions:
-                «FOR dimension : dimensions»
-                        «dimension»
-                «ENDFOR»
-        Constraints:
-                «FOR constraint : constraints»
-                        «constraint»
-                «ENDFOR»
+                Dimensions:
+                        «FOR dimension : dimensions»
+                                «dimension»
+                        «ENDFOR»
+                Constraints:
+                        «FOR constraint : constraints»
+                                «constraint»
+                        «ENDFOR»
         '''
 
+        def createSignature() {
+                val size = dimensions.size + constraints.size
+                val lowerBounds = newArrayOfSize(size)
+                val upperBounds = newArrayOfSize(size)
+                var int i = 0
+                for (dimension : dimensions) {
+                        lowerBounds.set(i, dimension.lowerBound)
+                        upperBounds.set(i, dimension.upperBound)
+                        i++
+                }
+                for (constraint : constraints) {
+                        lowerBounds.set(i, constraint.lowerBound)
+                        upperBounds.set(i, constraint.upperBound)
+                        i++
+                }
+                new PolyhedronSignature.Bounds(lowerBounds, upperBounds)
+        }
+
+        def applySignature(PolyhedronSignature.Bounds signature) {
+                val lowerBounds = signature.lowerBounds
+                val upperBounds = signature.upperBounds
+                var int i = 0
+                for (dimension : dimensions) {
+                        dimension.lowerBound = lowerBounds.get(i)
+                        dimension.upperBound = upperBounds.get(i)
+                        i++
+                }
+                for (constraint : constraints) {
+                        constraint.lowerBound = lowerBounds.get(i)
+                        constraint.upperBound = upperBounds.get(i)
+                        i++
+                }
+        }
+}
+
+abstract class PolyhedronSignature {
+        public static val EMPTY = new PolyhedronSignature {
+                override toString() {
+                        "PolyhedronSignature.EMPTY"
+                }
+        }
+
+        private new() {
+        }
+
+        @Data
+        static class Bounds extends PolyhedronSignature {
+                val Integer[] lowerBounds
+                val Integer[] upperBounds
+        }
 }
 
 @Accessors
@@ -80,6 +131,11 @@ abstract class LinearBoundedExpression {
                         upperBound = tighterBound
                 }
         }
+
+        def void assertEqualsTo(int bound) {
+                tightenLowerBound(bound)
+                tightenUpperBound(bound)
+        }
 }
 
 @Accessors
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend
index 52a390a8..013e53e1 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend
@@ -117,9 +117,12 @@ class RelationConstraintCalculator {
                         var inverseUpperMultiplicity = -1
                         val inverseRelation = inverseRelations.get(relation)
                         if (inverseRelation !== null) {
-                                inverseUpperMultiplicity = upperMultiplicities.get(relation)
+                                inverseUpperMultiplicity = upperMultiplicities.get(inverseRelation)
                                 container = containmentRelations.contains(inverseRelation)
                         }
+                        if (containment) {
+                                inverseUpperMultiplicity = 1
+                        }
                         val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container,
                                 lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity)
                         if (constraint.isActive) {
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 0bdb202e..2376fb38 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
@@ -14,7 +14,7 @@ import org.eclipse.xtend.lib.annotations.Accessors
 

 class ScopePropagator {

         @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation

-        val ModelGenerationStatistics statistics

+        @Accessors(PROTECTED_GETTER) val ModelGenerationStatistics statistics

         val Map<PartialTypeInterpratation, Scope> type2Scope

         @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes

         @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes

@@ -59,12 +59,21 @@ class ScopePropagator {
                                 }

                         }

                 } while (changed)

+                

+                copyScopeBoundsToHeuristic()

         }

 

         def propagateAllScopeConstraints() {

                 statistics.incrementScopePropagationCount()

                 doPropagateAllScopeConstraints()

         }

+        

+        protected def copyScopeBoundsToHeuristic() {

+                partialInterpretation.minNewElementsHeuristic = partialInterpretation.minNewElements

+                for (scope : partialInterpretation.scopes) {

+                        scope.minNewElementsHeuristic = scope.minNewElements

+                }

+        }

 

         protected def void doPropagateAllScopeConstraints() {

                 // Nothing to propagate.

@@ -73,12 +82,17 @@ class ScopePropagator {
         def propagateAdditionToType(PartialTypeInterpratation t) {

 //              println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')

                 val targetScope = type2Scope.get(t)

-                targetScope.removeOne

-                val sups = superScopes.get(targetScope)

-                sups.forEach[removeOne]

+                if (targetScope !== null) {

+                        targetScope.removeOne

+                        val sups = superScopes.get(targetScope)

+                        sups.forEach[removeOne]

+                }

                 if (this.partialInterpretation.minNewElements > 0) {

                         this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1

                 }

+                if (this.partialInterpretation.minNewElementsHeuristic > 0) {

+                        this.partialInterpretation.minNewElementsHeuristic = this.partialInterpretation.minNewElementsHeuristic - 1

+                }

                 if (this.partialInterpretation.maxNewElements > 0) {

                         this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1

                 } else if (this.partialInterpretation.maxNewElements === 0) {

@@ -105,5 +119,8 @@ class ScopePropagator {
                 if (scope.minNewElements > 0) {

                         scope.minNewElements = scope.minNewElements - 1

                 }

+                if (scope.minNewElementsHeuristic > 0) {

+                        scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1

+                }

         }

 }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend
index b0ed75cb..3165917a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend
@@ -16,7 +16,9 @@ enum PolyhedralScopePropagatorSolver {
 }
 
 abstract class ScopePropagatorStrategy {
-        public static val Count = new Simple("Count")
+        public static val None = new Simple("None")
+        
+        public static val Basic = new Simple("Basic")
 
         public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy")
 
@@ -47,14 +49,19 @@ abstract class ScopePropagatorStrategy {
 
                 val PolyhedralScopePropagatorConstraints constraints
                 val PolyhedralScopePropagatorSolver solver
+                val boolean updateHeuristic
                 val double timeoutSeconds
 
                 @FinalFieldsConstructor
                 new() {
                 }
 
+                new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver, boolean updateHeuristic) {
+                        this(constraints, solver, updateHeuristic, UNLIMITED_TIME)
+                }
+                
                 new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) {
-                        this(constraints, solver, UNLIMITED_TIME)
+                        this(constraints, solver, true)
                 }
 
                 override requiresUpperBoundIndexing() {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend
index be8ef00a..d1704b39 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend
@@ -27,12 +27,16 @@ class TypeHierarchyScopePropagator extends ScopePropagator {
         }
 
         private def propagateLowerLimitUp(Scope subScope, Scope superScope) {
+                var changed = false
                 if (subScope.minNewElements > superScope.minNewElements) {
                         superScope.minNewElements = subScope.minNewElements
-                        return true
-                } else {
-                        return false
+                        changed = true
+                }
+                if (subScope.minNewElementsHeuristic > superScope.minNewElementsHeuristic) {
+                        superScope.minNewElementsHeuristic = subScope.minNewElementsHeuristic
+                        changed = true
                 }
+                changed
         }
 
         private def propagateUpperLimitDown(Scope subScope, Scope superScope) {
@@ -50,16 +54,20 @@ class TypeHierarchyScopePropagator extends ScopePropagator {
         }
 
         private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) {
+                var changed = false
                 if (subScope.minNewElements > p.minNewElements) {
 //                      println('''
 //                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes
 //                      p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements»
 //                      ''')
                         p.minNewElements = subScope.minNewElements
-                        return true
-                } else {
-                        return false
+                        changed = true
+                }
+                if (subScope.minNewElementsHeuristic > p.minNewElementsHeuristic) {
+                        p.minNewElementsHeuristic = subScope.minNewElementsHeuristic
+                        changed = true
                 }
+                changed
         }
 
         private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend
index 23444956..3b831433 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend
@@ -13,6 +13,7 @@ import java.math.BigDecimal
 import java.math.MathContext
 import java.math.RoundingMode
 import java.util.Map
+import org.eclipse.xtend.lib.annotations.Accessors
 import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
 
 class Z3PolyhedronSolver implements PolyhedronSolver {
@@ -28,10 +29,33 @@ class Z3PolyhedronSolver implements PolyhedronSolver {
         }
 
         override createSaturationOperator(Polyhedron polyhedron) {
+                new DisposingZ3SaturationOperator(this, polyhedron)
+        }
+
+        def createPersistentSaturationOperator(Polyhedron polyhedron) {
                 new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds)
         }
 }
 
+@FinalFieldsConstructor
+class DisposingZ3SaturationOperator implements PolyhedronSaturationOperator {
+        val Z3PolyhedronSolver solver
+        @Accessors val Polyhedron polyhedron
+
+        override saturate() {
+                val persistentOperator = solver.createPersistentSaturationOperator(polyhedron)
+                try {
+                        persistentOperator.saturate
+                } finally {
+                        persistentOperator.close
+                }
+        }
+
+        override close() throws Exception {
+                // Nothing to close.
+        }
+}
+
 class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
         static val INFINITY_SYMBOL_NAME = "oo"
         static val MULT_SYMBOL_NAME = "*"
@@ -106,9 +130,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
                                 IntNum:
                                         resultExpr.getInt()
                                 RatNum:
-                                        floor(resultExpr)
+                                        ceil(resultExpr)
                                 AlgebraicNum:
-                                        floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING))
+                                        ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING))
                                 default:
                                         if (isNegativeInfinity(resultExpr)) {
                                                 null
@@ -136,9 +160,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
                                 IntNum:
                                         resultExpr.getInt()
                                 RatNum:
-                                        ceil(resultExpr)
+                                        floor(resultExpr)
                                 AlgebraicNum:
-                                        ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING))
+                                        floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING))
                                 default:
                                         if (isPositiveInfinity(resultExpr)) {
                                                 null
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 1b0db90e..5c35fb54 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
@@ -16,8 +16,11 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Transform
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality

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

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

+import java.util.Collection

 import java.util.HashMap

 import java.util.Map

 import org.eclipse.emf.ecore.EAttribute

@@ -26,7 +29,6 @@ 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 hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy

 

 class PatternGenerator {

         @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this)

@@ -104,7 +106,9 @@ class PatternGenerator {
         }

 

         def isRepresentative(Relation relation, Relation inverse) {

-                if (inverse === null) {

+                if (relation === null) {

+                        return false

+                } else if (inverse === null) {

                         return true

                 } else {

                         relation.name.compareTo(inverse.name) < 1

@@ -144,7 +148,8 @@ class PatternGenerator {
                 PartialInterpretation emptySolution,

                 Map<String, PQuery> fqn2PQuery,

                 TypeAnalysisResult typeAnalysisResult,

-                RelationConstraints constraints

+                RelationConstraints constraints,

+                Collection<LinearTypeConstraintHint> hints

         ) {

 

                 return '''

@@ -294,6 +299,13 @@ class PatternGenerator {
                         // 4.3 Relation refinement

                         //////////

                         «relationRefinementGenerator.generateRefineReference(problem)»

+                        

+                        //////////

+                        // 5 Hints

+                        //////////

+                        «FOR hint : hints»

+                                «hint.getAdditionalPatterns(this)»

+                        «ENDFOR»

                 '''

         }

 }

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 eadf0ae0..f5c85524 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
@@ -26,6 +26,7 @@ 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

 class GeneratedPatterns {

@@ -62,7 +63,8 @@ class PatternProvider {
 

         def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics,

                 Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod,

-                ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, boolean writeToFile) {

+                ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, 

+                Collection<LinearTypeConstraintHint> hints, boolean writeToFile) {

                 val fqn2Query = existingQueries.toMap[it.fullyQualifiedName]

                 val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy)

                 val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) {

@@ -75,7 +77,7 @@ class PatternProvider {
                                 null

                         }

                 val baseIndexerFile = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query,

-                        typeAnalysisResult, relationConstraints)

+                        typeAnalysisResult, relationConstraints, hints)

                 if (writeToFile) {

                         workspace.writeText('''generated3valued.vql_deactivated''', baseIndexerFile)

                 }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
index fa73c861..d915d47e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend
@@ -44,7 +44,7 @@ class RelationRefinementGenerator {
 

         def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName,

                 String inverseInterpretationName, String sourceName,

-                String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»inverseInterpretationName, «ENDIF»«sourceName», «targetName»);'''

+                String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);'''

 

         def getRefineRelationQueries(LogicProblem p) {

 //              val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend
index 15b5a047..a8a07756 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend
@@ -1,5 +1,6 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns

 

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint

@@ -76,21 +77,26 @@ class UnfinishedIndexer {
                         «IF indexUpperMultiplicities»

                                 «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse»

                                         private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) {

-                                                find interpretation(problem,interpretation);

-                                                find mustExist(problem,interpretation,source);

-                                                «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")»

-                                                find mustExist(problem,interpretation,target);

-                                                «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")»

-                                                neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)»

-                                                «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)»

+                                                «IF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration»

+                                                        «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")»

+                                                «ELSE»

+                                                        «IF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration»

+                                                                «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")»

+                                                        «ELSE»

+                                                                find interpretation(problem,interpretation);

+                                                                find mustExist(problem,interpretation,source);

+                                                                «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")»

+                                                                find mustExist(problem,interpretation,target);

+                                                                «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")»

+                                                                neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)»

+                                                                «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)»

+                                                        «ENDIF»

+                                                «ENDIF»

                                         }

                                 «ENDIF»

                                 

                                 «IF constraint.constrainsUnrepairable»

                                         private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) {

-                                                find interpretation(problem,interpretation);

-                                                find mustExist(problem,interpretation,object);

-                                                «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")»

                                                 find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity);

                                                 numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _);

                                                 check(numberOfRepairMatches < missingMultiplicity);

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 bf816de9..7891ebd8 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
@@ -67,7 +67,8 @@ class RefinementRuleProvider {
                 if(containmentRelation != null) {

                         if(inverseRelation!= null) {

                                 ruleBuilder.action[match |

-                                        //println(name)

+                                        statistics.incrementTransformationCount

+//                                      println(name)

                                         val startTime = System.nanoTime

                                         //val problem = match.get(0) as LogicProblem

                                         val interpretation = match.get(1) as PartialInterpretation

@@ -107,7 +108,8 @@ class RefinementRuleProvider {
                                 ]

                         } else {

                                 ruleBuilder.action[match |

-                                        //println(name)

+                                        statistics.incrementTransformationCount

+//                                      println(name)

                                         val startTime = System.nanoTime

                                         //val problem = match.get(0) as LogicProblem

                                         val interpretation = match.get(1) as PartialInterpretation

@@ -144,6 +146,9 @@ class RefinementRuleProvider {
                         }

                 } else {

                         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

@@ -198,8 +203,9 @@ class RefinementRuleProvider {
                         .precondition(lhs)

                 if (inverseRelation == null) {

                         ruleBuilder.action [ match |

+                                statistics.incrementTransformationCount

                             val startTime = System.nanoTime

-                                //println(name)

+//                              println(name)

                                 // val problem = match.get(0) as LogicProblem

                                 // val interpretation = match.get(1) as PartialInterpretation

                                 val relationInterpretation = match.get(2) as PartialRelationInterpretation

@@ -217,8 +223,9 @@ class RefinementRuleProvider {
                         ]

                 } else {

                         ruleBuilder.action [ match |

+                                statistics.incrementTransformationCount

                             val startTime = System.nanoTime

-                                //println(name)

+//                              println(name)

                                 // val problem = match.get(0) as LogicProblem

                                 // val interpretation = match.get(1) as PartialInterpretation

                                 val relationInterpretation = match.get(2) as PartialRelationInterpretation