Partially improve coding style (leaving for soccer)

author: ArenBabikian <aren.babikian@mail.mcgill.ca> 2019-03-05 21:33:28 -0500
committer: ArenBabikian <aren.babikian@mail.mcgill.ca> 2019-03-05 21:33:28 -0500
commit: 89929078ca93c74a80ad70d58934d5d6d43d0e4f (patch)
tree: a8dd965a65a3545b9919f1276151b509d29c82e2
parent: Implement type scope handling (diff)
download: VIATRA-Generator-89929078ca93c74a80ad70d58934d5d6d43d0e4f.tar.gz
VIATRA-Generator-89929078ca93c74a80ad70d58934d5d6d43d0e4f.tar.zst
VIATRA-Generator-89929078ca93c74a80ad70d58934d5d6d43d0e4f.zip
28 files changed, 349 insertions, 350 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
index 135b3f07..3c672f4b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
@@ -1,15 +1,17 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
-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.RelationDeclaration
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
+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.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
 import java.util.HashMap
 import java.util.Map
@@ -22,17 +24,29 @@ class Logic2VampireLanguageMapperTrace {
        public var VampireModel specification
        public var VLSFofFormula logicLanguageBody
        public var VLSTerm formula
-//NOT NEEDED    //public var VLSFunction constantDec
        
+        //Necessary containers
        public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace
        
+        public val Map<Type, VLSFunction> type2Predicate = new HashMap;
+        public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap
+        public val Map<Type, VLSTerm> type2PossibleNot = new HashMap
+        public val Map<Type, VLSTerm> type2And = new HashMap
+        
+        public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions
+        public var Map<RelationDeclaration, RelationDefinition> relationDefinitions
+        public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap
+        
+        
+//NOT NEEDED    //public var VLSFunction constantDec
+        
+        
+        
        
 //NOT NEEDED    //public val Map<ConstantDeclaration, VLSFunctionDeclaration> constantDeclaration2LanguageField = new HashMap
        //public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap
        
-        public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions
        
-        public var Map<RelationDeclaration, RelationDefinition> relationDefinitions
        public val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
        public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap
                
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index 6f3b13ef..23b57701 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -24,52 +24,97 @@ class Logic2VampireLanguageMapper_RelationMapper {
                this.base = base
        }
-        def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace) {
+        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) {
                // 1. store all variables in support wrt their name
                // 1.1 if variable has type, creating list of type declarations
+                val List<VLSVariable> relVar2VLS = new ArrayList
+                val List<VLSFunction> relVar2TypeDecComply = new ArrayList
+                val typedefs = new ArrayList<VLSTerm>
+                for (i : 0 ..< r.parameters.length) {
+                        val v = createVLSVariable => [
+                                it.name = support.toIDMultiple("V", i.toString)
+                        ]
+                        relVar2VLS.add(v)
+                        
+                        val relType = (r.parameters.get(i) as ComplexTypeReference).referred
+                        val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v)
+                        relVar2TypeDecComply.add(varTypeComply)
+                }
+                val comply = createVLSFofFormula => [
+                        val nameArray = r.name.split(" ")
+                        it.name = support.toIDMultiple("compliance", nameArray.get(0),
+                                nameArray.get(2))
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                for (v : relVar2VLS) {
+                                        it.variables += support.duplicate(v)
+                                }
+                                it.operand = createVLSImplies => [
+                                        it.left = createVLSFunction => [
+                                                it.constant = support.toIDMultiple("rel", r.name)
+                                                for (i : 0 ..< r.parameters.length) {
+                                                        val v = createVLSVariable => [
+                                                                it.name = relVar2VLS.get(i).name
+                                                        ]
+                                                        it.terms += v
+                                                }
+                                        ]
+                                        it.right = support.unfoldAnd(relVar2TypeDecComply)
+                                ]
+                        ]
+                ]
+                // trace.relationDefinition2Predicate.put(r,res)
+                trace.specification.formulas += comply
+        }
+        def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) {
+                // 1. store all variables in support wrt their name
+                // 1.1 if variable has type, creating list of type declarations
+//              val VLSVariable variable = createVLSVariable => [it.name = "A"]
                val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
                val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
                val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
                val typedefs = new ArrayList<VLSTerm>
-                for (variable : r.variables) {
+                for (variable : reldef.variables) {
                        val v = createVLSVariable => [
-                                it.name = support.toIDMultiple("Var", variable.name)
+                                it.name = support.toIDMultiple("V", variable.name)
                        ]
                        relationVar2VLS.put(variable, v)
                        val varTypeComply = createVLSFunction => [
                                it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
-                                it.terms += createVLSVariable => [
+                                it.terms += support.duplicate(v)
-                                        it.name = support.toIDMultiple("Var", variable.name)
-                                ]
                        ]
                        relationVar2TypeDecComply.put(variable, varTypeComply)
-                        
+                        relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
-                        val varTypeRes = createVLSFunction => [
-                                it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
-                                it.terms += createVLSVariable => [
-                                        it.name = support.toIDMultiple("Var", variable.name)
-                                ]
-                        ]                       
-                        relationVar2TypeDecRes.put(variable, varTypeRes)
                }
                val comply = createVLSFofFormula => [
-                        it.name = support.toIDMultiple("compliance", r.name)
+                        val nameArray = reldef.name.split(" ")
+                        it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
+                                nameArray.get(nameArray.length - 1))
                        it.fofRole = "axiom"
                        it.fofFormula = createVLSUniversalQuantifier => [
-                                for (variable : r.variables) {
+                                for (variable : reldef.variables) {
-                                        val v = createVLSVariable => [
+                                        it.variables += support.duplicate(variable.lookup(relationVar2VLS))
-                                                it.name = variable.lookup(relationVar2VLS).name
-                                        ]
-                                        it.variables += v
                                }
                                it.operand = createVLSImplies => [
                                        it.left = createVLSFunction => [
-                                                it.constant = support.toIDMultiple("rel", r.name)
+                                                it.constant = support.toIDMultiple("rel", reldef.name)
-                                                for (variable : r.variables) {
+                                                for (variable : reldef.variables) {
                                                        val v = createVLSVariable => [
                                                                it.name = variable.lookup(relationVar2VLS).name
                                                        ]
@@ -82,10 +127,10 @@ class Logic2VampireLanguageMapper_RelationMapper {
                ]
                val res = createVLSFofFormula => [
-                        it.name = support.toIDMultiple("relation", r.name)
+                        it.name = support.toIDMultiple("relation", reldef.name)
                        it.fofRole = "axiom"
                        it.fofFormula = createVLSUniversalQuantifier => [
-                                for (variable : r.variables) {
+                                for (variable : reldef.variables) {
                                        val v = createVLSVariable => [
                                                it.name = variable.lookup(relationVar2VLS).name
                                        ]
@@ -96,8 +141,8 @@ class Logic2VampireLanguageMapper_RelationMapper {
                                        it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
                                        it.right = createVLSEquivalent => [
                                                it.left = createVLSFunction => [
-                                                        it.constant = support.toIDMultiple("rel", r.name)
+                                                        it.constant = support.toIDMultiple("rel", reldef.name)
-                                                        for (variable : r.variables) {
+                                                        for (variable : reldef.variables) {
                                                                val v = createVLSVariable => [
                                                                        it.name = variable.lookup(relationVar2VLS).name
                                                                ]
@@ -105,7 +150,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                                                        }
                                                ]
-                                                it.right = base.transformTerm(r.value, trace, relationVar2VLS)
+                                                it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
                                        ]
                                ]
@@ -119,65 +164,5 @@ class Logic2VampireLanguageMapper_RelationMapper {
                trace.specification.formulas += res;
        }
-        
-        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) {
-                // 1. store all variables in support wrt their name
-                // 1.1 if variable has type, creating list of type declarations
-                val List<VLSVariable> relationVar2VLS = new ArrayList
-                val List<VLSFunction> relationVar2TypeDecComply = new ArrayList
-                val typedefs = new ArrayList<VLSTerm>
-                
-                for (i : 0..<r.parameters.length) {
-                        
-                        val v = createVLSVariable => [
-                                it.name = support.toIDMultiple("Var", i.toString)
-                        ]
-                        relationVar2VLS.add(v)
-                        val varTypeComply = createVLSFunction => [
-                                it.constant = support.toIDMultiple("t", (r.parameters.get(i) as ComplexTypeReference).referred.name)
-                                it.terms += createVLSVariable => [
-                                        it.name = support.toIDMultiple("Var", i.toString)
-                                ]
-                        ]
-                        relationVar2TypeDecComply.add(varTypeComply)
-                }
-                
-                val comply = createVLSFofFormula => [
-                        it.name = support.toIDMultiple("compliance", r.name)
-                        it.fofRole = "axiom"
-                        it.fofFormula = createVLSUniversalQuantifier => [
-                                
-                                for (i : 0..<r.parameters.length) {
-                                        val v = createVLSVariable => [
-                                                it.name = relationVar2VLS.get(i).name
-                                        ]
-                                        it.variables += v
-                                }
-                                
-                                it.operand = createVLSImplies => [
-                                        it.left = createVLSFunction => [
-                                                it.constant = support.toIDMultiple("rel", r.name)
-                                                
-                                                for (i : 0..<r.parameters.length) {
-                                                        val v = createVLSVariable => [
-                                                                it.name = relationVar2VLS.get(i).name
-                                                        ]
-                                                        it.terms += v
-                                                }
-                                                
-                                        ]
-                                        it.right = support.unfoldAnd(relationVar2TypeDecComply)
-                                ]
-                        ]
-                ]
-                // trace.relationDefinition2Predicate.put(r,res)
-                trace.specification.formulas += comply
-        }
 }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index 06ec585c..090cf916 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -1,20 +1,21 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
 import java.util.ArrayList
 import java.util.HashMap
 import java.util.List
 import java.util.Map
 import org.eclipse.emf.common.util.EList
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality
 class Logic2VampireLanguageMapper_Support {
        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -28,10 +29,28 @@ class Logic2VampireLanguageMapper_Support {
                ids.split("\\s+").join("_")
        }
+        //Term Handling
        //TODO Make more general
-        def protected VLSVariable duplicate(VLSVariable vrbl) {
+        def protected VLSVariable duplicate(VLSVariable term) {
-                return createVLSVariable => [it.name = vrbl.name]
+                return createVLSVariable => [it.name = term.name]
+        }
+        
+        def protected VLSFunction duplicate(VLSFunction term) {
+                return createVLSFunction => [
+                        it.constant = term.constant
+                        for ( v : term.terms){
+                                it.terms += duplicate(v as VLSVariable)
+                        }
+                        ]
        }
+        
+        def protected VLSFunction duplicate(VLSFunction term, VLSVariable v) {
+                return createVLSFunction => [
+                        it.constant = term.constant
+                        it.terms += duplicate(v)
+                        ]
+        }
+        
        def protected VLSFunction topLevelTypeFunc() {
                return createVLSFunction => [
@@ -175,6 +194,21 @@ class Logic2VampireLanguageMapper_Support {
                ]
        }
+        
+        def protected boolean dfsSupertypeCheck(Type type, Type type2) {
+                // There is surely a better way to do this
+                if (type.supertypes.isEmpty)
+                        return false
+                else {
+                        if (type.supertypes.contains(type2))
+                                return true
+                        else {
+                                for (supertype : type.supertypes) {
+                                        if(dfsSupertypeCheck(supertype, type2)) return true
+                                }
+                        }
+                }
+        }
        def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) {
                new HashMap(map1) => [putAll(map2)]
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
index 88e1e23a..ea72940e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -22,21 +22,20 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                LogicproblemPackage.eINSTANCE.class
        }
-        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements,
+        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
-                Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
+                
-                val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
+//              val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
-                trace.typeMapperTrace = typeTrace
+//              trace.typeMapperTrace = typeTrace
-                // The variable
                val VLSVariable variable = createVLSVariable => [it.name = "A"]
                // 1. Each type (class) is a predicate with a single variable as input
                for (type : types) {
                        val typePred = createVLSFunction => [
-                                it.constant = support.toIDMultiple("t", type.name)
+                                it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
                                it.terms += support.duplicate(variable)
                        ]
-                        typeTrace.type2Predicate.put(type, typePred)
+//                      typeTrace.type2Predicate.put(type, typePred)
+                        trace.type2Predicate.put(type, typePred)
                }
                // 2. Map each ENUM type definition to fof formula
@@ -44,15 +43,16 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                        val List<VLSFunction> orElems = newArrayList
                        for (e : type.elements) {
                                val enumElemPred = createVLSFunction => [
-                                        it.constant = support.toIDMultiple("e", e.name, type.name)
+                                        it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2))
                                        it.terms += support.duplicate(variable)
                                ]
-                                typeTrace.element2Predicate.put(e, enumElemPred)
+//                              typeTrace.element2Predicate.put(e, enumElemPred)
+                                trace.element2Predicate.put(e, enumElemPred)
                                orElems.add(enumElemPred)
                        }
                        val res = createVLSFofFormula => [
-                                it.name = support.toIDMultiple("typeDef", type.name)
+                                it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
                                // below is temporary solution
                                it.fofRole = "axiom"
                                it.fofFormula = createVLSUniversalQuantifier => [
@@ -62,7 +62,8 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
 //                                                      it.constant = type.lookup(typeTrace.type2Predicate).constant
 //                                                      it.terms += createVLSVariable => [it.name = "A"]
 //                                              ]
-                                                it.left = type.lookup(typeTrace.type2Predicate)
+//                                              it.left = type.lookup(typeTrace.type2Predicate)
+                                                it.left = type.lookup(trace.type2Predicate)
                                                it.right = support.unfoldOr(orElems)
@@ -92,31 +93,23 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                for (t1 : types.filter[!isIsAbstract]) {
                        for (t2 : types) {
                                // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
-                                if (t1 == t2 || dfsSupertypeCheck(t1, t2)) {
+                                if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
-                                        typeTrace.type2PossibleNot.put(t2, createVLSFunction => [
+//                                      typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
-                                                it.constant = t2.lookup(typeTrace.type2Predicate).constant
+                                        trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
-                                                it.terms += support.duplicate(variable)
-                                        ])
                                } else {
-                                        typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
+//                                      typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
-                                                it.operand = createVLSFunction => [
+                                        trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
-                                                        it.constant = t2.lookup(typeTrace.type2Predicate).constant
+                                                it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
-                                                        it.terms += support.duplicate(variable)
-                                                ]
                                        ])
                                }
-//                              typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate))
                        }
-                        typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
+//                      typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
-//                      typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) )
+//                      typeTrace.type2PossibleNot.clear
-                        typeTrace.type2PossibleNot.clear
+                        trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values)))
+                        trace.type2PossibleNot.clear
                }
                // 5. create fof function that is an or with all the elements in map
-                
-                
-                
-                
                val hierarch = createVLSFofFormula => [
                        it.name = "hierarchyHandler"
                        it.fofRole = "axiom"
@@ -124,7 +117,8 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                                it.variables += support.duplicate(variable)
                                it.operand = createVLSEquivalent => [
                                        it.left = support.topLevelTypeFunc
-                                        it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
+//                                      it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
+                                        it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values))
                                ]
                        ]
                ]
@@ -133,21 +127,6 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
        }
-        def boolean dfsSupertypeCheck(Type type, Type type2) {
-                // There is surely a better way to do this
-                if (type.supertypes.isEmpty)
-                        return false
-                else {
-                        if (type.supertypes.contains(type2))
-                                return true
-                        else {
-                                for (supertype : type.supertypes) {
-                                        if(dfsSupertypeCheck(supertype, type2)) return true
-                                }
-                        }
-                }
-        }
        override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
                Logic2VampireLanguageMapperTrace trace) {
                throw new UnsupportedOperationException("TODO: auto-generated method stub")
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index 4a4eedf5..bda7463e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index 55f0ac1e..a062fcec 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index e91f89cc..5fc0da27 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index 154ff393..562b9bbf 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index 5d6ad730..dd7bdf86 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 7c787543..496d27b3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 34f3b285..4a03f2ce 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index f8d6cd3f..511f4a1f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index 7b2b11f8..37e9480c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
index 7e8336e2..f473c4bc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
index a2229dba..e53791d6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index d82649ff..1b112c56 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index 030a0be9..c8284658 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
index 87203ed8..89d4c657 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
index 65689b0c..3c98bd64 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
index 855815f8..2b491209 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
@@ -8,8 +8,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
 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.RelationDeclaration;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition;
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
 import java.util.HashMap;
 import java.util.Map;
@@ -24,10 +26,20 @@ public class Logic2VampireLanguageMapperTrace {
  
  public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace;
  
+  public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();
+  
+  public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>();
+  
+  public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>();
+  
+  public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>();
+  
  public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions;
  
  public Map<RelationDeclaration, RelationDefinition> relationDefinitions;
  
+  public Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap<RelationDeclaration, VLSFunction>();
+  
  public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>();
  
  public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>();
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
index bce50fcc..4f5c6acc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -15,6 +15,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
 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.Type;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
@@ -44,17 +45,84 @@ public class Logic2VampireLanguageMapper_RelationMapper {
    this.base = base;
  }
  
-  public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace) {
+  public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) {
+    final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>();
+    final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>();
+    final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();
+    int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
+    ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true);
+    for (final Integer i : _doubleDotLessThan) {
+      {
+        VLSVariable _createVLSVariable = this.factory.createVLSVariable();
+        final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
+          it.setName(this.support.toIDMultiple("V", i.toString()));
+        };
+        final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
+        relVar2VLS.add(v);
+        TypeReference _get = r.getParameters().get((i).intValue());
+        final Type relType = ((ComplexTypeReference) _get).getReferred();
+        final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v);
+        relVar2TypeDecComply.add(varTypeComply);
+      }
+    }
+    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
+    final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
+      final String[] nameArray = r.getName().split(" ");
+      it.setName(this.support.toIDMultiple("compliance", nameArray[0], 
+        nameArray[2]));
+      it.setFofRole("axiom");
+      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
+      final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
+        for (final VLSVariable v : relVar2VLS) {
+          EList<VLSVariable> _variables = it_1.getVariables();
+          VLSVariable _duplicate = this.support.duplicate(v);
+          _variables.add(_duplicate);
+        }
+        VLSImplies _createVLSImplies = this.factory.createVLSImplies();
+        final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {
+          VLSFunction _createVLSFunction = this.factory.createVLSFunction();
+          final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {
+            it_3.setConstant(this.support.toIDMultiple("rel", r.getName()));
+            int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
+            ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true);
+            for (final Integer i_1 : _doubleDotLessThan_1) {
+              {
+                VLSVariable _createVLSVariable = this.factory.createVLSVariable();
+                final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> {
+                  it_4.setName(relVar2VLS.get((i_1).intValue()).getName());
+                };
+                final VLSVariable v_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);
+                EList<VLSTerm> _terms = it_3.getTerms();
+                _terms.add(v_1);
+              }
+            }
+          };
+          VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);
+          it_2.setLeft(_doubleArrow);
+          it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply));
+        };
+        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
+        it_1.setOperand(_doubleArrow);
+      };
+      VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
+      it.setFofFormula(_doubleArrow);
+    };
+    final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
+    EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
+    _formulas.add(comply);
+  }
+  
+  public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) {
    final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>();
    final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>();
    final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>();
    final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();
-    EList<Variable> _variables = r.getVariables();
+    EList<Variable> _variables = reldef.getVariables();
    for (final Variable variable : _variables) {
      {
        VLSVariable _createVLSVariable = this.factory.createVLSVariable();
        final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
-          it.setName(this.support.toIDMultiple("Var", variable.getName()));
+          it.setName(this.support.toIDMultiple("V", variable.getName()));
        };
        final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
        relationVar2VLS.put(variable, v);
@@ -63,56 +131,39 @@ public class Logic2VampireLanguageMapper_RelationMapper {
          TypeReference _range = variable.getRange();
          it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));
          EList<VLSTerm> _terms = it.getTerms();
-          VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
+          VLSVariable _duplicate = this.support.duplicate(v);
-          final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> {
+          _terms.add(_duplicate);
-            it_1.setName(this.support.toIDMultiple("Var", variable.getName()));
-          };
-          VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);
-          _terms.add(_doubleArrow);
        };
        final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
        relationVar2TypeDecComply.put(variable, varTypeComply);
-        VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction();
+        relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply));
-        final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> {
-          TypeReference _range = variable.getRange();
-          it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));
-          EList<VLSTerm> _terms = it.getTerms();
-          VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
-          final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> {
-            it_1.setName(this.support.toIDMultiple("Var", variable.getName()));
-          };
-          VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3);
-          _terms.add(_doubleArrow);
-        };
-        final VLSFunction varTypeRes = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_2);
-        relationVar2TypeDecRes.put(variable, varTypeRes);
      }
    }
    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
    final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
-      it.setName(this.support.toIDMultiple("compliance", r.getName()));
+      final String[] nameArray = reldef.getName().split(" ");
+      int _length = nameArray.length;
+      int _minus = (_length - 2);
+      int _length_1 = nameArray.length;
+      int _minus_1 = (_length_1 - 1);
+      it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], 
+        nameArray[_minus_1]));
      it.setFofRole("axiom");
      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
      final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
-        EList<Variable> _variables_1 = r.getVariables();
+        EList<Variable> _variables_1 = reldef.getVariables();
        for (final Variable variable_1 : _variables_1) {
-          {
+          EList<VLSVariable> _variables_2 = it_1.getVariables();
-            VLSVariable _createVLSVariable = this.factory.createVLSVariable();
+          VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS));
-            final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> {
+          _variables_2.add(_duplicate);
-              it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName());
-            };
-            final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2);
-            EList<VLSVariable> _variables_2 = it_1.getVariables();
-            _variables_2.add(v);
-          }
        }
        VLSImplies _createVLSImplies = this.factory.createVLSImplies();
        final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {
          VLSFunction _createVLSFunction = this.factory.createVLSFunction();
          final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {
-            it_3.setConstant(this.support.toIDMultiple("rel", r.getName()));
+            it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName()));
-            EList<Variable> _variables_2 = r.getVariables();
+            EList<Variable> _variables_3 = reldef.getVariables();
-            for (final Variable variable_2 : _variables_2) {
+            for (final Variable variable_2 : _variables_3) {
              {
                VLSVariable _createVLSVariable = this.factory.createVLSVariable();
                final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> {
@@ -139,11 +190,11 @@ public class Logic2VampireLanguageMapper_RelationMapper {
    final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
    VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
    final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
-      it.setName(this.support.toIDMultiple("relation", r.getName()));
+      it.setName(this.support.toIDMultiple("relation", reldef.getName()));
      it.setFofRole("axiom");
      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
      final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
-        EList<Variable> _variables_1 = r.getVariables();
+        EList<Variable> _variables_1 = reldef.getVariables();
        for (final Variable variable_1 : _variables_1) {
          {
            VLSVariable _createVLSVariable = this.factory.createVLSVariable();
@@ -164,8 +215,8 @@ public class Logic2VampireLanguageMapper_RelationMapper {
          final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> {
            VLSFunction _createVLSFunction = this.factory.createVLSFunction();
            final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> {
-              it_4.setConstant(this.support.toIDMultiple("rel", r.getName()));
+              it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName()));
-              EList<Variable> _variables_2 = r.getVariables();
+              EList<Variable> _variables_2 = reldef.getVariables();
              for (final Variable variable_2 : _variables_2) {
                {
                  VLSVariable _createVLSVariable = this.factory.createVLSVariable();
@@ -180,7 +231,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
            };
            VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5);
            it_3.setLeft(_doubleArrow);
-            it_3.setRight(this.base.transformTerm(r.getValue(), trace, relationVar2VLS));
+            it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS));
          };
          VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);
          it_2.setRight(_doubleArrow);
@@ -198,89 +249,6 @@ public class Logic2VampireLanguageMapper_RelationMapper {
    _formulas_1.add(res);
  }
  
-  public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) {
-    final List<VLSVariable> relationVar2VLS = new ArrayList<VLSVariable>();
-    final List<VLSFunction> relationVar2TypeDecComply = new ArrayList<VLSFunction>();
-    final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();
-    int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
-    ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true);
-    for (final Integer i : _doubleDotLessThan) {
-      {
-        VLSVariable _createVLSVariable = this.factory.createVLSVariable();
-        final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
-          it.setName(this.support.toIDMultiple("Var", i.toString()));
-        };
-        final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
-        relationVar2VLS.add(v);
-        VLSFunction _createVLSFunction = this.factory.createVLSFunction();
-        final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
-          TypeReference _get = r.getParameters().get((i).intValue());
-          it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _get).getReferred().getName()));
-          EList<VLSTerm> _terms = it.getTerms();
-          VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
-          final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> {
-            it_1.setName(this.support.toIDMultiple("Var", i.toString()));
-          };
-          VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);
-          _terms.add(_doubleArrow);
-        };
-        final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
-        relationVar2TypeDecComply.add(varTypeComply);
-      }
-    }
-    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
-    final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
-      it.setName(this.support.toIDMultiple("compliance", r.getName()));
-      it.setFofRole("axiom");
-      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-      final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
-        int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
-        ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true);
-        for (final Integer i_1 : _doubleDotLessThan_1) {
-          {
-            VLSVariable _createVLSVariable = this.factory.createVLSVariable();
-            final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> {
-              it_2.setName(relationVar2VLS.get((i_1).intValue()).getName());
-            };
-            final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2);
-            EList<VLSVariable> _variables = it_1.getVariables();
-            _variables.add(v);
-          }
-        }
-        VLSImplies _createVLSImplies = this.factory.createVLSImplies();
-        final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {
-          VLSFunction _createVLSFunction = this.factory.createVLSFunction();
-          final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {
-            it_3.setConstant(this.support.toIDMultiple("rel", r.getName()));
-            int _length_2 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
-            ExclusiveRange _doubleDotLessThan_2 = new ExclusiveRange(0, _length_2, true);
-            for (final Integer i_2 : _doubleDotLessThan_2) {
-              {
-                VLSVariable _createVLSVariable = this.factory.createVLSVariable();
-                final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> {
-                  it_4.setName(relationVar2VLS.get((i_2).intValue()).getName());
-                };
-                final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);
-                EList<VLSTerm> _terms = it_3.getTerms();
-                _terms.add(v);
-              }
-            }
-          };
-          VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);
-          it_2.setLeft(_doubleArrow);
-          it_2.setRight(this.support.unfoldAnd(relationVar2TypeDecComply));
-        };
-        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
-        it_1.setOperand(_doubleArrow);
-      };
-      VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
-      it.setFofFormula(_doubleArrow);
-    };
-    final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
-    EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
-    _formulas.add(comply);
-  }
-  
  public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) {
    if (r instanceof RelationDeclaration) {
      _transformRelation((RelationDeclaration)r, trace);
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
index dfe624be..35497eab 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -17,6 +17,7 @@ import com.google.common.collect.Iterables;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term;
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
 import java.util.ArrayList;
@@ -52,14 +53,39 @@ public class Logic2VampireLanguageMapper_Support {
    return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_");
  }
  
-  protected VLSVariable duplicate(final VLSVariable vrbl) {
+  protected VLSVariable duplicate(final VLSVariable term) {
    VLSVariable _createVLSVariable = this.factory.createVLSVariable();
    final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
-      it.setName(vrbl.getName());
+      it.setName(term.getName());
    };
    return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
  }
  
+  protected VLSFunction duplicate(final VLSFunction term) {
+    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
+    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
+      it.setConstant(term.getConstant());
+      EList<VLSTerm> _terms = term.getTerms();
+      for (final VLSTerm v : _terms) {
+        EList<VLSTerm> _terms_1 = it.getTerms();
+        VLSVariable _duplicate = this.duplicate(((VLSVariable) v));
+        _terms_1.add(_duplicate);
+      }
+    };
+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
+  }
+  
+  protected VLSFunction duplicate(final VLSFunction term, final VLSVariable v) {
+    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
+    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
+      it.setConstant(term.getConstant());
+      EList<VLSTerm> _terms = it.getTerms();
+      VLSVariable _duplicate = this.duplicate(v);
+      _terms.add(_duplicate);
+    };
+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
+  }
+  
  protected VLSFunction topLevelTypeFunc() {
    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
@@ -287,6 +313,30 @@ public class Logic2VampireLanguageMapper_Support {
    return _xblockexpression;
  }
  
+  protected boolean dfsSupertypeCheck(final Type type, final Type type2) {
+    boolean _xifexpression = false;
+    boolean _isEmpty = type.getSupertypes().isEmpty();
+    if (_isEmpty) {
+      return false;
+    } else {
+      boolean _xifexpression_1 = false;
+      boolean _contains = type.getSupertypes().contains(type2);
+      if (_contains) {
+        return true;
+      } else {
+        EList<Type> _supertypes = type.getSupertypes();
+        for (final Type supertype : _supertypes) {
+          boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2);
+          if (_dfsSupertypeCheck) {
+            return true;
+          }
+        }
+      }
+      _xifexpression = _xifexpression_1;
+    }
+    return _xifexpression;
+  }
+  
  protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) {
    HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1);
    final Procedure1<HashMap<Variable, VLSVariable>> _function = (HashMap<Variable, VLSVariable> it) -> {
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
index 1e845d94..b582fb96 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
@@ -4,7 +4,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
@@ -46,8 +45,6 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
  
  @Override
  public void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {
-    final Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes();
-    trace.typeMapperTrace = typeTrace;
    VLSVariable _createVLSVariable = this.factory.createVLSVariable();
    final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
      it.setName("A");
@@ -57,13 +54,13 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
      {
        VLSFunction _createVLSFunction = this.factory.createVLSFunction();
        final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
-          it.setConstant(this.support.toIDMultiple("t", type.getName()));
+          it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0]));
          EList<VLSTerm> _terms = it.getTerms();
          VLSVariable _duplicate = this.support.duplicate(variable);
          _terms.add(_duplicate);
        };
        final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
-        typeTrace.type2Predicate.put(type, typePred);
+        trace.type2Predicate.put(type, typePred);
      }
    }
    Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);
@@ -75,19 +72,19 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
          {
            VLSFunction _createVLSFunction = this.factory.createVLSFunction();
            final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
-              it.setConstant(this.support.toIDMultiple("e", e.getName(), type_1.getName()));
+              it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2]));
              EList<VLSTerm> _terms = it.getTerms();
              VLSVariable _duplicate = this.support.duplicate(variable);
              _terms.add(_duplicate);
            };
            final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
-            typeTrace.element2Predicate.put(e, enumElemPred);
+            trace.element2Predicate.put(e, enumElemPred);
            orElems.add(enumElemPred);
          }
        }
        VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
        final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
-          it.setName(this.support.toIDMultiple("typeDef", type_1.getName()));
+          it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0]));
          it.setFofRole("axiom");
          VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
          final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
@@ -96,7 +93,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
            _variables.add(_duplicate);
            VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
            final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> {
-              it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate));
+              it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate));
              it_2.setRight(this.support.unfoldOr(orElems));
            };
            VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);
@@ -118,37 +115,21 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
    for (final Type t1 : _filter_1) {
      {
        for (final Type t2 : types) {
-          if ((Objects.equal(t1, t2) || this.dfsSupertypeCheck(t1, t2))) {
+          if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) {
-            VLSFunction _createVLSFunction = this.factory.createVLSFunction();
+            trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
-            final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> {
-              it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(t2, typeTrace.type2Predicate).getConstant());
-              EList<VLSTerm> _terms = it.getTerms();
-              VLSVariable _duplicate = this.support.duplicate(variable);
-              _terms.add(_duplicate);
-            };
-            VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2);
-            typeTrace.type2PossibleNot.put(t2, _doubleArrow);
          } else {
            VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
-            final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {
+            final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> {
-              VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction();
+              it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
-              final Procedure1<VLSFunction> _function_4 = (VLSFunction it_1) -> {
-                it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(t2, typeTrace.type2Predicate).getConstant());
-                EList<VLSTerm> _terms = it_1.getTerms();
-                VLSVariable _duplicate = this.support.duplicate(variable);
-                _terms.add(_duplicate);
-              };
-              VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_4);
-              it.setOperand(_doubleArrow_1);
            };
-            VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);
+            VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);
-            typeTrace.type2PossibleNot.put(t2, _doubleArrow_1);
+            trace.type2PossibleNot.put(t2, _doubleArrow);
          }
        }
-        Collection<VLSTerm> _values = typeTrace.type2PossibleNot.values();
+        Collection<VLSTerm> _values = trace.type2PossibleNot.values();
        ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
-        typeTrace.type2And.put(t1, this.support.unfoldAnd(_arrayList));
+        trace.type2And.put(t1, this.support.unfoldAnd(_arrayList));
-        typeTrace.type2PossibleNot.clear();
+        trace.type2PossibleNot.clear();
      }
    }
    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
@@ -163,7 +144,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
        VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
        final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> {
          it_2.setLeft(this.support.topLevelTypeFunc());
-          Collection<VLSTerm> _values = typeTrace.type2And.values();
+          Collection<VLSTerm> _values = trace.type2And.values();
          ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
          it_2.setRight(this.support.unfoldOr(_arrayList));
        };
@@ -178,30 +159,6 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
    _formulas.add(hierarch);
  }
  
-  public boolean dfsSupertypeCheck(final Type type, final Type type2) {
-    boolean _xifexpression = false;
-    boolean _isEmpty = type.getSupertypes().isEmpty();
-    if (_isEmpty) {
-      return false;
-    } else {
-      boolean _xifexpression_1 = false;
-      boolean _contains = type.getSupertypes().contains(type2);
-      if (_contains) {
-        return true;
-      } else {
-        EList<Type> _supertypes = type.getSupertypes();
-        for (final Type supertype : _supertypes) {
-          boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2);
-          if (_dfsSupertypeCheck) {
-            return true;
-          }
-        }
-      }
-      _xifexpression = _xifexpression_1;
-    }
-    return _xifexpression;
-  }
-  
  @Override
  public List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {
    throw new UnsupportedOperationException("TODO: auto-generated method stub");
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
index 1f220d6f..865b3155 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
@@ -1,25 +1,25 @@
 % This is an initial Test Comment
-fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( t_FunctionType_enum ( A ) <=> ( e_Root_literal_FunctionType_FunctionType_enum ( A ) | ( e_Intermediate_literal_FunctionType_FunctionType_enum ( A ) | e_Leaf_literal_FunctionType_FunctionType_enum ( A ) ) ) ) ) .
+fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) .
-fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
+fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalData ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
 fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) .
 fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) .
-fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) .
+fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_interface_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
-fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) .
+fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_model_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) .
-fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_Function_class ( Var_1 ) ) ) ) .
+fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_parent_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) .
-fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( t_FunctionalArchitectureModel_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) .
+fof ( compliance_rootElements_FunctionalArchitectureModel , axiom , ! [ V_0 , V_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( V_0 , V_1 ) => ( t_FunctionalArchitectureModel ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
-fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) .
+fof ( compliance_subElements_Function , axiom , ! [ V_0 , V_1 ] : ( rel_subElements_reference_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
-fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( t_FAMTerminator_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) .
+fof ( compliance_data_FAMTerminator , axiom , ! [ V_0 , V_1 ] : ( rel_data_reference_FAMTerminator ( V_0 , V_1 ) => ( t_FAMTerminator ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) .
-fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalOutput_class ( Var_1 ) ) ) ) .
+fof ( compliance_from_InformationLink , axiom , ! [ V_0 , V_1 ] : ( rel_from_reference_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalOutput ( V_1 ) ) ) ) .
-fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalInput_class ( Var_1 ) ) ) ) .
+fof ( compliance_to_InformationLink , axiom , ! [ V_0 , V_1 ] : ( rel_to_reference_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalInput ( V_1 ) ) ) ) .
-fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) .
+fof ( compliance_data_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( rel_data_reference_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) .
-fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) .
+fof ( compliance_element_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( rel_element_reference_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
-fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( t_FunctionalInput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) .
+fof ( compliance_IncomingLinks_FunctionalInput , axiom , ! [ V_0 , V_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( V_0 , V_1 ) => ( t_FunctionalInput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) .
-fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( t_FunctionalOutput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) .
+fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( V_0 , V_1 ) => ( t_FunctionalOutput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) .
-fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FAMTerminator_class ( Var_1 ) ) ) ) .
+fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( rel_terminator_reference_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) .
-fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) .
+fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( rel_interface_reference_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
-fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionType_enum ( Var_1 ) ) ) ) .
+fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( rel_type_attribute_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) .
-fof ( compliance_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) => ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) ) ) .
+fof ( compliance_queries_terminatorAndInformation , axiom , ! [ V_parameter_T , V_parameter_I ] : ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( V_parameter_T , V_parameter_I ) => ( t_FAMTerminator_class ( V_parameter_T ) & t_InformationLink_class ( V_parameter_I ) ) ) ) .
-fof ( relation_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) => ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( t_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , Var_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , Var_parameter_T ) ) ) | ? [ Var_variable_In ] : ( t_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( Var_parameter_I , Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , Var_parameter_T ) ) ) ) ) ) ) .
+fof ( relation_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ V_parameter_T , V_parameter_I ] : ( ( t_FAMTerminator_class ( V_parameter_T ) & t_InformationLink_class ( V_parameter_I ) ) => ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( V_parameter_T , V_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( t_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , V_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , V_parameter_T ) ) ) | ? [ Var_variable_In ] : ( t_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( V_parameter_I , Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , V_parameter_T ) ) ) ) ) ) ) .
 fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
 fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( t_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) .
 fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & t_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
index 59a3bc01..2cd47088 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
index ebca0881..b4d3bda8 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
index e9359697..ece511d9 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
index 1f7b3ee7..a7cea425 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
Binary files differ
author	ArenBabikian <aren.babikian@mail.mcgill.ca>	2019-03-05 21:33:28 -0500
committer	ArenBabikian <aren.babikian@mail.mcgill.ca>	2019-03-05 21:33:28 -0500
commit	89929078ca93c74a80ad70d58934d5d6d43d0e4f (patch)
tree	a8dd965a65a3545b9919f1276151b509d29c82e2
parent	Implement type scope handling (diff)
download	VIATRA-Generator-89929078ca93c74a80ad70d58934d5d6d43d0e4f.tar.gz VIATRA-Generator-89929078ca93c74a80ad70d58934d5d6d43d0e4f.tar.zst VIATRA-Generator-89929078ca93c74a80ad70d58934d5d6d43d0e4f.zip