diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src')
5 files changed, 327 insertions, 178 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend index e511a961..fd4374f5 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend | |||
@@ -11,7 +11,5 @@ import org.eclipse.xtend.lib.annotations.Data | |||
11 | class CanonisedFormulae { | 11 | class CanonisedFormulae { |
12 | CharSequence viatraCode | 12 | CharSequence viatraCode |
13 | Map<Assertion,String> assertion2ConstraintPattern | 13 | Map<Assertion,String> assertion2ConstraintPattern |
14 | Map<ConstantDefinition,String> constant2ValuePattern | ||
15 | Map<RelationDefinition,String> relation2ValuePattern | 14 | Map<RelationDefinition,String> relation2ValuePattern |
16 | Map<FunctionDefinition,String> function2ValuePattern | ||
17 | } \ No newline at end of file | 15 | } \ 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/formulacanonization/FormulaCanoniser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend index 0af0b36a..182f3a3a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend | |||
@@ -5,17 +5,35 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | |||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
7 | import java.util.List | 7 | import java.util.List |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
8 | 11 | ||
9 | /** | 12 | /** |
10 | * Translates a set of assertions and definitions to viatra patterns. | 13 | * Translates a Terms into format |
14 | * <P(x1,...,xn)> := Bodies(x1,...,xn) | ||
15 | * <Bodies(x1,...,xn)> := <Body(x1,...,xn)> | <Body(x1,...,xn)> or <Bodies(x1,...,xn)> | ||
16 | * <Body(x1,...,xn)> := Exists y1,...,ym : <Constraints(x1,...,xn,y1,....,ym)> | ||
17 | * <Constraints(x1,...,xn)> := Constraint(x1,...xn) | Constraint(x1,...,xn) and <Constraints(x1,...,xn)> | ||
11 | */ | 18 | */ |
12 | class FormulaCanoniser { | 19 | class FormulaCanoniser { |
13 | def canonise( | 20 | // def canonise( |
14 | List<Assertion> assertions, | 21 | // List<Assertion> assertions, |
15 | List<RelationDefinition> relations, | 22 | // List<RelationDefinition> relations) |
16 | List<ConstantDefinition> constants, | 23 | // { |
17 | List<FunctionDefinition> functions) | 24 | // |
18 | { | 25 | // } |
19 | 26 | // | |
20 | } | 27 | // |
28 | // def canoniseToConstraintBlock(Term predicate, List<Variable> variables) { | ||
29 | // val | ||
30 | // } | ||
31 | // | ||
32 | // def freeVariables(Term t) { | ||
33 | // val subterms = #[t]+t.eAllContents.toList | ||
34 | // val variables = subterms.filter(Variable).toSet | ||
35 | // val variableReferences = subterms.filter(SymbolicValue).filter[it.symbolicReference instanceof Variable] | ||
36 | // val freeVariables = variableReferences.filter[!variables.contains(it.symbolicReference)] | ||
37 | // return freeVariables.map | ||
38 | // } | ||
21 | } \ No newline at end of file | 39 | } \ 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/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend new file mode 100644 index 00000000..64fbb2f1 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend | |||
@@ -0,0 +1,192 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.XExpressionExtractor | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
5 | import org.eclipse.emf.ecore.EAttribute | ||
6 | import org.eclipse.emf.ecore.EEnumLiteral | ||
7 | import org.eclipse.emf.ecore.EReference | ||
8 | import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey | ||
9 | import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey | ||
10 | import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey | ||
11 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
12 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | ||
13 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality | ||
14 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter | ||
15 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
16 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality | ||
17 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall | ||
18 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint | ||
19 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure | ||
20 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue | ||
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall | ||
22 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint | ||
23 | |||
24 | class PConstraintTransformer { | ||
25 | val extension RelationDefinitionIndexer relationDefinitionIndexer; | ||
26 | val expressionExtractor = new XExpressionExtractor | ||
27 | |||
28 | new(RelationDefinitionIndexer relationDefinitionIndexer) { | ||
29 | this.relationDefinitionIndexer = relationDefinitionIndexer | ||
30 | } | ||
31 | |||
32 | dispatch def transformConstraint(TypeConstraint constraint, Modality modality) { | ||
33 | val touple = constraint.variablesTuple | ||
34 | if(touple.size == 1) { | ||
35 | val inputKey = constraint.equivalentJudgement.inputKey | ||
36 | if(inputKey instanceof EClassTransitiveInstancesKey) { | ||
37 | return relationDefinitionIndexer.base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, | ||
38 | constraint.getVariableInTuple(0).canonizeName) | ||
39 | } else if(inputKey instanceof EDataTypeInSlotsKey){ | ||
40 | return '''// type constraint is enforced by construction''' | ||
41 | } | ||
42 | |||
43 | } else if(touple.size == 2){ | ||
44 | val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey | ||
45 | if(key instanceof EReference) { | ||
46 | return base.referRelationByName( | ||
47 | key, | ||
48 | constraint.getVariableInTuple(0).canonizeName, | ||
49 | constraint.getVariableInTuple(1).canonizeName, | ||
50 | modality.toMustMay) | ||
51 | } else if (key instanceof EAttribute) { | ||
52 | return base.referAttributeByName(key, | ||
53 | constraint.getVariableInTuple(0).canonizeName, | ||
54 | constraint.getVariableInTuple(1).canonizeName, | ||
55 | modality.toMustMay) | ||
56 | } else throw new UnsupportedOperationException('''unknown key: «key.class»''') | ||
57 | } else { | ||
58 | throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') | ||
59 | } | ||
60 | } | ||
61 | dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) { | ||
62 | val touple = constraint.variablesTuple | ||
63 | if(touple.size == 1) { | ||
64 | val inputKey = constraint.equivalentJudgement.inputKey | ||
65 | if(inputKey instanceof EClassTransitiveInstancesKey) { | ||
66 | return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, | ||
67 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName) | ||
68 | } else if(inputKey instanceof EDataTypeInSlotsKey){ | ||
69 | return '''// type constraint is enforced by construction''' | ||
70 | } | ||
71 | |||
72 | } else if(touple.size == 2){ | ||
73 | val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey | ||
74 | if(key instanceof EReference) { | ||
75 | return base.referRelationByName( | ||
76 | key, | ||
77 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, | ||
78 | (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, | ||
79 | modality.toMustMay) | ||
80 | } else if (key instanceof EAttribute) { | ||
81 | return base.referAttributeByName(key, | ||
82 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, | ||
83 | (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, | ||
84 | modality.toMustMay) | ||
85 | } else throw new UnsupportedOperationException('''unknown key: «key.class»''') | ||
86 | } else { | ||
87 | throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') | ||
88 | } | ||
89 | } | ||
90 | |||
91 | dispatch def transformConstraint(Equality equality, Modality modality) { | ||
92 | val a = equality.who | ||
93 | val b = equality.withWhom | ||
94 | transformEquality(modality.toMustMay, a, b) | ||
95 | } | ||
96 | |||
97 | private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { | ||
98 | if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
99 | else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
100 | } | ||
101 | |||
102 | dispatch def transformConstraint(Inequality inequality, Modality modality) { | ||
103 | val a = inequality.who | ||
104 | val b = inequality.withWhom | ||
105 | if(modality.isCurrent) { | ||
106 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
107 | } else if(modality.isMust) { | ||
108 | return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
109 | } else { // modality.isMay | ||
110 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
111 | } | ||
112 | } | ||
113 | |||
114 | dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) { | ||
115 | val params = (0..<pcall.actualParametersTuple.size).map[index | | ||
116 | val variable = pcall.actualParametersTuple.get(index) as PVariable | ||
117 | return variable.canonizeName | ||
118 | ] | ||
119 | return referPattern(pcall.referredQuery,params,modality.dual,false,false) | ||
120 | } | ||
121 | |||
122 | dispatch def transformConstraint(PositivePatternCall pcall, Modality modality) { | ||
123 | val params = (0..<pcall.variablesTuple.size).map[index | | ||
124 | val variable = pcall.variablesTuple.get(index) as PVariable | ||
125 | return variable.canonizeName | ||
126 | ] | ||
127 | return referPattern(pcall.referredQuery,params,modality,true,false) | ||
128 | } | ||
129 | dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality) { | ||
130 | val params = (0..1).map[index | | ||
131 | val variable = pcall.getVariableInTuple(index) as PVariable | ||
132 | return variable.canonizeName | ||
133 | ] | ||
134 | return referPattern(pcall.referredQuery,params,modality,true,true) | ||
135 | } | ||
136 | dispatch def transformConstraint(ExportedParameter e, Modality modality) { | ||
137 | return '''// «e.parameterName» is exported''' | ||
138 | } | ||
139 | dispatch def transformConstraint(ConstantValue c, Modality modality) { | ||
140 | val target = c.supplierKey | ||
141 | |||
142 | var String targetString; | ||
143 | var String additionalDefinition; | ||
144 | if(target instanceof EEnumLiteral) { | ||
145 | targetString = '''const_«target.name»_«target.EEnum.name»''' | ||
146 | additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);''' | ||
147 | } else if(target instanceof Integer) { | ||
148 | targetString = '''const_«target»_Integer''' | ||
149 | additionalDefinition = '''IntegerElement.value(«targetString»,«target»);''' | ||
150 | } else if(target instanceof Boolean) { | ||
151 | targetString = '''const_«target»_Boolean''' | ||
152 | additionalDefinition = '''BooleanElement.value(«targetString»,«target»);''' | ||
153 | } else if(target instanceof String) { | ||
154 | targetString = '''const_«target»_String''' | ||
155 | additionalDefinition = '''StringElement.value(«targetString»,"«target»");''' | ||
156 | } else if(target instanceof Double) { | ||
157 | targetString = '''const_«target»_Number''' | ||
158 | additionalDefinition = '''RealElement.value(«targetString»,"«target»");''' | ||
159 | } else if(target instanceof Float) { | ||
160 | targetString = '''const_«target»_Number''' | ||
161 | additionalDefinition = '''RealElement.value(«targetString»,"«target»");''' | ||
162 | } else { | ||
163 | throw new UnsupportedOperationException('''Unknown constant type: «target.class»''') | ||
164 | } | ||
165 | |||
166 | val source = c.variablesTuple | ||
167 | var String sourceName | ||
168 | if(source.size == 1) | ||
169 | sourceName = (source.get(0) as PVariable).canonizeName | ||
170 | else throw new UnsupportedOperationException("unknown source") | ||
171 | return '''«sourceName» == «targetString»;«additionalDefinition»'''; | ||
172 | } | ||
173 | |||
174 | |||
175 | |||
176 | dispatch def transformConstrait(ExpressionEvaluation e, Modality modality) { | ||
177 | if(e.outputVariable!==null) { | ||
178 | throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''') | ||
179 | } else { | ||
180 | val expression = expressionExtractor.extractExpression(e.evaluator) | ||
181 | if(modality.isMust) { | ||
182 | return '''''' | ||
183 | } else if(modality.isMay) { | ||
184 | return '''''' | ||
185 | } | ||
186 | } | ||
187 | } | ||
188 | |||
189 | dispatch def transformConstraint(PConstraint c, Modality modality) { | ||
190 | throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''') | ||
191 | } | ||
192 | } \ 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/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index 04163962..379e334a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend | |||
@@ -200,18 +200,116 @@ class PatternGenerator { | |||
200 | //////////////////////// | 200 | //////////////////////// |
201 | // 0.2 Equivalence | 201 | // 0.2 Equivalence |
202 | //////////////////////// | 202 | //////////////////////// |
203 | pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { | 203 | pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) |
204 | // For non-primitive type. Boolean types always must equivalent or cannot equivalent | ||
205 | { | ||
204 | find mayExist(problem,interpretation,a); | 206 | find mayExist(problem,interpretation,a); |
205 | find mayExist(problem,interpretation,b); | 207 | find mayExist(problem,interpretation,b); |
206 | a == b; | 208 | a == b; |
209 | } or { | ||
210 | find mayExist(problem,interpretation,a); | ||
211 | find mayExist(problem,interpretation,b); | ||
212 | IntegerElement(a); | ||
213 | IntegerElement(b); | ||
214 | PrimitiveElement.valueSet(a,false); | ||
215 | } or { | ||
216 | find mayExist(problem,interpretation,a); | ||
217 | find mayExist(problem,interpretation,b); | ||
218 | IntegerElement(a); | ||
219 | IntegerElement(b); | ||
220 | PrimitiveElement.valueSet(b,false); | ||
221 | } or { | ||
222 | find mayExist(problem,interpretation,a); | ||
223 | find mayExist(problem,interpretation,b); | ||
224 | RealElement(a); | ||
225 | RealElement(b); | ||
226 | PrimitiveElement.valueSet(a,false); | ||
227 | } or { | ||
228 | find mayExist(problem,interpretation,a); | ||
229 | find mayExist(problem,interpretation,b); | ||
230 | RealElement(a); | ||
231 | RealElement(b); | ||
232 | PrimitiveElement.valueSet(b,false); | ||
233 | } or { | ||
234 | find mayExist(problem,interpretation,a); | ||
235 | find mayExist(problem,interpretation,b); | ||
236 | RealElement(a); | ||
237 | IntegerElement(b); | ||
238 | PrimitiveElement.valueSet(a,false); | ||
239 | } or { | ||
240 | find mayExist(problem,interpretation,a); | ||
241 | find mayExist(problem,interpretation,b); | ||
242 | RealElement(a); | ||
243 | IntegerElement(b); | ||
244 | PrimitiveElement.valueSet(b,false); | ||
245 | } or { | ||
246 | find mayExist(problem,interpretation,a); | ||
247 | find mayExist(problem,interpretation,b); | ||
248 | IntegerElement(a); | ||
249 | RealElement(b); | ||
250 | PrimitiveElement.valueSet(a,false); | ||
251 | } or { | ||
252 | find mayExist(problem,interpretation,a); | ||
253 | find mayExist(problem,interpretation,b); | ||
254 | IntegerElement(a); | ||
255 | RealElement(b); | ||
256 | PrimitiveElement.valueSet(b,false); | ||
257 | } or { | ||
258 | find mayExist(problem,interpretation,a); | ||
259 | find mayExist(problem,interpretation,b); | ||
260 | StringElement(a); | ||
261 | StringElement(b); | ||
262 | PrimitiveElement.valueSet(a,false); | ||
263 | } or { | ||
264 | find mayExist(problem,interpretation,a); | ||
265 | find mayExist(problem,interpretation,b); | ||
266 | StringElement(a); | ||
267 | StringElement(b); | ||
268 | PrimitiveElement.valueSet(b,false); | ||
207 | } | 269 | } |
270 | |||
208 | pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { | 271 | pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { |
272 | // For non-primitive and Boolean primitive type | ||
209 | find mustExist(problem,interpretation,a); | 273 | find mustExist(problem,interpretation,a); |
210 | find mustExist(problem,interpretation,b); | 274 | find mustExist(problem,interpretation,b); |
211 | a == b; | 275 | a == b; |
276 | } or { | ||
277 | find mustExist(problem,interpretation,a); | ||
278 | find mustExist(problem,interpretation,b); | ||
279 | PrimitiveElement.valueSet(a,true); | ||
280 | PrimitiveElement.valueSet(b,true); | ||
281 | IntegerElement.value(a,value); | ||
282 | IntegerElement.value(b,value); | ||
283 | } or { | ||
284 | find mustExist(problem,interpretation,a); | ||
285 | find mustExist(problem,interpretation,b); | ||
286 | PrimitiveElement.valueSet(a,true); | ||
287 | PrimitiveElement.valueSet(b,true); | ||
288 | RealElement.value(a,value); | ||
289 | RealElement.value(b,value); | ||
290 | } or { | ||
291 | find mustExist(problem,interpretation,a); | ||
292 | find mustExist(problem,interpretation,b); | ||
293 | PrimitiveElement.valueSet(a,true); | ||
294 | PrimitiveElement.valueSet(b,true); | ||
295 | RealElement.value(a,value); | ||
296 | IntegerElement.value(b,value); | ||
297 | } or { | ||
298 | find mustExist(problem,interpretation,a); | ||
299 | find mustExist(problem,interpretation,b); | ||
300 | PrimitiveElement.valueSet(a,true); | ||
301 | PrimitiveElement.valueSet(b,true); | ||
302 | IntegerElement.value(a,value); | ||
303 | RealElement.value(b,value); | ||
304 | } or { | ||
305 | find mustExist(problem,interpretation,a); | ||
306 | find mustExist(problem,interpretation,b); | ||
307 | PrimitiveElement.valueSet(a,true); | ||
308 | PrimitiveElement.valueSet(b,true); | ||
309 | StringElement.value(a,value); | ||
310 | StringElement.value(b,value); | ||
212 | } | 311 | } |
213 | 312 | ||
214 | |||
215 | ////////// | 313 | ////////// |
216 | // 1. Problem-Specific Base Indexers | 314 | // 1. Problem-Specific Base Indexers |
217 | ////////// | 315 | ////////// |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend index 9723373f..6b9818b4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend | |||
@@ -5,35 +5,22 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | |||
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | 5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
7 | import java.util.Map | 7 | import java.util.Map |
8 | import org.eclipse.emf.ecore.EAttribute | ||
9 | import org.eclipse.emf.ecore.EEnumLiteral | ||
10 | import org.eclipse.emf.ecore.EReference | ||
11 | import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey | ||
12 | import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey | ||
13 | import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey | ||
14 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
15 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | 8 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable |
16 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality | ||
17 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter | ||
18 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality | ||
19 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall | ||
20 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure | 9 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure |
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue | ||
22 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall | ||
23 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint | ||
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 10 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
25 | 11 | ||
26 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
27 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint | ||
28 | 13 | ||
29 | class RelationDefinitionIndexer { | 14 | class RelationDefinitionIndexer { |
30 | val PatternGenerator base; | 15 | public val PatternGenerator base; |
16 | val PConstraintTransformer constraintTransformer; | ||
31 | 17 | ||
32 | new(PatternGenerator base) { | 18 | new(PatternGenerator base) { |
33 | this.base = base | 19 | this.base = base |
20 | this.constraintTransformer = new PConstraintTransformer(this); | ||
34 | } | 21 | } |
35 | 22 | ||
36 | public def generateRelationDefinitions( | 23 | def generateRelationDefinitions( |
37 | LogicProblem problem, | 24 | LogicProblem problem, |
38 | Iterable<RelationDefinition> relations, | 25 | Iterable<RelationDefinition> relations, |
39 | Map<String,PQuery> fqn2PQuery) { | 26 | Map<String,PQuery> fqn2PQuery) { |
@@ -74,7 +61,7 @@ class RelationDefinitionIndexer { | |||
74 | private def relationDefinitionName(RelationDefinition relation, Modality modality) | 61 | private def relationDefinitionName(RelationDefinition relation, Modality modality) |
75 | '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' | 62 | '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' |
76 | 63 | ||
77 | private def canonizeName(PVariable v) { | 64 | def canonizeName(PVariable v) { |
78 | return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»''' | 65 | return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»''' |
79 | } | 66 | } |
80 | 67 | ||
@@ -87,7 +74,7 @@ class RelationDefinitionIndexer { | |||
87 | «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{ | 74 | «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{ |
88 | find interpretation(problem,interpretation); | 75 | find interpretation(problem,interpretation); |
89 | «FOR constraint : body.constraints» | 76 | «FOR constraint : body.constraints» |
90 | «constraint.transformConstraint(modality)» | 77 | «this.constraintTransformer.transformConstraint(constraint,modality)» |
91 | «ENDFOR» | 78 | «ENDFOR» |
92 | }«ENDFOR» | 79 | }«ENDFOR» |
93 | ''' | 80 | ''' |
@@ -104,158 +91,14 @@ class RelationDefinitionIndexer { | |||
104 | ''' | 91 | ''' |
105 | } | 92 | } |
106 | 93 | ||
107 | private def toMustMay(Modality modality) { | 94 | def toMustMay(Modality modality) { |
108 | if(modality == Modality::MAY) return Modality::MAY | 95 | if(modality == Modality::MAY) return Modality::MAY |
109 | else return Modality::MUST | 96 | else return Modality::MUST |
110 | } | 97 | } |
111 | 98 | ||
112 | def public referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' | 99 | def referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' |
113 | «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»); | 100 | «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»); |
114 | ''' | 101 | ''' |
115 | 102 | ||
116 | private dispatch def transformConstraint(TypeConstraint constraint, Modality modality) { | ||
117 | val touple = constraint.variablesTuple | ||
118 | if(touple.size == 1) { | ||
119 | val inputKey = constraint.equivalentJudgement.inputKey | ||
120 | if(inputKey instanceof EClassTransitiveInstancesKey) { | ||
121 | return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, | ||
122 | constraint.getVariableInTuple(0).canonizeName) | ||
123 | } else if(inputKey instanceof EDataTypeInSlotsKey){ | ||
124 | return '''// type constraint is enforced by construction''' | ||
125 | } | ||
126 | |||
127 | } else if(touple.size == 2){ | ||
128 | val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey | ||
129 | if(key instanceof EReference) { | ||
130 | return base.referRelationByName( | ||
131 | key, | ||
132 | constraint.getVariableInTuple(0).canonizeName, | ||
133 | constraint.getVariableInTuple(1).canonizeName, | ||
134 | modality.toMustMay) | ||
135 | } else if (key instanceof EAttribute) { | ||
136 | return base.referAttributeByName(key, | ||
137 | constraint.getVariableInTuple(0).canonizeName, | ||
138 | constraint.getVariableInTuple(1).canonizeName, | ||
139 | modality.toMustMay) | ||
140 | } else throw new UnsupportedOperationException('''unknown key: «key.class»''') | ||
141 | } else { | ||
142 | throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') | ||
143 | } | ||
144 | } | ||
145 | private dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) { | ||
146 | val touple = constraint.variablesTuple | ||
147 | if(touple.size == 1) { | ||
148 | val inputKey = constraint.equivalentJudgement.inputKey | ||
149 | if(inputKey instanceof EClassTransitiveInstancesKey) { | ||
150 | return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, | ||
151 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName) | ||
152 | } else if(inputKey instanceof EDataTypeInSlotsKey){ | ||
153 | return '''// type constraint is enforced by construction''' | ||
154 | } | ||
155 | |||
156 | } else if(touple.size == 2){ | ||
157 | val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey | ||
158 | if(key instanceof EReference) { | ||
159 | return base.referRelationByName( | ||
160 | key, | ||
161 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, | ||
162 | (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, | ||
163 | modality.toMustMay) | ||
164 | } else if (key instanceof EAttribute) { | ||
165 | return base.referAttributeByName(key, | ||
166 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, | ||
167 | (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, | ||
168 | modality.toMustMay) | ||
169 | } else throw new UnsupportedOperationException('''unknown key: «key.class»''') | ||
170 | } else { | ||
171 | throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') | ||
172 | } | ||
173 | } | ||
174 | |||
175 | private dispatch def transformConstraint(Equality equality, Modality modality) { | ||
176 | val a = equality.who | ||
177 | val b = equality.withWhom | ||
178 | transformEquality(modality.toMustMay, a, b) | ||
179 | } | ||
180 | |||
181 | private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { | ||
182 | if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
183 | else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
184 | } | ||
185 | |||
186 | private dispatch def transformConstraint(Inequality inequality, Modality modality) { | ||
187 | val a = inequality.who | ||
188 | val b = inequality.withWhom | ||
189 | if(modality.isCurrent) { | ||
190 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
191 | } else if(modality.isMust) { | ||
192 | return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
193 | } else { // modality.isMay | ||
194 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
195 | } | ||
196 | } | ||
197 | |||
198 | private dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) { | ||
199 | val params = (0..<pcall.actualParametersTuple.size).map[index | | ||
200 | val variable = pcall.actualParametersTuple.get(index) as PVariable | ||
201 | return variable.canonizeName | ||
202 | ] | ||
203 | return referPattern(pcall.referredQuery,params,modality.dual,false,false) | ||
204 | } | ||
205 | 103 | ||
206 | private dispatch def transformConstraint(PositivePatternCall pcall, Modality modality) { | ||
207 | val params = (0..<pcall.variablesTuple.size).map[index | | ||
208 | val variable = pcall.variablesTuple.get(index) as PVariable | ||
209 | return variable.canonizeName | ||
210 | ] | ||
211 | return referPattern(pcall.referredQuery,params,modality,true,false) | ||
212 | } | ||
213 | private dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality) { | ||
214 | val params = (0..1).map[index | | ||
215 | val variable = pcall.getVariableInTuple(index) as PVariable | ||
216 | return variable.canonizeName | ||
217 | ] | ||
218 | return referPattern(pcall.referredQuery,params,modality,true,true) | ||
219 | } | ||
220 | private dispatch def transformConstraint(ExportedParameter e, Modality modality) { | ||
221 | return '''// «e.parameterName» is exported''' | ||
222 | } | ||
223 | private dispatch def transformConstraint(ConstantValue c, Modality modality) { | ||
224 | val target = c.supplierKey | ||
225 | |||
226 | var String targetString; | ||
227 | var String additionalDefinition; | ||
228 | if(target instanceof EEnumLiteral) { | ||
229 | targetString = '''const_«target.name»_«target.EEnum.name»''' | ||
230 | additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);''' | ||
231 | } else if(target instanceof Integer) { | ||
232 | targetString = '''const_«target»_Integer''' | ||
233 | additionalDefinition = '''IntegerElement.value(«targetString»,«target»);''' | ||
234 | } else if(target instanceof Boolean) { | ||
235 | targetString = '''const_«target»_Boolean''' | ||
236 | additionalDefinition = '''BooleanElement.value(«targetString»,«target»);''' | ||
237 | } else if(target instanceof String) { | ||
238 | targetString = '''const_«target»_String''' | ||
239 | additionalDefinition = '''StringElement.value(«targetString»,"«target»");''' | ||
240 | } else if(target instanceof Double) { | ||
241 | targetString = '''const_«target»_Number''' | ||
242 | additionalDefinition = '''RealElement.value(«targetString»,"«target»");''' | ||
243 | } else if(target instanceof Float) { | ||
244 | targetString = '''const_«target»_Number''' | ||
245 | additionalDefinition = '''RealElement.value(«targetString»,"«target»");''' | ||
246 | } else { | ||
247 | throw new UnsupportedOperationException('''Unknown constant type: «target.class»''') | ||
248 | } | ||
249 | |||
250 | val source = c.variablesTuple | ||
251 | var String sourceName | ||
252 | if(source.size == 1) | ||
253 | sourceName = (source.get(0) as PVariable).canonizeName | ||
254 | else throw new UnsupportedOperationException("unknown source") | ||
255 | return '''«sourceName» == «targetString»;«additionalDefinition»'''; | ||
256 | } | ||
257 | |||
258 | private dispatch def transformConstraint(PConstraint c, Modality modality) { | ||
259 | throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''') | ||
260 | } | ||
261 | } \ No newline at end of file | 104 | } \ No newline at end of file |