Migrating Additional projects

author: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
committer: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
commit: 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree: 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner
parent: Initial commit, migrating from SVN (diff)
download: VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
16 files changed, 3113 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_TypeMapperInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend
new file mode 100644
index 00000000..44708f44
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend
@@ -0,0 +1,36 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
+import java.util.List
+import java.util.Map
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2SMT_TypeMapperInterpretation {
+        
+        val Map<Type, ? extends List<DefinedElement>> type2Elements
+        val Map<DefinedElement, ValueType> logic2smt
+        val Map<SMTSymbolicDeclaration, DefinedElement> smt2logic
+        
+        public new(
+                Map<Type, ? extends List<DefinedElement>> type2Elements,
+                Map<DefinedElement, ValueType> logic2smt,
+                Map<SMTSymbolicDeclaration, DefinedElement> smt2logic) {
+                this.type2Elements = type2Elements
+                this.logic2smt = logic2smt
+                this.smt2logic = smt2logic
+        }
+        
+        public def getElements(Type type) {
+                return type2Elements.get(type)
+        }
+        
+        public def ValueType logicElement2Smt(DefinedElement element) {
+                return element.lookup(this.logic2smt)
+        }
+        
+        public def smtElement2Logic(SMTSymbolicDeclaration element) {
+                return element.lookup(this.smt2logic)
+        }
+}
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend
new file mode 100644
index 00000000..aad43716
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend
@@ -0,0 +1,1055 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningTactic
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.LinkedHashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.emf.ecore.util.EcoreUtil
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtext.xbase.lib.Functions.Function0
+import org.eclipse.xtext.xbase.lib.Functions.Function1
+import org.eclipse.xtext.xbase.lib.Functions.Function2
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
+class Logic2SmtMapper{
+        val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
+        val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport
+        @Accessors val Logic2Smt_TypeMapper typeMapper;
+        
+        LogicProblemBuilder b
+        
+        new(Logic2Smt_TypeMapper typeMapper) {
+                this.typeMapper = typeMapper
+        }
+        
+        public def TracedOutput<SMTDocument, Logic2SmtMapperTrace> transformProblem(LogicProblem problem, TypeScopes scope, SMTReasoningTactic strategy) {
+                val documentInput = createSMTInput => [getModelCommand = createSMTGetModelCommand]
+                if(strategy == null) documentInput.satCommand = createSMTSimpleSatCommand
+                else documentInput.satCommand = createSMTComplexSatCommand => [it.method = EcoreUtil.copy(strategy)]
+                
+                val document = createSMTDocument => [input = documentInput]
+                val trace = new Logic2SmtMapperTrace => [
+                        it.forwardMapper = this
+                        it.problem = problem
+                ]
+                // Trafo
+                this.typeMapper.transformTypes(documentInput,problem,trace, scope)
+                problem.functions.filter(FunctionDeclaration).forEach[it.transformFunctionDeclaration(documentInput,trace)]
+                problem.functions.filter(FunctionDefinition) .forEach[it.transformFunctionDefinition(documentInput,trace)]
+                problem.relations.filter(RelationDeclaration).forEach[it.transformRelationDeclaration(documentInput,trace)]
+                problem.relations.filter(RelationDefinition) .forEach[it.transformRelationDefinition(documentInput,trace)]
+                problem.constants.filter(ConstantDeclaration).forEach[it.transformConstantDeclaration(documentInput,trace)]
+                problem.constants.filter(ConstantDefinition) .forEach[it.transformConstantDefinition(documentInput,trace)]
+                
+                problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)]
+                documentInput.assertions += problem.assertions.map[transformAssertion(trace)]
+                // End trafo
+                
+                document.input.assertions.forEach[it.value.nameAllUnnamedVariable]
+                document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable]
+                document.cleanDocument
+                return new TracedOutput(document,trace)
+        }
+        
+        private def toID(String name) {name.split("\\s+").join("!") }
+        
+        private def nameAllUnnamedVariable(SMTTerm root) {
+                var index = 1
+                val unnamedVariables = root.eAllContents.filter(SMTSortedVariable).filter[it.name == null].toList
+                for(unnamedVariable : unnamedVariables) {
+                        unnamedVariable.name = '''var«index++»'''
+                }
+        }
+        
+//      def protected maxIntegerRageDefiniton(SMTInput documentInput) {
+//              val upperlimit = createSMTFunctionDeclaration
+//      }
+        
+        def dispatch protected List<TypeConstraint> transformTypeReference(BoolTypeReference boolTypeReference, Logic2SmtMapperTrace trace) {
+                return #[new TypeConstraint(createSMTBoolTypeReference,null)]
+        }
+        def dispatch protected List<TypeConstraint> transformTypeReference(IntTypeReference intTypeReference, Logic2SmtMapperTrace trace) {
+                return #[new TypeConstraint(createSMTIntTypeReference,null)]
+        }
+        def dispatch protected List<TypeConstraint> transformTypeReference(RealTypeReference realTypeReference, Logic2SmtMapperTrace trace) {
+                return #[new TypeConstraint(createSMTRealTypeReference,null)]
+        }
+        def dispatch protected List<TypeConstraint> transformTypeReference(ComplexTypeReference complexTypeReference, Logic2SmtMapperTrace trace) {
+                return typeMapper.transformTypeReference(complexTypeReference.referred,trace)
+        }
+        
+        ///////////////////////////////////////////////////////
+        // Definitions
+        ///////////////////////////////////////////////////////
+        
+        def transformFunctionDeclaration(FunctionDeclaration function, SMTInput input, Logic2SmtMapperTrace trace) {
+                val parameterTypeCombinations = unfolder.getPermutations(function.parameters.map[x|transformTypeReference(x,trace)])
+                val rangeTypeCombinations = function.range.transformTypeReference(trace)
+                
+                if(rangeTypeCombinations.size == 1) {
+                        val rangeType = rangeTypeCombinations.head
+                        // Map it as function
+                        var index = 1
+                        for(combination : parameterTypeCombinations) {
+                                val nameWithIndex = if (parameterTypeCombinations.size > 1)
+                                        toID('''function «function.name.toID» «index++»''')
+                                else
+                                        toID('''function «function.name.toID»''')
+                                        
+                                createFunctionDeclaration(function,nameWithIndex,combination,rangeType,true, input,trace)
+                        }
+                } else {
+                        // Map it as a relation
+                        var index = 1
+                        for(combination : parameterTypeCombinations) {
+                                val type2function = new HashMap
+                                for(rangeType : rangeTypeCombinations) {
+                                        val nameWithIndex = toID('''function «function.name.toID» «index++»''')
+                                        val f = createFunctionDeclaration(function,nameWithIndex,combination,rangeType,false,input,trace)
+                                        type2function.put(rangeType,f)
+                                }
+                                // for all rangeTypes, there is
+                                // 1. at least one range type that satisfies the relation
+                                input.assertions+=createSMTAssertion => [
+                                        it.value = createSMTForall => [f|
+                                                var paramIndex = 1
+                                                for(param : combination) {
+                                                        val paramName = '''p«paramIndex++»'''
+                                                        val variable = createSMTSortedVariable => [
+                                                                it.name = paramName
+                                                                it.range = param.type
+                                                        ]
+                                                        f.quantifiedVariables += variable
+                                                }
+                                                f.expression = createSMTOr => [
+                                                        operands+=rangeTypeCombinations.map[t|
+                                                                createSMTExists => [
+                                                                        val v = createSMTSortedVariable => [
+                                                                                it.name = "r"
+                                                                                it.range = EcoreUtil.copy(t.type)
+                                                                        ]
+                                                                        it.quantifiedVariables += v
+                                                                        it.expression = createSMTSymbolicValue => [
+                                                                                it.symbolicReference = type2function.get(t)
+                                                                                it.parameterSubstitutions += f.quantifiedVariables.map[fv|
+                                                                                        createSMTSymbolicValue => [it.symbolicReference = fv]
+                                                                                ]
+                                                                                it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = v]       
+                                                                        ]
+                                                                ]
+                                                        ]
+                                                ]
+                                        ]
+                                ]
+                                // 2. at most one range type that satisfies the relation
+                                // TODO a
+                        }
+                }
+        }
+        
+        private def createFunctionDeclaration(
+                Function function,
+                String nameWithIndex,
+                List<TypeConstraint> combination,
+                TypeConstraint rangeType,
+                boolean useFunction,
+                SMTInput input,
+                Logic2SmtMapperTrace trace
+        ) {
+                val smtFunction = if(useFunction) {
+                        createSMTFunctionDeclaration => [
+                                it.name = nameWithIndex
+                                it.parameters += combination.map[it.type]
+                                it.range = rangeType.type
+                        ]
+                } else {
+                        createSMTFunctionDeclaration => [
+                                it.name = nameWithIndex
+                                it.parameters += combination.map[it.type]
+                                it.parameters += rangeType.type
+                                it.range = createSMTBoolTypeReference
+                        ]
+                }
+                
+                val descriptor = new Descriptor<Function>((combination+#[rangeType]).toList.map[
+                        TypeDescriptor.createFromTypeReference(it.type)],function)
+                trace.functionMap.put(descriptor,smtFunction)
+                input.functionDeclarations += smtFunction
+                trace.functionUnfolding.put(function,#[descriptor])
+                
+                if(!useFunction) {
+                        input.assertions += createSMTAssertion => [
+                                it.value = createSMTForall => [f|
+                                        var pi = 0
+                                        for(param : combination) {
+                                                val variable = createSMTSortedVariable
+                                                variable.name = "p"+pi.toString
+                                                variable.range = EcoreUtil.copy(combination.get(pi).type)
+                                                f.quantifiedVariables+=variable
+                                                pi++
+                                        }
+                                        val resultParam1 = createSMTSortedVariable => [
+                                                it.name = "res1"
+                                                it.range = EcoreUtil.copy(rangeType.type)
+                                        ]
+                                        f.quantifiedVariables+=resultParam1
+                                        val resultParam2 = createSMTSortedVariable => [
+                                                it.name = "res2"
+                                                it.range = EcoreUtil.copy(rangeType.type)
+                                        ]
+                                        f.quantifiedVariables+=resultParam2
+                                        f.expression = createSMTImpl => [
+                                                it.leftOperand = createSMTAnd => [
+                                                        it.operands += createSMTSymbolicValue => [
+                                                                it.symbolicReference = smtFunction
+                                                                it.parameterSubstitutions += (0..<combination.size).map[x|
+                                                                        createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]]
+                                                                it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam1]
+                                                        ]
+                                                        it.operands += createSMTSymbolicValue => [
+                                                                it.symbolicReference = smtFunction
+                                                                it.parameterSubstitutions += (0..<combination.size).map[x|
+                                                                        createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]]
+                                                                it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam2]
+                                                        ]
+                                                ]
+                                                it.rightOperand = createSMTEquals => [
+                                                        it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam1]
+                                                        it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam2]
+                                                ]
+                                        ]
+                                ]
+                        ]
+                }
+                
+                if(rangeType.constraint != null) {
+                        input.assertions += createSMTAssertion => [
+                                it.value = createSMTForall => [f|
+                                        var pi = 0
+                                        for(param : combination) {
+                                                val variable = createSMTSortedVariable
+                                                variable.name = "p"+pi.toString
+                                                variable.range = EcoreUtil.copy(combination.get(pi).type)
+                                                f.quantifiedVariables+=variable
+                                                pi++
+                                        }
+                                        val resultParam = createSMTSortedVariable => [
+                                                it.name = "res"
+                                                it.range = EcoreUtil.copy(rangeType.type)
+                                        ]
+                                        f.quantifiedVariables += resultParam
+                                        f.expression = createSMTImpl => [
+                                                it.leftOperand = if(useFunction)
+                                                {
+                                                        createSMTEquals => [
+                                                                leftOperand = createSMTSymbolicValue => [
+                                                                        it.symbolicReference = smtFunction
+                                                                        it.parameterSubstitutions += (0..<combination.size).map[x|
+                                                                                createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]
+                                                                        ]
+                                                                ]
+                                                                rightOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam]
+                                                        ]
+                                                } else {
+                                                        createSMTSymbolicValue => [
+                                                                it.symbolicReference = smtFunction
+                                                                it.parameterSubstitutions += (0..<combination.size).map[x|
+                                                                        createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]]
+                                                                it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam]
+                                                        ]
+                                                }
+                                                it.rightOperand = rangeType.constraint.apply(resultParam)
+                                        ]
+                                ]
+                        ]
+                }
+                return smtFunction
+        }
+        
+        def transformFunctionDefinition(FunctionDefinition function, SMTInput input, Logic2SmtMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        def protected transformRelationDeclaration(RelationDeclaration relation, SMTInput input, Logic2SmtMapperTrace trace) {
+                val parameterTypeCombinations = unfolder.getPermutations(relation.parameters.map[x|transformTypeReference(x,trace)])
+                var relationIndex = 1
+                val unfolding = new ArrayList(parameterTypeCombinations.size)
+                for(parameterTypeCombination : parameterTypeCombinations) {
+                        /// Create a name for the relation
+                        val nameWithIndex = if (parameterTypeCombinations.size > 1)
+                                        toID('''relation «relation.name.toID» «relationIndex++»''')
+                                else
+                                        toID('''relation «relation.name.toID»''')
+                        
+                        // Adding an unfolded relation
+                        val smtRelation = createSMTFunctionDeclaration => [
+                                name = nameWithIndex
+                                parameters+= parameterTypeCombination.map[typeConstraint | EcoreUtil.copy(typeConstraint.type)]
+                                range = createSMTBoolTypeReference
+                        ]
+                        val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[
+                                TypeDescriptor.createFromTypeReference(it.type)],relation)
+                        trace.relationMap.put(descriptor,smtRelation)
+                        input.functionDeclarations += smtRelation
+                        unfolding += descriptor
+                        
+                        // If there is a type constraint
+                        if(parameterTypeCombination.exists[it.constraint != null]) {
+                                // create a constraint that specifies that the relation contains elemenents with the required properties
+                                val and = createSMTAnd
+                                val rel = createSMTSymbolicValue => [it.symbolicReference = smtRelation]
+                                val forall = createSMTForall => [
+                                        it.expression = createSMTImpl => [
+                                                it.leftOperand = rel
+                                                it.rightOperand = and
+                                        ]
+                                ]
+                                var paramIndex = 0
+                                for(param : parameterTypeCombination) {
+                                        val paramName = '''p«paramIndex++»'''
+                                        val variable = createSMTSortedVariable => [
+                                                it.name = paramName
+                                                it.range = param.type
+                                        ]
+                                        forall.quantifiedVariables += variable
+                                        rel.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = variable]
+                                        if(param.constraint != null) {
+                                                and.operands+=param.constraint.apply(variable)
+                                        }
+                                }
+                                input.assertions += createSMTAssertion => [
+                                        it.value = forall
+                                ]
+                        }
+                }
+                trace.relationUnfolding.put(relation,unfolding)
+        }
+        def protected transformRelationDefinition(RelationDefinition relation, SMTInput input, Logic2SmtMapperTrace trace) {
+                val parameterTypeCombinations = unfolder.getPermutations(relation.variables.map[x|transformTypeReference(x.range,trace)]).toList
+                var relationIndex = 1
+                val unfolding = new ArrayList(parameterTypeCombinations.size)
+                for(parameterTypeCombination : parameterTypeCombinations) {
+                        /// Create a name for the relation
+                        val nameWithIndex = if (parameterTypeCombinations.size > 1)
+                                        toID('''relation «relation.name.toID» «relationIndex++»''')
+                                else
+                                        toID('''relation «relation.name.toID»''')
+                        
+                        // creating an unfolded relation
+                        val smtRelation = createSMTFunctionDefinition => [
+                                name = nameWithIndex
+                                range = createSMTBoolTypeReference
+                        ]
+                        /*
+                        // adding variables as parameters
+                        val Map<Variable, SMTSortedVariable> variables = new HashMap
+                        var paramIndex = 0
+                        val constraintList = new LinkedList
+                        for(param : parameterTypeCombination) {
+                                val paramName = relation.variables.get(paramIndex).name.toID
+                                val variable = createSMTSortedVariable => [
+                                        it.name = paramName
+                                        it.range = param.type
+                                ]
+                                
+                                smtRelation.parameters+=variable
+                                variables.put(relation.variables.get(paramIndex),variable)
+                                if(param.constraint != null) {
+                                        constraintList+=param.constraint.apply(variable)
+                                }
+                                paramIndex++
+                        }
+                        val definition = transformTerm(relation.value,trace,variables)
+                        if(constraintList.empty) {
+                                smtRelation.value = definition.expectLogic.value
+                        } else if(constraintList.size == 1) {
+                                smtRelation.value = createSMTAnd => [
+                                        it.operands += constraintList.head
+                                        it.operands += definition.expectLogic.value
+                                ]
+                        } else {
+                                smtRelation.value = createSMTAnd => [
+                                        it.operands += createSMTAnd => [operands += constraintList]
+                                        it.operands += definition.expectLogic.value
+                                ]
+                        }
+                        */
+                        // 
+                        val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[
+                                TypeDescriptor.createFromTypeReference(it.type)],relation)
+                        trace.relationMap.put(descriptor,smtRelation)
+                        input.functionDefinition += smtRelation
+                        unfolding += descriptor
+                }
+                trace.relationUnfolding.put(relation,unfolding)
+        }
+        def transformRelationDefinition_definition(RelationDefinition relation, SMTInput input, Logic2SmtMapperTrace trace) {
+                val parameterTypeCombinations = unfolder.getPermutations(relation.variables.map[x|transformTypeReference(x.range,trace)]).toList
+                for(parameterTypeCombination : parameterTypeCombinations) {
+                        val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[
+                                TypeDescriptor.createFromTypeReference(it.type)],relation)
+                        val smtRelation = descriptor.lookup(trace.relationMap) as SMTFunctionDefinition
+                        
+                        // adding variables as parameters
+                        val Map<Variable, SMTSortedVariable> variables = new HashMap
+                        var paramIndex = 0
+                        val constraintList = new LinkedList
+                        for(param : parameterTypeCombination) {
+                                val paramName = relation.variables.get(paramIndex).name.toID
+                                val variable = createSMTSortedVariable => [
+                                        it.name = paramName
+                                        it.range = param.type
+                                ]
+                                
+                                smtRelation.parameters+=variable
+                                variables.put(relation.variables.get(paramIndex),variable)
+                                if(param.constraint != null) {
+                                        constraintList+=param.constraint.apply(variable)
+                                }
+                                paramIndex++
+                        }
+                        val definition = transformTerm(relation.value,trace,variables)
+                        if(constraintList.empty) {
+                                smtRelation.value = definition.expectLogic.value
+                        } else if(constraintList.size == 1) {
+                                smtRelation.value = createSMTAnd => [
+                                        it.operands += constraintList.head
+                                        it.operands += definition.expectLogic.value
+                                ]
+                        } else {
+                                smtRelation.value = createSMTAnd => [
+                                        it.operands += createSMTAnd => [operands += constraintList]
+                                        it.operands += definition.expectLogic.value
+                                ]
+                        }
+                }
+        }
+        
+        def transformConstantDeclaration(ConstantDeclaration constant,SMTInput input, Logic2SmtMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        def transformConstantDefinition(ConstantDefinition constant, SMTInput input, Logic2SmtMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        
+        def protected SMTAssertion transformAssertion(Assertion assertion, Logic2SmtMapperTrace trace) {
+                val a = assertion.value.transformTerm(trace,emptyMap)
+                createSMTAssertion => [value = a.expectLogic.value]
+        }
+        
+        ///////////////////////////////////////////////////////
+        // Logic -> Logic value transformation
+        ///////////////////////////////////////////////////////
+        
+        ///////////////////////////////////////////////////////
+        // Literals
+        ///////////////////////////////////////////////////////
+        def dispatch protected TransformedSubterm transformTerm(BoolLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                new LogicSubterm(createSMTBoolLiteral => [value = literal.value])       }
+        def dispatch protected TransformedSubterm transformTerm(IntLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables)  {
+                if(literal.value>=0) { new NumericSubterm(#[],#[],createSMTIntLiteral  => [value = literal.value])}
+                else {new NumericSubterm(#[],#[],createSMTMinus => [ leftOperand = (createSMTIntLiteral => [value = - (literal.value) ] ) ]) } }
+        def dispatch protected TransformedSubterm transformTerm(RealLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                new NumericSubterm(#[],#[],createSMTRealLiteral => [value = literal.value])     }
+        
+        ///////////////////////////////////////////////////////
+        // NumericOperators
+        ///////////////////////////////////////////////////////
+        def dispatch protected TransformedSubterm transformTerm(Plus plus, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                return transformBinaryNumericOperator(
+                        plus.leftOperand,plus.rightOperand,
+                        [l,r|createSMTPlus => [ leftOperand = l rightOperand = r ]],
+                        trace,variables)
+        }
+        def dispatch protected TransformedSubterm transformTerm(Minus minus, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                return transformBinaryNumericOperator(
+                        minus.leftOperand,minus.rightOperand,
+                        [l,r|createSMTMinus => [ leftOperand = l rightOperand = r ]],
+                        trace,variables)
+        }
+        def dispatch protected TransformedSubterm transformTerm(Multiply multiply, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                return transformBinaryNumericOperator(
+                        multiply.leftOperand,multiply.rightOperand,
+                        [l,r|createSMTMultiply => [ leftOperand = l rightOperand = r ]],
+                        trace,variables)
+        }
+        def dispatch protected TransformedSubterm transformTerm(Divison div, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                return transformBinaryNumericOperator(
+                        div.leftOperand,div.rightOperand,
+                        [l,r|createSMTDiv => [ leftOperand = l rightOperand = r ]],
+                        trace,variables)
+        }
+        def dispatch protected TransformedSubterm transformTerm(Mod mod, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                return transformBinaryNumericOperator(
+                        mod.leftOperand,mod.rightOperand,
+                        [l,r|createSMTMod => [ leftOperand = l rightOperand = r ]],
+                        trace,variables)
+        }
+        
+        def protected TransformedSubterm transformBinaryNumericOperator(
+                Term leftOperand,
+                Term rightOperand,
+                Function2<SMTTerm,SMTTerm,SMTTerm> combinator,
+                Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables)
+        {
+                val left  = leftOperand. transformTerm(trace,variables).expectNumber.getPossibleValues
+                val right = rightOperand.transformTerm(trace,variables).expectNumber.getPossibleValues
+                val values = new ArrayList(left.size * right.size)
+                for(combination : TransformedSubterm.allCombinations(left,right)) {
+                        val l = combination.get(0)
+                        val r = combination.get(1)
+                        values += new SubtermOption(
+                                #[l,r],#[],#[],
+                                combinator.apply(l.expression, r.expression),
+                                TypeDescriptor.numericTypeDescriptor_Instance
+                        )
+                }
+                return new NumericSubterm(values)
+        }
+        
+        ///////////////////////////////////////////////////////
+        // LogicOperators
+        ///////////////////////////////////////////////////////
+        def dispatch protected TransformedSubterm transformTerm(Not not, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                val operand = not.operand.transformTerm(trace,variables).expectLogic
+                new LogicSubterm(createSMTNot => [operand = operand.value]) }
+        def dispatch protected TransformedSubterm transformTerm(And and, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                transformBinaryLogicOperator2(and.operands,[x|createSMTAnd => [operands += x]],trace,variables) }
+        def dispatch protected TransformedSubterm transformTerm(Or or, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                transformBinaryLogicOperator2(or.operands,[x|createSMTOr => [operands += x]],trace,variables) }
+        def dispatch protected TransformedSubterm transformTerm(Impl impl, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                transformBinaryLogicOperator1(impl.leftOperand,impl.rightOperand,[l,r|createSMTImpl =>[leftOperand = l rightOperand = r]],trace,variables) }
+        def dispatch protected TransformedSubterm transformTerm(Iff iff, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                transformBinaryLogicOperator1(iff.leftOperand,iff.rightOperand,[l,r|createSMTIff => [leftOperand = l rightOperand = r]],trace,variables)}
+        
+        /**
+         * Logic combinator with two values
+         */
+        def protected transformBinaryLogicOperator1(
+                Term leftOperand, Term rightOperand,
+                Function2<SMTTerm,SMTTerm,SMTTerm> combinator,
+                Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                val left = leftOperand.transformTerm(trace,variables).expectLogic
+                val right = rightOperand.transformTerm(trace,variables).expectLogic
+                return new LogicSubterm(combinator.apply(left.value, right.value))
+        }
+        /**
+         * Logic combinator with multiple values
+         */
+        def protected transformBinaryLogicOperator2(
+                Iterable<? extends Term> operands,
+                Function1<Iterable<? extends SMTTerm>,SMTTerm> combinator,
+                Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                val smtOperands = operands.map[transformTerm(trace,variables).expectLogic.value]
+                return new LogicSubterm(combinator.apply(smtOperands))
+        }
+        
+        ///////////////////////////////////////////////////////
+        // Numeric -> Logic
+        ///////////////////////////////////////////////////////
+        def dispatch protected TransformedSubterm transformTerm(MoreThan moreThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                transformNumericComparison(moreThan.leftOperand,moreThan.rightOperand, [l,r|createSMTMT => [ leftOperand = l rightOperand = r ]],trace,variables)}
+        def dispatch protected TransformedSubterm transformTerm(LessThan lessThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                transformNumericComparison(lessThan.leftOperand,lessThan.rightOperand, [l,r|createSMTLT => [ leftOperand = l rightOperand = r ]],trace,variables)}
+        def dispatch protected TransformedSubterm transformTerm(MoreOrEqualThan moreThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                transformNumericComparison(moreThan.leftOperand,moreThan.rightOperand, [l,r|createSMTMEQ => [ leftOperand = l rightOperand = r ]],trace,variables)}
+        def dispatch protected TransformedSubterm transformTerm(LessOrEqualThan lessThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                transformNumericComparison(lessThan.leftOperand,lessThan.rightOperand, [l,r|createSMTLEQ => [ leftOperand = l rightOperand = r ]],trace,variables)}
+        
+        def protected transformNumericComparison(Term leftOperand, Term rightOperand, Function2<SMTTerm,SMTTerm,SMTTerm> combinator, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables){
+                val left = leftOperand.transformTerm(trace,variables).getPossibleValues
+                val right = rightOperand.transformTerm(trace,variables).getPossibleValues
+                val values = new ArrayList(left.size * right.size)
+                for(combination : TransformedSubterm.allCombinations(left,right)) {
+                        val l = combination.get(0)
+                        val r = combination.get(1)
+                        values += LogicSubterm::resolveToLogic(#[l,r],combinator.apply(l.expression, r.expression))
+                }
+                val res = createSMTOr =>[operands += values]
+                return new LogicSubterm(res)
+        }
+        
+        ///////////////////////////////////////////////////////
+        // Equals and Distinct
+        ///////////////////////////////////////////////////////
+        
+        def dispatch protected TransformedSubterm transformTerm(Equals equals, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                val left = equals.leftOperand.transformTerm(trace,variables)
+                val rightX = equals.rightOperand.transformTerm(trace,variables)
+                if(left instanceof LogicSubterm) {
+                        val right = rightX.expectLogic
+                        new LogicSubterm(createSMTEquals => [
+                                leftOperand = left.value
+                                rightOperand = right.value ])
+                } else if(left instanceof NumericSubterm) {
+                        val right = rightX.expectNumber
+                        val leftOperands = left.possibleValues
+                        val rightOperands = right.possibleValues
+                        val values = new ArrayList(leftOperands.size * rightOperands.size)
+                        for(combination : TransformedSubterm.allCombinations(left.possibleValues,right.possibleValues)) {
+                                val l = combination.get(0)
+                                val r = combination.get(1)
+                                values += TransformedSubterm.resolveToLogic(#[l,r],
+                                createSMTEquals => [
+                                        leftOperand = combination.get(0).expression
+                                        rightOperand = combination.get(1).expression])
+                        }
+                        return new LogicSubterm(createSMTOr =>[operands += values])
+                } else if(left instanceof ComplexSubterm){
+                        val right = rightX as ComplexSubterm
+                        
+                        val values = new LinkedList
+                        for(combination : TransformedSubterm.allCombinations(left.possibleValues,right.possibleValues)) {
+                                val l = combination.get(0)
+                                val r = combination.get(1)
+                                if(l.type.complexType == r.type.complexType) {
+                                        values += TransformedSubterm.resolveToLogic(#[l,r],createSMTEquals => [
+                                                leftOperand = l.expression
+                                                rightOperand = r.expression ])
+                                } /*else dont add*/
+                        }
+                        
+                        if(values.size == 0) {
+                                return new LogicSubterm(createSMTBoolLiteral => [it.value = false])
+                        } else if(values.size == 1) {
+                                return new LogicSubterm(values.head)
+                        } else {
+                                return new LogicSubterm(createSMTOr => [operands += values])
+                        }
+                }
+        }
+        
+        def dispatch protected TransformedSubterm transformTerm(Distinct distinct, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                val o = distinct.operands.map[transformTerm(trace,variables)]
+                if(o.empty) {
+                        throw new IllegalArgumentException('''empty distinct''')
+                } else if(o.size == 1) {
+                        // 1 element is always distinct
+                        new LogicSubterm(createSMTBoolLiteral => [it.value = true])
+                } else {
+                        val head = o.head
+                        if(head instanceof LogicSubterm) {
+                                return new LogicSubterm(createSMTDistinct => [
+                                                it.operands += o.map[expectLogic.value]])
+                        } else if(head instanceof NumericSubterm) {
+                                val numbers = o.map[expectNumber.possibleValues]
+                                val distincts = new LinkedList
+                                for(combination : TransformedSubterm.allCombinations(numbers)) {
+                                        distincts += LogicSubterm::resolveToLogic(combination,createSMTDistinct => [operands += combination.map[it.expression]])
+                                }
+                                new LogicSubterm(createSMTOr => [it.operands += distincts])
+                        } else {
+                                val objects = o.map[possibleValues]
+                                val distincts = new LinkedList
+                                for(combination : TransformedSubterm.allCombinations(objects)) {                
+                                        val Map<SMTType,LinkedList<SubtermOption>> type2Terms = new LinkedHashMap;
+                                        for(param:combination) {
+                                                val type = param.type.complexType
+                                                val value = param
+                                                var LinkedList<SubtermOption> list;
+                                                if(type2Terms.containsKey(type)) {
+                                                        list = type2Terms.get(type)
+                                                } else {
+                                                        list = new LinkedList
+                                                        type2Terms.put(type,list)
+                                                }
+                                                list+=value
+                                        }
+                                        
+                                        val groups = type2Terms.values.map[elementList|
+                                                if(elementList.size == 1) return null
+                                                else return LogicSubterm.resolveToLogic(elementList,createSMTDistinct => [it.operands += elementList.map[expression]])
+                                        ].filterNull
+                                        if(groups.empty) {
+                                                // One of the group is trivially satisfied
+                                                return new LogicSubterm(createSMTBoolLiteral => [it.value = true])
+                                        } else {
+                                                val and = createSMTAnd => [operands += groups]
+                                                distincts.add(and)
+                                        }
+                                }
+                                if(distincts.size == 1) {
+                                        return new LogicSubterm(distincts.head)
+                                } else {
+                                        return new LogicSubterm(createSMTOr => [it.operands += distincts])
+                                }
+                        }
+                }
+        }
+        
+        ///////////////////////////////////////////////////////
+        // Quantifiers
+        ///////////////////////////////////////////////////////
+        
+        def dispatch protected TransformedSubterm transformTerm(Forall forall, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                new LogicSubterm(transformQuantifiedExpression(forall,trace,variables,
+                        [createSMTForall],
+                        [q|createSMTAnd=>[operands+=q]],
+                        [precondition,expression|createSMTImpl=>[leftOperand=precondition rightOperand=expression]]))
+        }
+        def dispatch protected TransformedSubterm transformTerm(Exists exists, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                new LogicSubterm(transformQuantifiedExpression(exists,trace,variables,
+                        [createSMTExists],
+                        [q|createSMTOr=>[operands+=q]],
+                        [precondition,expression|createSMTAnd=>[operands+=precondition operands+=expression]]))
+        }
+        
+        def protected SMTTerm transformQuantifiedExpression(
+                QuantifiedExpression q, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables,
+                Function0<SMTQuantifiedExpression> constructor,
+                Function1<Iterable<SMTQuantifiedExpression>,SMTTerm> combinator,
+                Function2<SMTTerm,SMTTerm,SMTTerm> preconditionCombinator
+        ) {
+                val permutations = unfolder.getPermutations(q.quantifiedVariables.map[it.range.transformTypeReference(trace)])
+                val ArrayList<SMTQuantifiedExpression> unfoldedQuantification = new ArrayList(permutations.size)
+                
+                for(permutation : permutations) {
+                        val allVariables = new HashMap(variables)
+                        val newSMTVariables = new ArrayList(q.quantifiedVariables.size)
+                        val typePrecondition = new ArrayList<SMTTerm>(q.quantifiedVariables.size)
+                        
+                        for(variableIndex: 0..<q.quantifiedVariables.size) {
+                                val logicVariable = q.quantifiedVariables.get(variableIndex)
+                                val elementInPermutation = permutation.get(variableIndex)
+                                
+                                val newSMTVariable = createSMTSortedVariable => [
+                                        name = logicVariable.name.toID
+                                        range = elementInPermutation.type
+                                ]
+                                allVariables.put(logicVariable, newSMTVariable)
+                                newSMTVariables+=newSMTVariable
+                                if(elementInPermutation.constraint != null) {
+                                        typePrecondition += elementInPermutation.constraint.apply(newSMTVariable)
+                                }
+                        }
+                        
+                        val expressionOfQuantifiedFormula =
+                                if(typePrecondition.isEmpty)
+                                        q.expression.transformTerm(trace,allVariables).expectLogic.value
+                                else if(typePrecondition.size == 1)
+                                        preconditionCombinator.apply(
+                                                typePrecondition.head,
+                                                q.expression.transformTerm(trace,allVariables).expectLogic.value)
+                                else
+                                        preconditionCombinator.apply(
+                                                createSMTAnd => [it.operands += typePrecondition],
+                                                q.expression.transformTerm(trace,allVariables).expectLogic.value)
+                        
+                        unfoldedQuantification += constructor.apply => [
+                                quantifiedVariables += newSMTVariables
+                                expression = expressionOfQuantifiedFormula
+                        ]
+                        
+//                      if(newSMTVariables.exists[it.range == null]) {
+//                              println(newSMTVariables.filter[it.range == null].map[name])
+//                      }
+                }
+                
+                if(permutations.size == 1) return unfoldedQuantification.head
+                else return combinator.apply(unfoldedQuantification)
+        }
+        
+        ///////////////////////////////////////////////////////
+        // If - Then - Else
+        ///////////////////////////////////////////////////////
+        def dispatch protected TransformedSubterm transformTerm(IfThenElse ite, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                val condition = ite.condition.transformTerm(trace,variables).expectLogic.value
+                val positiveTerm = ite.ifTrue.transformTerm(trace,variables)
+                val positives = positiveTerm.possibleValues
+                val negativeTerm = ite.ifFalse.transformTerm(trace,variables)
+                val negatives = negativeTerm.possibleValues
+                // Simple ITE
+                if(positives.size == 1 && negatives.size == 1 && positives.head.type == negatives.head.type) {
+                        val t = positives.head.type
+                        if(t.isLogic) {
+                                return new LogicSubterm(createSMTITE => [
+                                        it.condition = condition
+                                        it.^if = positives.head.expression
+                                        it.^else = negatives.head.expression])
+                        } else if(t.isNumeric) {
+                                return new NumericSubterm(
+                                        (positives.head.variables + negatives.head.variables).toList,
+                                        (positives.head.preconditions + negatives.head.preconditions).toList,
+                                        createSMTITE => [
+                                        it.condition = condition
+                                        it.^if = positives.head.expression
+                                        it.^else = negatives.head.expression
+                                ])
+                        } else {
+                                return new ComplexSubterm(
+                                        (positives.head.variables + negatives.head.variables).toList,
+                                        (positives.head.preconditions + negatives.head.preconditions).toList,
+                                        createSMTITE => [
+                                                it.condition = condition
+                                                it.^if = positives.head.expression
+                                                it.^else = negatives.head.expression],
+                                        t
+                                )
+                        }
+                // else the ite need to be unfolded
+                } else {
+                        if(positiveTerm instanceof LogicSubterm) {
+                                throw new AssertionError('''If the subterm has logic value it should be transformed as "Simple ITE""''')
+                        } else if (positiveTerm instanceof NumericSubterm){
+                                return new NumericSubterm(unfoldIte(positives, condition, negatives))
+                        } else {
+                                return new ComplexSubterm(unfoldIte(positives, condition, negatives))
+                        }
+                }
+        }
+        
+        private def List<SubtermOption> unfoldIte(List<SubtermOption> positives, SMTTerm condition, List<SubtermOption> negatives) {
+                (positives.map[
+                        new SubtermOption(#[it],#[],#[condition],it.expression,it.type)
+                ] +
+                negatives.map[
+                        new SubtermOption(#[it],#[],#[createSMTNot => [it.operand = condition]],it.expression,it.type)
+                ]).toList
+        }
+        
+        ///////////////////////////////////////////////////////
+        // instanceof
+        ///////////////////////////////////////////////////////
+        
+        def dispatch protected TransformedSubterm transformTerm(InstanceOf i, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                val value = i.value.transformTerm(trace,variables)
+                val range = i.range
+                if(range instanceof BoolTypeReference) {
+                        return new LogicSubterm(createSMTBoolLiteral=>[it.value = (value instanceof LogicSubterm)])
+                } else if(range instanceof IntTypeReference || range instanceof RealTypeReference) {
+                        return new LogicSubterm(createSMTBoolLiteral=>[it.value = (value instanceof NumericSubterm)])
+                } else {
+                        val requestedTypes = this.typeMapper.transformTypeReference((range as ComplexTypeReference).referred,trace)
+                        val possileValues = value.possibleValues
+                        val options = new ArrayList(requestedTypes.size)
+                        for(typeConstraint : requestedTypes) {
+                                val possibleValue = possileValues.filter[it.type.complexType == (typeConstraint.type as SMTComplexTypeReference).referred].head
+                                if(possibleValue != null) {
+                                        val x = if(typeConstraint.constraint != null ) {
+                                                if(possibleValue.expression instanceof SMTSymbolicValue && (possibleValue.expression as SMTSymbolicValue).symbolicReference instanceof SMTSortedVariable) {
+                                                        val referred = (possibleValue.expression as SMTSymbolicValue).symbolicReference as SMTSortedVariable
+                                                        typeConstraint.constraint.apply(referred)
+                                                } else {
+                                                        createSMTForall => [
+                                                                val v = createSMTSortedVariable => [it.range = EcoreUtil.copy(typeConstraint.type)]
+                                                                it.quantifiedVariables += v
+                                                                it.expression = createSMTImpl => [
+                                                                        leftOperand = createSMTEquals => [
+                                                                                it.leftOperand = possibleValue.expression
+                                                                                it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = v]
+                                                                        ]
+                                                                        rightOperand = typeConstraint.constraint.apply(v)
+                                                                ]
+                                                        ]
+                                                }
+                                        } else if(typeConstraint.constraint == null) {
+                                                createSMTBoolLiteral => [it.value = true]
+                                        }
+                                        options += LogicSubterm::resolveToLogic(#[possibleValue],x)
+                                }
+                        }
+                        
+                        if(options.size == 0) {
+                                return new LogicSubterm(createSMTBoolLiteral=>[it.value = false])
+                        } else if(options.size == 1) {
+                                return new LogicSubterm(options.head)
+                        } else {
+                                return new LogicSubterm(createSMTOr => [it.operands += options])
+                        }
+                }
+                
+        }
+        
+        ///////////////////////////////////////////////////////
+        // SymbolicReference
+        ///////////////////////////////////////////////////////
+        
+        def dispatch protected TransformedSubterm transformTerm(SymbolicValue symbolicValue, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                val referred = symbolicValue.symbolicReference
+                val params = symbolicValue.parameterSubstitutions
+                return transformSymbolicReference(referred,params,trace,variables)
+        }
+        
+        def dispatch protected TransformedSubterm transformSymbolicReference(Relation referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                val parameters = parameterSubstitution.map[transformTerm(it,trace,variables)]
+                val list = new LinkedList
+                for(combination : TransformedSubterm.allCombinations(parameters.map[it.possibleValues])) {
+                        val descriptor = new Descriptor(combination.map[it.type],referred)
+                        val targetRelation = descriptor.lookup(trace.relationMap)
+                        if(targetRelation == null) {
+                                throw new AssertionError('''target relation should not be null (yet)''')
+                        
+                        } else {
+                                list += TransformedSubterm.resolveToLogic(combination,createSMTSymbolicValue => [
+                                        it.symbolicReference = targetRelation
+                                        it.parameterSubstitutions += combination.map[it.expression]
+                                ])
+                        }
+                }
+                
+                if(list.size == 1) {
+                        return new LogicSubterm(list.head)
+                } else {
+                        return new LogicSubterm(createSMTOr => [ operands += list ])
+                }
+        }
+        
+        
+        def dispatch protected TransformedSubterm transformSymbolicReference(Function referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                throw new UnsupportedOperationException
+        }
+        
+        def dispatch protected TransformedSubterm transformSymbolicReference(Variable referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                if(!variables.containsKey(referred)) {
+                        val container = referred.eContainer
+                        println("X" + container)
+                        for(v : variables.keySet) {
+                                println(v)
+                                println("in " +v.eContainer)
+                        }
+                        return null
+                }
+                val v = referred.lookup(variables)
+                
+                val expression = createSMTSymbolicValue => [it.symbolicReference = v]
+                if(v.range instanceof SMTBoolTypeReference) {
+                        return new LogicSubterm(expression)
+                } else if(v.range instanceof SMTIntTypeReference || v.range instanceof SMTRealTypeReference) {
+                        return new NumericSubterm(#[],#[],expression)
+                } else {
+                        return new ComplexSubterm(#[],#[],expression,
+                                new TypeDescriptor((v.range as SMTComplexTypeReference).referred));
+                }
+        }
+        
+        def dispatch protected TransformedSubterm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                this.typeMapper.transformSymbolicReference(referred,trace)
+        }
+        
+        def dispatch protected TransformedSubterm transformSymbolicReference(Void referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                throw new NullPointerException('''unfilled symbolic reference!''')
+        }
+        
+        ///////////
+        
+        /*def transformContainment(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) {
+                val containmentRelation_oo = createSMTFunctionDefinition=>[
+                        it.name="containment!oo"
+                        it.range=createSMTBoolTypeReference
+                        val child = createSMTSortedVariable => [
+                                it.name = 
+                        ]
+                ]
+        }*/
+        
+        ///////////
+        
+        def cleanDocument(SMTDocument document) {
+                val content = document.eAllContents.toList
+                for(object:content) {
+                        for(containmentReference : object.eClass.EAllReferences.filter[containment]) {
+                                val child = object.eGet(containmentReference) {
+                                        if(child!=null) {
+                                                if(containmentReference.isMany) {
+                                                        val list = child as List<EObject>
+                                                        for(index : 0..<list.size) {
+                                                                val single = list.get(index)
+                                                                val newSingle = replaceWith(single)
+                                                                if(newSingle!=null) {
+                                                                        list.set(index,newSingle)
+                                                                }
+                                                        }
+                                                } else {
+                                                        val single = child as EObject
+                                                        val newSingle = replaceWith(single)
+                                                        if(newSingle!=null) {
+                                                                object.eSet(containmentReference,newSingle)
+                                                        }
+                                                }
+                                        }
+                                }
+                        }
+                }
+        }
+        def private dispatch replaceWith(SMTOr or) {
+                if(or.operands.empty) {
+                        return createSMTBoolLiteral => [it.value = false]
+                } else return null
+        }
+        def private dispatch replaceWith(SMTAnd and) {
+                if(and.operands.empty) {
+                        return createSMTBoolLiteral => [it.value = true]
+                } else return null
+        }
+        def private dispatch replaceWith(EObject object)  {
+                null
+        }
+}
+\ 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/Logic2SmtMapperTrace.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapperTrace.xtend
new file mode 100644
index 00000000..69111a11
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapperTrace.xtend
@@ -0,0 +1,23 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+class Logic2SmtMapperTrace {
+        public var LogicProblem problem
+        public var Logic2SmtMapper forwardMapper
+        public var Logic2Smt_TypeMapperTrace typeMapperTrace
+        public val Map<Relation,List<Descriptor<Relation>>> relationUnfolding = new HashMap
+        public val Map<Descriptor<Relation>,SMTSymbolicDeclaration> relationMap = new HashMap
+        public val Map<Function,List<Descriptor<Function>>> functionUnfolding = new HashMap
+        public val Map<Descriptor<Function>,SMTSymbolicDeclaration> functionMap = new HashMap
+        public val Map<Function,List<Descriptor<Constant>>> constantUnfolding = new HashMap
+        public val Map<Descriptor<Constant>,SMTSymbolicDeclaration> constantMap = new HashMap
+}
+\ 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/Logic2SmtMapper_UnfoldingSupport.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper_UnfoldingSupport.xtend
new file mode 100644
index 00000000..8c2d5dad
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper_UnfoldingSupport.xtend
@@ -0,0 +1,33 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+//import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
+import java.util.ArrayList
+import java.util.List
+class Logic2SmtMapper_UnfoldingSupport {
+        //val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
+        
+        def List<List<TypeConstraint>> getPermutations(List<List<TypeConstraint>> lists) {
+                if(lists.size == 1) {
+                        val elements = lists.head
+                        val result = new ArrayList(elements.size)
+                        for(element: elements){
+                                result.add(#[element.copy])
+                        }
+                        return result
+                } else {
+                        val permuteThis = lists.head
+                        val withThat = getPermutations(lists.tail.toList)
+                        val result = new ArrayList(permuteThis.size*withThat.size)
+                        for(h:permuteThis) {
+                                for(t:withThat) {
+                                        val l = new ArrayList(withThat.size+1)
+                                        l+=h.copy
+                                        l.addAll(t.map[copy])
+                                        result.add(l)
+                                }
+                        }
+                        return result
+                }
+        }
+}
+\ 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.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend
new file mode 100644
index 00000000..71cfd0e0
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend
@@ -0,0 +1,38 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTypeReference
+import java.util.List
+import org.eclipse.emf.ecore.util.EcoreUtil
+import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.xtext.xbase.lib.Functions.Function1
+interface Logic2Smt_TypeMapper {
+        def void transformTypes(
+                SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes)
+                
+        def List<TypeConstraint> transformTypeReference(Type type, Logic2SmtMapperTrace trace)
+        def TransformedSubterm transformSymbolicReference(DefinedElement referred, Logic2SmtMapperTrace trace)
+        def Logic2SMT_TypeMapperInterpretation getTypeInterpretation(LogicProblem problem,SMTDocument document,SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace)
+}
+@Data
+class TypeConstraint {
+        SMTTypeReference type
+        Function1<SMTSortedVariable,SMTTerm> constraint
+        
+        def public copy() {
+                return new TypeConstraint(EcoreUtil.copy(this.type),this.constraint)
+        }
+}
+interface Logic2Smt_TypeMapperTrace{
+        def Logic2Smt_TypeMapperTrace copy(SMTInput newModel)
+}
+\ 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_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 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher
+import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSetTypeDeclaration
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.viatra.query.runtime.emf.EMFScope
+import org.eclipse.xtext.xbase.lib.Functions.Function0
+import org.eclipse.xtext.xbase.lib.Functions.Function1
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2Smt_TypeMapperTrace_FilteredTypes implements Logic2Smt_TypeMapperTrace{
+        public var Map<Type, SMTType> independentClasses = new HashMap
+        /**
+         * SMT type for the new objects
+         */
+        public var SMTType newObjects
+        /**
+         * SMT type for the existing objects
+         */
+        public var SMTEnumeratedTypeDeclaration oldObjects
+        /**
+         * existing element -> SMT literal map
+         */
+        public var Map<DefinedElement, SMTEnumLiteral> elementMap = new HashMap
+        
+        public var SMTEnumeratedTypeDeclaration oldObjectTypes
+        public var Map<Type, SMTEnumLiteral> oldObjectTypeMap = new HashMap
+        public var SMTFunctionDefinition oldObjectTypeFunction
+        public var Map<Type, SMTFunctionDefinition> oldObjectTypePredicates = new HashMap
+        
+        public var SMTEnumeratedTypeDeclaration newObjectTypes
+        public var Map<Type, SMTEnumLiteral> newObjectTypeMap = new HashMap
+        public var SMTFunctionDeclaration newObjectTypeFunction
+        public var Map<Type, SMTFunctionDefinition> newObjectTypePredicates = new HashMap
+        
+        override copy(SMTInput newModel) {
+                val a = this
+                val b = new Logic2Smt_TypeMapperTrace_FilteredTypes
+                
+                b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name])
+                
+                b.newObjects = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head
+                b.oldObjects = newModel.typeDeclarations.filter[it.name == a.oldObjects.name].head as SMTEnumeratedTypeDeclaration
+                b.elementMap = a.elementMap.copyMap(b.oldObjects.elements,[name])
+                
+                b.oldObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head as SMTEnumeratedTypeDeclaration
+                b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name])
+                b.oldObjectTypeFunction = newModel.functionDefinition.filter[it.name == a.oldObjectTypeFunction.name].head
+                b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name])
+                
+                b.newObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjectTypes.name].head as SMTEnumeratedTypeDeclaration
+                b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name])
+                b.newObjectTypeFunction = newModel.functionDeclarations.filter[it.name == a.newObjectTypeFunction.name].head
+                b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name])
+                
+                return b
+        }
+}
+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 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]
+                
+                val connectedTypesWithoutDefintypesWithoutDefinedSupertype = connectedTypes.filter(TypeDeclaration).filter[!hasDefinedSupertype].toList
+                val hasOldElements = !connectedElements.empty
+                val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty
+                
+                // 0. map the simple types
+                this.transformIndependentTypes(independentTypes,trace)
+                
+                // 1. Has old elements => create supertype for it
+                if(hasOldElements) {
+                        this.transformDefinedElements(connectedElements, trace,document)
+                }
+                // 2. Has new types => create a supertype for it
+                if(hasNewElements) {
+                        this.transformUndefinedElements(scopes,trace,document)
+                }
+                // 3. Adding type definitions of the types
+                // 3.1: Type definition to old elements
+                if(hasOldElements) {
+                        this.transformOldTypes(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 @@
+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_Horizontal.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend
new file mode 100644
index 00000000..a5abbb44
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend
@@ -0,0 +1,63 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
+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.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import java.util.List
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+class Logic2Smt_TypeMapperTrace_Horizontal implements Logic2Smt_TypeMapperTrace{
+        
+        override copy(SMTInput newModel) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+}
+class Logic2Smt_TypeMapper_Horizontal implements Logic2Smt_TypeMapper {
+        val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
+        
+        private def toID(List<String> names) {names.join("!") }
+        
+        override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) {
+                val typeTrace = new Logic2Smt_TypeMapperTrace_Horizontal
+                trace.typeMapperTrace = typeTrace
+                
+                // mapping of known elements
+                
+        }
+        
+        private def Logic2Smt_TypeMapperTrace_Horizontal getTypeTrace(Logic2SmtMapperTrace trace) {
+                val typeTrace = trace.typeMapperTrace
+                if(typeTrace instanceof Logic2Smt_TypeMapperTrace_Horizontal) {
+                        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]
+                }
+        }
+        
+        override transformTypeReference(Type type, Logic2SmtMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override transformSymbolicReference(DefinedElement referred, Logic2SmtMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getTypeInterpretation(LogicProblem problem, SMTDocument document, SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+}
+\ 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/SMTSolver.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend
new file mode 100644
index 00000000..d371b89e
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend
@@ -0,0 +1,49 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.SmtLanguageStandaloneSetupGenerated
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
+import hu.bme.mit.inf.dslreasoner.smt.reasoner.builder.SmtSolverHandler
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguagePackage
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import org.eclipse.emf.ecore.util.EcoreUtil
+class SMTSolver extends LogicReasoner{
+        
+        public new() {
+                SmtLanguagePackage.eINSTANCE.eClass
+                val x = new SmtLanguageStandaloneSetupGenerated
+                x.createInjectorAndDoEMFRegistration
+        }
+        
+        val forwardMapper = new Logic2SmtMapper(new Logic2Smt_TypeMapper_FilteredTypes);
+        val backMapper = new Smt2LogicMapper;
+        val handler = new SmtSolverHandler
+        
+        override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) {
+                if(configuration instanceof SmtSolverConfiguration) {
+                        val transformationStart = System.currentTimeMillis
+                        val transformationResult = forwardMapper.transformProblem(problem,configuration.typeScopes,configuration.strategy)
+                        val SMTDocument inputModel= transformationResult.output
+                        val trace = transformationResult.trace
+                        val input = workspace.writeModel(inputModel,"problem.smt2")
+                        val transformationTime = System.currentTimeMillis-transformationStart
+                        val solverTimeStart = System.currentTimeMillis
+                        handler.callSolver(input,configuration)
+                        val solverTime = System.currentTimeMillis - solverTimeStart
+                        val outputModel = workspace.reloadModel(typeof(SMTDocument), "problem.smt2")
+                        EcoreUtil.resolveAll(outputModel)
+                        workspace.deactivateModel("problem.smt2")
+                        return backMapper.transformOutput(problem,outputModel.output,trace, transformationTime, solverTime)
+                } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''')
+        }
+        
+        override getInterpretation(ModelResult modelResult) {
+                val representation = modelResult.representation as SMTDocument
+                val trace = modelResult.trace as Logic2SmtMapperTrace
+                return new SmtModelInterpretation(trace.problem,representation,trace.forwardMapper,trace)
+        }
+}
+\ 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/Smt2LogicMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend
new file mode 100644
index 00000000..cbabc7b0
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend
@@ -0,0 +1,71 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticsSection
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticIntValue
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticDoubleValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTErrorResult
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSatResult
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTUnsupportedResult
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticValue
+import java.math.BigDecimal
+class Smt2LogicMapper {
+        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
+        
+        public def transformOutput(LogicProblem problem, SMTOutput output, Logic2SmtMapperTrace trace, long transformationTime, long solverTime) {
+                val satResult = output.satResult
+                if(satResult === null) { // Timeout
+                        return createInsuficientResourcesResult => [ init(problem,output,transformationTime,solverTime) it.resourceName = "time"]
+                } else {
+                        if(satResult instanceof SMTErrorResult) {
+                                return createErrorResult => [init(problem,output,transformationTime,solverTime) message = satResult.message]
+                        } else if(satResult instanceof SMTUnsupportedResult) {
+                                return createUndecidableResult => [init(problem,output,transformationTime,solverTime)]
+                        } else if(satResult instanceof SMTSatResult) {
+                                if(satResult.sat) {
+                                        return createModelResult => [
+                                                init(problem,output,transformationTime,solverTime)
+                                                representation += output.eContainer
+                                                it.trace = trace
+                                        ]
+                                } else if(satResult.unsat) {
+                                        return createInconsistencyResult => [init(problem,output,transformationTime,solverTime)]
+                                } else if(satResult.unknown) {
+                                        return createUndecidableResult => [init(problem,output,transformationTime,solverTime)]  
+                                }
+                        } else throw new LogicReasonerException("The solver resulted with unknown result.")
+                }
+        }
+        
+        private def init(LogicResult result,LogicProblem problem, SMTOutput output, long transformationTime, long solverTime) {
+                result.problem = problem
+                result.statistics = output.statistics.transformStatistics(transformationTime,solverTime)
+        }
+        
+        protected def transformStatistics(SMTStatisticsSection section, long transformationTime, long solverTime) {
+                createStatistics => [
+                        it.transformationTime = transformationTime.intValue
+                        it.solverTime = solverTime.intValue
+                        
+                        val memorySection = section.values.filter[it.name==":memory"].head
+                        if(memorySection != null) {
+                                it.solverMemory = ((memorySection as SMTStatisticDoubleValue).value.add(BigDecimal.valueOf(0.5))).intValue
+                        }
+                        entries += section.values.map[transformEntry]
+                ]
+        }
+        
+        protected def dispatch transformEntry(SMTStatisticIntValue entry) {
+                createIntStatisticEntry => [name = entry.exportName value = entry.value] }
+        protected def dispatch transformEntry(SMTStatisticDoubleValue entry) {
+                createRealStatisticEntry => [name = entry.exportName value = entry.value.doubleValue] }
+        
+        private def exportName(SMTStatisticValue value) {
+                return value.name.replaceFirst(":","")
+        }
+}
+\ 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/SmtModelInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend
new file mode 100644
index 00000000..fb0739ab
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend
@@ -0,0 +1,167 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.smt.reasoner.builder.SmtModelQueryEngine
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.Data
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
+@Data
+class ValueType {
+        TypeDescriptor descriptor
+        Object value
+}
+class SmtModelInterpretation implements LogicModelInterpretation {
+        //val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        @Accessors(PUBLIC_GETTER) val SmtModelQueryEngine queryEngine;
+        
+        // Trace info
+        val Logic2SmtMapperTrace newTrace;
+        val Logic2SMT_TypeMapperInterpretation typeInterpretation
+        
+        /**
+         * Creates a model builder which queries a logic structure.
+         * @param document The whole SMT2 document.
+         * @param trace The trace of the [Logic problem -> SMT problem] mapping 
+         */
+        new(LogicProblem problem, SMTDocument document, Logic2SmtMapper forwardMapper, Logic2SmtMapperTrace forwardTrace) {
+                //document.input.typeDeclarations.forEach[typeNames.put(it.name,it)]
+                
+                this.queryEngine = new SmtModelQueryEngine(document)
+                this.newTrace = initialiseNewTrace(document,forwardTrace)
+                this.typeInterpretation = forwardMapper.typeMapper.getTypeInterpretation(problem,document,this,newTrace)
+        }
+        
+        /**
+         * Creates a new trace from the logic model to the new smt file by using the old trace.
+         */
+        def protected Logic2SmtMapperTrace initialiseNewTrace(SMTDocument document, Logic2SmtMapperTrace oldTrace) {
+                val i = document.input
+                
+                val res = new Logic2SmtMapperTrace => [ typeMapperTrace = oldTrace.typeMapperTrace.copy(i) ]
+                
+                for(entry : oldTrace.relationUnfolding.entrySet) {
+                        val rel = entry.key
+                        val descriptors = entry.value.map[old | 
+                                new Descriptor<Relation>(
+                                        old.parameterTypes.map[copyTypeDescriptor(i)],
+                                        old.relation)
+                        ]
+                        res.relationUnfolding.put(rel,descriptors)
+                }
+                
+                for(entry : oldTrace.relationMap.entrySet) {
+                        val desc = new Descriptor<Relation>(
+                                        entry.key.parameterTypes.map[copyTypeDescriptor(i)],
+                                        entry.key.relation)
+                        val fun = i.functionDeclarations.filter[it.name == entry.value.name].head
+                        res.relationMap.put(desc,fun)
+                }
+                
+                return res
+        }
+        
+        def private copyTypeDescriptor(TypeDescriptor original, SMTInput i) {
+                if(original.complexType == null) return original
+                else {
+                        val newType = i.typeDeclarations.filter[it.name == original.complexType.name].head
+                        new TypeDescriptor(newType)
+                }
+        }
+        
+        /*def protected initialiseTypes(SMTDocument document) {
+                val model = document.output.getModelResult as SMTModelResult
+                val smtUndefinedType2LogicType = this.newTrace.typeDeclarationMap.bijectiveInverse
+                
+                for(cardinalityConstraint : model.typeDefinitions) {
+                        val targetType = (cardinalityConstraint.type as SMTComplexTypeReference).referred as SMTSetTypeDeclaration
+                        val List<DefinedElement> elementCollection = new LinkedList
+                        for(element : cardinalityConstraint.elements.map[symbolicReference]) {
+                                if(element instanceof SMTFunctionDeclaration) {
+                                        val definedElementRepresentation = createDefinedElement => [name += element.name.split("!")]
+                                        newElement2Constants.put(definedElementRepresentation,element)
+                                        newConstants2Elements.put(element,definedElementRepresentation)
+                                } else{
+                                        throw new UnsupportedOperationException(
+                                                "Unresolvable reference in cardinality constraint: " + element.class.name + ": " + element.name)        
+                                }
+                        }
+                        undefinedTypeDefinitions.put(targetType.lookup(smtUndefinedType2LogicType),elementCollection);
+                }
+        }*/
+        
+        def private dispatch ValueType logicLiteral2SmtLiteral(Integer literal) {
+                new ValueType(TypeDescriptor::numericTypeDescriptor_Instance, literal)
+        }
+        def private dispatch ValueType logicLiteral2SmtLiteral(Boolean literal) {
+                new ValueType(TypeDescriptor::logicTypeDescriptor_Instance, literal)
+        }
+        def private dispatch ValueType logicLiteral2SmtLiteral(DefinedElement literal) {
+                this.typeInterpretation.logicElement2Smt(literal)
+        }
+//      def private dispatch Object smt2Literal2LogicLiteral(Integer literal) { literal }
+//      def private dispatch Object smt2Literal2LogicLiteral(Boolean literal) { literal }
+//      def private dispatch Object smt2Literal2LogicLiteral(SMTSymbolicDeclaration literal) { 
+//              this.typeInterpretation.smtElement2Logic(literal)
+//      }
+        override getElements(Type type) {
+                return this.typeInterpretation.getElements(type)
+        }
+        
+        override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
+                /*queryEngine.resolveFunctionDeclaration(
+                        function.lookup(newTrace.functionDeclarationMap),
+                        parameterSubstitution.map[logicLiteral2SmtLiteral]
+                ).smt2Literal2LogicLiteral*/
+                throw new UnsupportedOperationException
+        }
+        
+        override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+                val transformedParameters = parameterSubstitution.map[logicLiteral2SmtLiteral]
+                
+                val smtFunction = new Descriptor<Relation>(
+                        transformedParameters.map[descriptor],
+                        relation)
+                        .lookup(newTrace.relationMap)
+                        
+                val result = queryEngine.resolveFunctionDeclaration(
+                        smtFunction as SMTFunctionDeclaration,
+                        transformedParameters.map[value]
+                ) as Boolean
+                
+                return result
+        }
+        
+        override getInterpretation(ConstantDeclaration constant) {
+                /*queryEngine.resolveFunctionDeclaration(
+                        constant.lookup(newTrace.constantDeclarationMap),
+                        Collections.EMPTY_LIST
+                ).smt2Literal2LogicLiteral*/
+                throw new UnsupportedOperationException
+        }
+        
+        override getMaximalInteger() {
+                100
+                //throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getMinimalInteger() {
+                -100
+                //throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+}
+\ 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/SmtSolverConfiguration.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtSolverConfiguration.xtend
new file mode 100644
index 00000000..2a926cb6
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtSolverConfiguration.xtend
@@ -0,0 +1,9 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningTactic
+class SmtSolverConfiguration extends LogicSolverConfiguration{
+        public boolean fixRandomSeed = false
+        public SMTReasoningTactic strategy = null
+}
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend
new file mode 100644
index 00000000..48952288
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend
@@ -0,0 +1,183 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
+import java.util.ArrayList
+import java.util.List
+import java.util.Map
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.emf.ecore.util.EcoreUtil
+import org.eclipse.xtend.lib.annotations.Data
+import java.util.HashMap
+import java.util.LinkedList
+abstract class TransformedSubterm {
+        val static extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
+        def LogicSubterm expectLogic() 
+        def NumericSubterm expectNumber()
+        
+        def List<SubtermOption> getPossibleValues()
+        
+        public static def List<List<SubtermOption>> allCombinations(List<SubtermOption>... possibleValues) {
+                return allCombinations(possibleValues.toList)
+        }
+        public static def List<List<SubtermOption>> allCombinations(Iterable<List<SubtermOption>> possibleValues) {
+                if(possibleValues.size == 1) {
+                        return possibleValues.head.map[x|#[x.copy]]
+                } else {
+                        val head = possibleValues.head
+                        val tails = possibleValues.tail.allCombinations
+                        val res = new ArrayList(tails.size * head.size)
+                        for(headElement : head) {
+                                for(tail : tails) {
+                                        val combination = new ArrayList(tail.size+1)
+                                        combination.add(headElement)
+                                        combination.addAll(tail.map[copy])
+                                        res.add(combination)
+                                }
+                        }
+                        return res
+                }
+        }
+        
+        public static def resolveToLogic(List<SubtermOption> subterms, SMTTerm value) {
+                val allDefinitions = subterms.map[it.variables].flatten
+                val allPreconditions = subterms.map[it.preconditions].flatten
+                val preconditionedExpression = if(allPreconditions.empty) {
+                        value
+                } else {
+                        createSMTAnd => [it.operands += allPreconditions it.operands += value]
+                }
+                val quantifiedExpression = if(allDefinitions.empty) {
+                        preconditionedExpression
+                } else {
+                        createSMTForall => [
+                                it.quantifiedVariables += allDefinitions
+                                it.expression = preconditionedExpression]
+                }
+                return quantifiedExpression
+        }
+}
+@Data class SubtermOption {
+        List<SMTSortedVariable> variables
+        List<SMTTerm> preconditions
+        SMTTerm expression
+        TypeDescriptor type
+        
+        public new(
+                List<SMTSortedVariable> variables,
+                List<SMTTerm> preconditions,
+                SMTTerm expression,
+                TypeDescriptor type)
+        {
+                this.variables = variables
+                this.preconditions = preconditions
+                this.expression = expression
+                this.type = type
+        }
+        
+        public new(
+                List<SubtermOption> previousSubterms,
+                List<SMTSortedVariable> newVariables,
+                List<SMTTerm> newPreconditions,
+                SMTTerm newExpression,
+                TypeDescriptor newType)
+        {
+                val old2New = new HashMap
+                variables = new LinkedList
+                for(variable : previousSubterms.map[getVariables].flatten) {
+                        val newVariable = EcoreUtil.copy(variable)
+                        old2New.put(variable,newVariable)
+                        variables+=newVariable
+                }
+                
+                preconditions = new LinkedList
+                preconditions += previousSubterms.map[getPreconditions].flatten.map[x|EcoreUtil.copy(x)]
+                preconditions += newPreconditions.map[x|EcoreUtil.copy(x)]
+                preconditions.forEach[relinkAllVariableReference(old2New)]
+                
+                expression = EcoreUtil.copy(newExpression)
+                relinkAllVariableReference(expression,old2New)
+                
+                type = newType
+        }
+        
+        public def copy() {
+                val old2New = variables.toInvertedMap[EcoreUtil.copy(it)]
+                val newPreconditions = preconditions.map[EcoreUtil.copy(it)]
+                newPreconditions.forEach[it.relinkAllVariableReference(old2New)]
+                val newExpression = EcoreUtil.copy(expression)
+                return new SubtermOption(variables.map[old2New.get(it)],newPreconditions,newExpression,type)
+        }
+        
+        def private relinkAllVariableReference(EObject root,Map<SMTSortedVariable, SMTSortedVariable> map) {
+                if(root instanceof SMTSymbolicValue) root.relinkVariableReference(map)
+                root.eAllContents().filter(SMTSymbolicValue).forEach[relinkVariableReference(map)]
+        }
+        def private relinkVariableReference(SMTSymbolicValue target,Map<SMTSortedVariable, SMTSortedVariable> map) {
+                if(map.containsKey(target.symbolicReference)) {
+                        target.symbolicReference = map.get(target.symbolicReference)
+                }
+        }
+}
+@Data
+class LogicSubterm extends TransformedSubterm{
+        
+        SMTTerm value
+        override expectLogic() {return this}
+        override expectNumber() { throw new AssertionError("A term is not a number") }
+        
+        public new(SMTTerm expression)
+        {
+                this.value = expression
+        }
+        override getPossibleValues() {
+                #[new SubtermOption(#[],#[],value,TypeDescriptor::logicTypeDescriptor_Instance)]
+        }
+}
+@Data
+class NumericSubterm extends TransformedSubterm {
+        List<SubtermOption> values
+        
+        public new(
+                List<SMTSortedVariable> variables,
+                List<SMTTerm> preconditions,
+                SMTTerm expression) {
+                this.values = #[new SubtermOption(variables,preconditions,expression,TypeDescriptor.numericTypeDescriptor_Instance)]
+        }
+        public new(List<SubtermOption> values) {
+                this.values = values
+        }
+        
+        override expectLogic() { throw new AssertionError("A term is not a logic value") }
+        override expectNumber() { return this }
+        
+        override getPossibleValues() {
+                values
+        }
+}
+@Data
+class ComplexSubterm extends TransformedSubterm {
+        List<SubtermOption> options
+        override expectLogic() { throw new AssertionError("A term is not a logic value") }
+        override expectNumber() { throw new AssertionError("A term is not a number") }
+        public new(List<SMTSortedVariable> variables,
+                List<SMTTerm> preconditions,
+                SMTTerm expression,
+                TypeDescriptor type)
+        {
+                this.options = #[new SubtermOption(variables,preconditions,expression,type)]
+        }
+        public new(List<SubtermOption> subterms) {
+                this.options = subterms
+        }
+        override getPossibleValues() {
+                this.options
+        }
+}
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TypeDescriptor.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TypeDescriptor.xtend
new file mode 100644
index 00000000..1aa5cf04
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TypeDescriptor.xtend
@@ -0,0 +1,44 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
+import java.util.List
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.Data
+@Data
+class Descriptor<T> {
+        List<TypeDescriptor> parameterTypes
+        T relation
+}
+@Data
+class TypeDescriptor {
+        val boolean logic
+        val boolean numeric
+        val SMTType complexType
+        
+        @Accessors(PUBLIC_GETTER)
+        static val LogicTypeDescriptor_Instance = new TypeDescriptor(true,false,null)
+        @Accessors(PUBLIC_GETTER)
+        static val NumericTypeDescriptor_Instance = new TypeDescriptor(false,true,null)
+        
+        private new(boolean logic, boolean numeric,     SMTType complexType) {
+                this.logic = logic
+                this.numeric = numeric
+                this.complexType = complexType
+        }
+        public new(SMTType complexType) {
+                this.logic = false
+                this.numeric = false
+                this.complexType = complexType
+        }
+        
+        def static dispatch createFromTypeReference(SMTBoolTypeReference ref) { return TypeDescriptor::LogicTypeDescriptor_Instance}
+        def static dispatch createFromTypeReference(SMTIntTypeReference ref) { return TypeDescriptor::NumericTypeDescriptor_Instance}
+        def static dispatch createFromTypeReference(SMTRealTypeReference ref) { return TypeDescriptor::NumericTypeDescriptor_Instance}
+        def static dispatch createFromTypeReference(SMTComplexTypeReference ref) { return new TypeDescriptor(false,false,ref.referred)}
+}
+\ 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/builder/SmtModelQueryEngine.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend
new file mode 100644
index 00000000..a259d103
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend
@@ -0,0 +1,314 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolLiteral
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEquals
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTITE
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMinus
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+class SmtModelQueryEngine {
+        private Map<SMTFunctionDeclaration, SMTFunctionDefinition> functionDeclarationToDefinitions =
+                new HashMap<SMTFunctionDeclaration, SMTFunctionDefinition>
+        
+        private val SMTInput input;
+        private val SMTOutput output
+        
+        new(SMTDocument model) {
+                val nameToFunctionDefiniton = new HashMap<String, SMTFunctionDefinition>
+                input = model.input
+                var SMTModelResult modelResult = null
+                
+                output = model.output
+                if(output!=null) {
+                        val result = output.getModelResult
+                        if(result instanceof SMTModelResult) {
+                                modelResult = result as SMTModelResult
+                        }
+                }
+                
+                input.functionDefinition.
+                        forEach[x|nameToFunctionDefiniton.put(x.name,x)]
+                if(modelResult!=null)
+                        modelResult.newFunctionDefinitions.
+                                forEach[x|nameToFunctionDefiniton.put(x.name,x)]
+                
+                input.functionDeclarations.
+                        forEach[x|functionDeclarationToDefinitions.put(x,x.name.lookup(nameToFunctionDefiniton))]
+                if(modelResult!=null)
+                        modelResult.newFunctionDeclarations.
+                                forEach[x|functionDeclarationToDefinitions.put(x,x.name.lookup(nameToFunctionDefiniton))]
+        }
+        
+        def protected <KEY_TYPE,VALUE_TYPE> VALUE_TYPE lookup(KEY_TYPE key, Map<? extends KEY_TYPE,? extends VALUE_TYPE> map) {
+                return map.get(key)
+        }
+        
+        def protected dispatch getDefaultValue(SMTIntTypeReference reference) { 0 }
+        def protected dispatch getDefaultValue(SMTBoolTypeReference reference) { false }
+        def protected dispatch getDefaultValue(SMTComplexTypeReference reference) {
+                val type = reference.referred
+                if(type instanceof SMTEnumeratedTypeDeclaration) return type.elements.head
+                else {
+                        val definition = (output.getModelResult as SMTModelResult).typeDefinitions.filter[it.type == type].head
+                        return definition.elements.head
+                }
+        }
+            
+        def protected isTerminal(
+                SMTTerm term,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                /*
+                 * An undefined function is a terminal.
+                 */
+                if(term instanceof SMTSymbolicValue) {
+                        val symbolicValue = term as SMTSymbolicValue
+                        
+                        if(symbolicValue.symbolicReference instanceof SMTFunctionDeclaration)
+                        {
+                                val function = symbolicValue.symbolicReference as SMTFunctionDeclaration;
+                                val hasDefinition = functionDeclarationToDefinitions.get(function) != null
+                                return ! hasDefinition
+                        }
+                        else return false
+                }
+                /*
+                 * A finite element is a terminal.
+                 */
+                else if(term instanceof SMTEnumLiteral)
+                        return true
+                else return false
+        }
+        def protected resolveTerminal(
+                SMTTerm terminal,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                if(terminal instanceof SMTEnumLiteral) {
+                        return terminal;
+                }
+                else if(terminal instanceof SMTSymbolicValue) {
+                        val symbolicValue = terminal as SMTSymbolicValue
+                        if(symbolicValue.symbolicReference instanceof SMTFunctionDeclaration)
+                        {
+                                val function = symbolicValue.symbolicReference as SMTFunctionDeclaration;
+                                return function
+                        }
+                }
+        }
+        
+        def public Object resolveFunctionDeclaration(
+                SMTFunctionDeclaration declaration,
+                List<Object> params)
+        {
+                
+                val definition = declaration.lookup(functionDeclarationToDefinitions)
+                if(definition == null) return declaration.range.defaultValue
+                else return definition.resolveFunctionDefinition(params)
+        }
+        def public Object resolveFunctionDefinition(
+                SMTFunctionDefinition definition,
+                List<Object> params)
+        {
+                if(params.nullOrEmpty && definition.parameters.nullOrEmpty) {
+                        return definition.resolveFunctionDefinition(emptyMap)
+                }
+                else if(params.size!=definition.parameters.size)
+                        throw new IllegalArgumentException(
+                                "Incorrect number of parameters!")
+                else {
+                        val substitution = new HashMap<SMTSortedVariable,Object>
+                        if(! definition.parameters.nullOrEmpty) {
+                                for(i : 0..definition.parameters.size-1) {
+                                        substitution.put(
+                                                definition.parameters.get(i),
+                                                params.get(i))
+                                }
+                        }
+                        val result=definition.resolveFunctionDefinition(substitution)
+                        //System::out.println(definition.name+"("+params.map[toString] + ") = " + result)
+                        return result
+                }
+        }
+        def protected Object resolveFunctionDefinition(
+                SMTFunctionDefinition definition,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                definition.value.resolveValue(substitution)
+        }
+        
+        def protected isBoolLiteral(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                term instanceof SMTBoolLiteral
+        }
+        def protected resolveBoolLiteral(SMTTerm boolValue, Map<SMTSortedVariable,Object> substitution) {
+                return (boolValue as SMTBoolLiteral).^value
+        }
+        
+        def protected isIntLiteral(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                term instanceof SMTIntLiteral ||
+                (term instanceof SMTMinus && (term as SMTMinus).rightOperand==null)
+        }
+        def protected resolveIntLiteral(SMTTerm intValue, Map<SMTSortedVariable,Object> substitution) {
+                if(intValue instanceof SMTIntLiteral) return (intValue as SMTIntLiteral).^value
+                else return -((intValue as SMTMinus).leftOperand as SMTIntLiteral).value
+        }
+        
+        def protected isParameterValue(
+                SMTTerm term,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                if(term instanceof SMTSymbolicValue) {
+                        return substitution.containsKey((term as SMTSymbolicValue).symbolicReference)
+                }
+                else return false
+        }
+        def protected Object resolveParameterValue(
+                SMTTerm term,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                return substitution.get((term as SMTSymbolicValue).symbolicReference);
+        }
+        
+        def protected isITE(
+                SMTTerm term,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                return term instanceof SMTITE;
+        }
+        def protected resolveITE(
+                SMTTerm term,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                val ite = term as SMTITE
+                val condition = ite.condition.resolveValue(substitution) as Boolean
+                
+                if(condition){
+                        return resolveValue(ite.^if,substitution)
+                }else{
+                        return resolveValue(ite.^else,substitution)
+                }
+        }
+        
+        def protected isAnd(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                term instanceof SMTAnd
+        }
+        def protected resolveAnd(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                val and = term as SMTAnd
+                for(operand : and.operands) {
+                        val operandValue = operand.resolveValue(substitution) as Boolean
+                        if(!operandValue) return false
+                }
+                return true
+        }
+        
+        def protected isEquals(
+                SMTTerm operand, 
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                return operand instanceof SMTEquals
+        }
+        def protected resolveEquals(SMTTerm term, Map<SMTSortedVariable,Object> substitution){
+                val equals = term as SMTEquals
+                val left = equals.leftOperand.resolveValue(substitution)
+                val right = equals.rightOperand.resolveValue(substitution)
+                val res = left.equals(right)
+                return res
+        }
+        
+        def protected isFiniteElementReference(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                if(term instanceof SMTSymbolicValue) {
+                        if((term as SMTSymbolicValue).symbolicReference instanceof SMTEnumLiteral) {
+                                return true
+                        }
+                }
+                return false;
+        }
+        def protected resolveFiniteElementReference(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                (term as SMTSymbolicValue).symbolicReference
+        }
+        
+        def protected isFunctionCall(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                if(term instanceof SMTSymbolicValue) {
+                        val functionCall = (term as SMTSymbolicValue).symbolicReference
+                        return functionCall instanceof SMTFunctionDeclaration || functionCall instanceof SMTFunctionDefinition
+                }
+                return false;
+        }
+        def protected resolveFunctionCall(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                if(term.isTerminal(substitution))
+                {
+                        return term.resolveTerminal(substitution);
+                }
+                else{
+                        val functionCall = term as SMTSymbolicValue
+                        var SMTFunctionDefinition calledFunction;
+                        var SMTFunctionDeclaration calledDeclaration;
+                        if(functionCall.symbolicReference instanceof SMTFunctionDeclaration) {
+                                calledDeclaration = functionCall.symbolicReference as SMTFunctionDeclaration
+                                calledFunction = functionCall.symbolicReference.lookup(functionDeclarationToDefinitions)}
+                        else {
+                                calledDeclaration = null;
+                                calledFunction = functionCall.symbolicReference as SMTFunctionDefinition
+                        }
+                        
+                        val newSubstitution = new HashMap<SMTSortedVariable,Object>
+                        if(! calledFunction.parameters.nullOrEmpty) {
+                                for(i : 0..calledFunction.parameters.size-1) {
+                                        newSubstitution.put(
+                                                calledFunction.parameters.get(i),
+                                                functionCall.parameterSubstitutions.get(i).resolveValue(substitution)
+                                        )
+                                }
+                        }
+                        return calledFunction.resolveFunctionDefinition(newSubstitution)
+                }
+        }
+        
+        def protected Object resolveValue(
+                SMTTerm value,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                if(value instanceof SMTSymbolicValue){
+                        (value as SMTSymbolicValue).symbolicReference
+                }
+                
+                if(value.isTerminal(substitution)) {
+                        return value.resolveTerminal(substitution)
+                }else if(value.isBoolLiteral(substitution)){
+                        return resolveBoolLiteral(value, substitution)
+                }else if(value.isIntLiteral(substitution)){
+                        return resolveIntLiteral(value, substitution)
+                }else if(value.isParameterValue(substitution)) {
+                        return resolveParameterValue(value,substitution)
+                }else if(value.isITE(substitution)){
+                        return resolveITE(value, substitution)
+                }else if(value.isAnd(substitution)) {
+                        return resolveAnd(value,substitution)
+                }else if(value.isEquals(substitution)) {
+                        return resolveEquals(value,substitution)
+                }else if(value.isFiniteElementReference(substitution)) {
+                        return resolveFiniteElementReference(value,substitution)
+                }else if(value.isFunctionCall(substitution)) {
+                        return resolveFunctionCall(value,substitution)
+                }else{
+                        throw new IllegalArgumentException("Can not resolve this term: " + value)
+                }
+        }
+}
+\ 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/builder/SmtSolverHandler.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend
new file mode 100644
index 00000000..38ae1dae
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend
@@ -0,0 +1,64 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner.builder
+import org.eclipse.emf.common.util.URI
+import java.io.InputStream
+import java.io.IOException
+import java.io.FileWriter
+import java.io.File
+import java.io.BufferedReader
+import java.io.InputStreamReader
+import org.eclipse.emf.common.CommonPlugin
+import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration
+class SmtSolverException extends Exception{
+        new(String s) { super(s) }
+        new(String s, Exception e) { super(s,e) }
+}
+class SmtSolverHandler {
+        public def callSolver(URI resourceURI, SmtSolverConfiguration configuration) {
+                val URI smtUri = CommonPlugin.resolve(resourceURI) 
+                val File smtFile = new File(smtUri.toFileString()) 
+                
+                val params =
+                        '''/smt2 /st«
+                        IF configuration.runtimeLimit != SmtSolverConfiguration::Unlimited» /T:«configuration.runtimeLimit»«ENDIF»«
+                        IF configuration.memoryLimit != SmtSolverConfiguration::Unlimited» /memory:«configuration.memoryLimit»«ENDIF»«
+                        IF configuration.fixRandomSeed» /rs:0«ENDIF
+                        » «smtFile.path»'''
+                        
+                val Runtime runTime = Runtime.getRuntime()
+                                
+                try {
+                        val process = runTime.exec(configuration.solverPath + " " + params)
+                        
+                        val FileWriter writer = new FileWriter(smtFile,true)
+                        writer.append("\n--------------\n")
+                        appendStream(writer, process.getInputStream())
+                        printStream(process.getErrorStream())
+                        writer.close
+                } catch (IOException e) {
+                        throw new SmtSolverException(
+                                "Error during the input/output handling of the reasoner.", e)
+                }
+                
+                return resourceURI
+        }
+        
+        def private void printStream(InputStream inputStream) throws IOException {
+                val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream))
+                var int line = -1
+                while ((line = input.read()) != -1) {
+                        System.out.print(line as char)
+                }
+                input.close()
+        }
+        def private appendStream(FileWriter writer, InputStream inputStream) throws IOException {
+                val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream))
+                var int line = -1
+                while ((line = input.read()) != -1) {
+                        writer.append(line as char)
+                }
+        }
+}
+\ No newline at end of file
author	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
committer	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
commit	60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree	5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner
parent	Initial commit, migrating from SVN (diff)
download	VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip