From f06427cd7375551582461f91b3458339a8227f9b Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 2 Nov 2020 02:02:40 +0100 Subject: Optimizing generator with linear objective functions --- .../ExtendedLinearExpressionBuilderFactory.xtend | 140 +++++++++++++++++++++ ...ExtendedPolyhedronScopePropagatorStrategy.xtend | 63 ++++++++++ .../cardinality/PolyhedronScopePropagator.xtend | 54 +++----- .../PolyhedronScopePropagatorStrategy.xtend | 92 ++++++++++++++ .../cardinality/PolyhedronSolver.xtend | 13 +- 5 files changed, 321 insertions(+), 41 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality') 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 typeBounds + val Map, LinearBoundedExpression> expressionsCache + + val ImmutableList.Builder dimensions = ImmutableList.builder + val Set constraints = new HashSet + val Set expressionsToSaturate = new HashSet + val Map patternMatchCounts = new HashMap + @Accessors(PUBLIC_GETTER) val List> saturationListeners = new ArrayList + + new(Polyhedron polyhedron, Map typeBounds, + Map, 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 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 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 extensionOperators + + var Map typeBounds + var Map, LinearBoundedExpression> initialExpressionsCache + + new(PolyhedronSolver solver, Collection extensionOperators, + ModelGenerationStatistics statistics) { + super(statistics) + this.solver = solver + this.extensionOperators = extensionOperators + } + + override setPolyhedron(Polyhedron polyhedron, Map typeBounds, + Map, 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 scopeBounds val LinearBoundedExpression topLevelBounds val Polyhedron polyhedron - val PolyhedronSaturationOperator operator + val PolyhedronScopePropagatorStrategy strategy val Set relevantRelations - val Cache cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build List updaters = emptyList new(PartialInterpretation p, ModelGenerationStatistics statistics, Set possibleNewDynamicTypes, Map unfinishedMultiplicityQueries, IQuerySpecification> hasElementInContainmentQuery, Map>> allPatternsByName, - Collection hints, PolyhedronSolver solver, boolean propagateRelations, - boolean updateHeuristic) { + Collection 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 typeBounds, + Map, 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 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 -- cgit v1.2.3-70-g09d2