diff options
author | 20001LastOrder <boqi.chen@mail.mcgill.ca> | 2020-11-04 01:33:58 -0500 |
---|---|---|
committer | 20001LastOrder <boqi.chen@mail.mcgill.ca> | 2020-11-04 01:33:58 -0500 |
commit | a20af4d0dbf5eab84ee271d426528aabb5a8ac3b (patch) | |
tree | a9ab772ee313125aaf3a941d66e131b408d949ba /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend | |
parent | changes in settings of measurements (diff) | |
parent | merge with current master, comment numerical solver related logging (diff) | |
download | VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.tar.gz VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.tar.zst VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.zip |
fix merging issue
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend | 174 |
1 files changed, 116 insertions, 58 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 f9e9baea..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,85 +1,93 @@ | |||
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 |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | 12 | import java.util.Map |
13 | import java.util.Set | ||
14 | import org.eclipse.xtend2.lib.StringConcatenationClient | ||
9 | 15 | ||
10 | class RelationRefinementGenerator { | 16 | class RelationRefinementGenerator { |
11 | PatternGenerator base; | 17 | PatternGenerator base; |
12 | public new(PatternGenerator base) { | 18 | |
19 | new(PatternGenerator base) { | ||
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 | return ''' | 24 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) { |
18 | «FOR relationRefinement: this.getRelationRefinements(p)» | 25 | val mustRelations = getMustRelations(unitPropagationPatternGenerators) |
19 | pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( | 26 | |
20 | problem:LogicProblem, interpretation:PartialInterpretation, | 27 | ''' |
21 | relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value != null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», | 28 | «FOR relationRefinement : this.getRelationRefinements(p)» |
22 | from: DefinedElement, to: DefinedElement) | 29 | pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( |
23 | { | 30 | problem:LogicProblem, interpretation:PartialInterpretation, |
24 | find interpretation(problem,interpretation); | 31 | relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», |
25 | PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); | 32 | from: DefinedElement, to: DefinedElement) |
26 | PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); | 33 | { |
27 | «IF relationRefinement.value != null» | 34 | find interpretation(problem,interpretation); |
28 | PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); | 35 | PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); |
29 | PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); | 36 | PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); |
30 | «ENDIF» | 37 | «IF relationRefinement.value !== null» |
31 | find mustExist(problem, interpretation, from); | 38 | PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); |
32 | find mustExist(problem, interpretation, to); | 39 | PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); |
33 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» | 40 | «ENDIF» |
34 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» | 41 | find mustExist(problem, interpretation, from); |
35 | «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» | 42 | find mustExist(problem, interpretation, to); |
36 | neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» | 43 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» |
37 | } | 44 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» |
38 | «ENDFOR» | 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» | ||
60 | «ENDIF» | ||
61 | «ENDFOR» | ||
39 | ''' | 62 | ''' |
40 | } | 63 | } |
41 | 64 | ||
42 | def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { | 65 | def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { |
43 | '''«IF inverseRelation != null | 66 | '''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' |
44 | »refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»« | ||
45 | ELSE | ||
46 | »refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' | ||
47 | } | 67 | } |
48 | 68 | ||
69 | def String mustPropagationQueryName(RelationDeclaration relation) { | ||
70 | '''mustPropagation_«base.canonizeName(relation.name)»''' | ||
71 | } | ||
72 | |||
49 | def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, | 73 | def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, |
50 | String inverseInterpretationName, String sourceName, String targetName) | 74 | String inverseInterpretationName, String sourceName, |
51 | '''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»);''' |
52 | 76 | ||
53 | def getRefineRelationQueries(LogicProblem p) { | 77 | def getRefineRelationQueries(LogicProblem p) { |
54 | // val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet | 78 | getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)] |
55 | // p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»'''] | ||
56 | /* | ||
57 | val res = new LinkedHashMap | ||
58 | for(relation: getRelationRefinements(p)) { | ||
59 | if(inverseRelations.containsKey(relation)) { | ||
60 | val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»''' | ||
61 | res.put(relation -> inverseRelations.get(relation),name) | ||
62 | } else { | ||
63 | val name = '''refineRelation_«base.canonizeName(relation.name)»''' | ||
64 | res.put(relation -> null,name) | ||
65 | } | ||
66 | } | ||
67 | return res*/ | ||
68 | |||
69 | getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key,it.value)] | ||
70 | } | 79 | } |
71 | |||
72 | 80 | ||
73 | def getRelationRefinements(LogicProblem p) { | 81 | def getRelationRefinements(LogicProblem p) { |
74 | val inverses = base.getInverseRelations(p) | 82 | val inverses = base.getInverseRelations(p) |
75 | val containments = base.getContainments(p) | 83 | val containments = base.getContainments(p) |
76 | val list = new LinkedList | 84 | val list = new LinkedList |
77 | for(relation : p.relations.filter(RelationDeclaration)) { | 85 | for (relation : p.relations.filter(RelationDeclaration)) { |
78 | if(!containments.contains(relation)) { | 86 | if (!containments.contains(relation)) { |
79 | if(inverses.containsKey(relation)) { | 87 | if (inverses.containsKey(relation)) { |
80 | val inverse = inverses.get(relation) | 88 | val inverse = inverses.get(relation) |
81 | if(!containments.contains(inverse)) { | 89 | if (!containments.contains(inverse)) { |
82 | if(base.isRepresentative(relation,inverse)) { | 90 | if (base.isRepresentative(relation, inverse)) { |
83 | list += (relation -> inverse) | 91 | list += (relation -> inverse) |
84 | } | 92 | } |
85 | } | 93 | } |
@@ -90,4 +98,54 @@ class RelationRefinementGenerator { | |||
90 | } | 98 | } |
91 | return list | 99 | return list |
92 | } | 100 | } |
93 | } \ No newline at end of file | 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 | } | ||
151 | } | ||