Configurability and better statistics for measurements

12 files changed, 218 insertions, 61 deletions

diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
index 8ea674d3..807d217a 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
@@ -293,7 +293,7 @@ class GenerationTaskExecutor {
                                         statistics.put("Domain to logic transformation time",domain2LogicTransformationTime/1000000)

                                         statistics.put("Logic to solver transformation time",solution.statistics.transformationTime)

                                         statistics.put("Solver time",solution.statistics.solverTime)

-                                        statistics.put("Postprocessing time",solutionVisualisationTime)

+                                        statistics.put("Postprocessing time",solutionVisualisationTime/1000000)

                                         for(entry: solution.statistics.entries) {

                                                 statistics.put(entry.name,statisticsUtil.readValue(entry))

                                         }

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 4b278188..8e061b63 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 org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 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

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

 

 class ModelGenerationStatistics {

         public var long transformationExecutionTime = 0

@@ -35,7 +36,25 @@ class ModelGenerationStatistics {
                 transformationExecutionTime += amount

         }

 

-        public var long PreliminaryTypeAnalisisTime = 0

+        public var long scopePropagationTime = 0

+

+        synchronized def addScopePropagationTime(long amount) {

+                scopePropagationTime += amount

+        }

+

+        public var long preliminaryTypeAnalisisTime = 0

+

+        public var int decisionsTried = 0

+        

+        synchronized def incrementDecisionCount() {

+                decisionsTried++

+        }

+        

+        public var int scopePropagatorInvocations

+        

+        synchronized def incrementScopePropagationCount() {

+                scopePropagatorInvocations++

+        }

 }

 

 @Data class ModelGenerationMethod {

@@ -84,12 +103,12 @@ 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)

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

                 scopePropagator.propagateAllScopeConstraints

-                val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>>

-                objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator,

+                val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator,

                         nameNewElements, statistics)

-                val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, statistics)

+                val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator,

+                        statistics)

 

                 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries)

                 val unfinishedWF = queries.getUnfinishedWFQueries.values

@@ -118,15 +137,26 @@ class ModelGenerationMethodProvider {
         }

 

         private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy,

-                PartialInterpretation emptySolution, GeneratedPatterns queries) {

+                PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) {

                 switch (scopePropagatorStrategy) {

-                        case BasicTypeHierarchy:

-                                new ScopePropagator(emptySolution)

-                        case PolyhedralTypeHierarchy,

-                        case PolyhedralRelations: {

+                        case ScopePropagatorStrategy.BasicTypeHierarchy:

+                                new ScopePropagator(emptySolution, statistics)

+                        ScopePropagatorStrategy.Polyhedral: {

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

-                                val solver = new CbcPolyhedronSolver

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

+                                val solver = switch (scopePropagatorStrategy.solver) {

+                                        case Z3Integer:

+                                                new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds)

+                                        case Z3Real:

+                                                new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds)

+                                        case Cbc:

+                                                new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true)

+                                        case Clp:

+                                                new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true)

+                                        default:

+                                                throw new IllegalArgumentException("Unknown polyhedron solver: " +

+                                                        scopePropagatorStrategy.solver)

+                                }

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

                                         queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing)

                         }

                         default:

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 f6b101b6..e7e40ab0 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
@@ -2,9 +2,12 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
 
 import com.google.common.collect.ImmutableList
 import com.google.common.collect.ImmutableMap
+import com.google.common.collect.ImmutableSet
 import com.google.common.collect.Maps
 import com.google.common.collect.Sets
+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.viatrasolver.logic2viatra.ModelGenerationStatistics
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnifinishedMultiplicityQueries
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
@@ -30,13 +33,14 @@ class PolyhedronScopePropagator extends ScopePropagator {
         val LinearBoundedExpression topLevelBounds
         val Polyhedron polyhedron
         val PolyhedronSaturationOperator operator
+        val Set<Relation> relevantRelations
         List<RelationConstraintUpdater> updaters = emptyList
 
-        new(PartialInterpretation p, Set<? extends Type> possibleNewDynamicTypes,
+        new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes,
                 Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries,
                 IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery,
                 PolyhedronSolver solver, boolean propagateRelations) {
-                super(p)
+                super(p, statistics)
                 val builder = new PolyhedronBuilder(p)
                 builder.buildPolyhedron(possibleNewDynamicTypes)
                 scopeBounds = builder.scopeBounds
@@ -54,11 +58,14 @@ class PolyhedronScopePropagator extends ScopePropagator {
                         }
                         builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery,
                                 maximumNumberOfNewNodes)
+                        relevantRelations = builder.relevantRelations
                         updaters = builder.updaters
+                } else {
+                        relevantRelations = emptySet
                 }
         }
 
-        override void propagateAllScopeConstraints() {
+        override void doPropagateAllScopeConstraints() {
                 resetBounds()
                 populatePolyhedronFromScope()
 //              println(polyhedron)
@@ -73,6 +80,13 @@ class PolyhedronScopePropagator extends ScopePropagator {
                         }
                 }
         }
+        
+        override propagateAdditionToRelation(Relation r) {
+                super.propagateAdditionToRelation(r)
+                if (relevantRelations.contains(r)) {
+                        propagateAllScopeConstraints()
+                }
+        }
 
         def resetBounds() {
                 for (dimension : polyhedron.dimensions) {
@@ -188,6 +202,7 @@ class PolyhedronScopePropagator extends ScopePropagator {
                 Map<Scope, LinearBoundedExpression> scopeBounds
                 LinearBoundedExpression topLevelBounds
                 Polyhedron polyhedron
+                Set<Relation> relevantRelations
                 List<RelationConstraintUpdater> updaters
 
                 def buildPolyhedron(Set<? extends Type> possibleNewDynamicTypes) {
@@ -222,9 +237,21 @@ class PolyhedronScopePropagator extends ScopePropagator {
                                         buildNonContainmentConstraints(constraint, pair.value)
                                 }
                         }
+                        buildRelevantRelations(constraints.keySet)
                         updaters = updatersBuilder.build
                         addCachedConstraintsToPolyhedron()
                 }
+                
+                private def buildRelevantRelations(Set<RelationMultiplicityConstraint> constraints) {
+                        val builder = ImmutableSet.builder
+                        for (constraint : constraints) {
+                                builder.add(constraint.relation)
+                                if (constraint.inverseRelation !== null) {
+                                        builder.add(constraint.inverseRelation)
+                                }
+                        }
+                        relevantRelations = builder.build
+                }
 
                 private def addCachedConstraintsToPolyhedron() {
                         val constraints = new HashSet
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 ffa9e6e6..52a390a8 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
@@ -20,6 +20,7 @@ class RelationConstraints {
 @Data
 class RelationMultiplicityConstraint {
         Relation relation
+        Relation inverseRelation
         boolean containment
         boolean container
         int lowerBound
@@ -47,7 +48,7 @@ class RelationMultiplicityConstraint {
         }
 
         def constrainsRemainingInverse() {
-                !containment && inverseUpperBoundFinite
+                lowerBound >= 1 && !containment && inverseUpperBoundFinite
         }
 
         def constrainsRemainingContents() {
@@ -119,8 +120,8 @@ class RelationConstraintCalculator {
                                 inverseUpperMultiplicity = upperMultiplicities.get(relation)
                                 container = containmentRelations.contains(inverseRelation)
                         }
-                        val constraint = new RelationMultiplicityConstraint(relation, containment, container, lowerMultiplicity,
-                                upperMultiplicity, inverseUpperMultiplicity)
+                        val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container,
+                                lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity)
                         if (constraint.isActive) {
                                 if (relation.parameters.size != 2) {
                                         throw new IllegalArgumentException('''Relation «relation.name» has multiplicity or containment constraints, but it is not binary''')
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 3b442cd3..7be6635c 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
@@ -1,5 +1,7 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality

 

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

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics

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

@@ -11,14 +13,15 @@ import java.util.Set
 import org.eclipse.xtend.lib.annotations.Accessors

 

 class ScopePropagator {

-        @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation

-        Map<PartialTypeInterpratation, Scope> type2Scope

-

+        @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation

+        val ModelGenerationStatistics statistics

+        val Map<PartialTypeInterpratation, Scope> type2Scope

         val Map<Scope, Set<Scope>> superScopes

         val Map<Scope, Set<Scope>> subScopes

 

-        new(PartialInterpretation p) {

+        new(PartialInterpretation p, ModelGenerationStatistics statistics) {

                 partialInterpretation = p

+                this.statistics = statistics

                 type2Scope = new HashMap

                 for (scope : p.scopes) {

                         type2Scope.put(scope.targetTypeInterpretation, scope)

@@ -57,8 +60,13 @@ class ScopePropagator {
                         }

                 } while (changed)

         }

-

+        

         def propagateAllScopeConstraints() {

+                statistics.incrementScopePropagationCount()

+                doPropagateAllScopeConstraints()

+        }

+

+        protected def doPropagateAllScopeConstraints() {

                 var boolean hadChanged

                 do {

                         hadChanged = false

@@ -95,6 +103,10 @@ class ScopePropagator {
 //              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»''')

         }

+        

+        def void propagateAdditionToRelation(Relation r) {

+                // Nothing to propagate.

+        }

 

         private def propagateLowerLimitUp(Scope subScope, Scope superScope) {

                 if (subScope.minNewElements > superScope.minNewElements) {

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java
deleted file mode 100644
index b1c5a658..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java
+++ /dev/null
@@ -1,18 +0,0 @@
-package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality;
-
-public enum ScopePropagatorStrategy {
-        BasicTypeHierarchy,
-
-        PolyhedralTypeHierarchy,
-
-        PolyhedralRelations {
-                @Override
-                public boolean requiresUpperBoundIndexing() {
-                        return true;
-                }
-        };
-
-        public boolean requiresUpperBoundIndexing() {
-                return false;
-        }
-}
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
new file mode 100644
index 00000000..37e56c9a
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend
@@ -0,0 +1,64 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+enum PolyhedralScopePropagatorConstraints {
+        TypeHierarchy,
+        Relational
+}
+
+enum PolyhedralScopePropagatorSolver {
+        Z3Real,
+        Z3Integer,
+        Cbc,
+        Clp
+}
+
+abstract class ScopePropagatorStrategy {
+        public static val BasicCount = new Simple("BasicCount")
+
+        public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy")
+
+        private new() {
+        }
+
+        def boolean requiresUpperBoundIndexing()
+
+        static class Simple extends ScopePropagatorStrategy {
+                val String name
+
+                @FinalFieldsConstructor
+                private new() {
+                }
+
+                override requiresUpperBoundIndexing() {
+                        false
+                }
+
+                override toString() {
+                        name
+                }
+        }
+
+        @Data
+        static class Polyhedral extends ScopePropagatorStrategy {
+                public static val UNLIMITED_TIME = -1
+
+                val PolyhedralScopePropagatorConstraints constraints
+                val PolyhedralScopePropagatorSolver solver
+                val double timeoutSeconds
+
+                @FinalFieldsConstructor
+                new() {
+                }
+
+                new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) {
+                        this(constraints, solver, UNLIMITED_TIME)
+                }
+
+                override requiresUpperBoundIndexing() {
+                        constraints == PolyhedralScopePropagatorConstraints.Relational
+                }
+        }
+}
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 b10c8e88..eadf0ae0 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
@@ -69,7 +69,7 @@ class PatternProvider {
                                 val startTime = System.nanoTime

                                 val result = typeAnalysis.performTypeAnalysis(problem, emptySolution)

                                 val typeAnalysisTime = System.nanoTime - startTime

-                                statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime

+                                statistics.preliminaryTypeAnalisisTime = typeAnalysisTime

                                 result

                         } else {

                                 null

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 5fefa551..bf816de9 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
@@ -98,10 +98,12 @@ class RefinementRuleProvider {
                                         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)

-                                        

-                                        statistics.addExecutionTime(System.nanoTime-startTime)

+                                        statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)

                                 ]

                         } else {

                                 ruleBuilder.action[match |

@@ -132,10 +134,12 @@ class RefinementRuleProvider {
                                         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)

-                                        

-                                        statistics.addExecutionTime(System.nanoTime-startTime)

+                                        statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)

                                 ]

                         }

                 } else {

@@ -162,29 +166,31 @@ class RefinementRuleProvider {
                                 typeInterpretation.elements += newElement

                                 typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]

                                 

+                                val propagatorStartTime = System.nanoTime

+                                statistics.addExecutionTime(propagatorStartTime-startTime)

+                                

                                 // Scope propagation

                                 scopePropagator.propagateAdditionToType(typeInterpretation)

-                                

-                                statistics.addExecutionTime(System.nanoTime-startTime)

+                                statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)

                         ]

                 }

                 return ruleBuilder.build

         }

         

-        def createRelationRefinementRules(GeneratedPatterns patterns, ModelGenerationStatistics statistics) {

+        def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) {

                 val res = new LinkedHashMap

                 for(LHSEntry: patterns.refinerelationQueries.entrySet) {

                         val declaration = LHSEntry.key.key

                         val inverseReference = LHSEntry.key.value

                         val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>>

-                        val rule = createRelationRefinementRule(declaration,inverseReference,lhs,statistics)

+                        val rule = createRelationRefinementRule(declaration,inverseReference,lhs,scopePropagator,statistics)

                         res.put(LHSEntry.key,rule)

                 }

                 return res

         }

         

         def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>

-                createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ModelGenerationStatistics statistics)

+                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 ruleBuilder = factory.createRule

@@ -201,7 +207,13 @@ class RefinementRuleProvider {
                                 val trg = match.get(4) as DefinedElement

                                 val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg]

                                 relationInterpretation.relationlinks += link

-                statistics.addExecutionTime(System.nanoTime-startTime)

+                                

+                                val propagatorStartTime = System.nanoTime

+                                statistics.addExecutionTime(propagatorStartTime-startTime)

+                                

+                                // Scope propagation

+                                scopePropagator.propagateAdditionToRelation(declaration)

+                                statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)

                         ]

                 } else {

                         ruleBuilder.action [ match |

@@ -217,7 +229,13 @@ class RefinementRuleProvider {
                                 relationInterpretation.relationlinks += link

                                 val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src]

                                 inverseInterpretation.relationlinks += inverseLink

-                                statistics.addExecutionTime(System.nanoTime-startTime)

+                                

+                                val propagatorStartTime = System.nanoTime

+                                statistics.addExecutionTime(propagatorStartTime-startTime)

+                                

+                                // Scope propagation

+                                scopePropagator.propagateAdditionToRelation(declaration)

+                                statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)

                         ]

                 }

 

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 a8db5e43..1abde0a8 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
@@ -39,6 +39,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.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory

 

 class ViatraReasoner extends LogicReasoner {

         val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()

@@ -137,11 +138,14 @@ class ViatraReasoner extends LogicReasoner {
 

                 dse.setInitialModel(emptySolution, false)

 

-                val IStateCoderFactory statecoder = if (viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) {

+                val IStateCoderFactory statecoder = switch (viatraConfig.stateCoderStrategy) {

+                        case Neighbourhood:

+                                new NeighbourhoodBasedStateCoderFactory

+                        case PairwiseNeighbourhood:

                                 new PairwiseNeighbourhoodBasedStateCoderFactory

-                        } else {

+                        default:

                                 new IdentifierBasedStateCoderFactory

-                        }

+                }

                 dse.stateCoderFactory = statecoder

 

                 dse.maxNumberOfThreads = 1

@@ -184,8 +188,12 @@ class ViatraReasoner extends LogicReasoner {
                                 it.value = (method.statistics.transformationExecutionTime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

+                                it.name = "ScopePropagationTime"

+                                it.value = (method.statistics.scopePropagationTime / 1000000) as int

+                        ]

+                        it.entries += createIntStatisticEntry => [

                                 it.name = "TypeAnalysisTime"

-                                it.value = (method.statistics.PreliminaryTypeAnalisisTime / 1000000) as int

+                                it.value = (method.statistics.preliminaryTypeAnalisisTime / 1000000) as int

                         ]

                         it.entries += createIntStatisticEntry => [

                                 it.name = "StateCoderTime"

@@ -199,6 +207,18 @@ class ViatraReasoner extends LogicReasoner {
                                 it.name = "SolutionCopyTime"

                                 it.value = (solutionCopier.getTotalCopierRuntime / 1000000) as int

                         ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "States"

+                                it.value = dse.numberOfStates as int

+                        ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "Decisions"

+                                it.value = method.statistics.decisionsTried

+                        ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "ScopePropagations"

+                                it.value = method.statistics.scopePropagatorInvocations

+                        ]

                         if (diversityChecker.isActive) {

                                 it.entries += createIntStatisticEntry => [

                                         it.name = "SolutionDiversityCheckTime"

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 7a3a2d67..a2f9cebe 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
@@ -14,9 +14,12 @@ import java.util.LinkedList
 import java.util.List

 import java.util.Set

 import org.eclipse.xtext.xbase.lib.Functions.Function1

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

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

 

 enum StateCoderStrategy {

         Neighbourhood,

+        PairwiseNeighbourhood,

         NeighbourhoodWithEquivalence,

         IDBased,

         DefinedByDiversity

@@ -25,7 +28,7 @@ enum StateCoderStrategy {
 class ViatraReasonerConfiguration extends LogicSolverConfiguration {

         // public var Iterable<PQuery> existingQueries

         public var nameNewElements = false

-        public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood

+        public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.PairwiseNeighbourhood

         public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis

         /**

          * Once per 1/randomBacktrackChance the search selects a random state.

@@ -50,9 +53,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
          * Configuration for cutting search space.

          */

         public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint

-        

-        public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.PolyhedralTypeHierarchy

 

+        public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.BasicTypeHierarchy

         public var List<CostObjectiveConfiguration> costObjectives = newArrayList

 }

 

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 144e7484..5af7fc69 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
@@ -189,6 +189,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
 //                              }

                                 logger.debug("Executing new activation: " + nextActivation);

                                 context.executeAcitvationId(nextActivation);

+                                method.getStatistics().incrementDecisionCount();

 

                                 visualiseCurrentState();

 //                              for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {