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 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.PropagationModality
+import java.util.Map
+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
+import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import java.util.LinkedList
+import java.util.List
+import org.eclipse.xtend.lib.annotations.Data
+import java.util.HashMap
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
+import java.util.Comparator
+import java.util.ArrayList
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
+import java.util.LinkedHashSet
+@Data class UnitPropagation {
+        val PQuery q
+        val PConstraint c
+        val PropagationModality pm
+        val Modality m3
+}
+@Data
+class UnitPropagationPreconditionGenerationResult {
+        List<CharSequence> definitions= new LinkedList
+        Map<UnitPropagation,String> unitPropagation2PatternName = new HashMap
+        Map<PConstraint,String> constraintOccurence2Name = new HashMap
+        
+        def registerQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3, String patternName, CharSequence definition) {
+                val key = new UnitPropagation(q,c,pm,m3)
+                definitions += definition
+                unitPropagation2PatternName.put(key,patternName)
+        }
+        def registerUnsatQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                val key = new UnitPropagation(q,c,pm,m3)
+                unitPropagation2PatternName.put(key,null)
+        }
+        def contains(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                val key = new UnitPropagation(q,c,pm,m3)
+                return unitPropagation2PatternName.containsKey(key)
+        }
+        def getName(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                val key = new UnitPropagation(q,c,pm,m3)
+                return key.lookup(unitPropagation2PatternName)
+        }
+        def isDefined(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                val key = new UnitPropagation(q,c,pm,m3)
+                return unitPropagation2PatternName.get(key) !== null
+        }
+}
+@Data
+class UnitPropagationPreconditionFinalResult {
+        CharSequence definitions
+        HashMap<PConstraint,String> constraint2MustPreconditionName
+        HashMap<PConstraint,String> constraint2CurrentPreconditionName
+}
+class UnitPropagationPreconditionGenerator {
+        val PatternGenerator base
+        val PConstraintTransformer constraintTransformer;
+        
+        new(PatternGenerator patternGenerator) {
+                this.base = patternGenerator
+                this.constraintTransformer = new PConstraintTransformer(base.relationDefinitionIndexer)
+        }
+        
+        def generateUnitPropagationRules(
+                LogicProblem problem,
+                Iterable<RelationDefinition> relations,
+                Map<String,PQuery> fqn2PQuery)
+        {
+                // Create an empty result
+                val res = new UnitPropagationPreconditionGenerationResult               
+                val wfs = base.wfQueries(problem)//.map[it.patternPQuery]
+                val Map<PConstraint,List<Pair<String,Integer>>> mainMustPropagationNames = new HashMap
+                val Map<PConstraint,List<Pair<String,Integer>>> mainCurrentPropagationNames = new HashMap
+                for(wf : wfs) {
+                        val query = wf.patternPQuery as PQuery
+                        val relation = wf.target
+                        val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation)
+                        
+                        for(referredCheck : allReferredChecks) {
+                                val mustPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST)
+                                val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT)
+                                if(!mainMustPropagationNames.containsKey(referredCheck)) {
+                                        mainMustPropagationNames.put(referredCheck,new LinkedList)
+                                }
+                                if(!mainCurrentPropagationNames.containsKey(referredCheck)) {
+                                        mainCurrentPropagationNames.put(referredCheck,new LinkedList)
+                                }
+                                if(mustPropagationPrecondition !== null) {
+                                        mainMustPropagationNames.get(referredCheck).add(mustPropagationPrecondition->query.parameterNames.size)
+                                }
+                                if(currentPropagationPrecondition !== null) {
+                                        mainCurrentPropagationNames.get(referredCheck).add(currentPropagationPrecondition->query.parameterNames.size)
+                                }
+                        }
+                }
+                val preconditions = new LinkedList
+                val constraint2MustPrecondition = new HashMap
+                val constraint2CurrentPrecondition = new HashMap
+                for(entry : mainMustPropagationNames.entrySet) {
+                        val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
+                        val def = '''
+                        pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
+                                «FOR propagation : entry.value SEPARATOR " or "»
+                                        { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
+                                «ENDFOR»'''
+                        preconditions+=def
+                        constraint2MustPrecondition.put(entry.key,name)
+                }
+                for(entry : mainCurrentPropagationNames.entrySet) {
+                        val name = '''UPCurrentPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
+                        val def = '''
+                        pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
+                                «FOR propagation : entry.value SEPARATOR " or "»
+                                        { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
+                                «ENDFOR»'''
+                        preconditions+=def
+                        constraint2CurrentPrecondition.put(entry.key,name)
+                }
+                
+                val definitions = '''
+                        «FOR def : res.definitions»
+                                «def»
+                        «ENDFOR»
+                        
+                        // Collected propagation preconditions:
+                        
+                        «FOR predondition : preconditions»
+                                «predondition»
+                        «ENDFOR»
+                '''
+                return new UnitPropagationPreconditionFinalResult(definitions,constraint2MustPrecondition,constraint2CurrentPrecondition)
+        }
+        def allReferredConstraints(Relation relation, PQuery query) {
+                val allReferredQueries = query.allReferredQueries
+                val problem = relation.eContainer as LogicProblem
+                val constraints = new LinkedHashSet
+                for(referredQuery: #[query]+allReferredQueries) {
+                        val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target
+                        val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
+                        constraints.addAll(bodies.map[getConstraints].flatten)
+                }
+                
+                return constraints
+        }
+        
+        def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                if(res.contains(q,c,pm,m3)) {
+                        return res.getName(q,c,pm,m3)
+                } else {
+                        res.generatePropagationRule(relation,q,c,pm,m3)
+                        return res.getName(q,c,pm,m3)
+                }
+        }
+        def getOrGenerateConstraintName(UnitPropagationPreconditionGenerationResult res, PConstraint c){
+                if(res.constraintOccurence2Name.containsKey(c)) {
+                        return res.constraintOccurence2Name.get(c)
+                } else {
+                        val constraintName = '''Constraint«res.constraintOccurence2Name.size»'''
+                        res.constraintOccurence2Name.put(c,constraintName)
+                        return constraintName
+                }
+        }
+        
+        def void generatePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
+                val name = relationDefinitionName(res,relation,q,c,pm,m3)
+                val constraintArity = c.arity
+                val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
+                val generatedBodies = new LinkedList
+                for(body : bodies) {
+                        if(body.constraints.contains(c)) {
+                                if(pm === PropagationModality::UP) {
+                                        generatedBodies += '''
+                                                // Original Constraints
+                                                «FOR constraint : body.constraints.filter[it !== c]»
+                                                        «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
+                                                «ENDFOR»
+                                                // Propagation for constraint
+                                                «this.constraintTransformer.transformConstraintUnset(c as ExpressionEvaluation,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
+                                                // Matching variables
+                                                «this.propagateVariables(c,pm)»
+                                        '''
+                                }
+                                // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied
+                        } else {
+                                val positives = body.constraints.filter(PositivePatternCall)
+                                for(positive: positives) {
+                                        val referredPQuery = positive.referredQuery
+                                        val referredRelation = (relation.eContainer as LogicProblem)
+                                                .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
+                                        if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
+                                                val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3)
+                                                if(referredName !== null) {
+                                                        generatedBodies += '''
+                                                                // Original Constraints
+                                                                «FOR constraint : body.constraints.filter[it !== positive]»
+                                                                        «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
+                                                                «ENDFOR»
+                                                                // Propagation for constraint referred indirectly from this pattern through «referredName»
+                                                                find «referredName»(problem, interpretation,
+                                                                        «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR»,
+                                                                        «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
+                                                        '''
+                                                }
+                                                // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either
+                                        }
+                                }
+                                
+                                val negatives = body.constraints.filter(NegativePatternCall)
+                                for(negative : negatives) {
+                                        val referredPQuery = negative.referredQuery
+                                        val referredRelation = (relation.eContainer as LogicProblem)
+                                                .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
+                                        if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
+                                                val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual)
+                                                if(referredName !== null) {
+                                                        generatedBodies += '''
+                                                                // Original Constraints
+                                                                «FOR constraint : body.constraints.filter[it !== negative]»
+                                                                        «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
+                                                                «ENDFOR»
+                                                                // Propagation for constraint referred indirectly from this pattern through «referredName»
+                                                                find «referredName»(problem, interpretation,
+                                                                        «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR»,
+                                                                        «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
+                                                        '''
+                                                } else {
+                                                        generatedBodies += '''
+                                                                // Original Constraints
+                                                                «FOR constraint : body.constraints.filter[it !== negative]»
+                                                                        «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
+                                                                «ENDFOR»
+                                                                // Propagation for constraint referred indirectly from this pattern through «referredName»,
+                                                                // which was unsatisfiable
+                                                        '''
+                                                }
+                                        }
+                                }
+                        }
+                }
+                
+                // Register the result
+                if(generatedBodies.empty) {
+                        res.registerUnsatQuery(q,c,pm,m3)
+                } else {
+                        val definition = '''
+                                private pattern «name»(
+                                        problem:LogicProblem, interpretation:PartialInterpretation,
+                                        «FOR param :  q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»,
+                                        «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR»)
+                                «FOR generatedBody: generatedBodies SEPARATOR " or "»{
+                                «generatedBody»
+                                }«ENDFOR»
+                        '''
+                        res.registerQuery(q,c,pm,m3,name,definition)
+                }
+        }
+        private def String relationDefinitionName(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3)
+                '''«pm.name»«m3.name»Propagate«res.getOrGenerateConstraintName(c)»_«base.canonizeName(relation.name)»'''
+        
+        def canonizeName(PVariable v) {
+                return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»'''
+        }
+        
+        def canonizeName(int index, PropagationModality m) {
+                return '''«m.name.toLowerCase»_«index»'''
+        }
+        
+        def dispatch propagateVariables(ExpressionEvaluation c, PropagationModality m) {
+                val comparator = new Comparator<PVariable>(){
+                        override compare(PVariable o1, PVariable o2) {
+                                o1.name.compareTo(o2.name)
+                        }
+                }
+                val variablesInOrder = new ArrayList(c.affectedVariables)
+                variablesInOrder.toList.sort(comparator)
+                return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»'''
+        }
+        def dispatch propagateVariables(PConstraint c, PropagationModality m) {
+                throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
+        }
+        
+        def dispatch arity(ExpressionEvaluation c) {
+                c.affectedVariables.size
+        }
+        def dispatch arity(PConstraint c) {
+                throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
+        }
+}
+\ No newline at end of file

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