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 --- .../logic2viatra/patterns/PatternGenerator.xtend | 150 +++++++------- .../logic2viatra/patterns/PatternProvider.xtend | 115 ++++++----- .../patterns/RelationRefinementGenerator.xtend | 102 +++++----- .../patterns/TypeRefinementGenerator.xtend | 4 +- .../logic2viatra/patterns/UnfinishedIndexer.xtend | 222 +++++++++++++++------ 5 files changed, 355 insertions(+), 238 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns') 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 + ) + ] } } -- cgit v1.2.3-70-g09d2