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 | 142 |
1 files changed, 90 insertions, 52 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 index f726a24f..d487db64 100644 --- 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 | |||
@@ -22,6 +22,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativeP | |||
22 | import java.util.Comparator | 22 | import java.util.Comparator |
23 | import java.util.ArrayList | 23 | import java.util.ArrayList |
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction | 24 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction |
25 | import java.util.LinkedHashSet | ||
25 | 26 | ||
26 | @Data class UnitPropagation { | 27 | @Data class UnitPropagation { |
27 | val PQuery q | 28 | val PQuery q |
@@ -57,6 +58,11 @@ class UnitPropagationPreconditionGenerationResult { | |||
57 | return unitPropagation2PatternName.get(key) !== null | 58 | return unitPropagation2PatternName.get(key) !== null |
58 | } | 59 | } |
59 | } | 60 | } |
61 | @Data | ||
62 | class UnitPropagationPreconditionFinalResult { | ||
63 | CharSequence definitions | ||
64 | HashMap<PConstraint,String> constraint2PreconditionName | ||
65 | } | ||
60 | 66 | ||
61 | class UnitPropagationPreconditionGenerator { | 67 | class UnitPropagationPreconditionGenerator { |
62 | val PatternGenerator base | 68 | val PatternGenerator base |
@@ -75,30 +81,59 @@ class UnitPropagationPreconditionGenerator { | |||
75 | // Create an empty result | 81 | // Create an empty result |
76 | val res = new UnitPropagationPreconditionGenerationResult | 82 | val res = new UnitPropagationPreconditionGenerationResult |
77 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] | 83 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] |
78 | val mainPropagationNames = new LinkedList | 84 | val Map<PConstraint,List<Pair<String,Integer>>> mainPropagationNames = new HashMap |
79 | for(wf : wfs) { | 85 | for(wf : wfs) { |
80 | val query = wf.patternPQuery as PQuery | 86 | val query = wf.patternPQuery as PQuery |
81 | val relation = wf.target | 87 | val relation = wf.target |
82 | val allReferredChecks = query.allReferredConstraints.filter(ExpressionEvaluation) | 88 | val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) |
83 | 89 | ||
84 | for(referredCheck : allReferredChecks) { | 90 | for(referredCheck : allReferredChecks) { |
85 | mainPropagationNames+= getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) | 91 | val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) |
92 | if(!mainPropagationNames.containsKey(referredCheck)) { | ||
93 | mainPropagationNames.put(referredCheck,new LinkedList) | ||
94 | } | ||
95 | if(propagationPrecondition !== null) { | ||
96 | mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size) | ||
97 | } | ||
86 | } | 98 | } |
87 | } | 99 | } |
88 | return ''' | 100 | val preconditions = new LinkedList |
101 | val constraint2Precondition = new HashMap | ||
102 | for(entry : mainPropagationNames.entrySet) { | ||
103 | val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; | ||
104 | val def = ''' | ||
105 | pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») | ||
106 | «FOR propagation : entry.value SEPARATOR " or "» | ||
107 | { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); } | ||
108 | «ENDFOR»''' | ||
109 | preconditions+=def | ||
110 | constraint2Precondition.put(entry.key,name) | ||
111 | } | ||
112 | |||
113 | val definitions = ''' | ||
89 | «FOR def : res.definitions» | 114 | «FOR def : res.definitions» |
90 | «def» | 115 | «def» |
91 | «ENDFOR» | 116 | «ENDFOR» |
92 | 117 | ||
93 | // Main propagations: | 118 | // Collected propagation preconditions: |
94 | «FOR name : mainPropagationNames» | 119 | |
95 | «name» | 120 | «FOR predondition : preconditions» |
121 | «predondition» | ||
96 | «ENDFOR» | 122 | «ENDFOR» |
97 | ''' | 123 | ''' |
124 | return new UnitPropagationPreconditionFinalResult(definitions,constraint2Precondition) | ||
98 | } | 125 | } |
99 | def allReferredConstraints(PQuery query) { | 126 | def allReferredConstraints(Relation relation, PQuery query) { |
100 | val allReferredQueries = query.allReferredQueries | 127 | val allReferredQueries = query.allReferredQueries |
101 | return (#[query]+allReferredQueries).map[it.disjunctBodies.bodies].flatten.map[constraints].flatten | 128 | val problem = relation.eContainer as LogicProblem |
129 | val constraints = new LinkedHashSet | ||
130 | for(referredQuery: #[query]+allReferredQueries) { | ||
131 | val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target | ||
132 | val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies | ||
133 | constraints.addAll(bodies.map[getConstraints].flatten) | ||
134 | } | ||
135 | |||
136 | return constraints | ||
102 | } | 137 | } |
103 | 138 | ||
104 | def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { | 139 | def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { |
@@ -141,64 +176,67 @@ class UnitPropagationPreconditionGenerator { | |||
141 | // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied | 176 | // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied |
142 | } else { | 177 | } else { |
143 | val positives = body.constraints.filter(PositivePatternCall) | 178 | val positives = body.constraints.filter(PositivePatternCall) |
144 | val positiveRefers = positives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] | 179 | for(positive: positives) { |
145 | for(positiveRefer: positiveRefers) { | 180 | val referredPQuery = positive.referredQuery |
146 | val referredPQuery = positiveRefer.referredQuery | ||
147 | val referredRelation = (relation.eContainer as LogicProblem) | 181 | val referredRelation = (relation.eContainer as LogicProblem) |
148 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target | 182 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target |
149 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3) | 183 | if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) { |
150 | if(referredName !== null) { | 184 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3) |
151 | generatedBodies += ''' | 185 | if(referredName !== null) { |
152 | // Original Constraints | 186 | generatedBodies += ''' |
153 | «FOR constraint : body.constraints.filter[it !== positiveRefer]» | 187 | // Original Constraints |
154 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | 188 | «FOR constraint : body.constraints.filter[it !== positive]» |
155 | «ENDFOR» | 189 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
156 | // Propagation for constraint referred indirectly from this pattern through «referredName» | 190 | «ENDFOR» |
157 | find «referredName»(problem, interpretation, | 191 | // Propagation for constraint referred indirectly from this pattern through «referredName» |
158 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positiveRefer.getVariableInTuple(index).canonizeName»«ENDFOR», | 192 | find «referredName»(problem, interpretation, |
159 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); | 193 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR», |
160 | ''' | 194 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); |
195 | ''' | ||
196 | } | ||
197 | // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either | ||
161 | } | 198 | } |
162 | // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either | ||
163 | } | 199 | } |
200 | |||
164 | val negatives = body.constraints.filter(NegativePatternCall) | 201 | val negatives = body.constraints.filter(NegativePatternCall) |
165 | val negativeRefers = negatives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] | 202 | for(negative : negatives) { |
166 | for(negativeRefer : negativeRefers) { | 203 | val referredPQuery = negative.referredQuery |
167 | val referredPQuery = negativeRefer.referredQuery | ||
168 | val referredRelation = (relation.eContainer as LogicProblem) | 204 | val referredRelation = (relation.eContainer as LogicProblem) |
169 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target | 205 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target |
170 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual) | 206 | if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) { |
171 | if(referredName !== null) { | 207 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual) |
172 | generatedBodies += ''' | 208 | if(referredName !== null) { |
173 | // Original Constraints | 209 | generatedBodies += ''' |
174 | «FOR constraint : body.constraints.filter[it !== negativeRefer]» | 210 | // Original Constraints |
175 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | 211 | «FOR constraint : body.constraints.filter[it !== negative]» |
176 | «ENDFOR» | 212 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
177 | // Propagation for constraint referred indirectly from this pattern through «referredName» | 213 | «ENDFOR» |
178 | find «referredName»(problem, interpretation, | 214 | // Propagation for constraint referred indirectly from this pattern through «referredName» |
179 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negativeRefer.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR», | 215 | find «referredName»(problem, interpretation, |
180 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); | 216 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR», |
181 | ''' | 217 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); |
182 | } else { | 218 | ''' |
183 | generatedBodies += ''' | 219 | } else { |
184 | // Original Constraints | 220 | generatedBodies += ''' |
185 | «FOR constraint : body.constraints.filter[it !== negativeRefer]» | 221 | // Original Constraints |
186 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | 222 | «FOR constraint : body.constraints.filter[it !== negative]» |
187 | «ENDFOR» | 223 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
188 | // Propagation for constraint referred indirectly from this pattern through «referredName», | 224 | «ENDFOR» |
189 | // which was unsatisfiable | 225 | // Propagation for constraint referred indirectly from this pattern through «referredName», |
190 | ''' | 226 | // which was unsatisfiable |
227 | ''' | ||
228 | } | ||
191 | } | 229 | } |
192 | } | 230 | } |
193 | } | 231 | } |
194 | } | 232 | } |
195 | 233 | ||
196 | // Register the result | 234 | // Register the result |
197 | if(generatedBodies.size>=0) { | 235 | if(generatedBodies.empty) { |
198 | res.registerUnsatQuery(q,c,pm,m3) | 236 | res.registerUnsatQuery(q,c,pm,m3) |
199 | } else { | 237 | } else { |
200 | val definition = ''' | 238 | val definition = ''' |
201 | pattern «name»( | 239 | private pattern «name»( |
202 | problem:LogicProblem, interpretation:PartialInterpretation, | 240 | problem:LogicProblem, interpretation:PartialInterpretation, |
203 | «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR», | 241 | «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR», |
204 | «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR») | 242 | «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR») |
@@ -229,7 +267,7 @@ class UnitPropagationPreconditionGenerator { | |||
229 | } | 267 | } |
230 | val variablesInOrder = new ArrayList(c.affectedVariables) | 268 | val variablesInOrder = new ArrayList(c.affectedVariables) |
231 | variablesInOrder.toList.sort(comparator) | 269 | variablesInOrder.toList.sort(comparator) |
232 | return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).name»==«canonizeName(variableIndex,m)»;«ENDFOR»''' | 270 | return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»''' |
233 | } | 271 | } |
234 | def dispatch propagateVariables(PConstraint c, PropagationModality m) { | 272 | def dispatch propagateVariables(PConstraint c, PropagationModality m) { |
235 | throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') | 273 | throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') |