From e3e8c7810679acebb3418dd355ca6732b9b117d2 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 24 Jul 2019 14:17:45 +0200 Subject: Containment root constraint propagator --- .../ModelGenerationMethodProvider.xtend | 5 +- .../cardinality/PolyhedronScopePropagator.xtend | 44 ++++++++++-- .../patterns/GenericTypeRefinementGenerator.xtend | 6 +- .../logic2viatra/patterns/PatternProvider.xtend | 6 +- .../patterns/TypeRefinementGenerator.xtend | 83 ++++++++++++---------- ...TypeRefinementWithPreliminaryTypeAnalysis.xtend | 6 +- 6 files changed, 99 insertions(+), 51 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf') 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 3a99d3bf..4b278188 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 @@ -45,6 +45,7 @@ class ModelGenerationStatistics { Collection> relationRefinementRules List unfinishedMultiplicities + Collection>> unfinishedWF Collection>> invalidWF @@ -125,8 +126,8 @@ class ModelGenerationMethodProvider { case PolyhedralRelations: { val types = queries.refineObjectQueries.keySet.map[newType].toSet val solver = new CbcPolyhedronSolver - new PolyhedronScopePropagator(emptySolution, types, queries.multiplicityConstraintQueries, solver, - scopePropagatorStrategy.requiresUpperBoundIndexing) + new PolyhedronScopePropagator(emptySolution, types, queries.multiplicityConstraintQueries, + queries.hasElementInContainmentQuery, 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/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 4f0c8f20..ce357272 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 @@ -3,6 +3,7 @@ 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 com.google.common.collect.Sets 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 @@ -18,6 +19,7 @@ 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 import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher import org.eclipse.viatra.query.runtime.emf.EMFScope @@ -32,6 +34,7 @@ class PolyhedronScopePropagator extends ScopePropagator { new(PartialInterpretation p, Set possibleNewDynamicTypes, Map unfinishedMultiplicityQueries, + IQuerySpecification> hasElementInContainmentQuery, PolyhedronSolver solver, boolean propagateRelations) { super(p) val builder = new PolyhedronBuilder(p) @@ -49,7 +52,8 @@ class PolyhedronScopePropagator extends ScopePropagator { if (maximumNumberOfNewNodes <= 0) { throw new IllegalStateException("Maximum number of new nodes is negative") } - builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, maximumNumberOfNewNodes) + builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, + maximumNumberOfNewNodes) updaters = builder.updaters } } @@ -57,6 +61,7 @@ class PolyhedronScopePropagator extends ScopePropagator { override void propagateAllScopeConstraints() { resetBounds() populatePolyhedronFromScope() + println(polyhedron) val result = operator.saturate() if (result == PolyhedronSaturationResult.EMPTY) { throw new IllegalStateException("Scope bounds cannot be satisfied") @@ -66,7 +71,7 @@ class PolyhedronScopePropagator extends ScopePropagator { super.propagateAllScopeConstraints() } } - // println(polyhedron) + println(polyhedron) } def resetBounds() { @@ -188,13 +193,16 @@ class PolyhedronScopePropagator extends ScopePropagator { def buildMultiplicityConstraints( Map constraints, + IQuerySpecification> hasElementInContainmentQuery, 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) { + val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType] + for (pair : containmentConstraints.entrySet) { buildContainmentConstraints(pair.key, pair.value) } + buildConstainmentRootConstraints(containmentConstraints.keySet, hasElementInContainmentQuery) for (pair : constraints.entrySet) { val constraint = pair.key if (!constraint.containment) { @@ -249,6 +257,19 @@ class PolyhedronScopePropagator extends ScopePropagator { updatersBuilder.add(updater) } + private def buildConstainmentRootConstraints(Set containedTypes, + IQuerySpecification> hasElementInContainmentQuery) { + val matcher = hasElementInContainmentQuery.getMatcher(queryEngine) + val rootDimensions = Sets.newHashSet(instanceCounts.values) + for (type : containedTypes) { + val containedDimensions = subtypeDimensions.get(type).keySet + rootDimensions.removeAll(containedDimensions) + } + for (dimension : rootDimensions) { + updatersBuilder.add(new ContainmentRootConstraintUpdater(dimension, matcher)) + } + } + private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, UnifinishedMultiplicityQueries queries) { } @@ -366,12 +387,23 @@ class PolyhedronScopePropagator extends ScopePropagator { orphansUpperBound.tightenLowerBound(sum) } } - + @FinalFieldsConstructor static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { - + val LinearBoundedExpression typeCardinality + val ViatraQueryMatcher hasElementInContainmentMatcher + override update(PartialInterpretation p) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + if (hasElementInContainmentMatcher.hasMatch(p)) { + typeCardinality.tightenUpperBound(0) + } else { + typeCardinality.tightenUpperBound(1) + } + } + + private static def hasMatch(ViatraQueryMatcher matcher, PartialInterpretation p) { + val match = matcher.newMatch(p.problem, p) + matcher.countMatches(match) != 0 } } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend index 2e03d6ed..c9f6abce 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend @@ -11,7 +11,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import java.util.HashMap class GenericTypeRefinementGenerator extends TypeRefinementGenerator { - public new(PatternGenerator base) { + new(PatternGenerator base) { super(base) } override requiresTypeAnalysis() { false } @@ -25,7 +25,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { inverseRelations.put(it.inverseB,it.inverseA) ] return ''' - private pattern hasElementInContainment(problem:LogicProblem, interpretation:PartialInterpretation) + pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation) «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{ find interpretation(problem,interpretation); «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» @@ -77,7 +77,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { typeInterpretation:PartialComplexTypeInterpretation) { find interpretation(problem,interpretation); - neg find hasElementInContainment(problem,interpretation); + neg find «hasElementInContainmentName»(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); PartialComplexTypeInterpretation.interpretationOf.name(type,"«type.name»"); «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» 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 90f79810..b10c8e88 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 @@ -12,6 +12,7 @@ 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.cardinality.ScopePropagatorStrategy 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 @@ -25,13 +26,13 @@ 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 multiplicityConstraintQueries + public IQuerySpecification> hasElementInContainmentQuery public Map>> unfinishedMulticiplicityQueries public Map>> refineObjectQueries public Map>> refineTypeQueries @@ -105,6 +106,8 @@ class PatternProvider { unrepairableMultiplicityQueryName?.lookup(queries), remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries)) ] + val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( + queries) val unfinishedMultiplicityQueries = multiplicityConstraintQueries.entrySet.filter [ value.unfinishedMultiplicityQuery !== null ].toMap([key.relation], [value.unfinishedMultiplicityQuery]) @@ -126,6 +129,7 @@ class PatternProvider { invalidWFQueries, unfinishedWFQueries, multiplicityConstraintQueries, + hasElementInContainmentQuery, 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/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 ee7299cd..4ef336ae 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 @@ -25,69 +25,76 @@ class ObjectCreationPrecondition { abstract class TypeRefinementGenerator { val protected PatternGenerator base; - public new(PatternGenerator base) { + + new(PatternGenerator base) { this.base = base } - - public def boolean requiresTypeAnalysis() - public def CharSequence generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) - public def CharSequence generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) - public def Map getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) - - public def getRefineObjectQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { - val Map objectCreationQueries = new LinkedHashMap + + def boolean requiresTypeAnalysis() + + def CharSequence generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, + TypeAnalysisResult typeAnalysisResult) + + def CharSequence generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, + TypeAnalysisResult typeAnalysisResult) + + def Map getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, + TypeAnalysisResult typeAnalysisResult) + + def getRefineObjectQueryNames(LogicProblem p, PartialInterpretation emptySolution, + TypeAnalysisResult typeAnalysisResult) { + val Map objectCreationQueries = new LinkedHashMap val containment = p.containmentHierarchies.head 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) ] - for(type: p.types.filter(TypeDeclaration).filter[!it.isAbstract]) { - if(containment.typeInContainment(type)) { - for(containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]) { - if(inverseRelations.containsKey(containmentRelation)) { + for (type : p.types.filter(TypeDeclaration).filter[!it.isAbstract]) { + if (containment.typeInContainment(type)) { + for (containmentRelation : containment.containmentRelations. + filter[canBeContainedByRelation(it, type)]) { + if (inverseRelations.containsKey(containmentRelation)) { objectCreationQueries.put( - new ObjectCreationPrecondition(containmentRelation,inverseRelations.get(containmentRelation),type), - this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)) + new ObjectCreationPrecondition(containmentRelation, + inverseRelations.get(containmentRelation), type), + this.patternName(containmentRelation, inverseRelations.get(containmentRelation), type)) } else { - objectCreationQueries.put( - new ObjectCreationPrecondition(containmentRelation,null,type), - patternName(containmentRelation,null,type)) + objectCreationQueries.put(new ObjectCreationPrecondition(containmentRelation, null, type), + patternName(containmentRelation, null, type)) } } - objectCreationQueries.put( - new ObjectCreationPrecondition(null,null,type), - patternName(null,null,type)) + objectCreationQueries.put(new ObjectCreationPrecondition(null, null, type), + patternName(null, null, type)) } else { - objectCreationQueries.put( - new ObjectCreationPrecondition(null,null,type), - this.patternName(null,null,type)) + objectCreationQueries.put(new ObjectCreationPrecondition(null, null, type), + this.patternName(null, null, type)) } } return objectCreationQueries } - + protected def canBeContainedByRelation(Relation r, Type t) { - if(r.parameters.size==2) { + if (r.parameters.size == 2) { val param = r.parameters.get(1) - if(param instanceof ComplexTypeReference) { + if (param instanceof ComplexTypeReference) { val allSuperTypes = t.transitiveClosureStar[it.supertypes] - for(superType : allSuperTypes) { + for (superType : allSuperTypes) { if(param.referred == superType) return true } } } return false } - + private def typeInContainment(ContainmentHierarchy hierarchy, Type type) { val allSuperTypes = type.transitiveClosureStar[it.supertypes] return allSuperTypes.exists[hierarchy.typesOrderedInHierarchy.contains(it)] } - + 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)»''' @@ -96,4 +103,8 @@ abstract class TypeRefinementGenerator { '''createObject_«base.canonizeName(newType.name)»''' } } -} \ No newline at end of file + + def hasElementInContainmentName() { + "hasElementInContainment" + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend index cbbbcb08..1a81695e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend @@ -10,7 +10,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import java.util.HashMap class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ - public new(PatternGenerator base) { + new(PatternGenerator base) { super(base) } override requiresTypeAnalysis() { true } @@ -24,7 +24,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ inverseRelations.put(it.inverseB,it.inverseA) ] return ''' - private pattern hasElementInContainment(problem:LogicProblem, interpretation:PartialInterpretation) + pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation) «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{ find interpretation(problem,interpretation); «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» @@ -76,7 +76,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ typeInterpretation:PartialComplexTypeInterpretation) { find interpretation(problem,interpretation); - neg find hasElementInContainment(problem,interpretation); + neg find «hasElementInContainmentName»(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» -- cgit v1.2.3-54-g00ecf