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_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.xtend | 501 |
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher | ||
12 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | ||
13 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
14 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral | ||
15 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration | ||
16 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration | ||
17 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
18 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
19 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult | ||
20 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSetTypeDeclaration | ||
21 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration | ||
22 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | ||
23 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType | ||
24 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | ||
25 | import java.util.ArrayList | ||
26 | import java.util.HashMap | ||
27 | import java.util.LinkedList | ||
28 | import java.util.List | ||
29 | import java.util.Map | ||
30 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
31 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
32 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | ||
33 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
34 | |||
35 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
36 | |||
37 | class 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 | |||
86 | class 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 | ||