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