From fc84d3fe670331bc89fb1e4c44104bc1fc811438 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 14 Aug 2019 18:26:33 +0200 Subject: Measurements WIP --- .../cardinality/LinearTypeConstraintHint.xtend | 30 ++++++ .../cardinality/PolyhedronScopePropagator.xtend | 106 ++++++++++++++++----- .../cardinality/PolyhedronSolver.xtend | 72 ++++++++++++-- .../cardinality/RelationConstraintCalculator.xtend | 5 +- .../logic2viatra/cardinality/ScopePropagator.xtend | 25 ++++- .../cardinality/ScopePropagatorStrategy.xtend | 11 ++- .../cardinality/TypeHierarchyScopePropagator.xtend | 20 ++-- .../cardinality/Z3PolyhedronSolver.xtend | 32 ++++++- 8 files changed, 254 insertions(+), 47 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.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/LinearTypeConstraintHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend new file mode 100644 index 00000000..8c21ca1d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend @@ -0,0 +1,30 @@ +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.patterns.PatternGenerator +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher + +interface LinearTypeExpressionBuilderFactory { + def ViatraQueryMatcher createMatcher(String queryName) + + def LinearTypeExpressionBuilder createBuilder() +} + +interface LinearTypeExpressionBuilder { + def LinearTypeExpressionBuilder add(int scale, Type type) + + def LinearBoundedExpression build() +} + +@FunctionalInterface +interface RelationConstraintUpdater { + def void update(PartialInterpretation p) +} + +interface LinearTypeConstraintHint { + def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator) + + def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) +} 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 7c05e818..51dba244 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,5 +1,7 @@ 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 @@ -15,6 +17,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope import java.util.ArrayDeque import java.util.ArrayList +import java.util.Collection import java.util.HashMap import java.util.HashSet import java.util.List @@ -29,26 +32,33 @@ 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 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, - PolyhedronSolver solver, boolean propagateRelations) { + Map>> allPatternsByName, + Collection hints, PolyhedronSolver solver, boolean propagateRelations, + boolean updateHeuristic) { super(p, statistics) + this.updateHeuristic = updateHeuristic val builder = new PolyhedronBuilder(p) builder.buildPolyhedron(possibleNewDynamicTypes) scopeBounds = builder.scopeBounds topLevelBounds = builder.topLevelBounds polyhedron = builder.polyhedron operator = solver.createSaturationOperator(polyhedron) + propagateAllScopeConstraints() if (propagateRelations) { - propagateAllScopeConstraints() val maximumNumberOfNewNodes = topLevelBounds.upperBound if (maximumNumberOfNewNodes === null) { throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") @@ -57,7 +67,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { throw new IllegalStateException("Maximum number of new nodes is not positive") } builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, - maximumNumberOfNewNodes) + allPatternsByName, hints, maximumNumberOfNewNodes) relevantRelations = builder.relevantRelations updaters = builder.updaters } else { @@ -66,21 +76,40 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } override void doPropagateAllScopeConstraints() { + super.doPropagateAllScopeConstraints() resetBounds() populatePolyhedronFromScope() // println(polyhedron) - val result = operator.saturate() -// println(polyhedron) - if (result == PolyhedronSaturationResult.EMPTY) { - setScopesInvalid() - } else { - populateScopesFromPolyhedron() - if (result != PolyhedronSaturationResult.SATURATED) { - super.propagateAllScopeConstraints() + 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) + 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) + } +// println(polyhedron) + if (updateHeuristic) { + copyScopeBoundsToHeuristic() } } - + override propagateAdditionToRelation(Relation r) { super.propagateAdditionToRelation(r) if (relevantRelations.contains(r)) { @@ -186,7 +215,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } @FinalFieldsConstructor - private static class PolyhedronBuilder { + private static class PolyhedronBuilder implements LinearTypeExpressionBuilderFactory { static val INFINITY_SCALE = 10 val PartialInterpretation p @@ -197,6 +226,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { Map typeBounds int infinity ViatraQueryEngine queryEngine + Map>> allPatternsByName ImmutableList.Builder updatersBuilder Map scopeBounds @@ -222,9 +252,11 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { def buildMultiplicityConstraints( Map constraints, IQuerySpecification> hasElementInContainmentQuery, - int maximumNuberOfNewNodes) { + Map>> allPatternsByName, + Collection hints, int maximumNuberOfNewNodes) { infinity = maximumNuberOfNewNodes * INFINITY_SCALE queryEngine = ViatraQueryEngine.on(new EMFScope(p)) + this.allPatternsByName = allPatternsByName updatersBuilder = ImmutableList.builder val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType] for (pair : containmentConstraints.entrySet) { @@ -238,10 +270,13 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } } buildRelevantRelations(constraints.keySet) + for (hint : hints) { + updatersBuilder.add(hint.createConstraintUpdater(this)) + } updaters = updatersBuilder.build addCachedConstraintsToPolyhedron() } - + private def buildRelevantRelations(Set constraints) { val builder = ImmutableSet.builder for (constraint : constraints) { @@ -345,7 +380,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } } - private def addCoefficients(Map accumulator, int scale, Map a) { + private static def addCoefficients(Map accumulator, int scale, Map a) { for (pair : a.entrySet) { val dimension = pair.key val currentValue = accumulator.get(pair.key) ?: 0 @@ -411,14 +446,41 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } scopeBoundsBuilder.build } + + override createMatcher(String queryName) { + val querySpecification = allPatternsByName.get(queryName) + if (querySpecification === null) { + throw new IllegalArgumentException("Unknown pattern: " + queryName) + } + querySpecification.getMatcher(queryEngine) + } + + override createBuilder() { + new PolyhedronBuilderLinearTypeExpressionBuilder(this) + } } - private static interface RelationConstraintUpdater { - def void update(PartialInterpretation p) + @FinalFieldsConstructor + private static class PolyhedronBuilderLinearTypeExpressionBuilder implements LinearTypeExpressionBuilder { + val PolyhedronBuilder polyhedronBuilder + val Map coefficients = new HashMap + + override add(int scale, Type type) { + val typeCoefficients = polyhedronBuilder.subtypeDimensions.get(type) + if (typeCoefficients === null) { + throw new IllegalArgumentException("Unknown type: " + type) + } + PolyhedronBuilder.addCoefficients(coefficients, scale, typeCoefficients) + this + } + + override build() { + polyhedronBuilder.toExpression(coefficients) + } } @FinalFieldsConstructor - static class ContainmentConstraintUpdater implements RelationConstraintUpdater { + private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { val String name val LinearBoundedExpression orphansLowerBound val LinearBoundedExpression orphansUpperBound @@ -460,7 +522,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } @FinalFieldsConstructor - static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { + private static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { val LinearBoundedExpression typeCardinality val ViatraQueryMatcher hasElementInContainmentMatcher @@ -479,7 +541,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } @FinalFieldsConstructor - static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { + private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { val String name val LinearBoundedExpression availableMultiplicityExpression val ViatraQueryMatcher unfinishedMultiplicityMatcher @@ -500,7 +562,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } @FinalFieldsConstructor - static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { + private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { val String name val LinearBoundedExpression targetCardinalityExpression val ViatraQueryMatcher unrepairableMultiplicityMatcher 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 9c6cb82e..4e046190 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 @@ -3,6 +3,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality import java.util.List import java.util.Map import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.Data import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor interface PolyhedronSolver { @@ -52,16 +53,66 @@ class Polyhedron { val List expressionsToSaturate override toString() ''' - Dimensions: - «FOR dimension : dimensions» - «dimension» - «ENDFOR» - Constraints: - «FOR constraint : constraints» - «constraint» - «ENDFOR» + Dimensions: + «FOR dimension : dimensions» + «dimension» + «ENDFOR» + Constraints: + «FOR constraint : constraints» + «constraint» + «ENDFOR» ''' + def createSignature() { + val size = dimensions.size + constraints.size + val lowerBounds = newArrayOfSize(size) + val upperBounds = newArrayOfSize(size) + var int i = 0 + for (dimension : dimensions) { + lowerBounds.set(i, dimension.lowerBound) + upperBounds.set(i, dimension.upperBound) + i++ + } + for (constraint : constraints) { + lowerBounds.set(i, constraint.lowerBound) + upperBounds.set(i, constraint.upperBound) + i++ + } + new PolyhedronSignature.Bounds(lowerBounds, upperBounds) + } + + def applySignature(PolyhedronSignature.Bounds signature) { + val lowerBounds = signature.lowerBounds + val upperBounds = signature.upperBounds + var int i = 0 + for (dimension : dimensions) { + dimension.lowerBound = lowerBounds.get(i) + dimension.upperBound = upperBounds.get(i) + i++ + } + for (constraint : constraints) { + constraint.lowerBound = lowerBounds.get(i) + constraint.upperBound = upperBounds.get(i) + i++ + } + } +} + +abstract class PolyhedronSignature { + public static val EMPTY = new PolyhedronSignature { + override toString() { + "PolyhedronSignature.EMPTY" + } + } + + private new() { + } + + @Data + static class Bounds extends PolyhedronSignature { + val Integer[] lowerBounds + val Integer[] upperBounds + } } @Accessors @@ -80,6 +131,11 @@ abstract class LinearBoundedExpression { upperBound = tighterBound } } + + def void assertEqualsTo(int bound) { + tightenLowerBound(bound) + tightenUpperBound(bound) + } } @Accessors 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 52a390a8..013e53e1 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 @@ -117,9 +117,12 @@ class RelationConstraintCalculator { var inverseUpperMultiplicity = -1 val inverseRelation = inverseRelations.get(relation) if (inverseRelation !== null) { - inverseUpperMultiplicity = upperMultiplicities.get(relation) + inverseUpperMultiplicity = upperMultiplicities.get(inverseRelation) container = containmentRelations.contains(inverseRelation) } + if (containment) { + inverseUpperMultiplicity = 1 + } val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container, lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity) if (constraint.isActive) { 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 0bdb202e..2376fb38 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 @@ -14,7 +14,7 @@ import org.eclipse.xtend.lib.annotations.Accessors class ScopePropagator { @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation - val ModelGenerationStatistics statistics + @Accessors(PROTECTED_GETTER) val ModelGenerationStatistics statistics val Map type2Scope @Accessors(PROTECTED_GETTER) val Map> superScopes @Accessors(PROTECTED_GETTER) val Map> subScopes @@ -59,12 +59,21 @@ class ScopePropagator { } } } while (changed) + + copyScopeBoundsToHeuristic() } def propagateAllScopeConstraints() { statistics.incrementScopePropagationCount() doPropagateAllScopeConstraints() } + + protected def copyScopeBoundsToHeuristic() { + partialInterpretation.minNewElementsHeuristic = partialInterpretation.minNewElements + for (scope : partialInterpretation.scopes) { + scope.minNewElementsHeuristic = scope.minNewElements + } + } protected def void doPropagateAllScopeConstraints() { // Nothing to propagate. @@ -73,12 +82,17 @@ class ScopePropagator { def propagateAdditionToType(PartialTypeInterpratation t) { // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') val targetScope = type2Scope.get(t) - targetScope.removeOne - val sups = superScopes.get(targetScope) - sups.forEach[removeOne] + if (targetScope !== null) { + targetScope.removeOne + val sups = superScopes.get(targetScope) + sups.forEach[removeOne] + } if (this.partialInterpretation.minNewElements > 0) { this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 } + if (this.partialInterpretation.minNewElementsHeuristic > 0) { + this.partialInterpretation.minNewElementsHeuristic = this.partialInterpretation.minNewElementsHeuristic - 1 + } if (this.partialInterpretation.maxNewElements > 0) { this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 } else if (this.partialInterpretation.maxNewElements === 0) { @@ -105,5 +119,8 @@ class ScopePropagator { if (scope.minNewElements > 0) { scope.minNewElements = scope.minNewElements - 1 } + if (scope.minNewElementsHeuristic > 0) { + scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1 + } } } 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 b0ed75cb..3165917a 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,9 @@ enum PolyhedralScopePropagatorSolver { } abstract class ScopePropagatorStrategy { - public static val Count = new Simple("Count") + public static val None = new Simple("None") + + public static val Basic = new Simple("Basic") public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") @@ -47,14 +49,19 @@ abstract class ScopePropagatorStrategy { val PolyhedralScopePropagatorConstraints constraints val PolyhedralScopePropagatorSolver solver + val boolean updateHeuristic val double timeoutSeconds @FinalFieldsConstructor new() { } + new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver, boolean updateHeuristic) { + this(constraints, solver, updateHeuristic, UNLIMITED_TIME) + } + new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) { - this(constraints, solver, UNLIMITED_TIME) + this(constraints, solver, true) } override requiresUpperBoundIndexing() { 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 index be8ef00a..d1704b39 100644 --- 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 @@ -27,12 +27,16 @@ class TypeHierarchyScopePropagator extends ScopePropagator { } private def propagateLowerLimitUp(Scope subScope, Scope superScope) { + var changed = false if (subScope.minNewElements > superScope.minNewElements) { superScope.minNewElements = subScope.minNewElements - return true - } else { - return false + changed = true + } + if (subScope.minNewElementsHeuristic > superScope.minNewElementsHeuristic) { + superScope.minNewElementsHeuristic = subScope.minNewElementsHeuristic + changed = true } + changed } private def propagateUpperLimitDown(Scope subScope, Scope superScope) { @@ -50,16 +54,20 @@ class TypeHierarchyScopePropagator extends ScopePropagator { } private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { + var changed = false 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 + changed = true + } + if (subScope.minNewElementsHeuristic > p.minNewElementsHeuristic) { + p.minNewElementsHeuristic = subScope.minNewElementsHeuristic + changed = true } + changed } private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend index 23444956..3b831433 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend @@ -13,6 +13,7 @@ import java.math.BigDecimal import java.math.MathContext import java.math.RoundingMode import java.util.Map +import org.eclipse.xtend.lib.annotations.Accessors import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor class Z3PolyhedronSolver implements PolyhedronSolver { @@ -28,10 +29,33 @@ class Z3PolyhedronSolver implements PolyhedronSolver { } override createSaturationOperator(Polyhedron polyhedron) { + new DisposingZ3SaturationOperator(this, polyhedron) + } + + def createPersistentSaturationOperator(Polyhedron polyhedron) { new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds) } } +@FinalFieldsConstructor +class DisposingZ3SaturationOperator implements PolyhedronSaturationOperator { + val Z3PolyhedronSolver solver + @Accessors val Polyhedron polyhedron + + override saturate() { + val persistentOperator = solver.createPersistentSaturationOperator(polyhedron) + try { + persistentOperator.saturate + } finally { + persistentOperator.close + } + } + + override close() throws Exception { + // Nothing to close. + } +} + class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { static val INFINITY_SYMBOL_NAME = "oo" static val MULT_SYMBOL_NAME = "*" @@ -106,9 +130,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { IntNum: resultExpr.getInt() RatNum: - floor(resultExpr) + ceil(resultExpr) AlgebraicNum: - floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) + ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) default: if (isNegativeInfinity(resultExpr)) { null @@ -136,9 +160,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { IntNum: resultExpr.getInt() RatNum: - ceil(resultExpr) + floor(resultExpr) AlgebraicNum: - ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) + floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) default: if (isPositiveInfinity(resultExpr)) { null -- cgit v1.2.3-54-g00ecf