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 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import java.util.HashMap
+import java.util.Map
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import java.util.List
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.viatra.query.runtime.emf.EMFScope
+class Logic2Smt_TypeMapperTrace_FilteredTypesSimple implements Logic2Smt_TypeMapperTrace{
+        public var Map<Type, SMTType> independentClasses = new HashMap
+        /**
+         * SMT type for the new objects
+         */
+        public var SMTEnumeratedTypeDeclaration objects
+        /**
+         * existing element -> SMT literal map
+         */
+        public var Map<DefinedElement, SMTEnumLiteral> elementMap = new HashMap
+        
+        public var SMTEnumeratedTypeDeclaration objectTypes
+        public var Map<Type, SMTEnumLiteral> objectTypeMap = new HashMap
+        public var SMTFunctionDefinition objectTypeFunction
+        public var Map<Type, SMTFunctionDefinition> objectTypePredicates = new HashMap
+        
+        override copy(SMTInput newModel) {
+                val a = this
+                val b = new Logic2Smt_TypeMapperTrace_FilteredTypesSimple
+                
+                b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name])
+                
+                b.objects = newModel.typeDeclarations.filter[it.name == a.objects.name].head as SMTEnumeratedTypeDeclaration
+                b.elementMap = a.elementMap.copyMap(b.objects.elements,[name])
+                
+                b.objectTypes = newModel.typeDeclarations.filter[it.name == a.objects.name].head as SMTEnumeratedTypeDeclaration
+                b.objectTypeMap = a.objectTypeMap.copyMap(b.objectTypes.elements,[name])
+                b.objectTypeFunction = newModel.functionDefinition.filter[it.name == a.objectTypeFunction.name].head
+                b.objectTypePredicates = a.objectTypePredicates.copyMap(newModel.functionDefinition,[name])
+                
+                return b
+        }
+}
+class Logic2Smt_TypeMapper_FilteredTypesSimple  implements Logic2Smt_TypeMapper{
+        val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
+        val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE
+        
+        private def toID(List<String> names) {names.join("!") }
+        private def toID(String name) {name.split("\\s+").toID}
+        
+        override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) {
+                val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes
+                trace.typeMapperTrace = typeTrace
+                val engine = ViatraQueryEngine.on(new EMFScope(problem))
+                
+                val independentTypes = problem.types.filter(TypeDefinition).filter[isIndependentType]
+                
+                val connectedTypes = problem.types.filter[!isIndependentType]
+                val connectedElements = problem.elements.filter[!isIndependentElement]
+                
+                // 0. map the simple types
+                this.transformIndependentTypes(independentTypes,trace)
+                
+                // 1. Has old elements => create supertype for it
+                
+                this.transformDefinedElements(connectedElements, trace,document)
+                this.transformUndefinedElements(scopes,trace,document)
+                
+                this.transforTypes(connectedTypes, connectedElements, trace, document, engine)
+                // 3.2: Type definition to new elements
+                if(hasNewElements) {
+                        this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine);
+                }
+        }
+        
+        private def isIndependentType(Type t) {
+                val res = (t instanceof TypeDefinition) && t.supertypes.empty && t.subtypes.empty
+                return res
+        }
+        private def isIndependentElement(DefinedElement e) {
+                val types = e.definedInType
+                return types.size == 1 && types.head.isIndependentType
+        }
+        
+        protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace) {
+                for(type: types) {
+                        val independentSMTType = createSMTEnumeratedTypeDeclaration => [
+                                name = toID(#["oldType",type.name])
+                        ]
+                        trace.typeTrace.independentClasses.put(type,independentSMTType)
+                        for(element : type.elements) {
+                                val enumLiteral = createSMTEnumLiteral => [it.name = toID(#["oldElement",element.name])]
+                                independentSMTType.elements += enumLiteral
+                                trace.typeTrace.elementMap.put(element,enumLiteral)
+                        }
+                }
+        }
+        
+        protected def transformDefinedElements(Iterable<DefinedElement> oldElements, Logic2SmtMapperTrace trace, SMTInput document) {
+                val List<SMTEnumLiteral> literals = new ArrayList(oldElements.size)
+                for(element : oldElements) {
+                        val elementName ='''oldElement «element.name»'''
+                        val literal = createSMTEnumLiteral => [name = elementName.toID]
+                        literals += literal
+                        trace.typeTrace.elementMap.put(element,literal)
+                }
+                trace.typeTrace.oldObjects = createSMTEnumeratedTypeDeclaration =>
+                        [name = "oldObjects" it.elements += literals]
+                document.typeDeclarations += trace.typeTrace.oldObjects
+        }
+        
+        protected def transformUndefinedElements(TypeScopes scopes, Logic2SmtMapperTrace trace, SMTInput document) {
+                var SMTType newObjects
+                if(scopes.maxNewElements == -1) {
+                        newObjects = createSMTSetTypeDeclaration => [
+                                name = "newObjects"
+                        ]
+                } else {
+                        val newElements = new ArrayList(scopes.maxNewElements)
+                        for(index : (1..<scopes.maxNewElements+1)) {
+                                val literal = createSMTEnumLiteral => [
+                                        name = #["newElement",index.toString].toID
+                                ]
+                                newElements += literal
+                        }
+                        newObjects = createSMTEnumeratedTypeDeclaration => [
+                                name = "newObjects"
+                                it.elements += newElements
+                        ]
+                }
+                trace.typeTrace.newObjects = newObjects
+                document.typeDeclarations += newObjects
+        }
+        
+        protected def transformOldTypes(Iterable<Type> oldTypes,Iterable<DefinedElement> oldElements, Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) {
+                val possibleTypeMatcher = PossibleDynamicTypeMatcher.on(engine)
+                val supertypeStarMatcher = SupertypeStarMatcher.on(engine)
+//              val possibleTypes = new LinkedList
+//              if(hasDefinedElement) possibleTypes += typesWithDefinedSupertype
+//              if(hasUndefinedElement) possibleTypes += typesWithoutDefinedSupertype
+//              val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract]
+//              val possibleConcreteTypes = possibleTypeMatcher.allValuesOfdynamic
+                
+                // 3.1.1. cretate a type for old types
+                val possibleConcreteTypeLiterals = new ArrayList()
+                for(possibleConcreteType: oldTypes.filter[!isIsAbstract]) {
+                        val typeName = '''oldType «possibleConcreteType.name»'''
+                        val literal = createSMTEnumLiteral => [name = typeName.toID]
+                        trace.typeTrace.oldObjectTypeMap.put(possibleConcreteType,literal)
+                        possibleConcreteTypeLiterals+=literal
+                }
+                val oldObjectTypes = createSMTEnumeratedTypeDeclaration => [
+                        it.name = "oldTypes"
+                        it.elements += possibleConcreteTypeLiterals
+                ]
+                trace.typeTrace.oldObjectTypes = oldObjectTypes
+                document.typeDeclarations += oldObjectTypes
+                
+                // 3.1.2 for each object, create a constant for its possible dynamic type
+                val Map<DefinedElement,SMTFunctionDeclaration> possibleTypesOfElement = new HashMap
+                val Map<DefinedElement,Type> onlyPossibleType = new HashMap
+                for(object: oldElements) {
+                        val types = possibleTypeMatcher.getAllValuesOfdynamic(null,object)
+                        if(types.size == 1) {
+                                onlyPossibleType.put(object,types.head)
+                        } else { // including 0 or more than 1
+                                // create a constant declaration
+                                val typeOfObjectConstant = createSMTFunctionDeclaration => [
+                                        it.name = toID(#["typeDecisions",toID(object.name)])
+                                        it.range = createSMTComplexTypeReference => [
+                                                it.referred = trace.typeTrace.oldObjectTypes
+                                        ]
+                                ]
+                                document.functionDeclarations += typeOfObjectConstant
+                                possibleTypesOfElement.put(object,typeOfObjectConstant)
+                                // add assertions to the constant to select valid values
+                                document.assertions += createSMTAssertion => [
+                                        val options = types.map[type | createSMTEquals => [
+                                                it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = typeOfObjectConstant]
+                                                it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = type.lookup(trace.typeTrace.oldObjectTypeMap)]
+                                        ]]
+                                        it.value = if(options.empty) {
+                                                createSMTBoolLiteral => [it.value = false]
+                                        } else {
+                                                createSMTOr=>[operands += options]
+                                        }
+                                ]
+                        }
+                }
+                
+                // 3.1.2 create a function: old elements -> old types
+                val oldTypeFunction = createSMTFunctionDefinition => [
+                        it.name = "oldTypeFunction"
+                        val o = createSMTSortedVariable => [
+                                it.name = "o"
+                                it.range= createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects] 
+                        ]
+                        it.parameters += o
+                        it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjectTypes]
+                        it.value = unfoldITE(oldElements,
+                                [createSMTSymbolicValue => [it.symbolicReference = o]],
+                                [DefinedElement e | createSMTSymbolicValue => [it.symbolicReference = e.lookup(trace.typeTrace.elementMap)]],
+                                [DefinedElement e |
+                                        if(onlyPossibleType.containsKey(e)) {
+                                                return createSMTSymbolicValue => [
+                                                        symbolicReference = e.lookup(onlyPossibleType).lookup(trace.typeTrace.oldObjectTypeMap) ]
+                                        } else {
+                                                return createSMTSymbolicValue => [
+                                                        symbolicReference = e.lookup(possibleTypesOfElement)
+                                                ]
+                                        }
+                                ]
+                        )
+                ]
+                trace.typeTrace.oldObjectTypeFunction = oldTypeFunction
+                document.functionDefinition += oldTypeFunction
+                
+                // 3.1.3 create a predicate for each type: old object -> {true, false}
+                for(oldType: oldTypes) {
+                        val oldTypePredicate = createSMTFunctionDefinition
+                        oldTypePredicate.name = toID(#["oldTypePredicate",oldType.name.toID])
+                        val param = createSMTSortedVariable => [
+                                name = "o"
+                                range = createSMTComplexTypeReference => [referred = trace.typeTrace.oldObjects]
+                        ]
+                        oldTypePredicate.parameters += param
+                        oldTypePredicate.range = createSMTBoolTypeReference
+                        val values = new LinkedList
+                        for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(oldType).filter[!isIsAbstract]) {
+                                val typeOfO = createSMTSymbolicValue => [
+                                        it.symbolicReference = oldTypeFunction
+                                        it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param]
+                                ]
+                                val valueOfConcreteSupbtype = createSMTSymbolicValue => [
+                                        it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.oldObjectTypeMap)
+                                ]
+                                values += createSMTEquals => [
+                                        it.leftOperand = typeOfO
+                                        it.rightOperand = valueOfConcreteSupbtype
+                                ]
+                        }
+                        oldTypePredicate.value = createSMTOr=>[it.operands +=values]
+                        
+                        document.functionDefinition += oldTypePredicate
+                        trace.typeTrace.oldObjectTypePredicates.put(oldType,oldTypePredicate)
+                }
+        }
+        
+        protected def transformNewTypes(
+                Iterable<TypeDeclaration> typesWithoutDefinedSupertype,
+                Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine)
+        {
+                val supertypeStarMatcher = SupertypeStarMatcher.on(engine)
+                val possibleTypes = typesWithoutDefinedSupertype
+                val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract].toList
+                
+                // 3.2.1. cretate a type for new types
+                val possibleConcreteTypeLiterals = new ArrayList()
+                for(possibleConcreteType: possibleConcreteTypes) {
+                        val typeName = '''newType «possibleConcreteType.name»'''
+                        val literal = createSMTEnumLiteral => [name = typeName.toID]
+                        trace.typeTrace.newObjectTypeMap.put(possibleConcreteType,literal)
+                        possibleConcreteTypeLiterals+=literal
+                }
+                val newObjectTypes = createSMTEnumeratedTypeDeclaration => [
+                        it.name = "newTypes"
+                        it.elements += possibleConcreteTypeLiterals
+                ]
+                trace.typeTrace.newObjectTypes = newObjectTypes
+                document.typeDeclarations += newObjectTypes
+                
+                // 3.2.2 create a function: new elements -> new types
+                val newTypeFunction = createSMTFunctionDeclaration => [
+                        it.name = "newTypeFunction"
+                        it.parameters += createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects] 
+                        it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjectTypes]
+                ]
+                trace.typeTrace.newObjectTypeFunction = newTypeFunction
+                document.functionDeclarations += newTypeFunction
+                
+                // 3.1.3 create a predicate for each type: new type -> {true, false}
+                for(newType: possibleTypes) {
+                        val newTypePredicate = createSMTFunctionDefinition 
+                        newTypePredicate.name = toID(#["newTypePredicate",newType.name.toID])
+                        val param = createSMTSortedVariable => [
+                                name = "o"
+                                range = createSMTComplexTypeReference => [referred = trace.typeTrace.newObjects]
+                        ]
+                        newTypePredicate.parameters += param
+                        newTypePredicate.range = createSMTBoolTypeReference
+                        val values = new LinkedList
+                        for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(newType).filter[!isIsAbstract]) {
+                                if(possibleConcreteTypes.contains(concreteSupbtype)) {
+                                        val typeOfO = createSMTSymbolicValue => [
+                                                it.symbolicReference = newTypeFunction
+                                                it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param]
+                                        ]
+                                        if(!trace.typeTrace.newObjectTypeMap.containsKey(concreteSupbtype)) {
+                                                println("gebasz")
+                                        }
+                                        val valueOfConcreteSupbtype = createSMTSymbolicValue => [
+                                                it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.newObjectTypeMap)
+                                        ]
+                                        values+= createSMTEquals => [
+                                                it.leftOperand = typeOfO
+                                                it.rightOperand = valueOfConcreteSupbtype
+                                        ]
+                                }
+                        }
+                        newTypePredicate.value = createSMTOr=>[it.operands +=values]
+                        
+                        document.functionDefinition += newTypePredicate
+                        trace.typeTrace.newObjectTypePredicates.put(newType,newTypePredicate)
+                }
+        }
+        
+        private def Logic2Smt_TypeMapperTrace_FilteredTypes getTypeTrace(Logic2SmtMapperTrace trace) {
+                val typeTrace = trace.typeMapperTrace
+                if(typeTrace instanceof Logic2Smt_TypeMapperTrace_FilteredTypes) {
+                        return typeTrace
+                } else {
+                        throw new IllegalArgumentException('''Unknown trace type: «typeTrace.class.name»''')
+                }
+        }
+        
+        private def boolean hasDefinedSupertype(Type type) {
+                if(type instanceof TypeDefinition) {
+                        return true
+                } else {
+                        if(type.supertypes.empty) return false
+                        else return type.supertypes.exists[it.hasDefinedSupertype]
+                }
+        }
+        
+        def private <T> SMTTerm unfoldITE(Iterable<T> options, Function0<SMTTerm> input, Function1<T,SMTTerm> conditionOfOption, Function1<T,SMTTerm> outputForOption) {
+                if(options.size == 1) {
+                        return outputForOption.apply(options.head)
+                } else {
+                        return createSMTITE => [
+                                it.condition = createSMTEquals => [
+                                        leftOperand = input.apply
+                                        rightOperand = conditionOfOption.apply(options.head)
+                                ]
+                                it.^if = outputForOption.apply(options.head)
+                                it.^else = unfoldITE(options.tail,input,conditionOfOption,outputForOption)
+                        ]
+                }
+        }
+        
+        override transformSymbolicReference(DefinedElement referred,Logic2SmtMapperTrace trace) {
+                val x = referred.lookup(trace.typeTrace.elementMap)
+                new ComplexSubterm(#[],#[],
+                        createSMTSymbolicValue => [it.symbolicReference = x],
+                        new TypeDescriptor(x.eContainer as SMTEnumeratedTypeDeclaration)
+                )
+        }
+        
+        override transformTypeReference(Type type, Logic2SmtMapperTrace trace) {
+                val list = new ArrayList
+                
+                if(trace.typeTrace.oldObjectTypePredicates.containsKey(type)) {
+                        list += new TypeConstraint(
+                                createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects],
+                                [x|createSMTSymbolicValue => [
+                                        it.symbolicReference = trace.typeTrace.oldObjectTypePredicates.get(type)
+                                        it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]]
+                        )
+                } 
+                if(trace.typeTrace.newObjectTypePredicates.containsKey(type)) {
+                        list += new TypeConstraint(
+                                createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects],
+                                [x|createSMTSymbolicValue => [
+                                        it.symbolicReference = trace.typeTrace.newObjectTypePredicates.get(type)
+                                        it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]]
+                        )
+                }
+                if(trace.typeTrace.independentClasses.containsKey(type)) {
+                        list += new TypeConstraint(
+                                createSMTComplexTypeReference => [it.referred = type.lookup(trace.typeTrace.independentClasses)],
+                                null
+                        )
+                }
+                
+                if(list.empty) throw new AssertionError('''Typereference to type is «type.name» empty''')
+                if(list.exists[it.type == null]){
+                        throw new AssertionError('''Typereference to null!''')
+                }
+                return list
+        }
+        
+        override getTypeInterpretation(LogicProblem problem, SMTDocument document, SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) {
+                val model = document.output.getModelResult as SMTModelResult
+                val newTypeDec = trace.typeTrace.newObjects
+                var List<ValueType> newElements = null
+                
+                if(newTypeDec instanceof SMTSetTypeDeclaration) {
+                        val newElementType = model.typeDefinitions.filter[
+                                (it.type as SMTComplexTypeReference).referred == newTypeDec
+                        ].head
+                        newElements = newElementType.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it.symbolicReference)]
+                } else if(newTypeDec instanceof SMTEnumeratedTypeDeclaration) {
+                        newElements = newTypeDec.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it)]
+                } else throw new IllegalArgumentException('''Unknown type : «newTypeDec.class.name»''')
+                
+                val Map<DefinedElement, ValueType> logic2smt = new HashMap<DefinedElement,ValueType>
+                val Map<SMTSymbolicDeclaration, DefinedElement> smt2logic = new HashMap<SMTSymbolicDeclaration,DefinedElement>
+                
+                var index = 1;
+                for(newElement : newElements) {
+                        val n = '''new «index++»'''
+                        val logic = factory2.createDefinedElement => [it.name = n]
+                        logic2smt.put(logic,newElement)
+                        smt2logic.put(newElement.value as SMTSymbolicDeclaration,logic)
+                }
+                for(oldElement : problem.elements) {
+                        val declaration = trace.typeTrace.oldObjectTypeMap.get(oldElement)
+                        logic2smt.put(oldElement,new ValueType(new TypeDescriptor(trace.typeTrace.oldObjects),declaration))
+                        smt2logic.put(declaration,oldElement)
+                }
+                
+                val engine = ViatraQueryEngine.on(new EMFScope(problem))
+                val supertypeStarMatcher = SupertypeStarMatcher.on(engine)
+                
+                val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet +
+                                                        trace.typeTrace.newObjectTypeMap.keySet)
+                                                        .toInvertedMap[new LinkedList<DefinedElement>]
+                
+                val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse
+                for(oldElement: trace.typeTrace.elementMap.values) {
+                        val type = interpretation.queryEngine.resolveFunctionDefinition(
+                                trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral
+                        val dynamicType = type.lookup(inverseOldTypeMap)
+                        val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
+                        supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)]
+                }
+                
+                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)
+                        supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)]
+                }
+                
+                return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic)
+        }
+        
+}
+\ No newline at end of file

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