diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns')
2 files changed, 71 insertions, 129 deletions
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 ac4a0855..2f7c9e2d 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 | |||
@@ -53,10 +53,8 @@ class ModalPatternQueries { | |||
53 | 53 | ||
54 | @Data | 54 | @Data |
55 | class UnifinishedMultiplicityQueries { | 55 | class UnifinishedMultiplicityQueries { |
56 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unfinishedMultiplicityQuery | 56 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingMultiplicityQuery |
57 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unrepairableMultiplicityQuery | 57 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingInverseMultiplicityQuery |
58 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingInverseMultiplicityQuery | ||
59 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingContentsQuery | ||
60 | } | 58 | } |
61 | 59 | ||
62 | class PatternProvider { | 60 | class PatternProvider { |
@@ -108,9 +106,8 @@ class PatternProvider { | |||
108 | 106 | ||
109 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints) | 107 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints) |
110 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ | 108 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ |
111 | new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries), | 109 | new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries), |
112 | unrepairableMultiplicityQueryName?.lookup(queries), | 110 | existingInverseMultiplicityQueryName?.lookup(queries)) |
113 | remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries)) | ||
114 | ] | 111 | ] |
115 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( | 112 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( |
116 | queries) | 113 | queries) |
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 a8a07756..65ad3d48 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 | |||
@@ -14,10 +14,8 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
14 | 14 | ||
15 | @Data | 15 | @Data |
16 | class UnifinishedMultiplicityQueryNames { | 16 | class UnifinishedMultiplicityQueryNames { |
17 | val String unfinishedMultiplicityQueryName | 17 | val String existingMultiplicityQueryName |
18 | val String unrepairableMultiplicityQueryName | 18 | val String existingInverseMultiplicityQueryName |
19 | val String remainingInverseMultiplicityQueryName | ||
20 | val String remainingContentsQueryName | ||
21 | } | 19 | } |
22 | 20 | ||
23 | class UnfinishedIndexer { | 21 | class UnfinishedIndexer { |
@@ -58,147 +56,94 @@ class UnfinishedIndexer { | |||
58 | def generateUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints, | 56 | def generateUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints, |
59 | Map<String, PQuery> fqn2PQuery) ''' | 57 | Map<String, PQuery> fqn2PQuery) ''' |
60 | «FOR constraint : constraints» | 58 | «FOR constraint : constraints» |
61 | «IF constraint.constrainsUnfinished» | 59 | «IF constraint.shouldIndexExistingMultiplicites(indexUpperMultiplicities)» |
62 | private pattern «unfinishedMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, missingMultiplicity:java Integer) { | 60 | private pattern «existingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, numberOfExistingReferences:java Integer«IF constraint.shouldIndexRepairMultiplcities(indexUpperMultiplicities)», numberOfRepairMatches: java Integer«ENDIF») { |
63 | find interpretation(problem,interpretation); | 61 | find interpretation(problem,interpretation); |
64 | find mustExist(problem,interpretation,object); | 62 | find mustExist(problem,interpretation,object); |
65 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | 63 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» |
66 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» | 64 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» |
67 | check(numberOfExistingReferences < «constraint.lowerBound»); | 65 | «IF constraint.shouldIndexRepairMultiplcities(indexUpperMultiplicities)» |
68 | missingMultiplicity == eval(«constraint.lowerBound»-numberOfExistingReferences); | 66 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); |
69 | } | 67 | «ENDIF» |
70 | |||
71 | pattern «unfinishedMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, missingMultiplicity:java Integer) { | ||
72 | find interpretation(problem,interpretation); | ||
73 | missingMultiplicity == sum find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); | ||
74 | } | 68 | } |
75 | «ENDIF» | 69 | «ENDIF» |
76 | 70 | ||
77 | «IF indexUpperMultiplicities» | 71 | «IF constraint.shouldIndexRepairMatches(indexUpperMultiplicities)» |
78 | «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse» | 72 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { |
79 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { | 73 | «IF constraint.containment || constraint.container» |
80 | «IF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration» | 74 | «repairMatchFallback(constraint, fqn2PQuery)» |
81 | «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")» | 75 | «ELSEIF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration» |
82 | «ELSE» | 76 | «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")» |
83 | «IF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration» | 77 | «ELSEIF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration» |
84 | «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")» | 78 | «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")» |
85 | «ELSE» | ||
86 | find interpretation(problem,interpretation); | ||
87 | find mustExist(problem,interpretation,source); | ||
88 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» | ||
89 | find mustExist(problem,interpretation,target); | ||
90 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» | ||
91 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» | ||
92 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» | ||
93 | «ENDIF» | ||
94 | «ENDIF» | ||
95 | } | ||
96 | «ENDIF» | ||
97 | |||
98 | «IF constraint.constrainsUnrepairable» | ||
99 | private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { | ||
100 | find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); | ||
101 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); | ||
102 | check(numberOfRepairMatches < missingMultiplicity); | ||
103 | unrepairableMultiplicity == eval(missingMultiplicity-numberOfRepairMatches); | ||
104 | } | ||
105 | |||
106 | private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) { | ||
107 | find interpretation(problem,interpretation); | ||
108 | unrepairableMultiplicity == max find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); | ||
109 | } or { | ||
110 | find interpretation(problem,interpretation); | ||
111 | neg find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, _); | ||
112 | unrepairableMultiplicity == 0; | ||
113 | } | ||
114 | «ENDIF» | ||
115 | |||
116 | «IF constraint.constrainsRemainingInverse» | ||
117 | private pattern «remainingMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) { | ||
118 | find interpretation(problem,interpretation); | ||
119 | find mustExist(problem,interpretation,object); | ||
120 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» | ||
121 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» | ||
122 | check(numberOfExistingReferences < «constraint.inverseUpperBound»); | ||
123 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object); | ||
124 | remainingMultiplicity == eval(Math.min(«constraint.inverseUpperBound»-numberOfExistingReferences, numberOfRepairMatches)); | ||
125 | } | ||
126 | |||
127 | pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | ||
128 | find interpretation(problem,interpretation); | ||
129 | remainingMultiplicity == sum find «remainingMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); | ||
130 | } | ||
131 | «ENDIF» | ||
132 | |||
133 | «IF constraint.constrainsRemainingContents» | ||
134 | «IF constraint.upperBoundFinite» | ||
135 | private pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) { | ||
136 | find interpretation(problem,interpretation); | ||
137 | find mustExist(problem,interpretation,object); | ||
138 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | ||
139 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» | ||
140 | check(numberOfExistingReferences < «constraint.upperBound»); | ||
141 | remainingMultiplicity == eval(«constraint.upperBound»-numberOfExistingReferences); | ||
142 | } | ||
143 | |||
144 | pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | ||
145 | find interpretation(problem,interpretation); | ||
146 | remainingMultiplicity == sum find «remainingContentsName(constraint)»_helper(problem, interpretation, _, #_); | ||
147 | } | ||
148 | «ELSE» | 79 | «ELSE» |
149 | pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation) { | 80 | «repairMatchFallback(constraint, fqn2PQuery)» |
150 | find interpretation(problem,interpretation); | ||
151 | find mustExist(problem,interpretation,object); | ||
152 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | ||
153 | } | ||
154 | |||
155 | pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | ||
156 | find interpretation(problem,interpretation); | ||
157 | find «remainingContentsName(constraint)»_helper(problem, interpretation); | ||
158 | remainingMultiplicity == -1; | ||
159 | } or { | ||
160 | find interpretation(problem,interpretation); | ||
161 | neg find «remainingContentsName(constraint)»_helper(problem, interpretation); | ||
162 | remainingMultiplicity == 0; | ||
163 | } | ||
164 | «ENDIF» | 81 | «ENDIF» |
165 | «ENDIF» | 82 | } |
83 | «ENDIF» | ||
84 | |||
85 | «IF constraint.shouldIndexInverseMultiplicites(indexUpperMultiplicities)» | ||
86 | private pattern «existingInverseMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, numberOfExistingReferences:java Integer, numberOfRepairMatches: java Integer) { | ||
87 | find interpretation(problem,interpretation); | ||
88 | find mustExist(problem,interpretation,object); | ||
89 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» | ||
90 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» | ||
91 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object); | ||
92 | } | ||
166 | «ENDIF» | 93 | «ENDIF» |
167 | «ENDFOR» | 94 | «ENDFOR» |
168 | ''' | 95 | ''' |
169 | 96 | ||
170 | def String unfinishedMultiplicityName( | 97 | private def repairMatchFallback(RelationMultiplicityConstraint constraint, Map<String, PQuery> fqn2PQuery) ''' |
171 | RelationMultiplicityConstraint constraint) '''unfinishedLowerMultiplicity_«base.canonizeName(constraint.relation.name)»''' | 98 | find interpretation(problem,interpretation); |
99 | find mustExist(problem,interpretation,source); | ||
100 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» | ||
101 | find mustExist(problem,interpretation,target); | ||
102 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» | ||
103 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» | ||
104 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» | ||
105 | ''' | ||
106 | |||
107 | def String existingMultiplicityName( | ||
108 | RelationMultiplicityConstraint constraint) '''existingMultiplicity_«base.canonizeName(constraint.relation.name)»''' | ||
172 | 109 | ||
173 | def String unrepairableMultiplicityName( | 110 | def String existingInverseMultiplicityName( |
174 | RelationMultiplicityConstraint constraint) '''unrepairableLowerMultiplicity_«base.canonizeName(constraint.relation.name)»''' | 111 | RelationMultiplicityConstraint constraint) '''existingInverseMultiplicity_«base.canonizeName(constraint.relation.name)»''' |
175 | 112 | ||
176 | private def String repairMatchName( | 113 | private def String repairMatchName( |
177 | RelationMultiplicityConstraint constraint) '''repair_«base.canonizeName(constraint.relation.name)»''' | 114 | RelationMultiplicityConstraint constraint) '''repair_«base.canonizeName(constraint.relation.name)»''' |
178 | 115 | ||
179 | def String remainingMultiplicityName( | ||
180 | RelationMultiplicityConstraint constraint) '''remainingInverseUpperMultiplicity_«base.canonizeName(constraint.relation.name)»''' | ||
181 | |||
182 | def String remainingContentsName( | ||
183 | RelationMultiplicityConstraint constraint) '''remainingContents_«base.canonizeName(constraint.relation.name)»''' | ||
184 | |||
185 | def getUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints) { | 116 | def getUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints) { |
186 | constraints.toInvertedMap [ constraint | | 117 | constraints.toInvertedMap [ constraint | |
187 | new UnifinishedMultiplicityQueryNames( | 118 | new UnifinishedMultiplicityQueryNames( |
188 | if(constraint.constrainsUnfinished) unfinishedMultiplicityName(constraint) else null, | 119 | if (constraint.shouldIndexExistingMultiplicites(indexUpperMultiplicities)) { |
189 | if (indexUpperMultiplicities && constraint.constrainsUnrepairable) | 120 | existingMultiplicityName(constraint) |
190 | unrepairableMultiplicityName(constraint) | 121 | } else { |
191 | else | 122 | null |
192 | null, | 123 | }, |
193 | if (indexUpperMultiplicities && constraint.constrainsRemainingInverse) | 124 | if (constraint.shouldIndexInverseMultiplicites(indexUpperMultiplicities)) { |
194 | remainingMultiplicityName(constraint) | 125 | existingInverseMultiplicityName(constraint) |
195 | else | 126 | } else { |
196 | null, | ||
197 | if (indexUpperMultiplicities && constraint.constrainsRemainingContents) | ||
198 | remainingContentsName(constraint) | ||
199 | else | ||
200 | null | 127 | null |
128 | } | ||
201 | ) | 129 | ) |
202 | ] | 130 | ] |
203 | } | 131 | } |
132 | |||
133 | static def shouldIndexExistingMultiplicites(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { | ||
134 | constrainsUnfinished || (indexUpperMultiplicities && constrainsRemainingContents) | ||
135 | } | ||
136 | |||
137 | static def shouldIndexRepairMultiplcities(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { | ||
138 | shouldIndexExistingMultiplicites(indexUpperMultiplicities) && constrainsUnrepairable | ||
139 | } | ||
140 | |||
141 | static def shouldIndexInverseMultiplicites(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { | ||
142 | indexUpperMultiplicities && constrainsRemainingInverse | ||
143 | } | ||
144 | |||
145 | static def shouldIndexRepairMatches(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { | ||
146 | shouldIndexRepairMultiplcities(indexUpperMultiplicities) || | ||
147 | shouldIndexInverseMultiplicites(indexUpperMultiplicities) | ||
148 | } | ||
204 | } | 149 | } |