Partially improve coding style (leaving for soccer)

4 files changed, 157 insertions, 145 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.name = support.toIDMultiple("Var", variable.name)
-                                ]
+                                it.terms += support.duplicate(v)
                         ]
                         relationVar2TypeDecComply.put(variable, 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)
+                        relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
                 }
 
                 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) {
-                                        val v = createVLSVariable => [
-                                                it.name = variable.lookup(relationVar2VLS).name
-                                        ]
-                                        it.variables += v
+                                for (variable : reldef.variables) {
+                                        it.variables += support.duplicate(variable.lookup(relationVar2VLS))
 
                                 }
                                 it.operand = createVLSImplies => [
                                         it.left = createVLSFunction => [
-                                                it.constant = support.toIDMultiple("rel", r.name)
-                                                for (variable : r.variables) {
+                                                it.constant = support.toIDMultiple("rel", reldef.name)
+                                                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)
-                                                        for (variable : r.variables) {
+                                                        it.constant = support.toIDMultiple("rel", reldef.name)
+                                                        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) {
-                return createVLSVariable => [it.name = vrbl.name]
+        def protected VLSVariable duplicate(VLSVariable term) {
+                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,
-                Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
-                val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
-                trace.typeMapperTrace = typeTrace
-
-                // The variable
+        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
+                
+//              val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
+//              trace.typeMapperTrace = typeTrace
                 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)) {
-                                        typeTrace.type2PossibleNot.put(t2, createVLSFunction => [
-                                                it.constant = t2.lookup(typeTrace.type2Predicate).constant
-                                                it.terms += support.duplicate(variable)
-                                        ])
+                                if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
+//                                      typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
+                                        trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
                                 } else {
-                                        typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
-                                                it.operand = createVLSFunction => [
-                                                        it.constant = t2.lookup(typeTrace.type2Predicate).constant
-                                                        it.terms += support.duplicate(variable)
-                                                ]
+//                                      typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
+                                        trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
+                                                it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
                                         ])
                                 }
-//                              typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate))
                         }
-                        typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
-//                      typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) )
-                        typeTrace.type2PossibleNot.clear
+//                      typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
+//                      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")