Restructure Vampire Reasoner project

43 files changed, 332 insertions, 384 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
index fef8d621..89a95266 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
index 3c37bd02..362c1696 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
index 76127556..67fbde4f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
index 467395cb..2f2eaa65 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
index 601c5a4c..4ff50857 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
index c60c4d59..bce7ab42 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
index 030267ff..b6c23926 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
index ef7ffcdf..19d1d4f6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
index 219fec58..503b9b33 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
index 47712412..279b2fbb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
index 831f0df4..bcff04c1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
index 696d67c0..66b7827f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
index 9bef3ff9..5bac2912 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
index dd65afb4..7cafc3c7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
index ee802a99..1d56892e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -3,7 +3,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner
 import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
 import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
@@ -14,6 +13,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper
 
 class VampireSolver extends LogicReasoner {
 
@@ -23,8 +23,7 @@ class VampireSolver extends LogicReasoner {
                 VampireLanguageStandaloneSetup::doSetup()
         }
 
-        val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(
-                new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
+        val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper
         val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
         val VampireHandler handler = new VampireHandler
 
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index 81af24e5..1dbc0055 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -51,11 +51,8 @@ class Logic2VampireLanguageMapper {
                 this)
         @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(
                 this)
-        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper
-
-        public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) {
-                this.typeMapper = typeMapper
-        }
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(
+                this)
 
         public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem,
                 VampireSolverConfiguration config) {
@@ -82,8 +79,7 @@ class Logic2VampireLanguageMapper {
 
                 // SCOPE MAPPER
                 scopeMapper.transformScope(config, trace)
-                
-                
+
                 trace.constantDefinitions = problem.collectConstantDefinitions
                 trace.relationDefinitions = problem.collectRelationDefinitions
 
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
index 1f071635..bc0b3e23 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
@@ -1,19 +1,157 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
+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.VampireLanguageFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
+import java.util.ArrayList
 import java.util.Collection
 import java.util.List
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 
-interface Logic2VampireLanguageMapper_TypeMapper {
-        def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace);
-        //samples below 2 lines
-        def List<VLSTerm> transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace)
-        def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace)
-        
-        def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace)
-        def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace)
-        
-        def VampireModelInterpretation_TypeInterpretation getTypeInterpreter()
-}
\ No newline at end of file
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+
+class Logic2VampireLanguageMapper_TypeMapper  {
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+        val Logic2VampireLanguageMapper base
+
+        new(Logic2VampireLanguageMapper base) {
+                LogicproblemPackage.eINSTANCE.class
+                this.base = base
+        }
+
+        def protected 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.split(" ").get(0))
+                                it.terms += support.duplicate(variable)
+                        ]
+//                      typeTrace.type2Predicate.put(type, typePred)
+                        trace.type2Predicate.put(type, typePred)
+                }
+
+                // 2. Map each ENUM type definition to fof formula
+                for (type : types.filter(TypeDefinition)) {
+                        val List<VLSFunction> orElems = newArrayList
+                        for (e : type.elements) {
+                                val enumElemPred = createVLSFunction => [
+                                        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)
+                                trace.element2Predicate.put(e, enumElemPred)
+                                orElems.add(enumElemPred)
+                        }
+
+                        val res = createVLSFofFormula => [
+                                it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
+                                // below is temporary solution
+                                it.fofRole = "axiom"
+                                it.fofFormula = createVLSUniversalQuantifier => [
+                                        it.variables += support.duplicate(variable)
+                                        it.operand = createVLSEquivalent => [
+//                                              it.left = createVLSFunction => [
+//                                                      it.constant = type.lookup(typeTrace.type2Predicate).constant
+//                                                      it.terms += createVLSVariable => [it.name = "A"]
+//                                              ]
+//                                              it.left = type.lookup(typeTrace.type2Predicate)
+                                                it.left = type.lookup(trace.type2Predicate)
+
+                                                it.right = support.unfoldOr(orElems)
+
+                                        // TEMPPPPPPP
+//                                              it.right = support.unfoldOr(type.elements.map [e |
+//                                                      
+//                                                      createVLSEquality => [
+//                                                              it.left = support.duplicate(variable)
+//                                                              it.right = createVLSDoubleQuote => [
+//                                                                      it.value = "\"a" + e.name + "\""
+//                                                              ]
+//                                                      ]
+//                                              ])
+                                        // END TEMPPPPP
+                                        ]
+                                ]
+
+                        ]
+                        trace.specification.formulas += res
+                }
+                
+                //HIERARCHY HANDLER
+                
+                
+                // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
+                // and store in a map
+                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 || 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 => [
+                                        trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
+                                                it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
+                                        ])
+                                }
+                        }
+//                      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"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                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>(trace.type2And.values))
+                                ]
+                        ]
+                ]
+
+                trace.specification.formulas += hierarch
+
+        }
+
+        //below are from previous interface
+        def protected transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
+                Logic2VampireLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+        def protected getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+        def protected getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+        def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) {
+                createVLSDoubleQuote => [
+                        it.value = "\"a" + referred.name + "\""
+                ]
+        }
+
+        def protected getTypeInterpreter() {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+}
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
deleted file mode 100644
index ea72940e..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ /dev/null
@@ -1,153 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
-
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
-import java.util.ArrayList
-import java.util.Collection
-
-import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import java.util.List
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
-
-class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {
-        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
-        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
-
-        new() {
-                LogicproblemPackage.eINSTANCE.class
-        }
-
-        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.split(" ").get(0))
-                                it.terms += support.duplicate(variable)
-                        ]
-//                      typeTrace.type2Predicate.put(type, typePred)
-                        trace.type2Predicate.put(type, typePred)
-                }
-
-                // 2. Map each ENUM type definition to fof formula
-                for (type : types.filter(TypeDefinition)) {
-                        val List<VLSFunction> orElems = newArrayList
-                        for (e : type.elements) {
-                                val enumElemPred = createVLSFunction => [
-                                        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)
-                                trace.element2Predicate.put(e, enumElemPred)
-                                orElems.add(enumElemPred)
-                        }
-
-                        val res = createVLSFofFormula => [
-                                it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
-                                // below is temporary solution
-                                it.fofRole = "axiom"
-                                it.fofFormula = createVLSUniversalQuantifier => [
-                                        it.variables += support.duplicate(variable)
-                                        it.operand = createVLSEquivalent => [
-//                                              it.left = createVLSFunction => [
-//                                                      it.constant = type.lookup(typeTrace.type2Predicate).constant
-//                                                      it.terms += createVLSVariable => [it.name = "A"]
-//                                              ]
-//                                              it.left = type.lookup(typeTrace.type2Predicate)
-                                                it.left = type.lookup(trace.type2Predicate)
-
-                                                it.right = support.unfoldOr(orElems)
-
-                                        // TEMPPPPPPP
-//                                              it.right = support.unfoldOr(type.elements.map [e |
-//                                                      
-//                                                      createVLSEquality => [
-//                                                              it.left = support.duplicate(variable)
-//                                                              it.right = createVLSDoubleQuote => [
-//                                                                      it.value = "\"a" + e.name + "\""
-//                                                              ]
-//                                                      ]
-//                                              ])
-                                        // END TEMPPPPP
-                                        ]
-                                ]
-
-                        ]
-                        trace.specification.formulas += res
-                }
-                
-                //HIERARCHY HANDLER
-                
-                
-                // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
-                // and store in a map
-                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 || 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 => [
-                                        trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
-                                                it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
-                                        ])
-                                }
-                        }
-//                      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"
-                        it.fofFormula = createVLSUniversalQuantifier => [
-                                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>(trace.type2And.values))
-                                ]
-                        ]
-                ]
-
-                trace.specification.formulas += hierarch
-
-        }
-
-        override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
-                Logic2VampireLanguageMapperTrace trace) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
-        }
-
-        override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
-        }
-
-        override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
-        }
-
-        override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) {
-                createVLSDoubleQuote => [
-                        it.value = "\"a" + referred.name + "\""
-                ]
-        }
-
-        override getTypeInterpreter() {
-                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 4828107b..e0766c08 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
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 64061f82..c38c96ad 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
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
index 1846ba2e..d9d75887 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
@@ -5,7 +5,6 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;

@@ -31,8 +30,7 @@ public class VampireSolver extends LogicReasoner {
     VampireLanguageStandaloneSetup.doSetup();

   }

   

-  private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(

-    new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes());

+  private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper();

   

   private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper();

   

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 f0cd1c7c..2c091b47 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
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 7d15db96..b05fd2c1 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
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 8fed8f56..7f6519eb 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
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 a40e27e4..d30eebe5 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
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 4b6b4a1e..921b79bd 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
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 c3035658..6b8d1dc0 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
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 2e21736e..83e57283 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
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 83697125..5a0087bc 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
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 063650c5..7d090297 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
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 e36d2270..c8ab54c2 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
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 5e5be153..3306fa73 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
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index dc2cd5ec..afe77bbe 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -89,11 +89,7 @@ public class Logic2VampireLanguageMapper {
   private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this);

   

   @Accessors(AccessorType.PUBLIC_GETTER)

-  private final Logic2VampireLanguageMapper_TypeMapper typeMapper;

-  

-  public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) {

-    this.typeMapper = typeMapper;

-  }

+  private final Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(this);

   

   public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) {

     VLSComment _createVLSComment = this.factory.createVLSComment();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
index c55e2421..d3dddcfc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -2,24 +2,191 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation;

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;

+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.VLSUnaryNegation;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

+import com.google.common.base.Objects;

+import com.google.common.collect.Iterables;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;

+import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;

+import java.util.ArrayList;

 import java.util.Collection;

 import java.util.List;

+import org.eclipse.emf.common.util.EList;

+import org.eclipse.xtext.xbase.lib.CollectionLiterals;

+import org.eclipse.xtext.xbase.lib.Extension;

+import org.eclipse.xtext.xbase.lib.Functions.Function1;

+import org.eclipse.xtext.xbase.lib.IterableExtensions;

+import org.eclipse.xtext.xbase.lib.ObjectExtensions;

+import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;

 

 @SuppressWarnings("all")

-public interface Logic2VampireLanguageMapper_TypeMapper {

-  public abstract void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace);

+public class Logic2VampireLanguageMapper_TypeMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

   

-  public abstract List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace);

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

   

-  public abstract VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace);

+  private final Logic2VampireLanguageMapper base;

   

-  public abstract int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace);

+  public Logic2VampireLanguageMapper_TypeMapper(final Logic2VampireLanguageMapper base) {

+    LogicproblemPackage.eINSTANCE.getClass();

+    this.base = base;

+  }

   

-  public abstract VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace);

+  protected boolean transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {

+    boolean _xblockexpression = false;

+    {

+      VLSVariable _createVLSVariable = this.factory.createVLSVariable();

+      final Procedure1<VLSVariable> _function = (VLSVariable it) -> {

+        it.setName("A");

+      };

+      final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);

+      for (final Type type : types) {

+        {

+          VLSFunction _createVLSFunction = this.factory.createVLSFunction();

+          final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {

+            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);

+          trace.type2Predicate.put(type, typePred);

+        }

+      }

+      Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);

+      for (final TypeDefinition type_1 : _filter) {

+        {

+          final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();

+          EList<DefinedElement> _elements = type_1.getElements();

+          for (final DefinedElement e : _elements) {

+            {

+              VLSFunction _createVLSFunction = this.factory.createVLSFunction();

+              final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {

+                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);

+              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().split(" ")[0]));

+            it.setFofRole("axiom");

+            VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

+            final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {

+              EList<VLSVariable> _variables = it_1.getVariables();

+              VLSVariable _duplicate = this.support.duplicate(variable);

+              _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, trace.type2Predicate));

+                it_2.setRight(this.support.unfoldOr(orElems));

+              };

+              VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);

+              it_1.setOperand(_doubleArrow);

+            };

+            VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);

+            it.setFofFormula(_doubleArrow);

+          };

+          final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);

+          EList<VLSFofFormula> _formulas = trace.specification.getFormulas();

+          _formulas.add(res);

+        }

+      }

+      final Function1<Type, Boolean> _function_1 = (Type it) -> {

+        boolean _isIsAbstract = it.isIsAbstract();

+        return Boolean.valueOf((!_isIsAbstract));

+      };

+      Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);

+      for (final Type t1 : _filter_1) {

+        {

+          for (final Type t2 : types) {

+            if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) {

+              trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));

+            } else {

+              VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

+              final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> {

+                it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));

+              };

+              VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);

+              trace.type2PossibleNot.put(t2, _doubleArrow);

+            }

+          }

+          Collection<VLSTerm> _values = trace.type2PossibleNot.values();

+          ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);

+          trace.type2And.put(t1, this.support.unfoldAnd(_arrayList));

+          trace.type2PossibleNot.clear();

+        }

+      }

+      VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

+      final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {

+        it.setName("hierarchyHandler");

+        it.setFofRole("axiom");

+        VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

+        final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> {

+          EList<VLSVariable> _variables = it_1.getVariables();

+          VLSVariable _duplicate = this.support.duplicate(variable);

+          _variables.add(_duplicate);

+          VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

+          final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> {

+            it_2.setLeft(this.support.topLevelTypeFunc());

+            Collection<VLSTerm> _values = trace.type2And.values();

+            ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);

+            it_2.setRight(this.support.unfoldOr(_arrayList));

+          };

+          VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);

+          it_1.setOperand(_doubleArrow);

+        };

+        VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3);

+        it.setFofFormula(_doubleArrow);

+      };

+      final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);

+      EList<VLSFofFormula> _formulas = trace.specification.getFormulas();

+      _xblockexpression = _formulas.add(hierarch);

+    }

+    return _xblockexpression;

+  }

   

-  public abstract VampireModelInterpretation_TypeInterpretation getTypeInterpreter();

+  protected void transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {

+    throw new UnsupportedOperationException("TODO: auto-generated method stub");

+  }

+  

+  protected void getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) {

+    throw new UnsupportedOperationException("TODO: auto-generated method stub");

+  }

+  

+  protected void getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) {

+    throw new UnsupportedOperationException("TODO: auto-generated method stub");

+  }

+  

+  protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) {

+    VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote();

+    final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> {

+      String _name = referred.getName();

+      String _plus = ("\"a" + _name);

+      String _plus_1 = (_plus + "\"");

+      it.setValue(_plus_1);

+    };

+    return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function);

+  }

+  

+  protected void getTypeInterpreter() {

+    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/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
deleted file mode 100644
index b582fb96..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
+++ /dev/null
@@ -1,193 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

-

-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

-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.VampireModelInterpretation_TypeInterpretation;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;

-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.VLSUnaryNegation;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

-import com.google.common.base.Objects;

-import com.google.common.collect.Iterables;

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;

-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;

-import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;

-import java.util.ArrayList;

-import java.util.Collection;

-import java.util.List;

-import org.eclipse.emf.common.util.EList;

-import org.eclipse.xtext.xbase.lib.CollectionLiterals;

-import org.eclipse.xtext.xbase.lib.Extension;

-import org.eclipse.xtext.xbase.lib.Functions.Function1;

-import org.eclipse.xtext.xbase.lib.IterableExtensions;

-import org.eclipse.xtext.xbase.lib.ObjectExtensions;

-import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;

-

-@SuppressWarnings("all")

-public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {

-  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

-  

-  @Extension

-  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

-  

-  public Logic2VampireLanguageMapper_TypeMapper_FilteredTypes() {

-    LogicproblemPackage.eINSTANCE.getClass();

-  }

-  

-  @Override

-  public void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {

-    VLSVariable _createVLSVariable = this.factory.createVLSVariable();

-    final Procedure1<VLSVariable> _function = (VLSVariable it) -> {

-      it.setName("A");

-    };

-    final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);

-    for (final Type type : types) {

-      {

-        VLSFunction _createVLSFunction = this.factory.createVLSFunction();

-        final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {

-          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);

-        trace.type2Predicate.put(type, typePred);

-      }

-    }

-    Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);

-    for (final TypeDefinition type_1 : _filter) {

-      {

-        final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();

-        EList<DefinedElement> _elements = type_1.getElements();

-        for (final DefinedElement e : _elements) {

-          {

-            VLSFunction _createVLSFunction = this.factory.createVLSFunction();

-            final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {

-              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);

-            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().split(" ")[0]));

-          it.setFofRole("axiom");

-          VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

-          final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {

-            EList<VLSVariable> _variables = it_1.getVariables();

-            VLSVariable _duplicate = this.support.duplicate(variable);

-            _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, trace.type2Predicate));

-              it_2.setRight(this.support.unfoldOr(orElems));

-            };

-            VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);

-            it_1.setOperand(_doubleArrow);

-          };

-          VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);

-          it.setFofFormula(_doubleArrow);

-        };

-        final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);

-        EList<VLSFofFormula> _formulas = trace.specification.getFormulas();

-        _formulas.add(res);

-      }

-    }

-    final Function1<Type, Boolean> _function_1 = (Type it) -> {

-      boolean _isIsAbstract = it.isIsAbstract();

-      return Boolean.valueOf((!_isIsAbstract));

-    };

-    Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);

-    for (final Type t1 : _filter_1) {

-      {

-        for (final Type t2 : types) {

-          if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) {

-            trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));

-          } else {

-            VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

-            final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> {

-              it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));

-            };

-            VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);

-            trace.type2PossibleNot.put(t2, _doubleArrow);

-          }

-        }

-        Collection<VLSTerm> _values = trace.type2PossibleNot.values();

-        ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);

-        trace.type2And.put(t1, this.support.unfoldAnd(_arrayList));

-        trace.type2PossibleNot.clear();

-      }

-    }

-    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

-    final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {

-      it.setName("hierarchyHandler");

-      it.setFofRole("axiom");

-      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

-      final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> {

-        EList<VLSVariable> _variables = it_1.getVariables();

-        VLSVariable _duplicate = this.support.duplicate(variable);

-        _variables.add(_duplicate);

-        VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

-        final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> {

-          it_2.setLeft(this.support.topLevelTypeFunc());

-          Collection<VLSTerm> _values = trace.type2And.values();

-          ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);

-          it_2.setRight(this.support.unfoldOr(_arrayList));

-        };

-        VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);

-        it_1.setOperand(_doubleArrow);

-      };

-      VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3);

-      it.setFofFormula(_doubleArrow);

-    };

-    final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);

-    EList<VLSFofFormula> _formulas = trace.specification.getFormulas();

-    _formulas.add(hierarch);

-  }

-  

-  @Override

-  public List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {

-    throw new UnsupportedOperationException("TODO: auto-generated method stub");

-  }

-  

-  @Override

-  public VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) {

-    throw new UnsupportedOperationException("TODO: auto-generated method stub");

-  }

-  

-  @Override

-  public int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) {

-    throw new UnsupportedOperationException("TODO: auto-generated method stub");

-  }

-  

-  @Override

-  public VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) {

-    VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote();

-    final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> {

-      String _name = referred.getName();

-      String _plus = ("\"a" + _name);

-      String _plus_1 = (_plus + "\"");

-      it.setValue(_plus_1);

-    };

-    return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function);

-  }

-  

-  @Override

-  public VampireModelInterpretation_TypeInterpretation getTypeInterpreter() {

-    throw new UnsupportedOperationException("TODO: auto-generated method stub");

-  }

-}

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 6d33db67..446cfded 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
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
index 1406c597..9ded2f72 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
index 20397ff3..2c84c402 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
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 9f3d423f..867fe276 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
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
index 8fc60bab..8364a369 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
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 4212d100..fa2a2fc1 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
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
index 78d32090..a6a6e1b8 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
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 d00afe64..26cbd485 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