aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers
diff options
context:
space:
mode:
authorLibravatar Oszkar Semerath <semerath@mit.bme.hu>2020-04-14 22:45:52 +0200
committerLibravatar Oszkar Semerath <semerath@mit.bme.hu>2020-04-14 22:45:52 +0200
commited434397058fd520ad92a938eccd8f93ef378d8a (patch)
tree210f3460809e2b050e315e933b5678e24d67c3c3 /Solvers
parentPrimitive object indexing update (diff)
downloadVIATRA-Generator-ed434397058fd520ad92a938eccd8f93ef378d8a.tar.gz
VIATRA-Generator-ed434397058fd520ad92a938eccd8f93ef378d8a.tar.zst
VIATRA-Generator-ed434397058fd520ad92a938eccd8f93ef378d8a.zip
restructured pattern generation
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/formulacanonization/CanonisedFormulae.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend36
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend192
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend102
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend173
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
11class CanonisedFormulae { 11class 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
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition 5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
7import java.util.List 7import java.util.List
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
10import 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 */
12class FormulaCanoniser { 19class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2
3import hu.bme.mit.inf.dslreasoner.viatra2logic.XExpressionExtractor
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
5import org.eclipse.emf.ecore.EAttribute
6import org.eclipse.emf.ecore.EEnumLiteral
7import org.eclipse.emf.ecore.EReference
8import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
9import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
10import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
11import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
12import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
13import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
14import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
15import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
16import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
17import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
18import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
19import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
22import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
23
24class 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
5import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery 5import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality 6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import java.util.Map 7import java.util.Map
8import org.eclipse.emf.ecore.EAttribute
9import org.eclipse.emf.ecore.EEnumLiteral
10import org.eclipse.emf.ecore.EReference
11import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
12import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
13import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
14import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
15import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable 8import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
16import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
17import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
18import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
19import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure 9import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
22import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
23import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
24import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 10import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
25 11
26import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 12import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
27import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
28 13
29class RelationDefinitionIndexer { 14class 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-01 08:53:19 +0000