From 64138e8d91bc8d7bb54d9b042f872b43550dec16 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 24 Jul 2019 10:59:02 +0200 Subject: Cardinality propagator WIP --- .../ModelGenerationMethodProvider.xtend | 12 +- .../MultiplicityGoalConstraintCalculator.xtend | 46 --- .../MultiplicityGoalConstraintCalculator.xtend | 46 +++ .../cardinality/PolyhedronScopePropagator.xtend | 355 +++++++++++++++++---- .../cardinality/PolyhedronSolver.xtend | 32 +- .../cardinality/RelationConstraintCalculator.xtend | 133 ++++++++ .../logic2viatra/cardinality/ScopePropagator.xtend | 5 - .../cardinality/ScopePropagatorStrategy.java | 18 ++ .../logic2viatra/patterns/PatternGenerator.xtend | 150 +++++---- .../logic2viatra/patterns/PatternProvider.xtend | 115 ++++--- .../patterns/RelationRefinementGenerator.xtend | 102 +++--- .../patterns/TypeRefinementGenerator.xtend | 4 +- .../logic2viatra/patterns/UnfinishedIndexer.xtend | 222 +++++++++---- .../rules/GoalConstraintProvider.xtend | 2 +- 14 files changed, 871 insertions(+), 371 deletions(-) delete mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java (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/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 index 0ceb5b2e..3a99d3bf 100644 --- 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 @@ -5,7 +5,9 @@ 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.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.patterns.GeneratedPatterns @@ -61,6 +63,7 @@ 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, @@ -77,8 +80,9 @@ class ModelGenerationMethodProvider { 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, writeFiles) + workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles) val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries) scopePropagator.propagateAllScopeConstraints val // LinkedHashMap, BatchTransformationRule>> @@ -117,10 +121,12 @@ class ModelGenerationMethodProvider { switch (scopePropagatorStrategy) { case BasicTypeHierarchy: new ScopePropagator(emptySolution) - case PolyhedralTypeHierarchy: { + case PolyhedralTypeHierarchy, + case PolyhedralRelations: { val types = queries.refineObjectQueries.keySet.map[newType].toSet val solver = new CbcPolyhedronSolver - new PolyhedronScopePropagator(emptySolution, types, solver) + new PolyhedronScopePropagator(emptySolution, types, queries.multiplicityConstraintQueries, solver, + scopePropagatorStrategy.requiresUpperBoundIndexing) } 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/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend deleted file mode 100644 index 4b9629df..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend +++ /dev/null @@ -1,46 +0,0 @@ -package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra - -import org.eclipse.emf.common.notify.Notifier -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 - -class MultiplicityGoalConstraintCalculator { - val String targetRelationName; - val IQuerySpecification querySpecification; - var ViatraQueryMatcher matcher; - - new(String targetRelationName, IQuerySpecification querySpecification) { - this.targetRelationName = targetRelationName - this.querySpecification = querySpecification - this.matcher = null - } - - new(MultiplicityGoalConstraintCalculator other) { - this.targetRelationName = other.targetRelationName - this.querySpecification = other.querySpecification - this.matcher = null - } - - def getName() { - targetRelationName - } - - def init(Notifier notifier) { - val engine = ViatraQueryEngine.on(new EMFScope(notifier)) - matcher = querySpecification.getMatcher(engine) - } - - def calculateValue() { - var res = 0 - val allMatches = this.matcher.allMatches - for(match : allMatches) { - //println(targetRelationName+ " missing multiplicity: "+match.get(3)) - val missingMultiplicity = match.get(4) as Integer - res += missingMultiplicity - } - //println(targetRelationName+ " all missing multiplicities: "+res) - return res - } -} \ 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/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend new file mode 100644 index 00000000..86a59aa1 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend @@ -0,0 +1,46 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import org.eclipse.emf.common.notify.Notifier +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 + +class MultiplicityGoalConstraintCalculator { + val String targetRelationName; + val IQuerySpecification querySpecification; + var ViatraQueryMatcher matcher; + + new(String targetRelationName, IQuerySpecification querySpecification) { + this.targetRelationName = targetRelationName + this.querySpecification = querySpecification + this.matcher = null + } + + new(MultiplicityGoalConstraintCalculator other) { + this.targetRelationName = other.targetRelationName + this.querySpecification = other.querySpecification + this.matcher = null + } + + def getName() { + targetRelationName + } + + def init(Notifier notifier) { + val engine = ViatraQueryEngine.on(new EMFScope(notifier)) + matcher = querySpecification.getMatcher(engine) + } + + def calculateValue() { + var res = 0 + val allMatches = this.matcher.allMatches + for(match : allMatches) { + //println(targetRelationName+ " missing multiplicity: "+match.get(3)) + val missingMultiplicity = match.get(2) as Integer + res += missingMultiplicity + } + //println(targetRelationName+ " all missing multiplicities: "+res) + return res + } +} 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 cebd89da..4f0c8f20 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend @@ -2,90 +2,60 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality import com.google.common.collect.ImmutableList import com.google.common.collect.ImmutableMap +import com.google.common.collect.Maps import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnifinishedMultiplicityQueries import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope import java.util.ArrayDeque +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 javax.naming.OperationNotSupportedException +import org.eclipse.viatra.query.runtime.api.IPatternMatch +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.xtend.lib.annotations.FinalFieldsConstructor class PolyhedronScopePropagator extends ScopePropagator { val Map scopeBounds - val LinearConstraint topLevelBounds + val LinearBoundedExpression topLevelBounds + val Polyhedron polyhedron val PolyhedronSaturationOperator operator + List updaters = emptyList - new(PartialInterpretation p, Set possibleNewDynamicTypes, PolyhedronSolver solver) { + new(PartialInterpretation p, Set possibleNewDynamicTypes, + Map unfinishedMultiplicityQueries, + PolyhedronSolver solver, boolean propagateRelations) { super(p) - val instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] - val primitiveDimensions = new HashMap - val constraintsBuilder = ImmutableList.builder - val scopeBoundsBuilder = ImmutableMap.builder - // Dimensions for instantiable types were created according to the type analysis, - // but for any possible primitive types, we create them on demand, - // as there is no Type directly associated with a PartialPrimitiveInterpretation. - // Below we will assume that each PartialTypeInterpretation has at most one Scope. - for (scope : p.scopes) { - switch (targetTypeInterpretation : scope.targetTypeInterpretation) { - PartialPrimitiveInterpretation: { - val dimension = primitiveDimensions.computeIfAbsent(targetTypeInterpretation) [ interpretation | - new Dimension(interpretation.eClass.name, 0, null) - ] - scopeBoundsBuilder.put(scope, dimension) - } - PartialComplexTypeInterpretation: { - val complexType = targetTypeInterpretation.interpretationOf - val dimensions = findSubtypeDimensions(complexType, instanceCounts) - switch (dimensions.size) { - case 0: - if (scope.minNewElements > 0) { - throw new IllegalArgumentException("Found scope for " + complexType.name + - ", but the type cannot be instantiated") - } - case 1: - scopeBoundsBuilder.put(scope, dimensions.head) - default: { - val constraint = new LinearConstraint(dimensions.toInvertedMap[1], null, null) - constraintsBuilder.add(constraint) - scopeBoundsBuilder.put(scope, constraint) - } - } - } - default: - throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + targetTypeInterpretation) - } - } - val allDimensions = ImmutableList.builder.addAll(instanceCounts.values).addAll(primitiveDimensions.values).build - scopeBounds = scopeBoundsBuilder.build - topLevelBounds = new LinearConstraint(allDimensions.toInvertedMap[1], null, null) - constraintsBuilder.add(topLevelBounds) - val expressionsToSaturate = ImmutableList.builder.addAll(scopeBounds.values).add(topLevelBounds).build - val polyhedron = new Polyhedron(allDimensions, constraintsBuilder.build, expressionsToSaturate) + val builder = new PolyhedronBuilder(p) + builder.buildPolyhedron(possibleNewDynamicTypes) + scopeBounds = builder.scopeBounds + topLevelBounds = builder.topLevelBounds + polyhedron = builder.polyhedron operator = solver.createSaturationOperator(polyhedron) - } - - private def findSubtypeDimensions(Type type, Map instanceCounts) { - val subtypes = new HashSet - val dimensions = new HashSet - val stack = new ArrayDeque - stack.addLast(type) - while (!stack.empty) { - val subtype = stack.removeLast - if (subtypes.add(subtype)) { - val dimension = instanceCounts.get(subtype) - if (dimension !== null) { - dimensions.add(dimension) - } - stack.addAll(subtype.subtypes) + 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") + } + if (maximumNumberOfNewNodes <= 0) { + throw new IllegalStateException("Maximum number of new nodes is negative") } + builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, maximumNumberOfNewNodes) + updaters = builder.updaters } - dimensions } override void propagateAllScopeConstraints() { + resetBounds() populatePolyhedronFromScope() val result = operator.saturate() if (result == PolyhedronSaturationResult.EMPTY) { @@ -96,21 +66,36 @@ class PolyhedronScopePropagator extends ScopePropagator { super.propagateAllScopeConstraints() } } + // println(polyhedron) + } + + def resetBounds() { + for (dimension : polyhedron.dimensions) { + dimension.lowerBound = 0 + dimension.upperBound = null + } + for (constraint : polyhedron.constraints) { + constraint.lowerBound = null + constraint.upperBound = null + } } private def populatePolyhedronFromScope() { - topLevelBounds.lowerBound = partialInterpretation.minNewElements + topLevelBounds.tightenLowerBound(partialInterpretation.minNewElements) if (partialInterpretation.maxNewElements >= 0) { - topLevelBounds.upperBound = partialInterpretation.maxNewElements + topLevelBounds.tightenUpperBound(partialInterpretation.maxNewElements) } for (pair : scopeBounds.entrySet) { val scope = pair.key val bounds = pair.value - bounds.lowerBound = scope.minNewElements + bounds.tightenLowerBound(scope.minNewElements) if (scope.maxNewElements >= 0) { - bounds.upperBound = scope.maxNewElements + bounds.tightenUpperBound(scope.maxNewElements) } } + for (updater : updaters) { + updater.update(partialInterpretation) + } } private def populateScopesFromPolyhedron() { @@ -151,4 +136,242 @@ class PolyhedronScopePropagator extends ScopePropagator { throw new IllegalArgumentException("Infinite upper bound: " + bounds) } } + + private static def getCalculatedMultiplicity(ViatraQueryMatcher matcher, + PartialInterpretation p) { + val match = matcher.newEmptyMatch + match.set(0, p.problem) + match.set(1, p) + val iterator = matcher.streamAllMatches(match).iterator + if (!iterator.hasNext) { + return null + } + val value = iterator.next.get(2) as Integer + if (iterator.hasNext) { + throw new IllegalArgumentException("Multiplicity calculation query has more than one match") + } + value + } + + @FinalFieldsConstructor + private static class PolyhedronBuilder { + static val INFINITY_SCALE = 10 + + val PartialInterpretation p + + Map instanceCounts + Map> subtypeDimensions + Map, LinearBoundedExpression> expressionsCache + Map typeBounds + int infinity + ViatraQueryEngine queryEngine + ImmutableList.Builder updatersBuilder + + Map scopeBounds + LinearBoundedExpression topLevelBounds + Polyhedron polyhedron + List updaters + + def buildPolyhedron(Set possibleNewDynamicTypes) { + instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] + val types = p.problem.types + expressionsCache = Maps.newHashMapWithExpectedSize(types.size) + subtypeDimensions = types.toInvertedMap[findSubtypeDimensions.toInvertedMap[1]] + typeBounds = ImmutableMap.copyOf(subtypeDimensions.mapValues[toExpression]) + scopeBounds = buildScopeBounds + topLevelBounds = instanceCounts.values.toInvertedMap[1].toExpression + val dimensions = ImmutableList.copyOf(instanceCounts.values) + val expressionsToSaturate = ImmutableList.copyOf(scopeBounds.values) + polyhedron = new Polyhedron(dimensions, new ArrayList, expressionsToSaturate) + addCachedConstraintsToPolyhedron() + } + + def buildMultiplicityConstraints( + Map constraints, + int maximumNuberOfNewNodes) { + infinity = maximumNuberOfNewNodes * INFINITY_SCALE + queryEngine = ViatraQueryEngine.on(new EMFScope(p)) + updatersBuilder = ImmutableList.builder + for (pair : constraints.entrySet.filter[key.containment].groupBy[key.targetType].entrySet) { + buildContainmentConstraints(pair.key, pair.value) + } + for (pair : constraints.entrySet) { + val constraint = pair.key + if (!constraint.containment) { + buildNonContainmentConstraints(constraint, pair.value) + } + } + updaters = updatersBuilder.build + addCachedConstraintsToPolyhedron() + } + + private def addCachedConstraintsToPolyhedron() { + val constraints = new HashSet + constraints.addAll(expressionsCache.values.filter(LinearConstraint)) + constraints.removeAll(polyhedron.constraints) + polyhedron.constraints.addAll(constraints) + } + + private def buildContainmentConstraints(Type containedType, + List> constraints) { + val typeCoefficients = subtypeDimensions.get(containedType) + val orphansLowerBoundCoefficients = new HashMap(typeCoefficients) + val orphansUpperBoundCoefficients = new HashMap(typeCoefficients) + val unfinishedMultiplicitiesMatchersBuilder = ImmutableList.builder + val remainingContentsQueriesBuilder = ImmutableList.builder + for (pair : constraints) { + val constraint = pair.key + val containerCoefficients = subtypeDimensions.get(constraint.sourceType) + if (constraint.isUpperBoundFinite) { + orphansLowerBoundCoefficients.addCoefficients(-constraint.upperBound, containerCoefficients) + } else { + orphansLowerBoundCoefficients.addCoefficients(-infinity, containerCoefficients) + } + orphansUpperBoundCoefficients.addCoefficients(-constraint.lowerBound, containerCoefficients) + val queries = pair.value + if (constraint.constrainsUnfinished) { + if (queries.unfinishedMultiplicityQuery === null) { + throw new IllegalArgumentException( + "Containment constraints need unfinished multiplicity queries") + } + unfinishedMultiplicitiesMatchersBuilder.add( + queries.unfinishedMultiplicityQuery.getMatcher(queryEngine)) + } + if (queries.remainingContentsQuery === null) { + throw new IllegalArgumentException("Containment constraints need remaining contents queries") + } + remainingContentsQueriesBuilder.add(queries.remainingContentsQuery.getMatcher(queryEngine)) + } + val orphanLowerBound = orphansLowerBoundCoefficients.toExpression + val orphanUpperBound = orphansUpperBoundCoefficients.toExpression + val updater = new ContainmentConstraintUpdater(containedType.name, orphanLowerBound, orphanUpperBound, + unfinishedMultiplicitiesMatchersBuilder.build, remainingContentsQueriesBuilder.build) + updatersBuilder.add(updater) + } + + private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, + UnifinishedMultiplicityQueries queries) { + } + + private def addCoefficients(Map accumulator, int scale, Map a) { + for (pair : a.entrySet) { + val dimension = pair.key + val currentValue = accumulator.get(pair.key) ?: 0 + val newValue = currentValue + scale * pair.value + if (newValue == 0) { + accumulator.remove(dimension) + } else { + accumulator.put(dimension, newValue) + } + } + } + + private def findSubtypeDimensions(Type type) { + val subtypes = new HashSet + val dimensions = new HashSet + val stack = new ArrayDeque + stack.addLast(type) + while (!stack.empty) { + val subtype = stack.removeLast + if (subtypes.add(subtype)) { + val dimension = instanceCounts.get(subtype) + if (dimension !== null) { + dimensions.add(dimension) + } + stack.addAll(subtype.subtypes) + } + } + dimensions + } + + private def toExpression(Map coefficients) { + expressionsCache.computeIfAbsent(coefficients) [ c | + if (c.size == 1 && c.entrySet.head.value == 1) { + c.entrySet.head.key + } else { + new LinearConstraint(c, null, null) + } + ] + } + + private def buildScopeBounds() { + val scopeBoundsBuilder = ImmutableMap.builder + for (scope : p.scopes) { + switch (targetTypeInterpretation : scope.targetTypeInterpretation) { + PartialPrimitiveInterpretation: + throw new OperationNotSupportedException("Primitive type scopes are not yet implemented") + PartialComplexTypeInterpretation: { + val complexType = targetTypeInterpretation.interpretationOf + val typeBound = typeBounds.get(complexType) + if (typeBound === null) { + if (scope.minNewElements > 0) { + throw new IllegalArgumentException("Found scope for " + complexType.name + + ", but the type cannot be instantiated") + } + } else { + scopeBoundsBuilder.put(scope, typeBound) + } + } + default: + throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + + targetTypeInterpretation) + } + } + scopeBoundsBuilder.build + } + } + + private static interface RelationConstraintUpdater { + def void update(PartialInterpretation p) + } + + @FinalFieldsConstructor + static class ContainmentConstraintUpdater implements RelationConstraintUpdater { + val String name + val LinearBoundedExpression orphansLowerBound + val LinearBoundedExpression orphansUpperBound + val List> unfinishedMultiplicitiesMatchers + val List> remainingContentsQueries + + override update(PartialInterpretation p) { + tightenLowerBound(p) + tightenUpperBound(p) + } + + private def tightenLowerBound(PartialInterpretation p) { + var int sum = 0 + for (matcher : remainingContentsQueries) { + val value = matcher.getCalculatedMultiplicity(p) + if (value === null) { + throw new IllegalArgumentException("Remaining contents count is missing for " + name) + } + if (value == -1) { + // Infinite upper bound, no need to tighten. + return + } + sum += value + } + orphansLowerBound.tightenUpperBound(sum) + } + + private def tightenUpperBound(PartialInterpretation p) { + var int sum = 0 + for (matcher : unfinishedMultiplicitiesMatchers) { + val value = matcher.getCalculatedMultiplicity(p) + if (value === null) { + throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) + } + sum += value + } + orphansUpperBound.tightenLowerBound(sum) + } + } + + @FinalFieldsConstructor + static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { + + override update(PartialInterpretation p) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + } } 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 08bf25b9..9c6cb82e 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 @@ -52,18 +52,14 @@ class Polyhedron { val List expressionsToSaturate override toString() ''' - Dimensions: - «FOR dimension : dimensions» - «dimension» - «ENDFOR» - Constraints: - «FOR constraint : constraints» - «constraint» - «ENDFOR» -««« Saturate: -««« «FOR expression : expressionsToSaturate» -««« «IF expression instanceof Dimension»dimension«ELSEIF expression instanceof LinearConstraint»constraint«ELSE»unknown«ENDIF» «expression» -««« «ENDFOR» + Dimensions: + «FOR dimension : dimensions» + «dimension» + «ENDFOR» + Constraints: + «FOR constraint : constraints» + «constraint» + «ENDFOR» ''' } @@ -72,6 +68,18 @@ class Polyhedron { abstract class LinearBoundedExpression { var Integer lowerBound var Integer upperBound + + def void tightenLowerBound(Integer tighterBound) { + if (lowerBound === null || (tighterBound !== null && lowerBound < tighterBound)) { + lowerBound = tighterBound + } + } + + def void tightenUpperBound(Integer tighterBound) { + if (upperBound === null || (tighterBound !== null && upperBound > tighterBound)) { + upperBound = tighterBound + } + } } @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 new file mode 100644 index 00000000..ffa9e6e6 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend @@ -0,0 +1,133 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import com.google.common.collect.ImmutableList +import com.google.common.collect.ImmutableSet +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import java.util.HashMap +import java.util.List +import org.eclipse.xtend.lib.annotations.Data + +@Data +class RelationConstraints { + val List multiplicityConstraints +} + +@Data +class RelationMultiplicityConstraint { + Relation relation + boolean containment + boolean container + int lowerBound + int upperBound + int inverseUpperBound + + def isUpperBoundFinite() { + upperBound >= 0 + } + + private def isInverseUpperBoundFinite() { + inverseUpperBound >= 0 + } + + private def canHaveMultipleSourcesPerTarget() { + inverseUpperBound != 1 + } + + def constrainsUnfinished() { + lowerBound >= 1 && (!container || lowerBound >= 2) + } + + def constrainsUnrepairable() { + constrainsUnfinished && canHaveMultipleSourcesPerTarget + } + + def constrainsRemainingInverse() { + !containment && inverseUpperBoundFinite + } + + def constrainsRemainingContents() { + containment + } + + def isActive() { + constrainsUnfinished || constrainsUnrepairable || constrainsRemainingInverse || constrainsRemainingContents + } + + def getSourceType() { + getParamType(0) + } + + def getTargetType() { + getParamType(1) + } + + private def getParamType(int i) { + val parameters = relation.parameters + if (i < parameters.size) { + val firstParam = parameters.get(i) + if (firstParam instanceof ComplexTypeReference) { + return firstParam.referred + } + } + throw new IllegalArgumentException("Constraint with unknown source type") + } +} + +class RelationConstraintCalculator { + def calculateRelationConstraints(LogicProblem problem) { + val containmentRelations = switch (problem.containmentHierarchies.size) { + case 0: + emptySet + case 1: + ImmutableSet.copyOf(problem.containmentHierarchies.head.containmentRelations) + default: + throw new IllegalArgumentException("Only a single containment hierarchy is supported") + } + val inverseRelations = new HashMap + val lowerMultiplicities = new HashMap + val upperMultiplicities = new HashMap + for (relation : problem.relations) { + lowerMultiplicities.put(relation, 0) + upperMultiplicities.put(relation, -1) + } + for (annotation : problem.annotations) { + switch (annotation) { + InverseRelationAssertion: { + inverseRelations.put(annotation.inverseA, annotation.inverseB) + inverseRelations.put(annotation.inverseB, annotation.inverseA) + } + LowerMultiplicityAssertion: + lowerMultiplicities.put(annotation.relation, annotation.lower) + UpperMultiplicityAssertion: + upperMultiplicities.put(annotation.relation, annotation.upper) + } + } + val multiplicityConstraintsBuilder = ImmutableList.builder() + for (relation : problem.relations) { + val containment = containmentRelations.contains(relation) + val lowerMultiplicity = lowerMultiplicities.get(relation) + val upperMultiplicity = upperMultiplicities.get(relation) + var container = false + var inverseUpperMultiplicity = -1 + val inverseRelation = inverseRelations.get(relation) + if (inverseRelation !== null) { + inverseUpperMultiplicity = upperMultiplicities.get(relation) + container = containmentRelations.contains(inverseRelation) + } + val constraint = new RelationMultiplicityConstraint(relation, containment, container, lowerMultiplicity, + upperMultiplicity, inverseUpperMultiplicity) + if (constraint.isActive) { + if (relation.parameters.size != 2) { + throw new IllegalArgumentException('''Relation «relation.name» has multiplicity or containment constraints, but it is not binary''') + } + multiplicityConstraintsBuilder.add(constraint) + } + } + new RelationConstraints(multiplicityConstraintsBuilder.build) + } +} 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 f0494214..3b442cd3 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 @@ -10,11 +10,6 @@ import java.util.Map import java.util.Set import org.eclipse.xtend.lib.annotations.Accessors -enum ScopePropagatorStrategy { - BasicTypeHierarchy, - PolyhedralTypeHierarchy -} - class ScopePropagator { @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation Map type2Scope diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java new file mode 100644 index 00000000..b1c5a658 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java @@ -0,0 +1,18 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality; + +public enum ScopePropagatorStrategy { + BasicTypeHierarchy, + + PolyhedralTypeHierarchy, + + PolyhedralRelations { + @Override + public boolean requiresUpperBoundIndexing() { + return true; + } + }; + + public boolean requiresUpperBoundIndexing() { + return false; + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index 24b3e870..1b0db90e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend @@ -1,7 +1,6 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion -import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference @@ -17,6 +16,7 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Transform import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import java.util.HashMap import java.util.Map @@ -26,22 +26,26 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.xtend.lib.annotations.Accessors import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy class PatternGenerator { - @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) - @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer(this) - @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer(this) + @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) + @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer( + this) + @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer( + this) @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this) @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this) - @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer = new UnfinishedIndexer(this) - @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this) - @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this) - - public new(TypeInferenceMethod typeInferenceMethod) { - if(typeInferenceMethod == TypeInferenceMethod.Generic) { + @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer + @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator // = new RefinementGenerator(this) + @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator( + this) + + new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) { + if (typeInferenceMethod == TypeInferenceMethod.Generic) { this.typeIndexer = new GenericTypeIndexer(this) this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this) - } else if(typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) { + } else if (typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) { this.typeIndexer = new TypeIndexerWithPreliminaryTypeAnalysis(this) this.typeRefinementGenerator = new TypeRefinementWithPreliminaryTypeAnalysis(this) } else { @@ -49,112 +53,100 @@ class PatternGenerator { this.typeRefinementGenerator = null throw new IllegalArgumentException('''Unknown type indexing technique : «typeInferenceMethod.name»''') } + this.unfinishedIndexer = new UnfinishedIndexer(this, scopePropagatorStrategy.requiresUpperBoundIndexing) } - - public def requiresTypeAnalysis() { + + def requiresTypeAnalysis() { typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis } - - public dispatch def CharSequence referRelation( - RelationDeclaration referred, - String sourceVariable, - String targetVariable, - Modality modality, - Map fqn2PQuery) - { - return this.relationDeclarationIndexer.referRelation(referred,sourceVariable,targetVariable,modality) + + dispatch def CharSequence referRelation(RelationDeclaration referred, String sourceVariable, String targetVariable, + Modality modality, Map fqn2PQuery) { + return this.relationDeclarationIndexer.referRelation(referred, sourceVariable, targetVariable, modality) } - public dispatch def CharSequence referRelation( - RelationDefinition referred, - String sourceVariable, - String targetVariable, - Modality modality, - Map fqn2PQuery) - { - val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery) - return this.relationDefinitionIndexer.referPattern(pattern,#[sourceVariable,targetVariable],modality,true,false) + + dispatch def CharSequence referRelation(RelationDefinition referred, String sourceVariable, String targetVariable, + Modality modality, Map fqn2PQuery) { + val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup( + fqn2PQuery) + return this.relationDefinitionIndexer.referPattern(pattern, #[sourceVariable, targetVariable], modality, true, + false) } - - def public referRelationByName(EReference reference, - String sourceVariable, - String targetVariable, - Modality modality) - { - '''find «modality.name.toLowerCase»InRelation«canonizeName('''«reference.name» reference «reference.EContainingClass.name»''') - »(problem,interpretation,«sourceVariable»,«targetVariable»);''' + + def referRelationByName(EReference reference, String sourceVariable, String targetVariable, Modality modality) { + '''find «modality.name.toLowerCase»InRelation«canonizeName('''«reference.name» reference «reference.EContainingClass.name»''')»(problem,interpretation,«sourceVariable»,«targetVariable»);''' } - - def public CharSequence referAttributeByName(EAttribute attribute, - String sourceVariable, - String targetVariable, - Modality modality) - { - '''find «modality.name.toLowerCase»InRelation«canonizeName('''«attribute.name» attribute «attribute.EContainingClass.name»''') - »(problem,interpretation,«sourceVariable»,«targetVariable»);''' + + def CharSequence referAttributeByName(EAttribute attribute, String sourceVariable, String targetVariable, + Modality modality) { + '''find «modality.name.toLowerCase»InRelation«canonizeName('''«attribute.name» attribute «attribute.EContainingClass.name»''')»(problem,interpretation,«sourceVariable»,«targetVariable»);''' } - - public def canonizeName(String name) { + + def canonizeName(String name) { name.split(' ').join('_') } - - public def lowerMultiplicities(LogicProblem problem) { - problem.assertions.map[annotations].flatten.filter(LowerMultiplicityAssertion).filter[!it.relation.isDerived] - } - public def wfQueries(LogicProblem problem) { - problem.assertions.map[it.annotations] - .flatten - .filter(TransformedViatraWellformednessConstraint) - .map[it.query] + + def wfQueries(LogicProblem problem) { + problem.assertions.map[it.annotations].flatten.filter(TransformedViatraWellformednessConstraint).map[it.query] } - public def getContainments(LogicProblem p) { + + def getContainments(LogicProblem p) { return p.containmentHierarchies.head.containmentRelations } - public def getInverseRelations(LogicProblem p) { + + def getInverseRelations(LogicProblem p) { val inverseRelations = new HashMap - p.annotations.filter(InverseRelationAssertion).forEach[ - inverseRelations.put(it.inverseA,it.inverseB) - inverseRelations.put(it.inverseB,it.inverseA) + p.annotations.filter(InverseRelationAssertion).forEach [ + inverseRelations.put(it.inverseA, it.inverseB) + inverseRelations.put(it.inverseB, it.inverseA) ] return inverseRelations } - public def isRepresentative(Relation relation, Relation inverse) { - if(inverse == null) { + + def isRepresentative(Relation relation, Relation inverse) { + if (inverse === null) { return true } else { - relation.name.compareTo(inverse.name)<1 + relation.name.compareTo(inverse.name) < 1 } } - - public def isDerived(Relation relation) { + + def isDerived(Relation relation) { relation.annotations.exists[it instanceof DefinedByDerivedFeature] } - public def getDerivedDefinition(RelationDeclaration relation) { + + def getDerivedDefinition(RelationDeclaration relation) { relation.annotations.filter(DefinedByDerivedFeature).head.query } - + private def allTypeReferences(LogicProblem problem) { problem.eAllContents.filter(TypeReference).toIterable } + protected def hasBoolean(LogicProblem problem) { problem.allTypeReferences.exists[it instanceof BoolTypeReference] } + protected def hasInteger(LogicProblem problem) { problem.allTypeReferences.exists[it instanceof IntTypeReference] } + protected def hasReal(LogicProblem problem) { problem.allTypeReferences.exists[it instanceof RealTypeReference] } + protected def hasString(LogicProblem problem) { problem.allTypeReferences.exists[it instanceof StringTypeReference] } - - public def transformBaseProperties( + + def transformBaseProperties( LogicProblem problem, PartialInterpretation emptySolution, - Map fqn2PQuery, - TypeAnalysisResult typeAnalysisResult + Map fqn2PQuery, + TypeAnalysisResult typeAnalysisResult, + RelationConstraints constraints ) { - + return ''' import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" @@ -188,7 +180,7 @@ class PatternGenerator { private pattern elementCloseWorld(element:DefinedElement) { PartialInterpretation.openWorldElements(i,element); - PartialInterpretation.maxNewElements(i,0); + PartialInterpretation.maxNewElements(i,0); } or { Scope.targetTypeInterpretation(scope,interpretation); PartialTypeInterpratation.elements(interpretation,element); @@ -221,7 +213,7 @@ class PatternGenerator { ////////// // 1.1.1 primitive Type Indexers ////////// -««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + ««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { ««« find interpretation(problem,interpretation); ««« PartialInterpretation.booleanelements(interpretation,element); ««« } @@ -279,7 +271,7 @@ class PatternGenerator { ////////// // 3.1 Unfinishedness Measured by Multiplicity ////////// - «unfinishedIndexer.generateUnfinishedMultiplicityQueries(problem,fqn2PQuery)» + «unfinishedIndexer.generateUnfinishedMultiplicityQueries(constraints.multiplicityConstraints,fqn2PQuery)» ////////// // 3.2 Unfinishedness Measured by WF Queries @@ -302,6 +294,6 @@ class PatternGenerator { // 4.3 Relation refinement ////////// «relationRefinementGenerator.generateRefineReference(problem)» - ''' + ''' } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index e87f52af..90f79810 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend @@ -10,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStati import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace @@ -23,78 +25,96 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.xtend.lib.annotations.Data import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy -@Data class GeneratedPatterns { - public Map>> invalidWFQueries - public Map>> unfinishedWFQueries - public Map>> unfinishedMulticiplicityQueries - public Map>> refineObjectQueries - public Map>> refineTypeQueries - public Map, IQuerySpecification>> refinerelationQueries +@Data +class GeneratedPatterns { + public Map>> invalidWFQueries + public Map>> unfinishedWFQueries + public Map multiplicityConstraintQueries + public Map>> unfinishedMulticiplicityQueries + public Map>> refineObjectQueries + public Map>> refineTypeQueries + public Map, IQuerySpecification>> refinerelationQueries public Map modalRelationQueries public Collection>> allQueries } -@Data class ModalPatternQueries { +@Data +class ModalPatternQueries { val IQuerySpecification> mayQuery val IQuerySpecification> mustQuery val IQuerySpecification> currentQuery } +@Data +class UnifinishedMultiplicityQueries { + val IQuerySpecification> unfinishedMultiplicityQuery + val IQuerySpecification> unrepairableMultiplicityQuery + val IQuerySpecification> remainingInverseMultiplicityQuery + val IQuerySpecification> remainingContentsQuery +} + class PatternProvider { - + val TypeAnalysis typeAnalysis = new TypeAnalysis - - public def generateQueries( - LogicProblem problem, - PartialInterpretation emptySolution, - ModelGenerationStatistics statistics, - Set existingQueries, - ReasonerWorkspace workspace, - TypeInferenceMethod typeInferenceMethod, - boolean writeToFile) - { + + def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, + Set existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, + ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, boolean writeToFile) { val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] - val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod) - val typeAnalysisResult = if(patternGenerator.requiresTypeAnalysis) { - val startTime = System.nanoTime - val result = typeAnalysis.performTypeAnalysis(problem,emptySolution) - val typeAnalysisTime = System.nanoTime - startTime - statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime - result - } else { - null - } - val baseIndexerFile = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) - if(writeToFile) { - workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) + val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) + val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { + val startTime = System.nanoTime + val result = typeAnalysis.performTypeAnalysis(problem, emptySolution) + val typeAnalysisTime = System.nanoTime - startTime + statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime + result + } else { + null + } + val baseIndexerFile = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, + typeAnalysisResult, relationConstraints) + if (writeToFile) { + workspace.writeText('''generated3valued.vql_deactivated''', baseIndexerFile) } val ParseUtil parseUtil = new ParseUtil val generatedQueries = parseUtil.parse(baseIndexerFile) - val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,generatedQueries); + val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, + relationConstraints, generatedQueries) return runtimeQueries } - + private def GeneratedPatterns calclulateRuntimeQueries( PatternGenerator patternGenerator, LogicProblem problem, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult, + RelationConstraints relationConstraints, Map>> queries ) { - val Map>> - invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] - val Map>> - unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] - val Map>> - unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)] - val Map>> - refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] - val Map>> - refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] - val Map, IQuerySpecification>> - refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] - val Map modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | + val invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues [ + it.lookup(queries) + ] + val unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues [ + it.lookup(queries) + ] + val multiplicityConstraintQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries( + relationConstraints.multiplicityConstraints).mapValues [ + new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries), + unrepairableMultiplicityQueryName?.lookup(queries), + remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries)) + ] + val unfinishedMultiplicityQueries = multiplicityConstraintQueries.entrySet.filter [ + value.unfinishedMultiplicityQuery !== null + ].toMap([key.relation], [value.unfinishedMultiplicityQuery]) + val refineObjectsQueries = patternGenerator.typeRefinementGenerator. + getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues[it.lookup(queries)] + val refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution, + typeAnalysisResult).mapValues[it.lookup(queries)] + val refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem). + mapValues[it.lookup(queries)] + val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | val indexer = patternGenerator.relationDefinitionIndexer new ModalPatternQueries( indexer.relationDefinitionName(relationDefinition, Modality.MAY).lookup(queries), @@ -105,6 +125,7 @@ class PatternProvider { return new GeneratedPatterns( invalidWFQueries, unfinishedWFQueries, + multiplicityConstraintQueries, unfinishedMultiplicityQueries, refineObjectsQueries, refineTypeQueries, diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend index f9e9baea..fa73c861 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend @@ -9,77 +9,71 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference class RelationRefinementGenerator { PatternGenerator base; + public new(PatternGenerator base) { this.base = base } - - def CharSequence generateRefineReference(LogicProblem p) { - return ''' - «FOR relationRefinement: this.getRelationRefinements(p)» - pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( - problem:LogicProblem, interpretation:PartialInterpretation, - relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value != null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», - from: DefinedElement, to: DefinedElement) - { - find interpretation(problem,interpretation); - PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); - PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); - «IF relationRefinement.value != null» - PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); - PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); - «ENDIF» - find mustExist(problem, interpretation, from); - find mustExist(problem, interpretation, to); - «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» - «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» - «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» - neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» - } + + def CharSequence generateRefineReference(LogicProblem p) ''' + «FOR relationRefinement : this.getRelationRefinements(p)» + pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», + from: DefinedElement, to: DefinedElement) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); + PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); + «IF relationRefinement.value !== null» + PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); + PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); + «ENDIF» + find mustExist(problem, interpretation, from); + find mustExist(problem, interpretation, to); + «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» + «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» + «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» + neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» + } «ENDFOR» - ''' - } - + ''' + def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { - '''«IF inverseRelation != null - »refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»« - ELSE - »refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' + '''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' } - + def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, - String inverseInterpretationName, String sourceName, String targetName) - '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation != null»inverseInterpretationName, «ENDIF»«sourceName», «targetName»);''' - + String inverseInterpretationName, String sourceName, + String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»inverseInterpretationName, «ENDIF»«sourceName», «targetName»);''' + def getRefineRelationQueries(LogicProblem p) { // val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet // p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»'''] /* - val res = new LinkedHashMap - for(relation: getRelationRefinements(p)) { - if(inverseRelations.containsKey(relation)) { - val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»''' - res.put(relation -> inverseRelations.get(relation),name) - } else { - val name = '''refineRelation_«base.canonizeName(relation.name)»''' - res.put(relation -> null,name) - } - } - return res*/ - - getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key,it.value)] + * val res = new LinkedHashMap + * for(relation: getRelationRefinements(p)) { + * if(inverseRelations.containsKey(relation)) { + * val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»''' + * res.put(relation -> inverseRelations.get(relation),name) + * } else { + * val name = '''refineRelation_«base.canonizeName(relation.name)»''' + * res.put(relation -> null,name) + * } + * } + return res*/ + getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)] } - def getRelationRefinements(LogicProblem p) { val inverses = base.getInverseRelations(p) val containments = base.getContainments(p) val list = new LinkedList - for(relation : p.relations.filter(RelationDeclaration)) { - if(!containments.contains(relation)) { - if(inverses.containsKey(relation)) { + for (relation : p.relations.filter(RelationDeclaration)) { + if (!containments.contains(relation)) { + if (inverses.containsKey(relation)) { val inverse = inverses.get(relation) - if(!containments.contains(inverse)) { - if(base.isRepresentative(relation,inverse)) { + if (!containments.contains(inverse)) { + if (base.isRepresentative(relation, inverse)) { list += (relation -> inverse) } } @@ -90,4 +84,4 @@ class RelationRefinementGenerator { } return list } -} \ 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/patterns/TypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend index 7e3fad91..ee7299cd 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend @@ -86,8 +86,8 @@ abstract class TypeRefinementGenerator { } protected def String patternName(Relation containmentRelation, Relation inverseContainment, Type newType) { - if(containmentRelation != null) { - if(inverseContainment != null) { + if(containmentRelation !== null) { + if(inverseContainment !== null) { '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»_with_«base.canonizeName(inverseContainment.name)»''' } else { '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»''' diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend index ad1c9033..286756a8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend @@ -1,85 +1,195 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns -import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem -import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransformedViatraWellformednessConstraint +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint +import java.util.LinkedHashMap +import java.util.List import java.util.Map import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import org.eclipse.xtend.lib.annotations.Data import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import java.util.LinkedHashMap -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference + +@Data +class UnifinishedMultiplicityQueryNames { + val String unfinishedMultiplicityQueryName + val String unrepairableMultiplicityQueryName + val String remainingInverseMultiplicityQueryName + val String remainingContentsQueryName +} class UnfinishedIndexer { val PatternGenerator base - - new(PatternGenerator patternGenerator) { + val boolean indexUpperMultiplicities + + new(PatternGenerator patternGenerator, boolean indexUpperMultiplicities) { this.base = patternGenerator + this.indexUpperMultiplicities = indexUpperMultiplicities } - - def generateUnfinishedWfQueries(LogicProblem problem, Map fqn2PQuery) { + + def generateUnfinishedWfQueries(LogicProblem problem, Map fqn2PQuery) { val wfQueries = base.wfQueries(problem) ''' - «FOR wfQuery: wfQueries» - pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation, - «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR») - { - «base.relationDefinitionIndexer.referPattern( + «FOR wfQuery : wfQueries» + pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation, + «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR») + { + «base.relationDefinitionIndexer.referPattern( wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery), wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters.map['''var_«it.name»'''], Modality.CURRENT, true,false)» - } - «ENDFOR» + } + «ENDFOR» ''' } + def getUnfinishedWFQueryNames(LogicProblem problem) { val wfQueries = base.wfQueries(problem) val map = new LinkedHashMap - for(wfQuery : wfQueries) { - map.put(wfQuery.target,'''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''') + for (wfQuery : wfQueries) { + map.put(wfQuery.target, '''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''') } return map } - def generateUnfinishedMultiplicityQueries(LogicProblem problem, Map fqn2PQuery) { - val lowerMultiplicities = base.lowerMultiplicities(problem) - return ''' - «FOR lowerMultiplicity : lowerMultiplicities» - pattern «unfinishedMultiplicityName(lowerMultiplicity)»(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,missingMultiplicity) { - find interpretation(problem,interpretation); - PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); - PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«lowerMultiplicity.relation.name»"); - «base.typeIndexer.referInstanceOf(lowerMultiplicity.firstParamTypeOfRelation,Modality::MUST,"object")» - numberOfExistingReferences == count «base.referRelation(lowerMultiplicity.relation,"object","_",Modality.MUST,fqn2PQuery)» - check(numberOfExistingReferences < «lowerMultiplicity.lower»); - missingMultiplicity == eval(«lowerMultiplicity.lower»-numberOfExistingReferences); - } + + def generateUnfinishedMultiplicityQueries(List constraints, + Map fqn2PQuery) ''' + «FOR constraint : constraints» + «IF constraint.constrainsUnfinished» + private pattern «unfinishedMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, missingMultiplicity:java Integer) { + find interpretation(problem,interpretation); + find mustExist(problem,interpretation,object); + «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» + numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» + check(numberOfExistingReferences < «constraint.lowerBound»); + missingMultiplicity == eval(«constraint.lowerBound»-numberOfExistingReferences); + } + + pattern «unfinishedMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, missingMultiplicity:java Integer) { + find interpretation(problem,interpretation); + missingMultiplicity == sum find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); + } + «ENDIF» + + «IF indexUpperMultiplicities» + «IF constraint.constrainsUnrepairable» + private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { + find interpretation(problem,interpretation); + find mustExist(problem,interpretation,source); + «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» + find mustExist(problem,interpretation,target); + «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» + neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» + «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» + } + + private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { + find interpretation(problem,interpretation); + find mustExist(problem,interpretation,object); + «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» + find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); + numerOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); + check(numerOfRepairMatches < missingMultiplicity); + unrepairableMultiplicity == eval(missingMultiplicity-numerOfRepairMatches); + } + + private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) { + find interpretation(problem,interpretation); + unrepairableMultiplicity == max find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); + } or { + find interpretation(problem,interpretation); + neg find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, _); + unrepairableMultiplicity == 0; + } + «ENDIF» + + «IF constraint.constrainsRemainingInverse» + private pattern «remainingMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) { + find interpretation(problem,interpretation); + find mustExist(problem,interpretation,object); + «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» + numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» + check(numberOfExistingReferences < «constraint.inverseUpperBound»); + remainingMultiplicity == eval(«constraint.inverseUpperBound»-numberOfExistingReferences); + } + + pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { + find interpretation(problem,interpretation); + remainingMultiplicity == sum find «remainingMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); + } + «ENDIF» + + «IF constraint.constrainsRemainingContents» + «IF constraint.upperBoundFinite» + private pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) { + find interpretation(problem,interpretation); + find mustExist(problem,interpretation,object); + «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» + numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» + check(numberOfExistingReferences < «constraint.upperBound»); + remainingMultiplicity == eval(«constraint.upperBound»-numberOfExistingReferences); + } + + pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { + find interpretation(problem,interpretation); + remainingMultiplicity == sum find «remainingContentsName(constraint)»_helper(problem, interpretation, _, #_); + } + «ELSE» + pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation) { + find interpretation(problem,interpretation); + find mustExist(problem,interpretation,object); + «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» + } + + pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { + find interpretation(problem,interpretation); + find «remainingContentsName(constraint)»_helper(problem, interpretation); + remainingMultiplicity == -1; + } or { + find interpretation(problem,interpretation); + neg find «remainingContentsName(constraint)»_helper(problem, interpretation); + remainingMultiplicity == 0; + } + «ENDIF» + «ENDIF» + «ENDIF» «ENDFOR» - ''' - } - def String unfinishedMultiplicityName(LowerMultiplicityAssertion lowerMultiplicityAssertion) - '''unfinishedLowerMultiplicity_«base.canonizeName(lowerMultiplicityAssertion.relation.name)»''' - - def public referUnfinishedMultiplicityQuery(LowerMultiplicityAssertion lowerMultiplicityAssertion) - '''find «unfinishedMultiplicityName(lowerMultiplicityAssertion)»(problem, interpretation ,object, missingMultiplicity);''' - - def getFirstParamTypeOfRelation(LowerMultiplicityAssertion lowerMultiplicityAssertion) { - val parameters = lowerMultiplicityAssertion.relation.parameters - if(parameters.size == 2) { - val firstParam = parameters.get(0) - if(firstParam instanceof ComplexTypeReference) { - return firstParam.referred - } - } - } - - def getUnfinishedMultiplicityQueries(LogicProblem problem) { - val lowerMultiplicities = base.lowerMultiplicities(problem) - val map = new LinkedHashMap - for(lowerMultiplicity : lowerMultiplicities) { - map.put(lowerMultiplicity.relation,unfinishedMultiplicityName(lowerMultiplicity)) - } - return map + ''' + + def String unfinishedMultiplicityName( + RelationMultiplicityConstraint constraint) '''unfinishedLowerMultiplicity_«base.canonizeName(constraint.relation.name)»''' + + def String unrepairableMultiplicityName( + RelationMultiplicityConstraint constraint) '''unrepairableLowerMultiplicity_«base.canonizeName(constraint.relation.name)»''' + + private def String repairMatchName( + RelationMultiplicityConstraint constraint) '''repair_«base.canonizeName(constraint.relation.name)»''' + + def String remainingMultiplicityName( + RelationMultiplicityConstraint constraint) '''remainingInverseUpperMultiplicity_«base.canonizeName(constraint.relation.name)»''' + + def String remainingContentsName( + RelationMultiplicityConstraint constraint) '''remainingContents_«base.canonizeName(constraint.relation.name)»''' + + def getUnfinishedMultiplicityQueries(List constraints) { + constraints.toInvertedMap [ constraint | + new UnifinishedMultiplicityQueryNames( + if(constraint.constrainsUnfinished) unfinishedMultiplicityName(constraint) else null, + if (indexUpperMultiplicities && constraint.constrainsUnrepairable) + unrepairableMultiplicityName(constraint) + else + null, + if (indexUpperMultiplicities && constraint.constrainsRemainingInverse) + remainingMultiplicityName(constraint) + else + null, + if (indexUpperMultiplicities && constraint.constrainsRemainingContents) + remainingContentsName(constraint) + else + null + ) + ] } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index e1be2742..b6fdbe06 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -1,6 +1,6 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns import java.util.ArrayList -- cgit v1.2.3-54-g00ecf