1 files changed, 98 insertions, 31 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
index c9bafa6c..2796e077 100644
--- 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
@@ -27,8 +27,10 @@ import java.util.HashMap
 import java.util.LinkedList
 import java.util.List
 import java.util.Map
+import org.eclipse.emf.ecore.EObject
 import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
 import org.eclipse.viatra.query.runtime.emf.EMFScope
+import org.eclipse.xtext.EcoreUtil2
 import org.eclipse.xtext.xbase.lib.Functions.Function0
 import org.eclipse.xtext.xbase.lib.Functions.Function1
@@ -63,32 +65,77 @@ class Logic2Smt_TypeMapperTrace_FilteredTypes implements Logic2Smt_TypeMapperTra
                val a = this
                val b = new Logic2Smt_TypeMapperTrace_FilteredTypes
                
-                b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name])
+                b.independentClasses = copyMap(a.independentClasses,newModel.typeDeclarations,[name])
-                
+                b.independentClasses.values.validate(newModel)
-                b.newObjects = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head
+                b.newObjects = newModel.typeDeclarations.copyValue(a.newObjects,[name])
-                b.oldObjects = newModel.typeDeclarations.filter[it.name == a.oldObjects.name].head as SMTEnumeratedTypeDeclaration
+                b.newObjects.validate(newModel)
-                b.elementMap = a.elementMap.copyMap(b.oldObjects.elements,[name])
+                b.oldObjects = newModel.typeDeclarations.copyValue(a.oldObjects,[name]) as SMTEnumeratedTypeDeclaration
+                b.oldObjects.validate(newModel)
+                b.elementMap = a.elementMap.copyMap(
+                        newModel.typeDeclarations
+                                .filter(SMTEnumeratedTypeDeclaration)
+                                .map[it.elements]
+                                .flatten,
+                        [name]
+                )
+                b.elementMap.values.validate(newModel)
                
-                b.oldObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head as SMTEnumeratedTypeDeclaration
+                b.oldObjectTypes = newModel.typeDeclarations.copyValue(a.newObjects,[name]) as SMTEnumeratedTypeDeclaration
+                b.oldObjectTypes.validate(newModel)
                b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name])
-                b.oldObjectTypeFunction = newModel.functionDefinition.filter[it.name == a.oldObjectTypeFunction.name].head
+                b.oldObjectTypeMap.values.validate(newModel)
+                b.oldObjectTypeFunction = newModel.functionDefinition.copyValue(a.oldObjectTypeFunction,[name])
+                b.oldObjectTypeFunction.validate(newModel)
                b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name])
+                b.oldObjectTypePredicates.values.validate(newModel)
                
-                b.newObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjectTypes.name].head as SMTEnumeratedTypeDeclaration
+                b.newObjectTypes = newModel.typeDeclarations.copyValue(a.newObjectTypes,[name]) as SMTEnumeratedTypeDeclaration
+                b.newObjectTypes.validate(newModel)
                b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name])
-                b.newObjectTypeFunction = newModel.functionDeclarations.filter[it.name == a.newObjectTypeFunction.name].head
+                b.newObjectTypeMap.values.validate(newModel)
+                b.newObjectTypeFunction = newModel.functionDeclarations.copyValue(a.newObjectTypeFunction,[name])
+                b.newObjectTypeFunction.validate(newModel)
                b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name])
-                
+                b.newObjectTypePredicates.values.validate(newModel)
                return b
        }
+        
+        def public static <Type, ValueType> copyValue(Iterable<? extends Type> collection, Type target, Function1<Type,ValueType> extractor) {
+                if(target===null) {
+                        return null
+                } else {
+                        val targetValue = extractor.apply(target)
+                        val res = collection.filter[extractor.apply(it)==targetValue].head
+                        return res
+                }
+        }
+        
+        def validate(EObject element, EObject other) {
+                if(element != null) {
+                        val headOfElement = EcoreUtil2.getContainerOfType(element,SMTDocument)
+                        val expectedHeadOfElement = EcoreUtil2.getContainerOfType(other,SMTDocument)
+                        if(headOfElement !== expectedHeadOfElement) {
+                                throw new AssertionError('''
+                                Element in different resource: «element»
+                                Expected root: «expectedHeadOfElement»
+                                Found root: «headOfElement»''')
+                        }
+                }
+        }
+        def validate(Iterable<? extends EObject> iterable, EObject root) {
+                if(iterable !== null)
+                        for(element : iterable) {
+                                element.validate(root)
+                        }
+        }
 }
 class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
        val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
        val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE
        
-        private def toID(List<String> names) {names.join("!") }
+        private def String toID(List<String> names) { names.map[split("\\s+").join("!")].join("!") }
-        private def toID(String name) {name.split("\\s+").toID}
+        private def String toID(String name) { name.split("\\s+").join("!")}
        
        override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) {
                val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes
@@ -105,7 +152,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
                val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty
                
                // 0. map the simple types
-                this.transformIndependentTypes(independentTypes,trace)
+                this.transformIndependentTypes(independentTypes,trace,document)
                
                // 1. Has old elements => create supertype for it
                if(hasOldElements) {
@@ -135,7 +182,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
                return types.size == 1 && types.head.isIndependentType
        }
        
-        protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace) {
+        protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace, SMTInput document) {
                for(type: types) {
                        val independentSMTType = createSMTEnumeratedTypeDeclaration => [
                                name = toID(#["oldType",type.name])
@@ -146,6 +193,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
                                independentSMTType.elements += enumLiteral
                                trace.typeTrace.elementMap.put(element,enumLiteral)
                        }
+                        document.typeDeclarations += independentSMTType
                }
        }
        
@@ -474,26 +522,45 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
                val engine = ViatraQueryEngine.on(new EMFScope(problem))
                val supertypeStarMatcher = SupertypeStarMatcher.on(engine)
                
-                val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet +
+                val Map<Type,List<DefinedElement>> type2Elements = new HashMap
-                                                        trace.typeTrace.newObjectTypeMap.keySet)
+                for(key : problem.types) {
-                                                        .toInvertedMap[new LinkedList<DefinedElement>]
+                        type2Elements.put(key,new LinkedList<DefinedElement>)
+                }
                
-                val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse
+                if(trace.typeTrace.independentClasses != null) {
-                for(oldElement: trace.typeTrace.elementMap.values) {
+                        for(type : trace.typeTrace.independentClasses.keySet) {
-                        val type = interpretation.queryEngine.resolveFunctionDefinition(
+                                if(type instanceof TypeDefinition) {
-                                trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral
+                                        type.lookup(type2Elements).addAll(type.elements)
-                        val dynamicType = type.lookup(inverseOldTypeMap)
+                                } else {
-                        val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
+                                        throw new AssertionError('''Independent classes are type definitions, but got: "«type»"''')
-                        supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)]
+                                }
+                        }
                }
                
-                val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse
+                if(trace.typeTrace.oldObjectTypeFunction != null) {
-                for(newElement: newElements.map[value as SMTSymbolicDeclaration]) {
+                        val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse
-                        val type = interpretation.queryEngine.resolveFunctionDeclaration(
+                        for(oldElement: trace.typeTrace.elementMap.values) {
-                                trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral
+                                val type = interpretation.queryEngine.resolveFunctionDefinition(
-                        val dynamicType = type.lookup(inverseNewTypeMap)
+                                        trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral
-                        val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
+                                val dynamicType = type.lookup(inverseOldTypeMap)
-                        supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)]
+                                val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
+                                for(superType : supertypes) {
+                                        superType.lookup(type2Elements) += oldElement.lookup(smt2logic)
+                                }
+                        }
+                }
+                
+                if(trace.typeTrace.newObjectTypeFunction !== null) {
+                        val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse
+                        for(newElement: newElements.map[value as SMTSymbolicDeclaration]) {
+                                val type = interpretation.queryEngine.resolveFunctionDeclaration(
+                                        trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral
+                                val dynamicType = type.lookup(inverseNewTypeMap)
+                                val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
+                                for(superType : supertypes) {
+                                        superType.lookup(type2Elements) += newElement.lookup(smt2logic)
+                                }
+                        }
                }
                
                return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic)

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 index c9bafa6c..2796e077 100644 --- 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
@@ -27,8 +27,10 @@ import java.util.HashMap
27	import java.util.LinkedList	27	import java.util.LinkedList
28	import java.util.List	28	import java.util.List
29	import java.util.Map	29	import java.util.Map
		30	import org.eclipse.emf.ecore.EObject
30	import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine	31	import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
31	import org.eclipse.viatra.query.runtime.emf.EMFScope	32	import org.eclipse.viatra.query.runtime.emf.EMFScope
		33	import org.eclipse.xtext.EcoreUtil2
32	import org.eclipse.xtext.xbase.lib.Functions.Function0	34	import org.eclipse.xtext.xbase.lib.Functions.Function0
33	import org.eclipse.xtext.xbase.lib.Functions.Function1	35	import org.eclipse.xtext.xbase.lib.Functions.Function1
34		36
@@ -63,32 +65,77 @@ class Logic2Smt_TypeMapperTrace_FilteredTypes implements Logic2Smt_TypeMapperTra
63	val a = this	65	val a = this
64	val b = new Logic2Smt_TypeMapperTrace_FilteredTypes	66	val b = new Logic2Smt_TypeMapperTrace_FilteredTypes
65		67
66	b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name])	68	b.independentClasses = copyMap(a.independentClasses,newModel.typeDeclarations,[name])
67		69	b.independentClasses.values.validate(newModel)
68	b.newObjects = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head	70	b.newObjects = newModel.typeDeclarations.copyValue(a.newObjects,[name])
69	b.oldObjects = newModel.typeDeclarations.filter[it.name == a.oldObjects.name].head as SMTEnumeratedTypeDeclaration	71	b.newObjects.validate(newModel)
70	b.elementMap = a.elementMap.copyMap(b.oldObjects.elements,[name])	72	b.oldObjects = newModel.typeDeclarations.copyValue(a.oldObjects,[name]) as SMTEnumeratedTypeDeclaration
		73	b.oldObjects.validate(newModel)
		74	b.elementMap = a.elementMap.copyMap(
		75	newModel.typeDeclarations
		76	.filter(SMTEnumeratedTypeDeclaration)
		77	.map[it.elements]
		78	.flatten,
		79	[name]
		80	)
		81	b.elementMap.values.validate(newModel)
71		82
72	b.oldObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head as SMTEnumeratedTypeDeclaration	83	b.oldObjectTypes = newModel.typeDeclarations.copyValue(a.newObjects,[name]) as SMTEnumeratedTypeDeclaration
		84	b.oldObjectTypes.validate(newModel)
73	b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name])	85	b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name])
74	b.oldObjectTypeFunction = newModel.functionDefinition.filter[it.name == a.oldObjectTypeFunction.name].head	86	b.oldObjectTypeMap.values.validate(newModel)
		87	b.oldObjectTypeFunction = newModel.functionDefinition.copyValue(a.oldObjectTypeFunction,[name])
		88	b.oldObjectTypeFunction.validate(newModel)
75	b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name])	89	b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name])
		90	b.oldObjectTypePredicates.values.validate(newModel)
76		91
77	b.newObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjectTypes.name].head as SMTEnumeratedTypeDeclaration	92	b.newObjectTypes = newModel.typeDeclarations.copyValue(a.newObjectTypes,[name]) as SMTEnumeratedTypeDeclaration
		93	b.newObjectTypes.validate(newModel)
78	b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name])	94	b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name])
79	b.newObjectTypeFunction = newModel.functionDeclarations.filter[it.name == a.newObjectTypeFunction.name].head	95	b.newObjectTypeMap.values.validate(newModel)
		96	b.newObjectTypeFunction = newModel.functionDeclarations.copyValue(a.newObjectTypeFunction,[name])
		97	b.newObjectTypeFunction.validate(newModel)
80	b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name])	98	b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name])
81		99	b.newObjectTypePredicates.values.validate(newModel)
82	return b	100	return b
83	}	101	}
		102
		103	def public static <Type, ValueType> copyValue(Iterable<? extends Type> collection, Type target, Function1<Type,ValueType> extractor) {
		104	if(target===null) {
		105	return null
		106	} else {
		107	val targetValue = extractor.apply(target)
		108	val res = collection.filter[extractor.apply(it)==targetValue].head
		109	return res
		110	}
		111	}
		112
		113	def validate(EObject element, EObject other) {
		114	if(element != null) {
		115	val headOfElement = EcoreUtil2.getContainerOfType(element,SMTDocument)
		116	val expectedHeadOfElement = EcoreUtil2.getContainerOfType(other,SMTDocument)
		117	if(headOfElement !== expectedHeadOfElement) {
		118	throw new AssertionError('''
		119	Element in different resource: «element»
		120	Expected root: «expectedHeadOfElement»
		121	Found root: «headOfElement»''')
		122	}
		123	}
		124	}
		125	def validate(Iterable<? extends EObject> iterable, EObject root) {
		126	if(iterable !== null)
		127	for(element : iterable) {
		128	element.validate(root)
		129	}
		130	}
84	}	131	}
85		132
86	class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {	133	class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
87	val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE	134	val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
88	val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE	135	val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE
89		136
90	private def toID(List<String> names) {names.join("!") }	137	private def String toID(List<String> names) { names.map[split("\\s+").join("!")].join("!") }
91	private def toID(String name) {name.split("\\s+").toID}	138	private def String toID(String name) { name.split("\\s+").join("!")}
92		139
93	override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) {	140	override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) {
94	val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes	141	val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes
@@ -105,7 +152,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
105	val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty	152	val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty
106		153
107	// 0. map the simple types	154	// 0. map the simple types
108	this.transformIndependentTypes(independentTypes,trace)	155	this.transformIndependentTypes(independentTypes,trace,document)
109		156
110	// 1. Has old elements => create supertype for it	157	// 1. Has old elements => create supertype for it
111	if(hasOldElements) {	158	if(hasOldElements) {
@@ -135,7 +182,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
135	return types.size == 1 && types.head.isIndependentType	182	return types.size == 1 && types.head.isIndependentType
136	}	183	}
137		184
138	protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace) {	185	protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace, SMTInput document) {
139	for(type: types) {	186	for(type: types) {
140	val independentSMTType = createSMTEnumeratedTypeDeclaration => [	187	val independentSMTType = createSMTEnumeratedTypeDeclaration => [
141	name = toID(#["oldType",type.name])	188	name = toID(#["oldType",type.name])
@@ -146,6 +193,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
146	independentSMTType.elements += enumLiteral	193	independentSMTType.elements += enumLiteral
147	trace.typeTrace.elementMap.put(element,enumLiteral)	194	trace.typeTrace.elementMap.put(element,enumLiteral)
148	}	195	}
		196	document.typeDeclarations += independentSMTType
149	}	197	}
150	}	198	}
151		199
@@ -474,26 +522,45 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
474	val engine = ViatraQueryEngine.on(new EMFScope(problem))	522	val engine = ViatraQueryEngine.on(new EMFScope(problem))
475	val supertypeStarMatcher = SupertypeStarMatcher.on(engine)	523	val supertypeStarMatcher = SupertypeStarMatcher.on(engine)
476		524
477	val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet +	525	val Map<Type,List<DefinedElement>> type2Elements = new HashMap
478	trace.typeTrace.newObjectTypeMap.keySet)	526	for(key : problem.types) {
479	.toInvertedMap[new LinkedList<DefinedElement>]	527	type2Elements.put(key,new LinkedList<DefinedElement>)
		528	}
480		529
481	val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse	530	if(trace.typeTrace.independentClasses != null) {
482	for(oldElement: trace.typeTrace.elementMap.values) {	531	for(type : trace.typeTrace.independentClasses.keySet) {
483	val type = interpretation.queryEngine.resolveFunctionDefinition(	532	if(type instanceof TypeDefinition) {
484	trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral	533	type.lookup(type2Elements).addAll(type.elements)
485	val dynamicType = type.lookup(inverseOldTypeMap)	534	} else {
486	val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)	535	throw new AssertionError('''Independent classes are type definitions, but got: "«type»"''')
487	supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)]	536	}
		537	}
488	}	538	}
489		539
490	val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse	540	if(trace.typeTrace.oldObjectTypeFunction != null) {
491	for(newElement: newElements.map[value as SMTSymbolicDeclaration]) {	541	val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse
492	val type = interpretation.queryEngine.resolveFunctionDeclaration(	542	for(oldElement: trace.typeTrace.elementMap.values) {
493	trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral	543	val type = interpretation.queryEngine.resolveFunctionDefinition(
494	val dynamicType = type.lookup(inverseNewTypeMap)	544	trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral
495	val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)	545	val dynamicType = type.lookup(inverseOldTypeMap)
496	supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)]	546	val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
		547	for(superType : supertypes) {
		548	superType.lookup(type2Elements) += oldElement.lookup(smt2logic)
		549	}
		550	}
		551	}
		552
		553	if(trace.typeTrace.newObjectTypeFunction !== null) {
		554	val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse
		555	for(newElement: newElements.map[value as SMTSymbolicDeclaration]) {
		556	val type = interpretation.queryEngine.resolveFunctionDeclaration(
		557	trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral
		558	val dynamicType = type.lookup(inverseNewTypeMap)
		559	val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
		560	for(superType : supertypes) {
		561	superType.lookup(type2Elements) += newElement.lookup(smt2logic)
		562	}
		563	}
497	}	564	}
498		565
499	return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic)	566	return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic)