1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
|
package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
import hu.bme.mit.inf.dslreasoner.viatra2logic.XExpressionExtractor
import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
import org.eclipse.emf.ecore.EAttribute
import org.eclipse.emf.ecore.EEnumLiteral
import org.eclipse.emf.ecore.EReference
import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.VariableMapping
import java.util.List
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
class PConstraintTransformer {
val extension RelationDefinitionIndexer relationDefinitionIndexer;
val expressionExtractor = new XExpressionExtractor
val expressionGenerator = new PExpressionGenerator
new(RelationDefinitionIndexer relationDefinitionIndexer) {
this.relationDefinitionIndexer = relationDefinitionIndexer
}
dispatch def transformConstraint(TypeConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
val touple = constraint.variablesTuple
if(touple.size == 1) {
val inputKey = constraint.equivalentJudgement.inputKey
if(inputKey instanceof EClassTransitiveInstancesKey) {
return relationDefinitionIndexer.base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
constraint.getVariableInTuple(0).canonizeName)
} else if(inputKey instanceof EDataTypeInSlotsKey){
return '''// type constraint is enforced by construction'''
}
} else if(touple.size == 2){
val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
if(key instanceof EReference) {
return base.referRelationByName(
key,
constraint.getVariableInTuple(0).canonizeName,
constraint.getVariableInTuple(1).canonizeName,
modality.toMustMay)
} else if (key instanceof EAttribute) {
return base.referAttributeByName(key,
constraint.getVariableInTuple(0).canonizeName,
constraint.getVariableInTuple(1).canonizeName,
modality.toMustMay)
} else throw new UnsupportedOperationException('''unknown key: «key.class»''')
} else {
throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
}
}
dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
val touple = constraint.variablesTuple
if(touple.size == 1) {
val inputKey = constraint.equivalentJudgement.inputKey
if(inputKey instanceof EClassTransitiveInstancesKey) {
return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
(constraint.getVariablesTuple.get(0) as PVariable).canonizeName)
} else if(inputKey instanceof EDataTypeInSlotsKey){
return '''// type constraint is enforced by construction'''
}
} else if(touple.size == 2){
val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
if(key instanceof EReference) {
return base.referRelationByName(
key,
(constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
(constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
modality.toMustMay)
} else if (key instanceof EAttribute) {
return base.referAttributeByName(key,
(constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
(constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
modality.toMustMay)
} else throw new UnsupportedOperationException('''unknown key: «key.class»''')
} else {
throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
}
}
dispatch def transformConstraint(Equality equality, Modality modality, List<VariableMapping> variableMapping) {
val a = equality.who
val b = equality.withWhom
transformEquality(modality.toMustMay, a, b)
}
private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) {
if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
}
dispatch def transformConstraint(Inequality inequality, Modality modality, List<VariableMapping> variableMapping) {
val a = inequality.who
val b = inequality.withWhom
if(modality.isCurrent) {
return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
} else if(modality.isMust) {
return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
} else { // modality.isMay
return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
}
}
dispatch def transformConstraint(NegativePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
val params = (0..<pcall.actualParametersTuple.size).map[index |
val variable = pcall.actualParametersTuple.get(index) as PVariable
return variable.canonizeName
]
return referPattern(pcall.referredQuery,params,modality.dual,false,false)
}
dispatch def transformConstraint(PositivePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
val params = (0..<pcall.variablesTuple.size).map[index |
val variable = pcall.variablesTuple.get(index) as PVariable
return variable.canonizeName
]
return referPattern(pcall.referredQuery,params,modality,true,false)
}
dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality, List<VariableMapping> variableMapping) {
val params = (0..1).map[index |
val variable = pcall.getVariableInTuple(index) as PVariable
return variable.canonizeName
]
return referPattern(pcall.referredQuery,params,modality,true,true)
}
dispatch def transformConstraint(ExportedParameter e, Modality modality, List<VariableMapping> variableMapping) {
val v1 = '''var_«e.parameterName»'''
val v2 = e.parameterVariable.canonizeName
if(v1.compareTo(v2) == 0) {
return '''// «v1» exported'''
} else {
return '''«v1» == «v2»;'''
}
}
dispatch def transformConstraint(ConstantValue c, Modality modality, List<VariableMapping> variableMapping) {
val target = c.supplierKey
var String targetString;
var String additionalDefinition;
if(target instanceof EEnumLiteral) {
targetString = '''const_«target.name»_«target.EEnum.name»'''
additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);'''
} else if(target instanceof Integer) {
targetString = '''const_«target»_Integer'''
additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); IntegerElement.value(«targetString»,«target»);'''
} else if(target instanceof Boolean) {
targetString = '''const_«target»_Boolean'''
additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); BooleanElement.value(«targetString»,«target»);'''
} else if(target instanceof String) {
targetString = '''const_«target»_String'''
additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); StringElement.value(«targetString»,"«target»");'''
} else if(target instanceof Double) {
targetString = '''const_«target»_Real'''
additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
} else if(target instanceof Float) {
targetString = '''const_«target»_Real'''
additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
} else {
throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')
}
val source = c.variablesTuple
var String sourceName
if(source.size == 1)
sourceName = (source.get(0) as PVariable).canonizeName
else throw new UnsupportedOperationException("unknown source")
return '''«sourceName» == «targetString»;«additionalDefinition»''';
}
protected def valueVariable(PVariable v) {
"value_"+v.canonizeName
}
protected def valueSetted(PVariable v) {
"setted_"+v.canonizeName
}
def hasValue(PVariable v, String target, Modality m, List<VariableMapping> variableMapping) {
val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference
if(m.isMay) {
'''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpressionByRef(typeReference,v,v.valueVariable)» check(!«v.valueSetted»||«v.valueVariable»==«target»));'''
} else { // Must or current
'''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpressionByRef(typeReference,v,target)»'''
}
}
private def hasValueExpression(List<VariableMapping> variableMapping, PVariable v, String target) {
val mapping = variableMapping.filter[
val v2 = (it.sourcePVariable as PVariable)
v2 === v
].head
val range = mapping.targetLogicVariable.range
hasValueExpressionByRef(
range,
v,
target
)
}
private def dispatch hasValueExpressionByRef(BoolTypeReference typeReference, PVariable v, String target) '''BooleanElement.value(«v.canonizeName»,«target»);'''
private def dispatch hasValueExpressionByRef(IntTypeReference typeReference, PVariable v, String target) '''IntegerElement.value(«v.canonizeName»,«target»);'''
private def dispatch hasValueExpressionByRef(RealTypeReference typeReference, PVariable v, String target) '''RealElement.value(«v.canonizeName»,«target»);'''
private def dispatch hasValueExpressionByRef(StringTypeReference typeReference, PVariable v, String target) '''StringElement.value(«v.canonizeName»,«target»);'''
private def dispatch hasValueExpressionByRef(TypeReference typeReference, PVariable v, String target) {
throw new UnsupportedOperationException('''Unsupported primitive type reference: «typeReference.class»''')
}
dispatch def transformConstraint(ExpressionEvaluation e, Modality modality, List<VariableMapping> variableMapping) {
if(e.outputVariable!==null) {
throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''')
} else {
val expression = expressionExtractor.extractExpression(e.evaluator)
if(modality.isMay) {
return '''
«FOR variable: e.affectedVariables»
PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
«ENDFOR»
check(
«FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»
||
(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])»)
);
'''
} else { // Must or Current
return '''
«FOR variable: e.affectedVariables»
PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
«ENDFOR»
check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])»);
'''
}
}
}
dispatch def transformConstraint(PConstraint c, Modality modality, List<VariableMapping> variableMapping) {
throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
}
dispatch def transformConstraintUnset(ExpressionEvaluation e, List<VariableMapping> variableMapping) {
return '''
«FOR variable: e.affectedVariables»
PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
«ENDFOR»
check(«FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»);
'''
}
dispatch def transformConstraintUnset(PConstraint c, List<VariableMapping> variableMapping) {
throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
}
}
|