diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit')
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra; | ||
2 | |||
3 | public 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 @@ | |||
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 | |||
25 | @Data class UnitPropagation { | ||
26 | val PQuery q | ||
27 | val PConstraint c | ||
28 | val PropagationModality pm | ||
29 | val Modality m3 | ||
30 | } | ||
31 | @Data | ||
32 | class 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 | |||
59 | class 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 | ||