diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend | 302 |
1 files changed, 302 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend new file mode 100644 index 00000000..400f47bc --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend | |||
@@ -0,0 +1,302 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.PropagationModality | ||
9 | import java.util.Map | ||
10 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
11 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | ||
12 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
13 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
14 | |||
15 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
16 | import java.util.LinkedList | ||
17 | import java.util.List | ||
18 | import org.eclipse.xtend.lib.annotations.Data | ||
19 | import java.util.HashMap | ||
20 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall | ||
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall | ||
22 | import java.util.Comparator | ||
23 | import java.util.ArrayList | ||
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction | ||
25 | import java.util.LinkedHashSet | ||
26 | |||
27 | @Data class UnitPropagation { | ||
28 | val PQuery q | ||
29 | val PConstraint c | ||
30 | val PropagationModality pm | ||
31 | val Modality m3 | ||
32 | } | ||
33 | @Data | ||
34 | class UnitPropagationPreconditionGenerationResult { | ||
35 | List<CharSequence> definitions= new LinkedList | ||
36 | Map<UnitPropagation,String> unitPropagation2PatternName = new HashMap | ||
37 | Map<PConstraint,String> constraintOccurence2Name = new HashMap | ||
38 | |||
39 | def registerQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3, String patternName, CharSequence definition) { | ||
40 | val key = new UnitPropagation(q,c,pm,m3) | ||
41 | definitions += definition | ||
42 | unitPropagation2PatternName.put(key,patternName) | ||
43 | } | ||
44 | def registerUnsatQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3) { | ||
45 | val key = new UnitPropagation(q,c,pm,m3) | ||
46 | unitPropagation2PatternName.put(key,null) | ||
47 | } | ||
48 | def contains(PQuery q, PConstraint c, PropagationModality pm, Modality m3) { | ||
49 | val key = new UnitPropagation(q,c,pm,m3) | ||
50 | return unitPropagation2PatternName.containsKey(key) | ||
51 | } | ||
52 | def getName(PQuery q, PConstraint c, PropagationModality pm, Modality m3) { | ||
53 | val key = new UnitPropagation(q,c,pm,m3) | ||
54 | return key.lookup(unitPropagation2PatternName) | ||
55 | } | ||
56 | def isDefined(PQuery q, PConstraint c, PropagationModality pm, Modality m3) { | ||
57 | val key = new UnitPropagation(q,c,pm,m3) | ||
58 | return unitPropagation2PatternName.get(key) !== null | ||
59 | } | ||
60 | } | ||
61 | @Data | ||
62 | class UnitPropagationPreconditionFinalResult { | ||
63 | CharSequence definitions | ||
64 | HashMap<PConstraint,String> constraint2MustPreconditionName | ||
65 | HashMap<PConstraint,String> constraint2CurrentPreconditionName | ||
66 | } | ||
67 | |||
68 | class UnitPropagationPreconditionGenerator { | ||
69 | val PatternGenerator base | ||
70 | val PConstraintTransformer constraintTransformer; | ||
71 | |||
72 | new(PatternGenerator patternGenerator) { | ||
73 | this.base = patternGenerator | ||
74 | this.constraintTransformer = new PConstraintTransformer(base.relationDefinitionIndexer) | ||
75 | } | ||
76 | |||
77 | def generateUnitPropagationRules( | ||
78 | LogicProblem problem, | ||
79 | Iterable<RelationDefinition> relations, | ||
80 | Map<String,PQuery> fqn2PQuery) | ||
81 | { | ||
82 | // Create an empty result | ||
83 | val res = new UnitPropagationPreconditionGenerationResult | ||
84 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] | ||
85 | val Map<PConstraint,List<Pair<String,Integer>>> mainMustPropagationNames = new HashMap | ||
86 | val Map<PConstraint,List<Pair<String,Integer>>> mainCurrentPropagationNames = new HashMap | ||
87 | for(wf : wfs) { | ||
88 | val query = wf.patternPQuery as PQuery | ||
89 | val relation = wf.target | ||
90 | val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) | ||
91 | |||
92 | for(referredCheck : allReferredChecks) { | ||
93 | val mustPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) | ||
94 | val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT) | ||
95 | if(!mainMustPropagationNames.containsKey(referredCheck)) { | ||
96 | mainMustPropagationNames.put(referredCheck,new LinkedList) | ||
97 | } | ||
98 | if(!mainCurrentPropagationNames.containsKey(referredCheck)) { | ||
99 | mainCurrentPropagationNames.put(referredCheck,new LinkedList) | ||
100 | } | ||
101 | if(mustPropagationPrecondition !== null) { | ||
102 | mainMustPropagationNames.get(referredCheck).add(mustPropagationPrecondition->query.parameterNames.size) | ||
103 | } | ||
104 | if(currentPropagationPrecondition !== null) { | ||
105 | mainCurrentPropagationNames.get(referredCheck).add(currentPropagationPrecondition->query.parameterNames.size) | ||
106 | } | ||
107 | } | ||
108 | } | ||
109 | val preconditions = new LinkedList | ||
110 | val constraint2MustPrecondition = new HashMap | ||
111 | val constraint2CurrentPrecondition = new HashMap | ||
112 | for(entry : mainMustPropagationNames.entrySet) { | ||
113 | val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; | ||
114 | val def = ''' | ||
115 | pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») | ||
116 | «FOR propagation : entry.value SEPARATOR " or "» | ||
117 | { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); } | ||
118 | «ENDFOR»''' | ||
119 | preconditions+=def | ||
120 | constraint2MustPrecondition.put(entry.key,name) | ||
121 | } | ||
122 | for(entry : mainCurrentPropagationNames.entrySet) { | ||
123 | val name = '''UPCurrentPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; | ||
124 | val def = ''' | ||
125 | pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») | ||
126 | «FOR propagation : entry.value SEPARATOR " or "» | ||
127 | { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); } | ||
128 | «ENDFOR»''' | ||
129 | preconditions+=def | ||
130 | constraint2CurrentPrecondition.put(entry.key,name) | ||
131 | } | ||
132 | |||
133 | val definitions = ''' | ||
134 | «FOR def : res.definitions» | ||
135 | «def» | ||
136 | «ENDFOR» | ||
137 | |||
138 | // Collected propagation preconditions: | ||
139 | |||
140 | «FOR predondition : preconditions» | ||
141 | «predondition» | ||
142 | «ENDFOR» | ||
143 | ''' | ||
144 | return new UnitPropagationPreconditionFinalResult(definitions,constraint2MustPrecondition,constraint2CurrentPrecondition) | ||
145 | } | ||
146 | def allReferredConstraints(Relation relation, PQuery query) { | ||
147 | val allReferredQueries = query.allReferredQueries | ||
148 | val problem = relation.eContainer as LogicProblem | ||
149 | val constraints = new LinkedHashSet | ||
150 | for(referredQuery: #[query]+allReferredQueries) { | ||
151 | val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target | ||
152 | val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies | ||
153 | constraints.addAll(bodies.map[getConstraints].flatten) | ||
154 | } | ||
155 | |||
156 | return constraints | ||
157 | } | ||
158 | |||
159 | def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { | ||
160 | if(res.contains(q,c,pm,m3)) { | ||
161 | return res.getName(q,c,pm,m3) | ||
162 | } else { | ||
163 | res.generatePropagationRule(relation,q,c,pm,m3) | ||
164 | return res.getName(q,c,pm,m3) | ||
165 | } | ||
166 | } | ||
167 | def getOrGenerateConstraintName(UnitPropagationPreconditionGenerationResult res, PConstraint c){ | ||
168 | if(res.constraintOccurence2Name.containsKey(c)) { | ||
169 | return res.constraintOccurence2Name.get(c) | ||
170 | } else { | ||
171 | val constraintName = '''Constraint«res.constraintOccurence2Name.size»''' | ||
172 | res.constraintOccurence2Name.put(c,constraintName) | ||
173 | return constraintName | ||
174 | } | ||
175 | } | ||
176 | |||
177 | def void generatePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { | ||
178 | val name = relationDefinitionName(res,relation,q,c,pm,m3) | ||
179 | val constraintArity = c.arity | ||
180 | val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies | ||
181 | val generatedBodies = new LinkedList | ||
182 | for(body : bodies) { | ||
183 | if(body.constraints.contains(c)) { | ||
184 | if(pm === PropagationModality::UP) { | ||
185 | generatedBodies += ''' | ||
186 | // Original Constraints | ||
187 | «FOR constraint : body.constraints.filter[it !== c]» | ||
188 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | ||
189 | «ENDFOR» | ||
190 | // Propagation for constraint | ||
191 | «this.constraintTransformer.transformConstraintUnset(c as ExpressionEvaluation,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | ||
192 | // Matching variables | ||
193 | «this.propagateVariables(c,pm)» | ||
194 | ''' | ||
195 | } | ||
196 | // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied | ||
197 | } else { | ||
198 | val positives = body.constraints.filter(PositivePatternCall) | ||
199 | for(positive: positives) { | ||
200 | val referredPQuery = positive.referredQuery | ||
201 | val referredRelation = (relation.eContainer as LogicProblem) | ||
202 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target | ||
203 | if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) { | ||
204 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3) | ||
205 | if(referredName !== null) { | ||
206 | generatedBodies += ''' | ||
207 | // Original Constraints | ||
208 | «FOR constraint : body.constraints.filter[it !== positive]» | ||
209 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | ||
210 | «ENDFOR» | ||
211 | // Propagation for constraint referred indirectly from this pattern through «referredName» | ||
212 | find «referredName»(problem, interpretation, | ||
213 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR», | ||
214 | «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); | ||
215 | ''' | ||
216 | } | ||
217 | // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either | ||
218 | } | ||
219 | } | ||
220 | |||
221 | val negatives = body.constraints.filter(NegativePatternCall) | ||
222 | for(negative : negatives) { | ||
223 | val referredPQuery = negative.referredQuery | ||
224 | val referredRelation = (relation.eContainer as LogicProblem) | ||
225 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target | ||
226 | if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) { | ||
227 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual) | ||
228 | if(referredName !== null) { | ||
229 | generatedBodies += ''' | ||
230 | // Original Constraints | ||
231 | «FOR constraint : body.constraints.filter[it !== negative]» | ||
232 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | ||
233 | «ENDFOR» | ||
234 | // Propagation for constraint referred indirectly from this pattern through «referredName» | ||
235 | find «referredName»(problem, interpretation, | ||
236 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR», | ||
237 | «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); | ||
238 | ''' | ||
239 | } else { | ||
240 | generatedBodies += ''' | ||
241 | // Original Constraints | ||
242 | «FOR constraint : body.constraints.filter[it !== negative]» | ||
243 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | ||
244 | «ENDFOR» | ||
245 | // Propagation for constraint referred indirectly from this pattern through «referredName», | ||
246 | // which was unsatisfiable | ||
247 | ''' | ||
248 | } | ||
249 | } | ||
250 | } | ||
251 | } | ||
252 | } | ||
253 | |||
254 | // Register the result | ||
255 | if(generatedBodies.empty) { | ||
256 | res.registerUnsatQuery(q,c,pm,m3) | ||
257 | } else { | ||
258 | val definition = ''' | ||
259 | private pattern «name»( | ||
260 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
261 | «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR», | ||
262 | «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR») | ||
263 | «FOR generatedBody: generatedBodies SEPARATOR " or "»{ | ||
264 | «generatedBody» | ||
265 | }«ENDFOR» | ||
266 | ''' | ||
267 | res.registerQuery(q,c,pm,m3,name,definition) | ||
268 | } | ||
269 | } | ||
270 | |||
271 | private def String relationDefinitionName(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) | ||
272 | '''«pm.name»«m3.name»Propagate«res.getOrGenerateConstraintName(c)»_«base.canonizeName(relation.name)»''' | ||
273 | |||
274 | def canonizeName(PVariable v) { | ||
275 | return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»''' | ||
276 | } | ||
277 | |||
278 | def canonizeName(int index, PropagationModality m) { | ||
279 | return '''«m.name.toLowerCase»_«index»''' | ||
280 | } | ||
281 | |||
282 | def dispatch propagateVariables(ExpressionEvaluation c, PropagationModality m) { | ||
283 | val comparator = new Comparator<PVariable>(){ | ||
284 | override compare(PVariable o1, PVariable o2) { | ||
285 | o1.name.compareTo(o2.name) | ||
286 | } | ||
287 | } | ||
288 | val variablesInOrder = new ArrayList(c.affectedVariables) | ||
289 | variablesInOrder.toList.sort(comparator) | ||
290 | return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»''' | ||
291 | } | ||
292 | def dispatch propagateVariables(PConstraint c, PropagationModality m) { | ||
293 | throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') | ||
294 | } | ||
295 | |||
296 | def dispatch arity(ExpressionEvaluation c) { | ||
297 | c.affectedVariables.size | ||
298 | } | ||
299 | def dispatch arity(PConstraint c) { | ||
300 | throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') | ||
301 | } | ||
302 | } \ No newline at end of file | ||