aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
blob: dd5cade1e9af3d4e1b44059854d49fc3eb3afde2 (plain) (blame)
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
268
269
270
271
272
273
274
275
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
import java.util.Map

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)
			val Map<PVariable, PrimitiveTypeReference> variable2Type = e.affectedVariables.toInvertedMap[v|variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference]
			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»
«««						«IF variable2Type.values.filter(RealTypeReference).empty»
«««						||
«««						(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»)
«««						«ENDIF»
«««					);
				'''
			} else { // Must or Current
				return '''
					«FOR variable: e.affectedVariables»
						PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
					«ENDFOR»
«««					«IF variable2Type.values.filter(RealTypeReference).empty»
«««						check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»);
«««					«ENDIF»
				'''
			}
		}
	}

	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»"!''')
	}
}