From 4fe7fce97aedbd516109ef81afc33e00112b7b68 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 28 Aug 2020 18:58:37 +0200 Subject: Must unit propagation --- .../patterns/RelationRefinementGenerator.xtend | 137 +++++++++++++++------ 1 file changed, 101 insertions(+), 36 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend') 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 783cd36b..6f5f2402 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 @@ -1,10 +1,17 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns +import com.google.common.collect.ImmutableList +import com.google.common.collect.ImmutableMap +import com.google.common.collect.ImmutableSet import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import java.util.Collection import java.util.LinkedList +import java.util.Map +import java.util.Set +import org.eclipse.xtend2.lib.StringConcatenationClient class RelationRefinementGenerator { PatternGenerator base; @@ -13,53 +20,61 @@ class RelationRefinementGenerator { this.base = base } - 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»"); + def CharSequence generateRefineReference(LogicProblem p, + Collection unitPropagationPatternGenerators) { + val mustRelations = getMustRelations(unitPropagationPatternGenerators) + + ''' + «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)» + } + + «IF isMustPropagationQueryNeeded(relationRefinement.key, relationRefinement.value, mustRelations)» + pattern «mustPropagationQueryName(relationRefinement.key)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», + from: DefinedElement, to: DefinedElement) + «FOR body : getMustPropagationBodies(relationRefinement.key, relationRefinement.value, mustRelations) SEPARATOR " or "» + { + «referRefinementQuery(relationRefinement.key, relationRefinement.value, "relationIterpretation", "oppositeInterpretation", "from", "to")» + «body» + } + «ENDFOR» «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» - ''' + «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»''' } + def String mustPropagationQueryName(RelationDeclaration relation) { + '''mustPropagation_«base.canonizeName(relation.name)»''' + } + 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»);''' 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)] } @@ -83,4 +98,54 @@ class RelationRefinementGenerator { } return list } + + def getMustPropagationQueries(LogicProblem p, + Collection unitPropagationPatternGenerators) { + val refinements = getRelationRefinements(p) + val mustRelations = getMustRelations(unitPropagationPatternGenerators) + refinements.filter[isMustPropagationQueryNeeded(key, value, mustRelations)].toInvertedMap [ + mustPropagationQueryName(key) + ] + } + + private def getMustRelations(Collection unitPropagationPatternGenerators) { + ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustPatterns.entrySet].groupBy[key].mapValues [ + ImmutableSet.copyOf(map[value]) + ]) + } + + private def isMustPropagationQueryNeeded(Relation relation, Relation inverseRelation, + Map> mustRelations) { + val mustSet = mustRelations.get(relation) + if (mustSet !== null && !mustSet.empty) { + return true + } + if (inverseRelation !== null) { + val inverseMustSet = mustRelations.get(inverseRelation) + if (inverseMustSet !== null && !inverseMustSet.empty) { + return true + } + } + false + } + + private def getMustPropagationBodies(Relation relation, Relation inverseRelation, + Map> mustRelations) { + val builder = ImmutableList.builder() + val mustSet = mustRelations.get(relation) + if (mustSet !== null) { + for (refinementQuery : mustSet) { + builder.add('''find «refinementQuery»(problem, interpretation, from, to);''') + } + } + if (inverseRelation !== null && inverseRelation != relation) { + val inverseMustSet = mustRelations.get(inverseRelation) + if (inverseMustSet !== null) { + for (refinementQuery : inverseMustSet) { + builder.add('''find «refinementQuery»(problem, interpretation, to, from);''') + } + } + } + builder.build + } } -- cgit v1.2.3-70-g09d2