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