1 files changed, 101 insertions, 36 deletions
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) '''
+        def CharSequence generateRefineReference(LogicProblem p,
-                «FOR relationRefinement : this.getRelationRefinements(p)»
+                Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {
-                        pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»(
+                val mustRelations = getMustRelations(unitPropagationPatternGenerators)
-                                problem:LogicProblem, interpretation:PartialInterpretation,
-                                relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF»,
+                '''
-                                from: DefinedElement, to: DefinedElement)
+                        «FOR relationRefinement : this.getRelationRefinements(p)»
-                        {
+                                pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»(
-                                find interpretation(problem,interpretation);
+                                        problem:LogicProblem, interpretation:PartialInterpretation,
-                                PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
+                                        relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF»,
-                                PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»");
+                                        from: DefinedElement, to: DefinedElement)
-                                «IF relationRefinement.value !== null»
+                                {
-                                        PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);
+                                        find interpretation(problem,interpretation);
-                                        PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»");
+                                        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);
+                        «ENDFOR»
-                                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»'''
        }
+        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<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {
+                val refinements = getRelationRefinements(p)
+                val mustRelations = getMustRelations(unitPropagationPatternGenerators)
+                refinements.filter[isMustPropagationQueryNeeded(key, value, mustRelations)].toInvertedMap [
+                        mustPropagationQueryName(key)
+                ]
+        }
+        private def getMustRelations(Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {
+                ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustPatterns.entrySet].groupBy[key].mapValues [
+                        ImmutableSet.copyOf(map[value])
+                ])
+        }
+        private def isMustPropagationQueryNeeded(Relation relation, Relation inverseRelation,
+                Map<Relation, ? extends Set<String>> 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<Relation, ? extends Set<String>> mustRelations) {
+                val builder = ImmutableList.<StringConcatenationClient>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
+        }
 }

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 @@
1	package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns	1	package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2		2
		3	import com.google.common.collect.ImmutableList
		4	import com.google.common.collect.ImmutableMap
		5	import com.google.common.collect.ImmutableSet
3	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation	6	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
4	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration	7	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
5	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem	8	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
6	import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality	9	import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
		10	import java.util.Collection
7	import java.util.LinkedList	11	import java.util.LinkedList
		12	import java.util.Map
		13	import java.util.Set
		14	import org.eclipse.xtend2.lib.StringConcatenationClient
8		15
9	class RelationRefinementGenerator {	16	class RelationRefinementGenerator {
10	PatternGenerator base;	17	PatternGenerator base;
@@ -13,53 +20,61 @@ class RelationRefinementGenerator {
13	this.base = base	20	this.base = base
14	}	21	}
15		22
16	def CharSequence generateRefineReference(LogicProblem p) '''	23	def CharSequence generateRefineReference(LogicProblem p,
17	«FOR relationRefinement : this.getRelationRefinements(p)»	24	Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {
18	pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»(	25	val mustRelations = getMustRelations(unitPropagationPatternGenerators)
19	problem:LogicProblem, interpretation:PartialInterpretation,	26
20	relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF»,	27	'''
21	from: DefinedElement, to: DefinedElement)	28	«FOR relationRefinement : this.getRelationRefinements(p)»
22	{	29	pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»(
23	find interpretation(problem,interpretation);	30	problem:LogicProblem, interpretation:PartialInterpretation,
24	PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);	31	relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF»,
25	PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»");	32	from: DefinedElement, to: DefinedElement)
26	«IF relationRefinement.value !== null»	33	{
27	PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);	34	find interpretation(problem,interpretation);
28	PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»");	35	PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
		36	PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»");
		37	«IF relationRefinement.value !== null»
		38	PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);
		39	PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»");
		40	«ENDIF»
		41	find mustExist(problem, interpretation, from);
		42	find mustExist(problem, interpretation, to);
		43	«base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")»
		44	«base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")»
		45	«base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)»
		46	neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)»
		47	}
		48
		49	«IF isMustPropagationQueryNeeded(relationRefinement.key, relationRefinement.value, mustRelations)»
		50	pattern «mustPropagationQueryName(relationRefinement.key)»(
		51	problem:LogicProblem, interpretation:PartialInterpretation,
		52	relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF»,
		53	from: DefinedElement, to: DefinedElement)
		54	«FOR body : getMustPropagationBodies(relationRefinement.key, relationRefinement.value, mustRelations) SEPARATOR " or "»
		55	{
		56	«referRefinementQuery(relationRefinement.key, relationRefinement.value, "relationIterpretation", "oppositeInterpretation", "from", "to")»
		57	«body»
		58	}
		59	«ENDFOR»
29	«ENDIF»	60	«ENDIF»
30	find mustExist(problem, interpretation, from);	61	«ENDFOR»
31	find mustExist(problem, interpretation, to);	62	'''
32	«base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")»	63	}
33	«base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")»
34	«base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)»
35	neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)»
36	}
37	«ENDFOR»
38	'''
39		64
40	def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) {	65	def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) {
41	'''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»'''	66	'''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»'''
42	}	67	}
43		68
		69	def String mustPropagationQueryName(RelationDeclaration relation) {
		70	'''mustPropagation_«base.canonizeName(relation.name)»'''
		71	}
		72
44	def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName,	73	def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName,
45	String inverseInterpretationName, String sourceName,	74	String inverseInterpretationName, String sourceName,
46	String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);'''	75	String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);'''
47		76
48	def getRefineRelationQueries(LogicProblem p) {	77	def getRefineRelationQueries(LogicProblem p) {
49	// val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet
50	// p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»''']
51	/*
52	* val res = new LinkedHashMap
53	* for(relation: getRelationRefinements(p)) {
54	* if(inverseRelations.containsKey(relation)) {
55	* val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»'''
56	* res.put(relation -> inverseRelations.get(relation),name)
57	* } else {
58	* val name = '''refineRelation_«base.canonizeName(relation.name)»'''
59	* res.put(relation -> null,name)
60	* }
61	* }
62	return res*/
63	getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)]	78	getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)]
64	}	79	}
65		80
@@ -83,4 +98,54 @@ class RelationRefinementGenerator {
83	}	98	}
84	return list	99	return list
85	}	100	}
		101
		102	def getMustPropagationQueries(LogicProblem p,
		103	Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {
		104	val refinements = getRelationRefinements(p)
		105	val mustRelations = getMustRelations(unitPropagationPatternGenerators)
		106	refinements.filter[isMustPropagationQueryNeeded(key, value, mustRelations)].toInvertedMap [
		107	mustPropagationQueryName(key)
		108	]
		109	}
		110
		111	private def getMustRelations(Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) {
		112	ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustPatterns.entrySet].groupBy[key].mapValues [
		113	ImmutableSet.copyOf(map[value])
		114	])
		115	}
		116
		117	private def isMustPropagationQueryNeeded(Relation relation, Relation inverseRelation,
		118	Map<Relation, ? extends Set<String>> mustRelations) {
		119	val mustSet = mustRelations.get(relation)
		120	if (mustSet !== null && !mustSet.empty) {
		121	return true
		122	}
		123	if (inverseRelation !== null) {
		124	val inverseMustSet = mustRelations.get(inverseRelation)
		125	if (inverseMustSet !== null && !inverseMustSet.empty) {
		126	return true
		127	}
		128	}
		129	false
		130	}
		131
		132	private def getMustPropagationBodies(Relation relation, Relation inverseRelation,
		133	Map<Relation, ? extends Set<String>> mustRelations) {
		134	val builder = ImmutableList.<StringConcatenationClient>builder()
		135	val mustSet = mustRelations.get(relation)
		136	if (mustSet !== null) {
		137	for (refinementQuery : mustSet) {
		138	builder.add('''find «refinementQuery»(problem, interpretation, from, to);''')
		139	}
		140	}
		141	if (inverseRelation !== null && inverseRelation != relation) {
		142	val inverseMustSet = mustRelations.get(inverseRelation)
		143	if (inverseMustSet !== null) {
		144	for (refinementQuery : inverseMustSet) {
		145	builder.add('''find «refinementQuery»(problem, interpretation, to, from);''')
		146	}
		147	}
		148	}
		149	builder.build
		150	}
86	}	151	}