aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers
diff options
context:
space:
mode:
authorLibravatar Oszkar Semerath <semerath@mit.bme.hu>2020-04-30 18:21:20 +0200
committerLibravatar Oszkar Semerath <semerath@mit.bme.hu>2020-04-30 18:21:20 +0200
commit6f2b33c214110ed5983a762b0da3280933fa3934 (patch)
tree8c8494f2016aaba3f4444466ccb3fa6e2f083673 /Solvers
parentMerge branch 'master' of https://github.com/viatra/VIATRA-Generator (diff)
downloadVIATRA-Generator-6f2b33c214110ed5983a762b0da3280933fa3934.tar.gz
VIATRA-Generator-6f2b33c214110ed5983a762b0da3280933fa3934.tar.zst
VIATRA-Generator-6f2b33c214110ed5983a762b0da3280933fa3934.zip
UP rule precondition provider
Diffstat (limited to 'Solvers')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java8
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend13
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend222
4 files changed, 244 insertions, 1 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
index f43ab96d..e7342ff7 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
@@ -69,7 +69,7 @@ class ModelGenerationMethodProvider {
69 69
70 val queries = patternProvider.generateQueries(logicProblem,emptySolution,statistics,existingQueries,workspace,typeInferenceMethod,writeFiles) 70 val queries = patternProvider.generateQueries(logicProblem,emptySolution,statistics,existingQueries,workspace,typeInferenceMethod,writeFiles)
71 val //LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> 71 val //LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>>
72 objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries,scopePropagator,nameNewElements,statistics) 72 objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, queries,scopePropagator,nameNewElements,statistics)
73 val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics) 73 val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics)
74 74
75 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) 75 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries)
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java
new file mode 100644
index 00000000..2288ad7e
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java
@@ -0,0 +1,8 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra;
2
3public enum PropagationModality {
4 /**The value was originally ? and set to 1 */
5 UP,
6 /**The value was originally ? and set to 0 */
7 DOWN
8}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
index a421d1fd..608ab994 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
@@ -240,4 +240,17 @@ class PConstraintTransformer {
240 dispatch def transformConstraint(PConstraint c, Modality modality, List<VariableMapping> variableMapping) { 240 dispatch def transformConstraint(PConstraint c, Modality modality, List<VariableMapping> variableMapping) {
241 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''') 241 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
242 } 242 }
243
244 dispatch def transformConstraintUnset(ExpressionEvaluation e, List<VariableMapping> variableMapping) {
245 return '''
246 «FOR variable: e.affectedVariables»
247 PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
248 «ENDFOR»
249 check(«FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»);
250 '''
251 }
252
253 dispatch def transformConstraintUnset(PConstraint c, List<VariableMapping> variableMapping) {
254 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
255 }
243} \ No newline at end of file 256} \ 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..25354af4
--- /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,222 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
5import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
6import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.PropagationModality
9import java.util.Map
10import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
11import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
12import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
13import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
14
15import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
16import java.util.LinkedList
17import java.util.List
18import org.eclipse.xtend.lib.annotations.Data
19import java.util.HashMap
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
22import java.util.Comparator
23import java.util.ArrayList
24
25@Data class UnitPropagation {
26 val PQuery q
27 val PConstraint c
28 val PropagationModality pm
29 val Modality m3
30}
31@Data
32class UnitPropagationPreconditionGenerationResult {
33 List<CharSequence> definitions= new LinkedList
34 Map<UnitPropagation,String> unitPropagation2PatternName = new HashMap
35
36 def registerQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3, String patternName, CharSequence definition) {
37 val key = new UnitPropagation(q,c,pm,m3)
38 definitions += definition
39 unitPropagation2PatternName.put(key,patternName)
40 }
41 def registerUnsatQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
42 val key = new UnitPropagation(q,c,pm,m3)
43 unitPropagation2PatternName.put(key,null)
44 }
45 def contains(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
46 val key = new UnitPropagation(q,c,pm,m3)
47 return unitPropagation2PatternName.containsKey(key)
48 }
49 def getName(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
50 val key = new UnitPropagation(q,c,pm,m3)
51 return key.lookup(unitPropagation2PatternName)
52 }
53 def isDefined(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
54 val key = new UnitPropagation(q,c,pm,m3)
55 return unitPropagation2PatternName.get(key) !== null
56 }
57}
58
59class UnitPropagationPreconditionGenerator {
60 val PatternGenerator base
61 val PConstraintTransformer constraintTransformer;
62
63 new(PatternGenerator patternGenerator) {
64 this.base = patternGenerator
65 this.constraintTransformer = new PConstraintTransformer(base.relationDefinitionIndexer)
66 }
67
68 def generateUnitPropagationRules(
69 LogicProblem problem,
70 Iterable<RelationDefinition> relations,
71 Map<String,PQuery> fqn2PQuery)
72 {
73 // Create an empty result
74 val res = new UnitPropagationPreconditionGenerationResult
75
76 val wfs = base.wfQueries(problem)//.map[it.patternPQuery]
77 for(wf : wfs) {
78 val query = wf.patternPQuery as PQuery
79 val relation = wf.target
80 val allReferredChecks = query.allReferredConstraints.filter(ExpressionEvaluation)
81
82 for(referredCheck : allReferredChecks) {
83 generatePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST)
84 }
85 }
86 }
87 def allReferredConstraints(PQuery query) {
88 val allReferredQueries = query.allReferredQueries
89 return (#[query]+allReferredQueries).map[it.disjunctBodies.bodies].flatten.map[constraints].flatten
90 }
91
92 def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
93 if(!res.contains(q,c,pm,m3)) {
94 return res.getName(q,c,pm,m3)
95 } else {
96 res.generatePropagationRule(relation,q,c,pm,m3)
97 return res.getName(q,c,pm,m3)
98 }
99 }
100
101 def void generatePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
102 val name = relationDefinitionName(relation,q,c,pm,m3)
103 val constraintArity = c.arity
104 val generatedBodies = new LinkedList
105 for(body : q.disjunctBodies.bodies) {
106 if(body.constraints.contains(c)) {
107 if(pm === PropagationModality::UP) {
108 generatedBodies += '''
109 // Original Constraints
110 «FOR constraint : body.constraints.filter[it !== c]»
111 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
112 «ENDFOR»
113 // Propagation for constraint
114 «this.constraintTransformer.transformConstraintUnset(c as ExpressionEvaluation,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
115 // Matching variables
116 «this.propagateVariables(c,pm)»
117 '''
118 }
119 // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied
120 } else {
121 val positives = body.constraints.filter(PositivePatternCall)
122 val positiveRefers = positives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)]
123 for(positiveRefer: positiveRefers) {
124 val referredPQuery = positiveRefer.referredQuery
125 val referredRelation = (relation.eContainer as LogicProblem)
126 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
127 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3)
128 if(referredName !== null) {
129 generatedBodies += '''
130 // Original Constraints
131 «FOR constraint : body.constraints.filter[it !== positiveRefer]»
132 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
133 «ENDFOR»
134 // Propagation for constraint referred indirectly from this pattern through «referredName»
135 find «referredName»(problem, interpretation,
136 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positiveRefer.getVariableInTuple(index).canonizeName»«ENDFOR»,
137 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
138 '''
139 }
140 // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either
141 }
142 val negatives = body.constraints.filter(NegativePatternCall)
143 val negativeRefers = negatives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)]
144 for(negativeRefer : negativeRefers) {
145 val referredPQuery = negativeRefer.referredQuery
146 val referredRelation = (relation.eContainer as LogicProblem)
147 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
148 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual)
149 if(referredName !== null) {
150 generatedBodies += '''
151 // Original Constraints
152 «FOR constraint : body.constraints.filter[it !== negativeRefer]»
153 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
154 «ENDFOR»
155 // Propagation for constraint referred indirectly from this pattern through «referredName»
156 find «referredName»(problem, interpretation,
157 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negativeRefer.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR»,
158 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
159 '''
160 } else {
161 generatedBodies += '''
162 // Original Constraints
163 «FOR constraint : body.constraints.filter[it !== negativeRefer]»
164 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
165 «ENDFOR»
166 // Propagation for constraint referred indirectly from this pattern through «referredName»,
167 // which was unsatisfiable
168 '''
169 }
170 }
171 }
172 }
173
174 // Register the result
175 if(generatedBodies.size>=0) {
176 res.registerUnsatQuery(q,c,pm,m3)
177 } else {
178 val definition = '''
179 pattern «name»(
180 problem:LogicProblem, interpretation:PartialInterpretation,
181 «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»,
182 «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR»)
183 «FOR generatedBody: generatedBodies SEPARATOR "or"»{
184 «generatedBody»
185 }«ENDFOR»
186 '''
187 res.registerQuery(q,c,pm,m3,name,definition)
188 }
189 }
190
191 private def String relationDefinitionName(Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3)
192 '''«pm.name»«m3.name»Propagate_«base.canonizeName(relation.name)»'''
193
194 def canonizeName(PVariable v) {
195 return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»'''
196 }
197
198 def canonizeName(int index, PropagationModality m) {
199 return '''«m.name.toLowerCase»_«index»'''
200 }
201
202 def dispatch propagateVariables(ExpressionEvaluation c, PropagationModality m) {
203 val comparator = new Comparator<PVariable>(){
204 override compare(PVariable o1, PVariable o2) {
205 o1.name.compareTo(o2.name)
206 }
207 }
208 val variablesInOrder = new ArrayList(c.affectedVariables)
209 variablesInOrder.toList.sort(comparator)
210 return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).name»==«canonizeName(variableIndex,m)»;«ENDFOR»'''
211 }
212 def dispatch propagateVariables(PConstraint c, PropagationModality m) {
213 throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
214 }
215
216 def dispatch arity(ExpressionEvaluation c) {
217 c.affectedVariables.size
218 }
219 def dispatch arity(PConstraint c) {
220 throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
221 }
222} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-01 00:43:46 +0000