Counting scope propagator (simpler than BasicTypeHierarchy)

6 files changed, 96 insertions, 75 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 8e061b63..23632d4d 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
@@ -10,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator

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

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

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

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

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider

@@ -27,7 +29,6 @@ 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

@@ -139,8 +140,10 @@ class ModelGenerationMethodProvider {
         private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy,

                 PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) {

                 switch (scopePropagatorStrategy) {

-                        case ScopePropagatorStrategy.BasicTypeHierarchy:

+                        case ScopePropagatorStrategy.Count:

                                 new ScopePropagator(emptySolution, statistics)

+                        case ScopePropagatorStrategy.BasicTypeHierarchy:

+                                new TypeHierarchyScopePropagator(emptySolution, statistics)

                         ScopePropagatorStrategy.Polyhedral: {

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

                                 val solver = switch (scopePropagatorStrategy.solver) {

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 e7e40ab0..7c05e818 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
@@ -28,7 +28,7 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 import org.eclipse.viatra.query.runtime.emf.EMFScope
 import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
 
-class PolyhedronScopePropagator extends ScopePropagator {
+class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
         val Map<Scope, LinearBoundedExpression> scopeBounds
         val LinearBoundedExpression topLevelBounds
         val Polyhedron polyhedron
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 7be6635c..0bdb202e 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
@@ -16,8 +16,8 @@ class ScopePropagator {
         @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

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

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

 

         new(PartialInterpretation p, ModelGenerationStatistics statistics) {

                 partialInterpretation = p

@@ -60,26 +60,14 @@ class ScopePropagator {
                         }

                 } while (changed)

         }

-        

+

         def propagateAllScopeConstraints() {

                 statistics.incrementScopePropagationCount()

                 doPropagateAllScopeConstraints()

         }

 

-        protected def doPropagateAllScopeConstraints() {

-                var boolean hadChanged

-                do {

-                        hadChanged = false

-                        for (superScopeEntry : superScopes.entrySet) {

-                                val sub = superScopeEntry.key

-                                hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged

-                                hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged

-                                for (sup : superScopeEntry.value) {

-                                        hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged

-                                        hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged

-                                }

-                        }

-                } while (hadChanged)

+        protected def void doPropagateAllScopeConstraints() {

+                // Nothing to propagate.

         }

 

         def propagateAdditionToType(PartialTypeInterpratation t) {

@@ -103,60 +91,11 @@ 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) {

-                        superScope.minNewElements = subScope.minNewElements

-                        return true

-                } else {

-                        return false

-                }

-        }

-

-        private def propagateUpperLimitDown(Scope subScope, Scope superScope) {

-                if (superScope.maxNewElements >= 0 &&

-                        (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) {

-//                      println('''

-//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»

-//                      subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements»

-//                      ''')

-                        subScope.maxNewElements = superScope.maxNewElements

-                        return true

-                } else {

-                        return false

-                }

-        }

-

-        private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) {

-                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

-                }

-        }

-

-        private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) {

-                if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) {

-//                      println('''

-//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes

-//                      subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements»

-//                      ''')

-                        subScope.maxNewElements = p.maxNewElements

-                        return true

-                } else {

-                        return false

-                }

-        }

-

         private def removeOne(Scope scope) {

                 if (scope.maxNewElements === 0) {

                         throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''')

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 37e56c9a..b0ed75cb 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,7 @@ enum PolyhedralScopePropagatorSolver {
 }
 
 abstract class ScopePropagatorStrategy {
-        public static val BasicCount = new Simple("BasicCount")
+        public static val Count = new Simple("Count")
 
         public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy")
 
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
new file mode 100644
index 00000000..be8ef00a
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend
@@ -0,0 +1,77 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
+
+class TypeHierarchyScopePropagator extends ScopePropagator {
+
+        new(PartialInterpretation p, ModelGenerationStatistics statistics) {
+                super(p, statistics)
+        }
+
+        protected override doPropagateAllScopeConstraints() {
+                var boolean hadChanged
+                do {
+                        hadChanged = false
+                        for (superScopeEntry : superScopes.entrySet) {
+                                val sub = superScopeEntry.key
+                                hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged
+                                hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged
+                                for (sup : superScopeEntry.value) {
+                                        hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged
+                                        hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged
+                                }
+                        }
+                } while (hadChanged)
+        }
+
+        private def propagateLowerLimitUp(Scope subScope, Scope superScope) {
+                if (subScope.minNewElements > superScope.minNewElements) {
+                        superScope.minNewElements = subScope.minNewElements
+                        return true
+                } else {
+                        return false
+                }
+        }
+
+        private def propagateUpperLimitDown(Scope subScope, Scope superScope) {
+                if (superScope.maxNewElements >= 0 &&
+                        (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) {
+//                      println('''
+//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»
+//                      subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements»
+//                      ''')
+                        subScope.maxNewElements = superScope.maxNewElements
+                        return true
+                } else {
+                        return false
+                }
+        }
+
+        private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) {
+                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
+                }
+        }
+
+        private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) {
+                if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) {
+//                      println('''
+//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes
+//                      subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements»
+//                      ''')
+                        subScope.maxNewElements = p.maxNewElements
+                        return true
+                } else {
+                        return false
+                }
+        }
+}
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 a2f9cebe..a5f42a5f 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
@@ -6,6 +6,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration

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

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

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

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

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

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind

@@ -14,8 +16,6 @@ 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,

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

         // public var Iterable<PQuery> existingQueries

         public var nameNewElements = false

-        public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.PairwiseNeighbourhood

+        public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood

         public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis

         /**

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

@@ -54,7 +54,9 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
          */

         public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint

 

-        public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.BasicTypeHierarchy

+        public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(

+                PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)

+

         public var List<CostObjectiveConfiguration> costObjectives = newArrayList

 }