Optimizing generator with linear objective functions

5 files changed, 321 insertions, 41 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend
new file mode 100644
index 00000000..6054affe
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend
@@ -0,0 +1,140 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import com.google.common.collect.ImmutableList
+import com.google.common.collect.ImmutableMap
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.HashSet
+import java.util.List
+import java.util.Map
+import java.util.Set
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+interface BoundSaturationListener {
+        def void boundsSaturated(Integer lower, Integer upper)
+}
+
+interface ExtendedLinearExpressionBuilderFactory {
+        def ExtendedLinearExpressionBuilder createBuilder()
+
+        def Dimension getDimension(IPatternMatch patternMatch)
+}
+
+interface ExtendedLinearExpressionBuilder extends LinearTypeExpressionBuilder {
+        override ExtendedLinearExpressionBuilder add(int scale, Type type)
+
+        def ExtendedLinearExpressionBuilder add(int scale, IPatternMatch patternMatch)
+
+        def ExtendedLinearExpressionBuilder add(int scale, Dimension dimension)
+
+        def LinearBoundedExpression build(BoundSaturationListener listener)
+}
+
+class ExtendedPolyhedronBuilder implements ExtendedLinearExpressionBuilderFactory {
+        val Map<Type, LinearBoundedExpression> typeBounds
+        val Map<Map<Dimension, Integer>, LinearBoundedExpression> expressionsCache
+
+        val ImmutableList.Builder<Dimension> dimensions = ImmutableList.builder
+        val Set<LinearConstraint> constraints = new HashSet
+        val Set<LinearBoundedExpression> expressionsToSaturate = new HashSet
+        val Map<IPatternMatch, Dimension> patternMatchCounts = new HashMap
+        @Accessors(PUBLIC_GETTER) val List<Pair<LinearBoundedExpression, BoundSaturationListener>> saturationListeners = new ArrayList
+
+        new(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds,
+                Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) {
+                this.typeBounds = typeBounds
+                this.expressionsCache = new HashMap(initialExpressionsCache)
+                dimensions.addAll(polyhedron.dimensions)
+                constraints.addAll(polyhedron.constraints)
+                expressionsToSaturate.addAll(polyhedron.expressionsToSaturate)
+        }
+
+        override createBuilder() {
+                new ExtendedLinearExpressionBuilderImpl(this)
+        }
+
+        override getDimension(IPatternMatch patternMatch) {
+                patternMatchCounts.computeIfAbsent(patternMatch) [ key |
+                        val dimension = new Dimension(key.toString, 0, null)
+                        dimensions.add(dimension)
+                        dimension
+                ]
+        }
+
+        def buildPolyhedron() {
+                new Polyhedron(
+                        dimensions.build,
+                        ImmutableList.copyOf(constraints),
+                        ImmutableList.copyOf(expressionsToSaturate)
+                )
+        }
+
+        @FinalFieldsConstructor
+        private static class ExtendedLinearExpressionBuilderImpl implements ExtendedLinearExpressionBuilder {
+                val ExtendedPolyhedronBuilder polyhedronBuilder
+
+                val Map<Dimension, Integer> coefficients = new HashMap
+
+                override add(int scale, Type type) {
+                        val expression = polyhedronBuilder.typeBounds.get(type)
+                        if (expression === null) {
+                                throw new IllegalArgumentException("Unknown Type: " + type)
+                        }
+                        add(scale, expression)
+                }
+
+                override add(int scale, IPatternMatch patternMatch) {
+                        val dimension = polyhedronBuilder.getDimension(patternMatch)
+                        add(scale, dimension)
+                }
+
+                private def add(int scale, LinearBoundedExpression expression) {
+                        switch (expression) {
+                                Dimension: add(scale, expression)
+                                LinearConstraint: add(scale, expression.coefficients)
+                                default: throw new IllegalArgumentException("Unknown LinearBoundedExpression: " + expression)
+                        }
+                }
+
+                private def add(int scale, Map<Dimension, Integer> coefficients) {
+                        for (pair : coefficients.entrySet) {
+                                add(scale * pair.value, pair.key)
+                        }
+                        this
+                }
+
+                override add(int scale, Dimension dimension) {
+                        coefficients.merge(dimension, scale)[a, b|a + b]
+                        this
+                }
+
+                override build() {
+                        val filteredCoefficients = ImmutableMap.copyOf(coefficients.filter [ _, coefficient |
+                                coefficient != 0
+                        ])
+                        polyhedronBuilder.expressionsCache.computeIfAbsent(filteredCoefficients) [ map |
+                                if (map.size == 1) {
+                                        val pair = map.entrySet.head
+                                        if (pair.value == 1) {
+                                                return pair.key
+                                        }
+                                }
+                                val constraint = new LinearConstraint(map)
+                                polyhedronBuilder.constraints.add(constraint)
+                                constraint
+                        ]
+                }
+
+                override build(BoundSaturationListener listener) {
+                        val expression = build()
+                        if (listener !== null) {
+                                polyhedronBuilder.expressionsToSaturate.add(expression)
+                                polyhedronBuilder.saturationListeners.add(expression -> listener)
+                        }
+                        expression
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend
new file mode 100644
index 00000000..32923396
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend
@@ -0,0 +1,63 @@
+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.ModelGenerationStatistics
+import java.util.Collection
+import java.util.Map
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+
+interface PolyhedronExtensionOperator {
+        def void extendPolyhedron(ExtendedLinearExpressionBuilderFactory factory)
+}
+
+class ExtendedPolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy {
+        val PolyhedronSolver solver
+        val Collection<PolyhedronExtensionOperator> extensionOperators
+
+        var Map<Type, LinearBoundedExpression> typeBounds
+        var Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache
+
+        new(PolyhedronSolver solver, Collection<PolyhedronExtensionOperator> extensionOperators,
+                ModelGenerationStatistics statistics) {
+                super(statistics)
+                this.solver = solver
+                this.extensionOperators = extensionOperators
+        }
+
+        override setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds,
+                Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) {
+                super.setPolyhedron(polyhedron, typeBounds, initialExpressionsCache)
+                this.typeBounds = typeBounds
+                this.initialExpressionsCache = initialExpressionsCache
+        }
+
+        override isRelevantRelation(Relation relation) {
+                true
+        }
+
+        override protected doSaturate() {
+                val builder = new ExtendedPolyhedronBuilder(polyhedron, typeBounds, initialExpressionsCache)
+                for (extensionOperator : extensionOperators) {
+                        extensionOperator.extendPolyhedron(builder)
+                }
+                val extendedPolyhedron = builder.buildPolyhedron()
+                val saturationOperator = solver.createSaturationOperator(extendedPolyhedron)
+                val result = try {
+                                saturationOperator.saturate()
+                        } finally {
+                                saturationOperator.close()
+                        }
+                if (result == PolyhedronSaturationResult.EMPTY) {
+                        // The partial model cannot be refined any more, we can't provide objective bounds.
+                        for (pair : builder.saturationListeners) {
+                                pair.value.boundsSaturated(null, null)
+                        }
+                        return false
+                }
+                for (pair : builder.saturationListeners) {
+                        val expression = pair.key
+                        pair.value.boundsSaturated(expression.lowerBound, expression.upperBound)
+                }
+                true
+        }
+}
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 c28d4caa..ad8f94ab 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,7 +1,5 @@
 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
@@ -23,7 +21,6 @@ import java.util.HashSet
 import java.util.List
 import java.util.Map
 import java.util.Set
-import javax.naming.OperationNotSupportedException
 import org.eclipse.viatra.query.runtime.api.IPatternMatch
 import org.eclipse.viatra.query.runtime.api.IQuerySpecification
 import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
@@ -32,31 +29,29 @@ 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 PolyhedronScopePropagatorStrategy strategy
         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,
                 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName,
-                Collection<LinearTypeConstraintHint> hints, PolyhedronSolver solver, boolean propagateRelations,
-                boolean updateHeuristic) {
+                Collection<LinearTypeConstraintHint> hints, PolyhedronScopePropagatorStrategy strategy,
+                boolean propagateRelations, boolean updateHeuristic) {
                 super(p, statistics)
                 this.updateHeuristic = updateHeuristic
+                this.strategy = strategy
                 val builder = new PolyhedronBuilder(p)
                 builder.buildPolyhedron(possibleNewDynamicTypes)
                 scopeBounds = builder.scopeBounds
                 topLevelBounds = builder.topLevelBounds
                 polyhedron = builder.polyhedron
-                operator = solver.createSaturationOperator(polyhedron)
+                strategy.setPolyhedron(polyhedron, builder.typeBounds, builder.expressionsCache)
                 propagateAllScopeConstraints()
                 if (propagateRelations) {
                         val maximumNumberOfNewNodes = topLevelBounds.upperBound
@@ -80,30 +75,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                 resetBounds()
                 populatePolyhedronFromScope()
 //              println(polyhedron)
-                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)
-//                                      println("INVALID")
-                                        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)
+                if (strategy.saturate) {
+                        populateScopesFromPolyhedron()
+                } else {
+                        setScopesInvalid()
                 }
 //              println(polyhedron)
                 if (updateHeuristic) {
@@ -112,9 +87,9 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
         }
 
         override isPropagationNeededAfterAdditionToRelation(Relation r) {
-                relevantRelations.contains(r) || super.isPropagationNeededAfterAdditionToRelation(r)
+                relevantRelations.contains(r) || strategy.isRelevantRelation(r) || super.isPropagationNeededAfterAdditionToRelation(r)
         }
-        
+
         override isQueryEngineFlushRequiredBeforePropagation() {
                 true
         }
@@ -253,7 +228,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                         }
                         buildRelevantRelations(constraints.keySet)
                         for (hint : hints) {
-                                updatersBuilder.add(hint.createConstraintUpdater(this))
+                                val updater = hint.createConstraintUpdater(this)
+                                if (updater !== null) {
+                                        updatersBuilder.add(updater)
+                                }
                         }
                         updaters = updatersBuilder.build
                         addCachedConstraintsToPolyhedron()
@@ -410,7 +388,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
                         for (scope : p.scopes) {
                                 switch (targetTypeInterpretation : scope.targetTypeInterpretation) {
                                         PartialPrimitiveInterpretation:
-                                                throw new OperationNotSupportedException("Primitive type scopes are not yet implemented")
+                                                throw new IllegalStateException("Primitive type scopes are not yet implemented")
                                         PartialComplexTypeInterpretation: {
                                                 val complexType = targetTypeInterpretation.interpretationOf
                                                 val typeBound = typeBounds.get(complexType)
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend
new file mode 100644
index 00000000..f93dcd18
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend
@@ -0,0 +1,92 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import com.google.common.cache.Cache
+import com.google.common.cache.CacheBuilder
+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 java.util.Map
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+@FinalFieldsConstructor
+abstract class PolyhedronScopePropagatorStrategy {
+        val ModelGenerationStatistics statistics
+
+        @Accessors(PUBLIC_GETTER) var Polyhedron polyhedron
+
+        def void setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds,
+                Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) {
+                if (this.polyhedron !== null) {
+                        throw new IllegalStateException("polyhedron was already set")
+                }
+                this.polyhedron = polyhedron
+                initialize()
+        }
+
+        def boolean saturate() {
+                if (polyhedron === null) {
+                        throw new IllegalStateException("polyhedron was not set")
+                }
+                doSaturate()
+        }
+        
+        def boolean isRelevantRelation(Relation relation) {
+                false
+        }
+
+        protected def incrementScopePropagationSolverCount() {
+                statistics.incrementScopePropagationSolverCount()
+        }
+
+        protected def void initialize() {
+        }
+
+        protected def boolean doSaturate()
+}
+
+@FinalFieldsConstructor
+class CachingSimplePolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy {
+        static val CACHE_SIZE = 10000
+
+        val PolyhedronSolver solver
+
+        val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build
+        var PolyhedronSaturationOperator operator
+
+        new(PolyhedronSolver solver, ModelGenerationStatistics statistics) {
+                super(statistics)
+                this.solver = solver
+        }
+
+        override protected initialize() {
+                operator = solver.createSaturationOperator(polyhedron)
+        }
+
+        override protected doSaturate() {
+                val signature = polyhedron.createSignature
+                val cachedSignature = cache.getIfPresent(signature)
+                switch (cachedSignature) {
+                        case null: {
+                                incrementScopePropagationSolverCount()
+                                val result = operator.saturate()
+                                if (result == PolyhedronSaturationResult.EMPTY) {
+                                        cache.put(signature, PolyhedronSignature.EMPTY)
+                                        false
+                                } else {
+                                        val resultSignature = polyhedron.createSignature
+                                        cache.put(signature, resultSignature)
+                                        true
+                                }
+                        }
+                        case PolyhedronSignature.EMPTY:
+                                false
+                        PolyhedronSignature.Bounds: {
+                                polyhedron.applySignature(signature)
+                                true
+                        }
+                        default:
+                                throw new IllegalStateException("Unknown polyhedron signature: " + signature)
+                }
+        }
+}
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 4e046190..21bd2d9e 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
@@ -116,7 +116,7 @@ abstract class PolyhedronSignature {
 }
 
 @Accessors
-abstract class LinearBoundedExpression {
+class Bounds {
         var Integer lowerBound
         var Integer upperBound
 
@@ -132,12 +132,19 @@ abstract class LinearBoundedExpression {
                 }
         }
 
+        def void assertBetween(Integer tighterLowerBound, Integer tighterUpperBound) {
+                tightenLowerBound(tighterLowerBound)
+                tightenUpperBound(tighterUpperBound)
+        }
+
         def void assertEqualsTo(int bound) {
-                tightenLowerBound(bound)
-                tightenUpperBound(bound)
+                assertBetween(bound, bound)
         }
 }
 
+abstract class LinearBoundedExpression extends Bounds {
+}
+
 @Accessors
 class Dimension extends LinearBoundedExpression {
         val String name