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 --- .../META-INF/MANIFEST.MF | 3 +- .../ModelGenerationMethodProvider.xtend | 226 --------------------- .../logic2viatra/ModelGenerationStatistics.xtend | 47 +++++ .../logic2viatra/TypeInferenceMethod.xtend | 44 ++++ .../ExtendedLinearExpressionBuilderFactory.xtend | 140 +++++++++++++ ...ExtendedPolyhedronScopePropagatorStrategy.xtend | 63 ++++++ .../cardinality/PolyhedronScopePropagator.xtend | 54 ++--- .../PolyhedronScopePropagatorStrategy.xtend | 92 +++++++++ .../cardinality/PolyhedronSolver.xtend | 13 +- 9 files changed, 414 insertions(+), 268 deletions(-) delete mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend 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') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF index b9da0f0b..ec1557e8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF @@ -8,7 +8,8 @@ Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval, hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators, hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, - hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries, + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", 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 deleted file mode 100644 index 3bcd9116..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ /dev/null @@ -1,226 +0,0 @@ -package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra - -import com.google.common.collect.ImmutableMap -import com.google.common.collect.ImmutableSet -import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem -import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator -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 -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation -import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace -import java.util.Collection -import java.util.List -import java.util.Map -import java.util.Set -import org.eclipse.viatra.query.runtime.api.GenericQueryGroup -import org.eclipse.viatra.query.runtime.api.IPatternMatch -import org.eclipse.viatra.query.runtime.api.IQuerySpecification -import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine -import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher -import org.eclipse.viatra.query.runtime.emf.EMFScope -import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint -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 - -class ModelGenerationStatistics { - public var long transformationExecutionTime = 0 - - synchronized def addExecutionTime(long amount) { - transformationExecutionTime += amount - } - - public var long scopePropagationTime = 0 - - synchronized def addScopePropagationTime(long amount) { - scopePropagationTime += amount - } - - public var long mustRelationPropagationTime = 0 - - synchronized def addMustRelationPropagationTime(long amount) { - mustRelationPropagationTime += amount - } - - public var long preliminaryTypeAnalisisTime = 0 - - public var int decisionsTried = 0 - - synchronized def incrementDecisionCount() { - decisionsTried++ - } - - public var int transformationInvocations - - synchronized def incrementTransformationCount() { - transformationInvocations++ - } - - public var int scopePropagatorInvocations - - synchronized def incrementScopePropagationCount() { - scopePropagatorInvocations++ - } - - public var int scopePropagatorSolverInvocations - - synchronized def incrementScopePropagationSolverCount() { - scopePropagatorSolverInvocations++ - } -} - -@Data class ModelGenerationMethod { - ModelGenerationStatistics statistics - - Collection> objectRefinementRules - Collection> relationRefinementRules - - List unfinishedMultiplicities - - Collection>> unfinishedWF - - Collection>> invalidWF - - Map>> mustUnitPropagationPreconditions - Map>> currentUnitPropagationPreconditions - - Map modalRelationQueries - - Collection>> allPatterns -} - -enum TypeInferenceMethod { - Generic, - PreliminaryAnalysis -} - -class ModelGenerationMethodProvider { - val PatternProvider patternProvider = new PatternProvider - val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider - val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider - val relationConstraintCalculator = new RelationConstraintCalculator - - def ModelGenerationMethod createModelGenerationMethod( - LogicProblem logicProblem, - PartialInterpretation emptySolution, - ReasonerWorkspace workspace, - boolean nameNewElements, - TypeInferenceMethod typeInferenceMethod, - boolean calculateObjectCreationCosts, - ScopePropagatorStrategy scopePropagatorStrategy, - Collection hints, - Collection unitPropagationPatternGenerators, - DocumentationLevel debugLevel - ) { - val statistics = new ModelGenerationStatistics - val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) - - val Set existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). - map[it.patternPQuery as PQuery].toSet - - val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) - val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, - workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, - unitPropagationPatternGenerators, writeFiles) - - val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) - scopePropagator.propagateAllScopeConstraints - val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, - queries, scopePropagator, statistics) - val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, - queries, unitRulePropagator, nameNewElements, statistics) - val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator, - statistics) - - val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, - calculateObjectCreationCosts) - - val unfinishedWF = queries.getUnfinishedWFQueries.values - - val modalRelationQueriesBuilder = ImmutableMap.builder - for (entry : queries.modalRelationQueries.entrySet) { - val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head - if (annotation !== null) { - modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) - } - } - val modalRelationQueries = modalRelationQueriesBuilder.build - - val invalidWF = queries.getInvalidWFQueries.values - - val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns - val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns - - val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( - queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll(queries. - multiplicityConstraintQueries.values.flatMap[allQueries]).addAll(queries.unfinishedWFQueries.values).addAll( - queries.invalidWFQueries.values).addAll(queries.mustUnitPropagationPreconditionPatterns.values).addAll( - queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build - val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) - GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) - - return new ModelGenerationMethod( - statistics, - objectRefinementRules.values, - relationRefinementRules.values, - unfinishedMultiplicities, - unfinishedWF, - invalidWF, - mustUnitPropagationPreconditions, - currentUnitPropagationPreconditions, - modalRelationQueries, - queries.allQueries - ) - } - - private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, - PartialInterpretation emptySolution, Collection hints, GeneratedPatterns queries, - ModelGenerationStatistics statistics) { - if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { - throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") - } - switch (scopePropagatorStrategy) { - case ScopePropagatorStrategy.None, - case ScopePropagatorStrategy.Basic: - new ScopePropagator(emptySolution, statistics) - case ScopePropagatorStrategy.BasicTypeHierarchy: - new TypeHierarchyScopePropagator(emptySolution, statistics) - ScopePropagatorStrategy.Polyhedral: { - val types = queries.refineObjectQueries.keySet.map[newType].toSet - val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] - val solver = switch (scopePropagatorStrategy.solver) { - case Z3Integer: - new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) - case Z3Real: - new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) - case Cbc: - new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) - case Clp: - new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) - default: - throw new IllegalArgumentException("Unknown polyhedron solver: " + - scopePropagatorStrategy.solver) - } - new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, - queries.hasElementInContainmentQuery, allPatternsByName, hints, solver, - scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) - } - default: - throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) - } - } -} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend new file mode 100644 index 00000000..bd5bf807 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend @@ -0,0 +1,47 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra + +class ModelGenerationStatistics { + public var long transformationExecutionTime = 0 + + synchronized def addExecutionTime(long amount) { + transformationExecutionTime += amount + } + + public var long scopePropagationTime = 0 + + synchronized def addScopePropagationTime(long amount) { + scopePropagationTime += amount + } + + public var long mustRelationPropagationTime = 0 + + synchronized def addMustRelationPropagationTime(long amount) { + mustRelationPropagationTime += amount + } + + public var long preliminaryTypeAnalisisTime = 0 + + public var int decisionsTried = 0 + + synchronized def incrementDecisionCount() { + decisionsTried++ + } + + public var int transformationInvocations + + synchronized def incrementTransformationCount() { + transformationInvocations++ + } + + public var int scopePropagatorInvocations + + synchronized def incrementScopePropagationCount() { + scopePropagatorInvocations++ + } + + public var int scopePropagatorSolverInvocations + + synchronized def incrementScopePropagationSolverCount() { + scopePropagatorSolverInvocations++ + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend new file mode 100644 index 00000000..9296a0be --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend @@ -0,0 +1,44 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra + +import com.google.common.collect.ImmutableMap +import com.google.common.collect.ImmutableSet +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CachingSimplePolyhedronScopePropagatorStrategy +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator +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 +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.util.Collection +import java.util.List +import java.util.Map +import java.util.Set +import org.eclipse.viatra.query.runtime.api.GenericQueryGroup +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.emf.EMFScope +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +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 + +enum TypeInferenceMethod { + Generic, + PreliminaryAnalysis +} \ No newline at end of file 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