5 files changed, 115 insertions, 29 deletions

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
+                }
+        }
+}