aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
committerLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
commit60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend
parentInitial commit, migrating from SVN (diff)
downloadVIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
Migrating Additional projects
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend')
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend501
1 files changed, 501 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend
new file mode 100644
index 00000000..c9bafa6c
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend
@@ -0,0 +1,501 @@
1package hu.bme.mit.inf.dslreasoner.smt.reasoner
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
10import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher
11import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher
12import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
13import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
14import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral
15import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration
16import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
17import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
18import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
19import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult
20import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSetTypeDeclaration
21import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
22import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
23import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
24import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
25import java.util.ArrayList
26import java.util.HashMap
27import java.util.LinkedList
28import java.util.List
29import java.util.Map
30import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
31import org.eclipse.viatra.query.runtime.emf.EMFScope
32import org.eclipse.xtext.xbase.lib.Functions.Function0
33import org.eclipse.xtext.xbase.lib.Functions.Function1
34
35import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
36
37class Logic2Smt_TypeMapperTrace_FilteredTypes implements Logic2Smt_TypeMapperTrace{
38 public var Map<Type, SMTType> independentClasses = new HashMap
39 /**
40 * SMT type for the new objects
41 */
42 public var SMTType newObjects
43 /**
44 * SMT type for the existing objects
45 */
46 public var SMTEnumeratedTypeDeclaration oldObjects
47 /**
48 * existing element -> SMT literal map
49 */
50 public var Map<DefinedElement, SMTEnumLiteral> elementMap = new HashMap
51
52 public var SMTEnumeratedTypeDeclaration oldObjectTypes
53 public var Map<Type, SMTEnumLiteral> oldObjectTypeMap = new HashMap
54 public var SMTFunctionDefinition oldObjectTypeFunction
55 public var Map<Type, SMTFunctionDefinition> oldObjectTypePredicates = new HashMap
56
57 public var SMTEnumeratedTypeDeclaration newObjectTypes
58 public var Map<Type, SMTEnumLiteral> newObjectTypeMap = new HashMap
59 public var SMTFunctionDeclaration newObjectTypeFunction
60 public var Map<Type, SMTFunctionDefinition> newObjectTypePredicates = new HashMap
61
62 override copy(SMTInput newModel) {
63 val a = this
64 val b = new Logic2Smt_TypeMapperTrace_FilteredTypes
65
66 b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name])
67
68 b.newObjects = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head
69 b.oldObjects = newModel.typeDeclarations.filter[it.name == a.oldObjects.name].head as SMTEnumeratedTypeDeclaration
70 b.elementMap = a.elementMap.copyMap(b.oldObjects.elements,[name])
71
72 b.oldObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head as SMTEnumeratedTypeDeclaration
73 b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name])
74 b.oldObjectTypeFunction = newModel.functionDefinition.filter[it.name == a.oldObjectTypeFunction.name].head
75 b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name])
76
77 b.newObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjectTypes.name].head as SMTEnumeratedTypeDeclaration
78 b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name])
79 b.newObjectTypeFunction = newModel.functionDeclarations.filter[it.name == a.newObjectTypeFunction.name].head
80 b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name])
81
82 return b
83 }
84}
85
86class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
87 val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
88 val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE
89
90 private def toID(List<String> names) {names.join("!") }
91 private def toID(String name) {name.split("\\s+").toID}
92
93 override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) {
94 val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes
95 trace.typeMapperTrace = typeTrace
96 val engine = ViatraQueryEngine.on(new EMFScope(problem))
97
98 val independentTypes = problem.types.filter(TypeDefinition).filter[isIndependentType]
99
100 val connectedTypes = problem.types.filter[!isIndependentType]
101 val connectedElements = problem.elements.filter[!isIndependentElement]
102
103 val connectedTypesWithoutDefintypesWithoutDefinedSupertype = connectedTypes.filter(TypeDeclaration).filter[!hasDefinedSupertype].toList
104 val hasOldElements = !connectedElements.empty
105 val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty
106
107 // 0. map the simple types
108 this.transformIndependentTypes(independentTypes,trace)
109
110 // 1. Has old elements => create supertype for it
111 if(hasOldElements) {
112 this.transformDefinedElements(connectedElements, trace,document)
113 }
114 // 2. Has new types => create a supertype for it
115 if(hasNewElements) {
116 this.transformUndefinedElements(scopes,trace,document)
117 }
118 // 3. Adding type definitions of the types
119 // 3.1: Type definition to old elements
120 if(hasOldElements) {
121 this.transformOldTypes(connectedTypes, connectedElements, trace, document, engine)
122 }
123 // 3.2: Type definition to new elements
124 if(hasNewElements) {
125 this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine);
126 }
127 }
128
129 private def isIndependentType(Type t) {
130 val res = (t instanceof TypeDefinition) && t.supertypes.empty && t.subtypes.empty
131 return res
132 }
133 private def isIndependentElement(DefinedElement e) {
134 val types = e.definedInType
135 return types.size == 1 && types.head.isIndependentType
136 }
137
138 protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace) {
139 for(type: types) {
140 val independentSMTType = createSMTEnumeratedTypeDeclaration => [
141 name = toID(#["oldType",type.name])
142 ]
143 trace.typeTrace.independentClasses.put(type,independentSMTType)
144 for(element : type.elements) {
145 val enumLiteral = createSMTEnumLiteral => [it.name = toID(#["oldElement",element.name])]
146 independentSMTType.elements += enumLiteral
147 trace.typeTrace.elementMap.put(element,enumLiteral)
148 }
149 }
150 }
151
152 protected def transformDefinedElements(Iterable<DefinedElement> oldElements, Logic2SmtMapperTrace trace, SMTInput document) {
153 val List<SMTEnumLiteral> literals = new ArrayList(oldElements.size)
154 for(element : oldElements) {
155 val elementName ='''oldElement «element.name»'''
156 val literal = createSMTEnumLiteral => [name = elementName.toID]
157 literals += literal
158 trace.typeTrace.elementMap.put(element,literal)
159 }
160 trace.typeTrace.oldObjects = createSMTEnumeratedTypeDeclaration =>
161 [name = "oldObjects" it.elements += literals]
162 document.typeDeclarations += trace.typeTrace.oldObjects
163 }
164
165 protected def transformUndefinedElements(TypeScopes scopes, Logic2SmtMapperTrace trace, SMTInput document) {
166 var SMTType newObjects
167 if(scopes.maxNewElements == -1) {
168 newObjects = createSMTSetTypeDeclaration => [
169 name = "newObjects"
170 ]
171 } else {
172 val newElements = new ArrayList(scopes.maxNewElements)
173 for(index : (1..<scopes.maxNewElements+1)) {
174 val literal = createSMTEnumLiteral => [
175 name = #["newElement",index.toString].toID
176 ]
177 newElements += literal
178 }
179 newObjects = createSMTEnumeratedTypeDeclaration => [
180 name = "newObjects"
181 it.elements += newElements
182 ]
183 }
184 trace.typeTrace.newObjects = newObjects
185 document.typeDeclarations += newObjects
186 }
187
188 protected def transformOldTypes(Iterable<Type> oldTypes,Iterable<DefinedElement> oldElements, Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) {
189 val possibleTypeMatcher = PossibleDynamicTypeMatcher.on(engine)
190 val supertypeStarMatcher = SupertypeStarMatcher.on(engine)
191// val possibleTypes = new LinkedList
192// if(hasDefinedElement) possibleTypes += typesWithDefinedSupertype
193// if(hasUndefinedElement) possibleTypes += typesWithoutDefinedSupertype
194// val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract]
195// val possibleConcreteTypes = possibleTypeMatcher.allValuesOfdynamic
196
197 // 3.1.1. cretate a type for old types
198 val possibleConcreteTypeLiterals = new ArrayList()
199 for(possibleConcreteType: oldTypes.filter[!isIsAbstract]) {
200 val typeName = '''oldType «possibleConcreteType.name»'''
201 val literal = createSMTEnumLiteral => [name = typeName.toID]
202 trace.typeTrace.oldObjectTypeMap.put(possibleConcreteType,literal)
203 possibleConcreteTypeLiterals+=literal
204 }
205 val oldObjectTypes = createSMTEnumeratedTypeDeclaration => [
206 it.name = "oldTypes"
207 it.elements += possibleConcreteTypeLiterals
208 ]
209 trace.typeTrace.oldObjectTypes = oldObjectTypes
210 document.typeDeclarations += oldObjectTypes
211
212 // 3.1.2 for each object, create a constant for its possible dynamic type
213 val Map<DefinedElement,SMTFunctionDeclaration> possibleTypesOfElement = new HashMap
214 val Map<DefinedElement,Type> onlyPossibleType = new HashMap
215 for(object: oldElements) {
216 val types = possibleTypeMatcher.getAllValuesOfdynamic(null,object)
217 if(types.size == 1) {
218 onlyPossibleType.put(object,types.head)
219 } else { // including 0 or more than 1
220 // create a constant declaration
221 val typeOfObjectConstant = createSMTFunctionDeclaration => [
222 it.name = toID(#["typeDecisions",toID(object.name)])
223 it.range = createSMTComplexTypeReference => [
224 it.referred = trace.typeTrace.oldObjectTypes
225 ]
226 ]
227 document.functionDeclarations += typeOfObjectConstant
228 possibleTypesOfElement.put(object,typeOfObjectConstant)
229 // add assertions to the constant to select valid values
230 document.assertions += createSMTAssertion => [
231 val options = types.map[type | createSMTEquals => [
232 it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = typeOfObjectConstant]
233 it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = type.lookup(trace.typeTrace.oldObjectTypeMap)]
234 ]]
235 it.value = if(options.empty) {
236 createSMTBoolLiteral => [it.value = false]
237 } else {
238 createSMTOr=>[operands += options]
239 }
240 ]
241 }
242 }
243
244 // 3.1.2 create a function: old elements -> old types
245 val oldTypeFunction = createSMTFunctionDefinition => [
246 it.name = "oldTypeFunction"
247 val o = createSMTSortedVariable => [
248 it.name = "o"
249 it.range= createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects]
250 ]
251 it.parameters += o
252 it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjectTypes]
253 it.value = unfoldITE(oldElements,
254 [createSMTSymbolicValue => [it.symbolicReference = o]],
255 [DefinedElement e | createSMTSymbolicValue => [it.symbolicReference = e.lookup(trace.typeTrace.elementMap)]],
256 [DefinedElement e |
257 if(onlyPossibleType.containsKey(e)) {
258 return createSMTSymbolicValue => [
259 symbolicReference = e.lookup(onlyPossibleType).lookup(trace.typeTrace.oldObjectTypeMap) ]
260 } else {
261 return createSMTSymbolicValue => [
262 symbolicReference = e.lookup(possibleTypesOfElement)
263 ]
264 }
265 ]
266 )
267 ]
268 trace.typeTrace.oldObjectTypeFunction = oldTypeFunction
269 document.functionDefinition += oldTypeFunction
270
271 // 3.1.3 create a predicate for each type: old object -> {true, false}
272 for(oldType: oldTypes) {
273 val oldTypePredicate = createSMTFunctionDefinition
274 oldTypePredicate.name = toID(#["oldTypePredicate",oldType.name.toID])
275 val param = createSMTSortedVariable => [
276 name = "o"
277 range = createSMTComplexTypeReference => [referred = trace.typeTrace.oldObjects]
278 ]
279 oldTypePredicate.parameters += param
280 oldTypePredicate.range = createSMTBoolTypeReference
281 val values = new LinkedList
282 for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(oldType).filter[!isIsAbstract]) {
283 val typeOfO = createSMTSymbolicValue => [
284 it.symbolicReference = oldTypeFunction
285 it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param]
286 ]
287 val valueOfConcreteSupbtype = createSMTSymbolicValue => [
288 it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.oldObjectTypeMap)
289 ]
290 values += createSMTEquals => [
291 it.leftOperand = typeOfO
292 it.rightOperand = valueOfConcreteSupbtype
293 ]
294 }
295 oldTypePredicate.value = createSMTOr=>[it.operands +=values]
296
297 document.functionDefinition += oldTypePredicate
298 trace.typeTrace.oldObjectTypePredicates.put(oldType,oldTypePredicate)
299 }
300 }
301
302 protected def transformNewTypes(
303 Iterable<TypeDeclaration> typesWithoutDefinedSupertype,
304 Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine)
305 {
306 val supertypeStarMatcher = SupertypeStarMatcher.on(engine)
307 val possibleTypes = typesWithoutDefinedSupertype
308 val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract].toList
309
310 // 3.2.1. cretate a type for new types
311 val possibleConcreteTypeLiterals = new ArrayList()
312 for(possibleConcreteType: possibleConcreteTypes) {
313 val typeName = '''newType «possibleConcreteType.name»'''
314 val literal = createSMTEnumLiteral => [name = typeName.toID]
315 trace.typeTrace.newObjectTypeMap.put(possibleConcreteType,literal)
316 possibleConcreteTypeLiterals+=literal
317 }
318 val newObjectTypes = createSMTEnumeratedTypeDeclaration => [
319 it.name = "newTypes"
320 it.elements += possibleConcreteTypeLiterals
321 ]
322 trace.typeTrace.newObjectTypes = newObjectTypes
323 document.typeDeclarations += newObjectTypes
324
325 // 3.2.2 create a function: new elements -> new types
326 val newTypeFunction = createSMTFunctionDeclaration => [
327 it.name = "newTypeFunction"
328 it.parameters += createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects]
329 it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjectTypes]
330 ]
331 trace.typeTrace.newObjectTypeFunction = newTypeFunction
332 document.functionDeclarations += newTypeFunction
333
334 // 3.1.3 create a predicate for each type: new type -> {true, false}
335 for(newType: possibleTypes) {
336 val newTypePredicate = createSMTFunctionDefinition
337 newTypePredicate.name = toID(#["newTypePredicate",newType.name.toID])
338 val param = createSMTSortedVariable => [
339 name = "o"
340 range = createSMTComplexTypeReference => [referred = trace.typeTrace.newObjects]
341 ]
342 newTypePredicate.parameters += param
343 newTypePredicate.range = createSMTBoolTypeReference
344 val values = new LinkedList
345 for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(newType).filter[!isIsAbstract]) {
346 if(possibleConcreteTypes.contains(concreteSupbtype)) {
347 val typeOfO = createSMTSymbolicValue => [
348 it.symbolicReference = newTypeFunction
349 it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param]
350 ]
351 if(!trace.typeTrace.newObjectTypeMap.containsKey(concreteSupbtype)) {
352 println("gebasz")
353 }
354 val valueOfConcreteSupbtype = createSMTSymbolicValue => [
355 it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.newObjectTypeMap)
356 ]
357 values+= createSMTEquals => [
358 it.leftOperand = typeOfO
359 it.rightOperand = valueOfConcreteSupbtype
360 ]
361 }
362 }
363 newTypePredicate.value = createSMTOr=>[it.operands +=values]
364
365 document.functionDefinition += newTypePredicate
366 trace.typeTrace.newObjectTypePredicates.put(newType,newTypePredicate)
367 }
368 }
369
370 private def Logic2Smt_TypeMapperTrace_FilteredTypes getTypeTrace(Logic2SmtMapperTrace trace) {
371 val typeTrace = trace.typeMapperTrace
372 if(typeTrace instanceof Logic2Smt_TypeMapperTrace_FilteredTypes) {
373 return typeTrace
374 } else {
375 throw new IllegalArgumentException('''Unknown trace type: «typeTrace.class.name»''')
376 }
377 }
378
379 private def boolean hasDefinedSupertype(Type type) {
380 if(type instanceof TypeDefinition) {
381 return true
382 } else {
383 if(type.supertypes.empty) return false
384 else return type.supertypes.exists[it.hasDefinedSupertype]
385 }
386 }
387
388 def private <T> SMTTerm unfoldITE(Iterable<T> options, Function0<SMTTerm> input, Function1<T,SMTTerm> conditionOfOption, Function1<T,SMTTerm> outputForOption) {
389 if(options.size == 1) {
390 return outputForOption.apply(options.head)
391 } else {
392 return createSMTITE => [
393 it.condition = createSMTEquals => [
394 leftOperand = input.apply
395 rightOperand = conditionOfOption.apply(options.head)
396 ]
397 it.^if = outputForOption.apply(options.head)
398 it.^else = unfoldITE(options.tail,input,conditionOfOption,outputForOption)
399 ]
400 }
401 }
402
403 override transformSymbolicReference(DefinedElement referred,Logic2SmtMapperTrace trace) {
404 val x = referred.lookup(trace.typeTrace.elementMap)
405 new ComplexSubterm(#[],#[],
406 createSMTSymbolicValue => [it.symbolicReference = x],
407 new TypeDescriptor(x.eContainer as SMTEnumeratedTypeDeclaration)
408 )
409 }
410
411 override transformTypeReference(Type type, Logic2SmtMapperTrace trace) {
412 val list = new ArrayList
413
414 if(trace.typeTrace.oldObjectTypePredicates.containsKey(type)) {
415 list += new TypeConstraint(
416 createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects],
417 [x|createSMTSymbolicValue => [
418 it.symbolicReference = trace.typeTrace.oldObjectTypePredicates.get(type)
419 it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]]
420 )
421 }
422 if(trace.typeTrace.newObjectTypePredicates.containsKey(type)) {
423 list += new TypeConstraint(
424 createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects],
425 [x|createSMTSymbolicValue => [
426 it.symbolicReference = trace.typeTrace.newObjectTypePredicates.get(type)
427 it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]]
428 )
429 }
430 if(trace.typeTrace.independentClasses.containsKey(type)) {
431 list += new TypeConstraint(
432 createSMTComplexTypeReference => [it.referred = type.lookup(trace.typeTrace.independentClasses)],
433 null
434 )
435 }
436
437 if(list.empty) throw new AssertionError('''Typereference to type is «type.name» empty''')
438 if(list.exists[it.type == null]){
439 throw new AssertionError('''Typereference to null!''')
440 }
441 return list
442 }
443
444 override getTypeInterpretation(LogicProblem problem, SMTDocument document, SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) {
445 val model = document.output.getModelResult as SMTModelResult
446 val newTypeDec = trace.typeTrace.newObjects
447 var List<ValueType> newElements = null
448
449 if(newTypeDec instanceof SMTSetTypeDeclaration) {
450 val newElementType = model.typeDefinitions.filter[
451 (it.type as SMTComplexTypeReference).referred == newTypeDec
452 ].head
453 newElements = newElementType.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it.symbolicReference)]
454 } else if(newTypeDec instanceof SMTEnumeratedTypeDeclaration) {
455 newElements = newTypeDec.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it)]
456 } else throw new IllegalArgumentException('''Unknown type : «newTypeDec.class.name»''')
457
458 val Map<DefinedElement, ValueType> logic2smt = new HashMap<DefinedElement,ValueType>
459 val Map<SMTSymbolicDeclaration, DefinedElement> smt2logic = new HashMap<SMTSymbolicDeclaration,DefinedElement>
460
461 var index = 1;
462 for(newElement : newElements) {
463 val n = '''new «index++»'''
464 val logic = factory2.createDefinedElement => [it.name = n]
465 logic2smt.put(logic,newElement)
466 smt2logic.put(newElement.value as SMTSymbolicDeclaration,logic)
467 }
468 for(oldElement : problem.elements) {
469 val declaration = trace.typeTrace.oldObjectTypeMap.get(oldElement)
470 logic2smt.put(oldElement,new ValueType(new TypeDescriptor(trace.typeTrace.oldObjects),declaration))
471 smt2logic.put(declaration,oldElement)
472 }
473
474 val engine = ViatraQueryEngine.on(new EMFScope(problem))
475 val supertypeStarMatcher = SupertypeStarMatcher.on(engine)
476
477 val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet +
478 trace.typeTrace.newObjectTypeMap.keySet)
479 .toInvertedMap[new LinkedList<DefinedElement>]
480
481 val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse
482 for(oldElement: trace.typeTrace.elementMap.values) {
483 val type = interpretation.queryEngine.resolveFunctionDefinition(
484 trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral
485 val dynamicType = type.lookup(inverseOldTypeMap)
486 val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
487 supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)]
488 }
489
490 val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse
491 for(newElement: newElements.map[value as SMTSymbolicDeclaration]) {
492 val type = interpretation.queryEngine.resolveFunctionDeclaration(
493 trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral
494 val dynamicType = type.lookup(inverseNewTypeMap)
495 val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
496 supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)]
497 }
498
499 return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic)
500 }
501} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 08:36:46 +0000