diff options
author | Oszkar Semerath <semerath@mit.bme.hu> | 2020-05-08 17:21:48 +0200 |
---|---|---|
committer | Oszkar Semerath <semerath@mit.bme.hu> | 2020-05-08 17:21:48 +0200 |
commit | 9d33b30f59574cb896e9f33bfb4b902d217d1c93 (patch) | |
tree | f782b5eb00790fcddaaaacf21414ae46db5bd4ed /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme | |
parent | Visualization fix for attributes with same value (diff) | |
download | VIATRA-Generator-9d33b30f59574cb896e9f33bfb4b902d217d1c93.tar.gz VIATRA-Generator-9d33b30f59574cb896e9f33bfb4b902d217d1c93.tar.zst VIATRA-Generator-9d33b30f59574cb896e9f33bfb4b902d217d1c93.zip |
Unit propagation trace fixes
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend | 109 |
1 files changed, 59 insertions, 50 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..b5e344f7 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 |
@@ -75,11 +76,11 @@ class UnitPropagationPreconditionGenerator { | |||
75 | // Create an empty result | 76 | // Create an empty result |
76 | val res = new UnitPropagationPreconditionGenerationResult | 77 | val res = new UnitPropagationPreconditionGenerationResult |
77 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] | 78 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] |
78 | val mainPropagationNames = new LinkedList | 79 | val mainPropagationNames = new LinkedHashSet |
79 | for(wf : wfs) { | 80 | for(wf : wfs) { |
80 | val query = wf.patternPQuery as PQuery | 81 | val query = wf.patternPQuery as PQuery |
81 | val relation = wf.target | 82 | val relation = wf.target |
82 | val allReferredChecks = query.allReferredConstraints.filter(ExpressionEvaluation) | 83 | val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) |
83 | 84 | ||
84 | for(referredCheck : allReferredChecks) { | 85 | for(referredCheck : allReferredChecks) { |
85 | mainPropagationNames+= getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) | 86 | mainPropagationNames+= getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) |
@@ -90,15 +91,20 @@ class UnitPropagationPreconditionGenerator { | |||
90 | «def» | 91 | «def» |
91 | «ENDFOR» | 92 | «ENDFOR» |
92 | 93 | ||
93 | // Main propagations: | 94 | // Main propagations: «FOR name : mainPropagationNames SEPARATOR ", "»«name»«ENDFOR» |
94 | «FOR name : mainPropagationNames» | ||
95 | «name» | ||
96 | «ENDFOR» | ||
97 | ''' | 95 | ''' |
98 | } | 96 | } |
99 | def allReferredConstraints(PQuery query) { | 97 | def allReferredConstraints(Relation relation, PQuery query) { |
100 | val allReferredQueries = query.allReferredQueries | 98 | val allReferredQueries = query.allReferredQueries |
101 | return (#[query]+allReferredQueries).map[it.disjunctBodies.bodies].flatten.map[constraints].flatten | 99 | val problem = relation.eContainer as LogicProblem |
100 | val constraints = new LinkedHashSet | ||
101 | for(referredQuery: #[query]+allReferredQueries) { | ||
102 | val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target | ||
103 | val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies | ||
104 | constraints.addAll(bodies.map[getConstraints].flatten) | ||
105 | } | ||
106 | |||
107 | return constraints | ||
102 | } | 108 | } |
103 | 109 | ||
104 | def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { | 110 | def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { |
@@ -141,60 +147,63 @@ class UnitPropagationPreconditionGenerator { | |||
141 | // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied | 147 | // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied |
142 | } else { | 148 | } else { |
143 | val positives = body.constraints.filter(PositivePatternCall) | 149 | val positives = body.constraints.filter(PositivePatternCall) |
144 | val positiveRefers = positives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] | 150 | for(positive: positives) { |
145 | for(positiveRefer: positiveRefers) { | 151 | val referredPQuery = positive.referredQuery |
146 | val referredPQuery = positiveRefer.referredQuery | ||
147 | val referredRelation = (relation.eContainer as LogicProblem) | 152 | val referredRelation = (relation.eContainer as LogicProblem) |
148 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target | 153 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target |
149 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3) | 154 | if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) { |
150 | if(referredName !== null) { | 155 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3) |
151 | generatedBodies += ''' | 156 | if(referredName !== null) { |
152 | // Original Constraints | 157 | generatedBodies += ''' |
153 | «FOR constraint : body.constraints.filter[it !== positiveRefer]» | 158 | // Original Constraints |
154 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | 159 | «FOR constraint : body.constraints.filter[it !== positive]» |
155 | «ENDFOR» | 160 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
156 | // Propagation for constraint referred indirectly from this pattern through «referredName» | 161 | «ENDFOR» |
157 | find «referredName»(problem, interpretation, | 162 | // Propagation for constraint referred indirectly from this pattern through «referredName» |
158 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positiveRefer.getVariableInTuple(index).canonizeName»«ENDFOR», | 163 | find «referredName»(problem, interpretation, |
159 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); | 164 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR», |
160 | ''' | 165 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); |
166 | ''' | ||
167 | } | ||
168 | // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either | ||
161 | } | 169 | } |
162 | // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either | ||
163 | } | 170 | } |
171 | |||
164 | val negatives = body.constraints.filter(NegativePatternCall) | 172 | val negatives = body.constraints.filter(NegativePatternCall) |
165 | val negativeRefers = negatives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] | 173 | for(negative : negatives) { |
166 | for(negativeRefer : negativeRefers) { | 174 | val referredPQuery = negative.referredQuery |
167 | val referredPQuery = negativeRefer.referredQuery | ||
168 | val referredRelation = (relation.eContainer as LogicProblem) | 175 | val referredRelation = (relation.eContainer as LogicProblem) |
169 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target | 176 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target |
170 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual) | 177 | if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) { |
171 | if(referredName !== null) { | 178 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual) |
172 | generatedBodies += ''' | 179 | if(referredName !== null) { |
173 | // Original Constraints | 180 | generatedBodies += ''' |
174 | «FOR constraint : body.constraints.filter[it !== negativeRefer]» | 181 | // Original Constraints |
175 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | 182 | «FOR constraint : body.constraints.filter[it !== negative]» |
176 | «ENDFOR» | 183 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
177 | // Propagation for constraint referred indirectly from this pattern through «referredName» | 184 | «ENDFOR» |
178 | find «referredName»(problem, interpretation, | 185 | // 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», | 186 | find «referredName»(problem, interpretation, |
180 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); | 187 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR», |
181 | ''' | 188 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); |
182 | } else { | 189 | ''' |
183 | generatedBodies += ''' | 190 | } else { |
184 | // Original Constraints | 191 | generatedBodies += ''' |
185 | «FOR constraint : body.constraints.filter[it !== negativeRefer]» | 192 | // Original Constraints |
186 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | 193 | «FOR constraint : body.constraints.filter[it !== negative]» |
187 | «ENDFOR» | 194 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
188 | // Propagation for constraint referred indirectly from this pattern through «referredName», | 195 | «ENDFOR» |
189 | // which was unsatisfiable | 196 | // Propagation for constraint referred indirectly from this pattern through «referredName», |
190 | ''' | 197 | // which was unsatisfiable |
198 | ''' | ||
199 | } | ||
191 | } | 200 | } |
192 | } | 201 | } |
193 | } | 202 | } |
194 | } | 203 | } |
195 | 204 | ||
196 | // Register the result | 205 | // Register the result |
197 | if(generatedBodies.size>=0) { | 206 | if(generatedBodies.empty) { |
198 | res.registerUnsatQuery(q,c,pm,m3) | 207 | res.registerUnsatQuery(q,c,pm,m3) |
199 | } else { | 208 | } else { |
200 | val definition = ''' | 209 | val definition = ''' |
@@ -229,7 +238,7 @@ class UnitPropagationPreconditionGenerator { | |||
229 | } | 238 | } |
230 | val variablesInOrder = new ArrayList(c.affectedVariables) | 239 | val variablesInOrder = new ArrayList(c.affectedVariables) |
231 | variablesInOrder.toList.sort(comparator) | 240 | variablesInOrder.toList.sort(comparator) |
232 | return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).name»==«canonizeName(variableIndex,m)»;«ENDFOR»''' | 241 | return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»''' |
233 | } | 242 | } |
234 | def dispatch propagateVariables(PConstraint c, PropagationModality m) { | 243 | def dispatch propagateVariables(PConstraint c, PropagationModality m) { |
235 | throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') | 244 | throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') |