15 files changed, 1805 insertions, 0 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
new file mode 100644
index 00000000..618980a3
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
@@ -0,0 +1,21 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner
+
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+
+class VampireSolverConfiguration extends LogicSolverConfiguration {
+        
+        //public var int symmetry = 0 // by default
+        //choose needed backend solver
+//      public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
+}
+
+
+enum VampireBackendSolver {
+        //add needed things
+}
+
+
+enum TypeMappingTechnique {
+        //default
+        FilteredTypes
+}
\ No newline at end of file
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
new file mode 100644
index 00000000..1d56892e
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -0,0 +1,104 @@
+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.Vampire2LogicMapper
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
+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 {
+
+        new() {
+                VampireLanguagePackage.eINSTANCE.eClass
+                val x = new VampireLanguageStandaloneSetupGenerated
+                VampireLanguageStandaloneSetup::doSetup()
+        }
+
+        val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper
+        val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
+        val VampireHandler handler = new VampireHandler
+
+        val fileName = "vampireProblem.tptp"
+
+        override solve(LogicProblem problem, LogicSolverConfiguration config,
+                ReasonerWorkspace workspace) throws LogicReasonerException {
+                val vampireConfig = config.asConfig
+
+                // Start: Logic -> Vampire mapping
+                val transformationStart = System.currentTimeMillis
+                // TODO
+                val result = forwardMapper.transformProblem(problem, vampireConfig)
+                val vampireProblem = result.output
+                val forwardTrace = result.trace
+
+                var String fileURI = null;
+                var String vampireCode = null;
+                vampireCode = workspace.writeModelToString(vampireProblem, fileName)
+
+                val writeFile = (
+                        vampireConfig.documentationLevel === DocumentationLevel::NORMAL ||
+                        vampireConfig.documentationLevel === DocumentationLevel::FULL)
+                if (writeFile) {
+                        fileURI = workspace.writeModel(vampireProblem, fileName).toFileString
+                }
+
+                // Result as String
+                val transformationTime = System.currentTimeMillis - transformationStart
+                // Finish: Logic -> Vampire mapping
+                /*        
+                 * // Start: Solving Alloy problem
+                 * val solverStart = System.currentTimeMillis
+                 * //Calling Solver (Currently Manually)
+                 * val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode)
+                 * //           val result2 = null
+                 * //TODO
+                 * //Backwards Mapper
+                 * val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
+                 * 
+                 * val solverFinish = System.currentTimeMillis-solverStart
+                 * // Finish: Solving Alloy problem
+                 *              
+                 * if(vampireConfig.writeToFile) workspace.deactivateModel(fileName)
+                 * 
+                 * return logicResult
+                 * 
+                 /*/
+                return null // for now
+                // */
+        }
+
+        def asConfig(LogicSolverConfiguration configuration) {
+                if (configuration instanceof VampireSolverConfiguration) {
+                        return configuration
+                } else {
+                        throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''')
+                }
+        }
+
+//      /*
+//       * not for now
+//       * 
+        override getInterpretations(ModelResult modelResult) {
+                // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
+//              val sols = modelResult.representation// as List<A4Solution>
+//              //val res = answers.map 
+//              sols.map[
+//                      new VampireModelInterpretation(
+//                              forwardMapper.typeMapper.typeInterpreter,
+//                              it as A4Solution,
+//                              forwardMapper,
+//                              modelResult.trace as Logic2AlloyLanguageMapperTrace
+//                      )
+//              ]
+        }
+//      */
+}
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
new file mode 100644
index 00000000..b7ad8f3d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -0,0 +1,387 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
+import java.util.Collections
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+import org.eclipse.xtend.lib.annotations.Accessors
+
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+
+class Logic2VampireLanguageMapper {
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support;
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(
+                this)
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(
+                this)
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(
+                this)
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(
+                this)
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(
+                this)
+
+        public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem,
+                VampireSolverConfiguration config) {
+                // create model bases
+                // TODO
+                val initialComment = createVLSComment => [
+                        it.comment = "This is an initial Test Comment"
+                ]
+
+                val specification = createVampireModel => [
+                        it.comments += initialComment
+                ]
+
+                val trace = new Logic2VampireLanguageMapperTrace => [
+                        it.specification = specification
+
+//                      it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem))
+                ]
+
+                // TYPE MAPPER
+                if (!problem.types.isEmpty) {
+                        typeMapper.transformTypes(problem.types, problem.elements, this, trace)
+                }
+
+                // SCOPE MAPPER
+                scopeMapper.transformScope(config, trace)
+
+                // RELATION MAPPER
+                trace.relationDefinitions = problem.collectRelationDefinitions
+                problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
+                
+                // CONTAINMENT MAPPER
+                containmentMapper.transformContainment(problem.containmentHierarchies, trace)
+
+                // CONSTANT MAPPER
+                // only transforms definitions
+                trace.constantDefinitions = problem.collectConstantDefinitions
+                // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)]
+                problem.constants.filter(ConstantDefinition).forEach [
+                        this.constantMapper.transformConstantDefinitionSpecification(it, trace)
+                ]
+
+                // ASSERTION MAPPER
+                for (assertion : problem.assertions) {
+                        transformAssertion(assertion, trace)
+                }
+                // OUTPUT
+                return new TracedOutput(specification, trace)
+        }
+
+        // End of transformProblem
+        // ////////////
+        // Type References
+        // ////////////
+        def dispatch protected VLSTerm transformTypeReference(BoolTypeReference boolTypeReference,
+                Logic2VampireLanguageMapperTrace trace) {
+                // TODO, Not Now
+                // return createALSReference => [ it.referred = support.getBooleanType(trace) ]
+        }
+
+        // ////////////
+        // Collectors
+        // ////////////
+        // exact Same as for Alloy
+        private def collectConstantDefinitions(LogicProblem problem) {
+                val res = new HashMap
+                problem.constants.filter(ConstantDefinition).filter[it.defines !== null].forEach [
+                        res.put(it.defines, it)
+                ]
+                return res
+        }
+
+        private def collectRelationDefinitions(LogicProblem problem) {
+                val res = new HashMap
+                problem.relations.filter(RelationDefinition).filter[it.defines !== null].forEach [
+                        res.put(it.defines, it)
+                ]
+                return res
+        }
+
+        // ////////////
+        // Assertions + Terms
+        // ////////////
+        def protected transformAssertion(Assertion assertion, Logic2VampireLanguageMapperTrace trace) {
+                val res = createVLSFofFormula => [
+                        it.name = support.toID(assertion.name)
+                        // below is temporary solution
+                        it.fofRole = "axiom"
+                        it.fofFormula = assertion.value.transformTerm(trace, Collections.EMPTY_MAP)
+                // it.annotation = nothing                      
+                ]
+                trace.specification.formulas += res
+        }
+
+        def dispatch protected VLSTerm transformTerm(BoolLiteral literal, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                if (literal.value == true) {
+                        createVLSTrue
+                } else {
+                        createVLSFalse
+                }
+        }
+
+        def dispatch protected VLSTerm transformTerm(IntLiteral literal, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                createVLSInt => [it.value = literal.value.toString()]
+        }
+
+        def dispatch protected VLSTerm transformTerm(RealLiteral literal, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                createVLSReal => [it.value = literal.value.toString()]
+        }
+
+        def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)]
+        }
+
+        def dispatch protected VLSTerm transformTerm(And and, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) { support.unfoldAnd(and.operands.map[transformTerm(trace, variables)]) }
+
+        def dispatch protected VLSTerm transformTerm(Or or, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) { support.unfoldOr(or.operands.map[transformTerm(trace, variables)]) }
+
+        def dispatch protected VLSTerm transformTerm(Impl impl, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                createVLSImplies => [
+                        left = impl.leftOperand.transformTerm(trace, variables)
+                        right = impl.rightOperand.transformTerm(trace, variables)
+                ]
+        }
+
+        def dispatch protected VLSTerm transformTerm(Iff iff, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                createVLSEquivalent => [
+                        left = iff.leftOperand.transformTerm(trace, variables)
+                        right = iff.rightOperand.transformTerm(trace, variables)
+                ]
+        }
+
+//      def dispatch protected VLSTerm transformTerm(MoreThan moreThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+//              createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] }
+//      def dispatch protected VLSTerm transformTerm(LessThan lessThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+//              createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] }
+//      def dispatch protected VLSTerm transformTerm(MoreOrEqualThan moreThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+//              createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] }
+//      def dispatch protected VLSTerm transformTerm(LessOrEqualThan lessThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+//              createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected VLSTerm transformTerm(Equals equals, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                createVLSEquality => [
+                        left = equals.leftOperand.transformTerm(trace, variables)
+                        right = equals.rightOperand.transformTerm(trace, variables)
+                ]
+        }
+
+        def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) { support.unfoldDistinctTerms(this, distinct.operands, trace, variables) }
+
+//      
+//              def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+//              createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] }
+//      def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+//              createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] }
+//      def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+//              createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] }
+//      def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+//              createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] }
+//      def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+//              createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] }
+//      
+        def dispatch protected VLSTerm transformTerm(Forall forall, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                support.createQuantifiedExpression(this, forall, trace, variables, true)
+        }
+
+        def dispatch protected VLSTerm transformTerm(Exists exists, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                support.createQuantifiedExpression(this, exists, trace, variables, false)
+        }
+
+        def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                return createVLSFunction => [
+                        it.constant = (instanceOf.range as ComplexTypeReference).referred.lookup(trace.type2Predicate).constant
+                        it.terms += instanceOf.value.transformTerm(trace, variables)
+                ]
+        }
+
+//      
+//      def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+//              return this.relationMapper.transformTransitiveRelationReference(
+//                      tc.relation,
+//                      tc.leftOperand.transformTerm(trace,variables),
+//                      tc.rightOperand.transformTerm(trace,variables),
+//                      trace
+//              )
+//      }
+//      
+        def dispatch protected VLSTerm transformTerm(SymbolicValue symbolicValue, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions, trace,
+                        variables)
+        }
+
+        def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                typeMapper.transformReference(referred, trace)
+        }
+
+        def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                // might need to make sure that only declared csts get transformed. see for Alloy
+                val res = createVLSConstant => [
+                        // ask if necessary VLSConstantDeclaration and not just directly strng
+                        it.name = support.toID(constant.name)
+                ]
+                // no postprocessing cuz booleans are accepted
+                return res
+        }
+
+        // NOT NEEDED FOR NOW
+        // TODO
+        def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+//              val res = createVLSFunctionCall => [
+//                      it.referredDefinition = constant.lookup(trace.constantDefinition2Function)
+//              ]
+//              return support.postprocessResultOfSymbolicReference(constant.type,res,trace)
+        }
+
+        def dispatch protected VLSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions,
+                Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+
+                // cannot treat variable as function (constant) because of name ID not being the same
+                // no need for potprocessing cuz booleans are supported
+                return support.duplicate(variable.lookup(variables))
+        }
+
+        // TODO
+        def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+//              if(trace.functionDefinitions.containsKey(function)) {
+//                      return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables)
+//              } else {
+//                      if(functionMapper.transformedToHostedField(function,trace)) {
+//                              val param = parameterSubstitutions.get(0).transformTerm(trace,variables)
+//                              val res = createVLSJoin => [
+//                                      leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace)
+//                                      rightOperand = createVLSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)]
+//                              ]
+//                              return support.postprocessResultOfSymbolicReference(function.range,res,trace)
+//                      } else {
+//                              val functionExpression = createVLSJoin=>[
+//                                              leftOperand = createVLSReference => [referred = trace.logicLanguage]
+//                                              rightOperand = createVLSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)]
+//                                      ]
+//                              val res =  support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables)
+//                              return support.postprocessResultOfSymbolicReference(function.range,res,trace)
+//                      }
+//              }
+        }
+
+        // TODO
+        def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+//              val result = createVLSFunctionCall => [
+//                      it.referredDefinition = function.lookup(trace.functionDefinition2Function)
+//                      it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)]
+//              ]
+//              return support.postprocessResultOfSymbolicReference(function.range,result,trace)
+        }
+
+        // TODO
+        /*
+         * def dispatch protected VLSTerm transformSymbolicReference(Relation relation,
+         *      List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+         *      Map<Variable, VLSVariable> variables) {
+         *      if (trace.relationDefinitions.containsKey(relation)) {
+         *              this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),
+         *                      parameterSubstitutions, trace, variables)
+         *      }
+         *      else {
+         * //                                           if (relationMapper.transformToHostedField(relation, trace)) {
+         * //                                                   val VLSRelation = relation.lookup(trace.relationDeclaration2Field)
+         * //                                                   // R(a,b) =>
+         * //                                                   // b in a.R
+         * //                                                   return createVLSSubset => [
+         * //                                                           it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables)
+         * //                                                           it.rightOperand = createVLSJoin => [
+         * //                                                                   it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables)
+         * //                                                                   it.rightOperand = createVLSReference => [it.referred = VLSRelation]
+         * //                                                           ]
+         * //                                                   ]
+         * //                                           } else {
+         * //                                                   val target = createVLSJoin => [
+         * //                                                           leftOperand = createVLSReference => [referred = trace.logicLanguage]
+         * //                                                           rightOperand = createVLSReference => [
+         * //                                                                   referred = relation.lookup(trace.relationDeclaration2Global)
+         * //                                                           ]
+         * //                                                   ]
+         * //                                                   val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables)
+         * //
+         * //                                                   return createVLSSubset => [
+         * //                                                           leftOperand = source
+         * //                                                           rightOperand = target
+         * //                                                   ]
+         * //                                           }
+         *      }
+         * }
+         */
+        // TODO
+        def dispatch protected VLSTerm transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions,
+                Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+//                                       createVLSFunction => [
+//                                              it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)
+//                                              it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
+//                                      ]
+                return createVLSFunction => [
+                        it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
+                        it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
+                ]
+        }
+
+}
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
new file mode 100644
index 00000000..22bd4ab5
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
@@ -0,0 +1,58 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
+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.List
+import java.util.Map
+
+interface Logic2VampireLanguageMapper_TypeMapperTrace {}
+
+class Logic2VampireLanguageMapperTrace {
+//      public var ViatraQueryEngine incQueryEngine;
+
+        //list of needed VLS components
+        public var VampireModel specification
+        public var VLSFofFormula logicLanguageBody
+        public var VLSTerm formula
+        
+        //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
+        //Uniqueness
+        public val List<VLSConstant> uniqueInstances = newArrayList
+        
+        
+        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 val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
+        public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap
+                
+}
\ No newline at end of file
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend
new file mode 100644
index 00000000..2366ea15
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend
@@ -0,0 +1,42 @@
+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 ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+
+class Logic2VampireLanguageMapper_ConstantMapper {
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+        val Logic2VampireLanguageMapper base
+        
+        public new(Logic2VampireLanguageMapper base) {
+                this.base = base
+        }
+        
+//NOT NEEDED
+//      def protected dispatch transformConstant(ConstantDeclaration constant, Logic2VampireLanguageMapperTrace trace) {
+//              val c = createVLSFunctionDeclaration=> [
+//                      it.name = support.toID(constant.name)
+//              ]
+//              trace.constantDec.constant = c
+//              trace.constantDeclaration2LanguageField.put(constant, c);
+//              
+//      }
+        
+//NOT Used In Sample    
+        def protected dispatch transformConstant(ConstantDefinition constant, Logic2VampireLanguageMapperTrace trace) {
+                //error
+                //TODO
+//              val c = createVLSFofFormula=> [
+//                      name = support.toID(constant.name)
+//                      fofRole = "axiom"
+//                      fofFormula = base.transformTypeReference()
+//              ]
+        }
+        
+        def protected transformConstantDefinitionSpecification(ConstantDefinition constant, Logic2VampireLanguageMapperTrace trace) {
+                //TODO
+        }
+        
+        
+}
\ No newline at end of file
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
new file mode 100644
index 00000000..0820f47d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
@@ -0,0 +1,123 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

+

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation

+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy

+import java.util.List

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference

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

+

+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference

+

+class Logic2VampireLanguageMapper_ContainmentMapper {

+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support

+        val Logic2VampireLanguageMapper base

+        private val VLSVariable variable = createVLSVariable => [it.name = "A"]

+

+        public new(Logic2VampireLanguageMapper base) {

+                this.base = base

+        }

+

+        def public void transformContainment(List<ContainmentHierarchy> hierarchies,

+                Logic2VampireLanguageMapperTrace trace) {

+

+                // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST

+                // TEMP

+                val hierarchy = hierarchies.get(0)

+

+                val containmentListCopy = hierarchy.typesOrderedInHierarchy

+                val relationsList = hierarchy.containmentRelations

+                // STEP 1

+                // Find root element

+                for (l : relationsList) {

+                        var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type

+                        containmentListCopy.remove(pointingTo)

+                        for (c : pointingTo.subtypes) {

+                                containmentListCopy.remove(c)

+                        }

+                }

+

+                // State that there must exist 1 and only 1 root element

+                val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString

+                val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))

+

+                val contTop = createVLSFofFormula => [

+                        it.name = support.toIDMultiple("containment_topLevel", topName)

+                        it.fofRole = "axiom"

+

+                        it.fofFormula = createVLSUniversalQuantifier => [

+                                it.variables += support.duplicate(variable)

+                                it.operand = createVLSEquivalent => [

+                                        it.left = topTerm

+                                        it.right = createVLSEquality => [

+                                                it.left = support.duplicate(variable)

+                                                it.right = createVLSConstant => [

+                                                        it.name = "o1"

+                                                ]

+                                        ]

+                                ]

+                        ]

+//                      it.fofFormula = support.duplicate(

+//                              topTerm,

+//                              createVLSFunctionAsTerm => [

+//                                      it.functor = "o1"

+//                              ]

+//                      )

+                ]

+                trace.specification.formulas += contTop

+

+                // STEP 2

+                // for each edge, if the pointedTo element exists,the edge must exist also

+                val varA = createVLSVariable => [it.name = "A"]

+                val varB = createVLSVariable => [it.name = "B"]

+                val varList = newArrayList(varB, varA)

+

+                for (l : relationsList) {

+                        val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString

+                        val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type

+                        val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type

+

+                        val relFormula = createVLSFofFormula => [

+                                it.name = support.toIDMultiple("containment", relName)

+                                it.fofRole = "axiom"

+

+                                it.fofFormula = createVLSUniversalQuantifier => [

+                                        it.variables += support.duplicate(varA)

+                                        it.operand = createVLSImplies => [

+                                                it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA)

+                                                it.right = createVLSExistentialQuantifier => [

+                                                        it.variables += support.duplicate(varB)

+                                                        it.operand = createVLSAnd => [

+                                                                it.left = support.duplicate(fromType.lookup(trace.type2Predicate), varB)

+                                                                it.right = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate),

+                                                                        varList)

+                                                        ]

+                                                ]

+

+                                                createVLSEquality => [

+                                                        it.left = support.duplicate(variable)

+                                                        it.right = createVLSConstant => [

+                                                                it.name = "o1"

+                                                        ]

+                                                ]

+                                        ]

+                                ]

+                        ]

+                        trace.specification.formulas += relFormula

+                        var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type

+                        containmentListCopy.remove(pointingTo)

+                        for (c : pointingTo.subtypes) {

+                                containmentListCopy.remove(c)

+                        }

+                }

+

+        // STEP 3

+        // Ensure that an objct only has 1 parent

+        // STEP 4

+        // Ensure that there are no cycles in the hierarchy (maybe same as for step3?)

+        }

+}

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
new file mode 100644
index 00000000..0ae06bc3
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -0,0 +1,160 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+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.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+
+class Logic2VampireLanguageMapper_RelationMapper {
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+        val Logic2VampireLanguageMapper base
+
+        public new(Logic2VampireLanguageMapper base) {
+                this.base = base
+        }
+
+        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
+                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 => [
+                                        val rel = createVLSFunction => [
+                                                it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2))
+                                                for (v : relVar2VLS) {
+                                                        it.terms += support.duplicate(v)
+                                                }
+                                        ]
+                                        trace.rel2Predicate.put(r, rel)
+                                        it.left = support.duplicate(rel)
+                                        it.right = support.unfoldAnd(relVar2TypeDecComply)
+                                ]
+                        ]
+                ]
+
+                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 : reldef.variables) {
+                        val v = createVLSVariable => [
+                                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 += support.duplicate(v)
+                        ]
+                        relationVar2TypeDecComply.put(variable, varTypeComply)
+                        relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
+                }
+                val nameArray = reldef.name.split(" ")
+                val comply = createVLSFofFormula => [
+                        it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
+                                nameArray.get(nameArray.length - 1))
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                for (variable : reldef.variables) {
+                                        it.variables += support.duplicate(variable.lookup(relationVar2VLS))
+
+                                }
+                                it.operand = createVLSImplies => [
+                                        it.left = createVLSFunction => [
+                                                it.constant = support.toIDMultiple("rel", reldef.name)
+                                                for (variable : reldef.variables) {
+                                                        val v = createVLSVariable => [
+                                                                it.name = variable.lookup(relationVar2VLS).name
+                                                        ]
+                                                        it.terms += v
+                                                }
+                                        ]
+                                        it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
+                                ]
+                        ]
+                ]
+
+                val res = createVLSFofFormula => [
+                        it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
+                                nameArray.get(nameArray.length - 1))
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                for (variable : reldef.variables) {
+                                        val v = createVLSVariable => [
+                                                it.name = variable.lookup(relationVar2VLS).name
+                                        ]
+                                        it.variables += v
+
+                                }
+                                it.operand = createVLSImplies => [
+                                        it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
+                                        it.right = createVLSEquivalent => [
+                                                it.left = createVLSFunction => [
+                                                        it.constant = support.toIDMultiple("rel", reldef.name)
+                                                        for (variable : reldef.variables) {
+                                                                val v = createVLSVariable => [
+                                                                        it.name = variable.lookup(relationVar2VLS).name
+                                                                ]
+                                                                it.terms += v
+
+                                                        }
+                                                ]
+                                                it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
+                                        ]
+
+                                ]
+
+                        ]
+
+                ]
+
+                // trace.relationDefinition2Predicate.put(r,res)
+                trace.specification.formulas += comply;
+                trace.specification.formulas += res;
+
+        }
+
+}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
new file mode 100644
index 00000000..548deda4
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -0,0 +1,162 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

+

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration

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

+import java.util.ArrayList

+import java.util.Map

+

+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

+import java.util.HashMap

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm

+import java.util.List

+

+class Logic2VampireLanguageMapper_ScopeMapper {

+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support

+        val Logic2VampireLanguageMapper base

+        private val VLSVariable variable = createVLSVariable => [it.name = "A"]

+

+        public new(Logic2VampireLanguageMapper base) {

+                this.base = base

+        }

+

+        def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {

+

+//              TODO HANDLE ERRORS RELATED TO MAX > MIN

+//              TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS

+//              TODO HANDLE 

+//              TODO NOT SPECIFIED MEANS =0 ?

+                // 1. make a list of constants equaling the min number of specified objects

+                val GLOBAL_MIN = config.typeScopes.minNewElements

+                val GLOBAL_MAX = config.typeScopes.maxNewElements

+

+                val localInstances = newArrayList

+

+                // Handling Minimum_General

+                if (GLOBAL_MIN != 0) {

+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false)

+                        for(i : trace.uniqueInstances){

+                                localInstances.add(support.duplicate(i))

+                        }

+                        

+                        makeFofFormula(localInstances, trace, true, null)

+                }

+

+                // Handling Maximum_General

+                if (GLOBAL_MAX != 0) {

+                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true)

+                        makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)

+                }

+

+                // Handling Minimum_Specific

+                var i = 1

+                var minNum = -1

+                var Map<Type, Integer> startPoints = new HashMap

+                for (t : config.typeScopes.minNewElementsByType.keySet) {

+                        minNum = t.lookup(config.typeScopes.minNewElementsByType)

+                        if (minNum != 0) {

+                                getInstanceConstants(i + minNum, i, localInstances, trace, true, false)

+                                startPoints.put(t, i)

+                                i += minNum

+                                makeFofFormula(localInstances, trace, true, t)

+                        }

+                }

+

+                // TODO: calc sum of mins, compare to current value of i

+                // Handling Maximum_Specific

+                for (t : config.typeScopes.maxNewElementsByType.keySet) {

+                        var maxNum = t.lookup(config.typeScopes.maxNewElementsByType)

+                        minNum = t.lookup(config.typeScopes.minNewElementsByType)

+                        var startpoint = t.lookup(startPoints)

+                        if (minNum != 0) {

+                                getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false)

+                        }

+                        if (maxNum != minNum) {

+                                var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum)

+                                getInstanceConstants(instEndInd, i, localInstances, trace, false, false)

+                                makeFofFormula(localInstances, trace, false, t)

+                        }

+                }

+

+// 3. Specify uniqueness of elements

+                if (trace.uniqueInstances.length != 0) {

+                        val uniqueness = createVLSFofFormula => [

+                                it.name = "typeUniqueness"

+                                it.fofRole = "axiom"

+                                it.fofFormula = support.establishUniqueness(trace.uniqueInstances)

+                        ]

+                        trace.specification.formulas += uniqueness

+                }

+

+        }

+

+        def protected void getInstanceConstants(int endInd, int startInd, ArrayList list,

+                Logic2VampireLanguageMapperTrace trace, boolean clear, boolean addToTrace) {

+                if (clear) {

+                        list.clear

+                }

+                for (var i = startInd; i < endInd; i++) {

+                        val num = i + 1

+                        val cst = createVLSConstant => [

+                                it.name = "o" + num

+                        ]

+                        if (addToTrace) {

+                                trace.uniqueInstances.add(cst)

+                        }

+                        list.add(cst)

+                }

+        }

+

+        def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum,

+                Type type) {

+                var nm = ""

+                var VLSTerm tm = null

+                if (type === null) {

+                        nm = "object"

+                        tm = support.topLevelTypeFunc

+                } else {

+                        nm = type.lookup(trace.type2Predicate).constant.toString

+                        tm = createVLSAnd => [

+                                it.left = support.duplicate(type.lookup(trace.type2Predicate))

+                                it.right = support.topLevelTypeFunc

+                        ]

+//                      tm = support.duplicate(type.lookup(trace.type2Predicate))

+                }

+                val name = nm

+                val term = tm

+

+                val cstDec = createVLSFofFormula => [

+                        it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name)

+                        it.fofRole = "axiom"

+                        it.fofFormula = createVLSUniversalQuantifier => [

+                                it.variables += support.duplicate(variable)

+                                // check below

+                                it.operand = createVLSImplies => [

+                                        if (minimum) {

+                                                it.left = support.unfoldOr(list.map [ i |

+                                                        createVLSEquality => [

+                                                                it.left = createVLSVariable => [it.name = variable.name]

+                                                                it.right = i

+                                                        ]

+                                                ])

+                                                it.right = term

+                                        } else {

+                                                it.left = term

+                                                it.right = support.unfoldOr(list.map [ i |

+                                                        createVLSEquality => [

+                                                                it.left = createVLSVariable => [it.name = variable.name]

+                                                                it.right = i

+                                                        ]

+                                                ])

+

+                                        }

+                                ]

+                        ]

+                ]

+                trace.specification.formulas += cstDec

+        }

+

+}

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
new file mode 100644
index 00000000..8d00d3e7
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -0,0 +1,242 @@
+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.VLSFunctionAsTerm
+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 static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+
+class Logic2VampireLanguageMapper_Support {
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
+
+        // ID Handler
+        def protected String toIDMultiple(String... ids) {
+                ids.map[it.split("\\s+").join("_")].join("_")
+        }
+
+        def protected String toID(String ids) {
+                ids.split("\\s+").join("_")
+        }
+
+        // Term Handling
+        // TODO Make more general
+        def protected VLSVariable duplicate(VLSVariable term) {
+                return createVLSVariable => [it.name = term.name]
+        }
+
+        def protected VLSFunctionAsTerm duplicate(VLSFunctionAsTerm term) {
+                return createVLSFunctionAsTerm => [it.functor = term.functor]
+        }
+
+        def protected VLSConstant duplicate(VLSConstant term) {
+                return createVLSConstant => [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 duplicate(VLSFunction term, List<VLSVariable> vars) {
+                return createVLSFunction => [
+                        it.constant = term.constant
+                        for (v : vars) {
+                                it.terms += duplicate(v)
+                        }
+                ]
+        }
+
+        def protected VLSFunction duplicate(VLSFunction term, VLSFunctionAsTerm v) {
+                return createVLSFunction => [
+                        it.constant = term.constant
+                        it.terms += duplicate(v)
+                ]
+        }
+
+        def protected VLSConstant toConstant(VLSFunctionAsTerm term) {
+                return createVLSConstant => [
+                        it.name = term.functor
+                ]
+        }
+
+        def protected VLSFunction topLevelTypeFunc() {
+                return createVLSFunction => [
+                        it.constant = "object"
+                        it.terms += createVLSVariable => [
+                                it.name = "A"
+                        ]
+                ]
+        }
+        
+        def protected VLSFunction topLevelTypeFunc(VLSVariable v) {
+                return createVLSFunction => [
+                        it.constant = "object"
+                        it.terms += duplicate(v)
+                ]
+        }
+
+        def protected VLSFunction topLevelTypeFunc(VLSFunctionAsTerm v) {
+                return createVLSFunction => [
+                        it.constant = "object"
+                        it.terms += duplicate(v)
+                ]
+        }
+
+        // TODO Make more general
+        def establishUniqueness(List<VLSConstant> terms) {
+                val List<VLSInequality> eqs = newArrayList
+                for (t1 : terms.subList(1, terms.length)) {
+                        for (t2 : terms.subList(0, terms.indexOf(t1))) {
+                                val eq = createVLSInequality => [
+                                        // TEMP
+                                        it.left = createVLSConstant => [it.name = t2.name]
+                                        it.right = createVLSConstant => [it.name = t1.name]
+                                // TEMP
+                                ]
+                                eqs.add(eq)
+                        }
+                }
+                return unfoldAnd(eqs)
+        }
+
+        // Support Functions
+        // booleans
+        // AND and OR
+        def protected VLSTerm unfoldAnd(List<? extends VLSTerm> operands) {
+                if (operands.size == 1) {
+                        return operands.head
+                } else if (operands.size > 1) {
+                        return createVLSAnd => [
+                                left = operands.head
+                                right = operands.subList(1, operands.size).unfoldAnd
+                        ]
+                } else
+                        throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+
+        def protected VLSTerm unfoldOr(List<? extends VLSTerm> operands) {
+//              if(operands.size == 0) {basically return true}
+                /*else*/ if (operands.size == 1) {
+                        return operands.head
+                } else if (operands.size > 1) {
+                        return createVLSOr => [
+                                left = operands.head
+                                right = operands.subList(1, operands.size).unfoldOr
+                        ]
+                } else
+                        throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP
+        }
+
+        // can delete below
+        def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands,
+                Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+                if (operands.size == 1) {
+                        return m.transformTerm(operands.head, trace, variables)
+                } else if (operands.size > 1) {
+                        val notEquals = new ArrayList<VLSTerm>(operands.size * operands.size / 2)
+                        for (i : 0 ..< operands.size) {
+                                for (j : i + 1 ..< operands.size) {
+                                        notEquals += createVLSInequality => [
+                                                it.left = m.transformTerm(operands.get(i), trace, variables)
+                                                it.right = m.transformTerm(operands.get(j), trace, variables)
+                                        ]
+                                }
+                        }
+                        return notEquals.unfoldAnd
+                } else
+                        throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+
+        // Symbolic
+        // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) {
+//              if(type instanceof BoolTypeReference) {
+//                      return booleanToLogicValue(term ,trace)
+//              }
+//              else return term
+//      }
+//      def booleanToLogicValue(VLSTerm term, Logic2VampireLanguageMapperTrace trace) {
+//              throw new UnsupportedOperationException("TODO: auto-generated method stub")
+//      }
+        /*
+         * def protected  String toID(List<String> ids) {
+         *      ids.map[it.split("\\s+").join("'")].join("'")
+         * }
+         */
+        // QUANTIFIERS + VARIABLES
+        def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper,
+                QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables,
+                boolean isUniversal) {
+                val variableMap = expression.quantifiedVariables.toInvertedMap [ v |
+                        createVLSVariable => [it.name = toIDMultiple("V", v.name)]
+                ]
+
+                val typedefs = new ArrayList<VLSTerm>
+                for (variable : expression.quantifiedVariables) {
+                        val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate),
+                                variable.lookup(variableMap))
+                        typedefs.add(eq)
+                }
+                if (isUniversal) {
+                        createVLSUniversalQuantifier => [
+                                it.variables += variableMap.values
+                                it.operand = createVLSImplies => [
+                                        it.left = unfoldAnd(typedefs)
+                                        it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))
+                                ]
+                        ]
+                } else {
+                        typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)))
+                        createVLSExistentialQuantifier => [
+                                it.variables += variableMap.values
+                                it.operand = unfoldAnd(typedefs)
+
+                        ]
+                }
+
+        }
+
+        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.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
new file mode 100644
index 00000000..4c4247ce
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
@@ -0,0 +1,197 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd
+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.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
+import java.util.ArrayList
+import java.util.Collection
+import java.util.List
+
+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 VLSVariable variable = createVLSVariable => [it.name = "A"]
+                var globalCounter = 0
+
+                // 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)
+                        ]
+                        trace.type2Predicate.put(type, typePred)
+                }
+
+                // 2. Map each ENUM type definition to fof formula
+                for (type : types.filter(TypeDefinition)) {
+
+                        // Create a VLSFunction for each Enum Element
+                        val List<VLSFunction> orElems = newArrayList
+                        for (e : type.elements) {
+                                val enumElemPred = createVLSFunction => [
+                                        val splitName = e.name.split(" ")
+                                        if (splitName.length > 2) {
+                                                it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2))
+                                        } else {
+                                                it.constant = support.toIDMultiple("e", splitName.get(0))
+                                        }
+                                        it.terms += support.duplicate(variable)
+                                ]
+                                trace.element2Predicate.put(e, enumElemPred)
+                        }
+
+                        // Similar to InheritanceHierarchy for the Enum
+                        val List<VLSTerm> possibleNots = newArrayList
+                        val List<VLSTerm> typeDefs = newArrayList
+
+                        for (t1 : type.elements) {
+                                for (t2 : type.elements) {
+                                        if (t1 == t2) {
+                                                val fct = support.duplicate(t2.lookup(trace.element2Predicate), variable)
+                                                possibleNots.add(fct)
+                                        } else {
+                                                val op = support.duplicate(t2.lookup(trace.element2Predicate), variable)
+                                                val negFct = createVLSUnaryNegation => [
+                                                        it.operand = op
+                                                ]
+                                                possibleNots.add(negFct)
+                                        }
+                                }
+                                typeDefs.add(support.unfoldAnd(possibleNots))
+                                possibleNots.clear
+                        }
+
+                        // Implement Enum Inheritence Hierarchy
+                        val res = createVLSFofFormula => [
+                                it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
+                                it.fofRole = "axiom"
+                                it.fofFormula = createVLSUniversalQuantifier => [
+                                        it.variables += support.duplicate(variable)
+                                        it.operand = createVLSEquivalent => [
+                                                it.left = type.lookup(trace.type2Predicate)
+                                                it.right = createVLSAnd => [
+                                                        it.left = support.topLevelTypeFunc(variable)
+                                                        it.right = support.unfoldOr(typeDefs)
+                                                ]
+//                                              it.right = support.unfoldOr((typeDefs))
+
+                                        ]
+                                ]
+                        ]
+                        trace.specification.formulas += res
+
+                        for (var i = globalCounter; i < globalCounter+type.elements.length; i++) {
+                                // Create objects for the enum elements
+                                val num = i + 1
+                                val cstTerm = createVLSFunctionAsTerm => [
+                                        it.functor = "eo" + num
+                                ]
+                                val cst = support.toConstant(cstTerm)
+                                trace.uniqueInstances.add(cst)
+
+                                val index = i
+                                val enumScope = createVLSFofFormula => [
+                                        it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0),
+                                                type.elements.get(index).name.split(" ").get(0))
+                                        it.fofRole = "axiom"
+                                        it.fofFormula = createVLSUniversalQuantifier => [
+                                                it.variables += support.duplicate(variable)
+                                                it.operand = createVLSEquivalent => [
+                                                        it.left = createVLSEquality => [
+                                                                it.left = support.duplicate(variable)
+                                                                it.right = support.duplicate(support.toConstant(cstTerm))
+                                                        ]
+                                                        it.right = support.duplicate(type.elements.get(index).lookup(trace.element2Predicate),
+                                                                variable)
+                                                ]
+                                        ]
+                                ]
+
+                                trace.specification.formulas += enumScope
+
+                        }
+                        globalCounter+=type.elements.size
+                }
+
+                // 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)) {
+                                        trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
+                                } else {
+                                        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 = "inheritanceHierarchyHandler"
+                        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))
+                                        val reversedList = new ArrayList<VLSTerm>(trace.type2And.values)
+//                                      Collections.reverse(reversedList)
+                                        it.right = support.unfoldOr(reversedList)
+                                ]
+                        ]
+                ]
+
+                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_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
new file mode 100644
index 00000000..aba47edb
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
@@ -0,0 +1,18 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import java.util.HashMap
+import java.util.Map
+
+class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace{
+        
+//      public var VLSFofFormula objectSuperClass
+        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
+
+}
\ No newline at end of file
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
new file mode 100644
index 00000000..9c9e65b4
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
@@ -0,0 +1,67 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

+

+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory

+

+class Vampire2LogicMapper {

+}

+//      val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE

+//      

+//      public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) {

+//              val models = vampireSolution.aswers.map[it.key].toList

+//              

+//              if(!monitoredAlloySolution.finishedBeforeTimeout) {

+//                      return createInsuficientResourcesResult => [

+//                              it.problem = problem

+//                              it.representation += models

+//                              it.trace = trace

+//                              it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

+//                      ]

+//              } else {

+//                      if(models.last.satisfiable || requiredNumberOfSolution == -1) {

+//                              return createModelResult => [

+//                                      it.problem = problem

+//                                      it.representation += models

+//                                      it.trace = trace

+//                                      it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

+//                              ]

+//                      } else {

+//                              return createInconsistencyResult => [

+//                                      it.problem = problem

+//                                      it.representation += models

+//                                      it.trace = trace

+//                                      it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

+//                              ]

+//                      }

+//              }

+//      }

+//      

+//      def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {

+//              createStatistics => [

+//                      it.transformationTime = transformationTime as int

+//                      for(solutionIndex : 0..<solution.aswers.size) {

+//                              val solutionTime = solution.aswers.get(solutionIndex).value

+//                               it.entries+= createIntStatisticEntry => [

+//                                      it.name = '''Answer«solutionIndex»Time'''

+//                                      it.value = solutionTime.intValue

+//                              ]

+//                      }

+//                      it.entries+= createIntStatisticEntry => [

+//                              it.name = "Alloy2KodKodTransformationTime"

+//                              it.value = solution.kodkodTime as int

+//                      ]

+//                      it.entries+= createIntStatisticEntry => [

+//                              it.name = "Alloy2KodKodTransformationTime"

+//                              it.value = solution.kodkodTime as int

+//                      ]

+//                      it.entries+= createStringStatisticEntry => [

+//                              it.name = "warnings"

+//                              it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''

+//                      ]

+//              ]

+//      }

+//      

+//      def sum(Iterable<Long> ints) {

+//              ints.reduce[p1, p2|p1+p2]

+//      }

+//}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
new file mode 100644
index 00000000..aefa1a7e
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
@@ -0,0 +1,214 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

+

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireBackendSolver

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel

+import com.google.common.util.concurrent.SimpleTimeLimiter

+import com.google.common.util.concurrent.UncheckedTimeoutException

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration

+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace

+import java.util.ArrayList

+import java.util.HashMap

+import java.util.LinkedList

+import java.util.List

+import java.util.Map

+import java.util.concurrent.Callable

+import java.util.concurrent.TimeUnit

+import org.eclipse.emf.common.command.Command

+import org.eclipse.xtend.lib.annotations.Data

+

+class VampireSolverException extends Exception{

+        new(String s) { super(s) }

+        new(String s, Exception e) { super(s,e) }

+        new(String s, List<String> errors, Exception e) {

+                super(s + '\n' + errors.join('\n'), e)

+        }

+}

+

+@Data class VampireSolutionModel{

+//      List<String> warnings

+//      List<String> debugs

+//      long kodkodTime

+//      val List<Pair<A4Solution, Long>> aswers

+//      val boolean finishedBeforeTimeout

+

+

+}

+

+class VampireHandler {

+

+        //val fileName = "problem.als"

+        

+        public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration,String vampireCode) {

+                /*

+                //Prepare

+                val warnings = new LinkedList<String>

+                val debugs = new LinkedList<String>

+                val runtime = new ArrayList<Long>

+                val reporter = new A4Reporter() {

+                        override debug(String message) { debugs += message }

+                        override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime }

+                        override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime }

+                        override warning(ErrorWarning msg) { warnings += msg.message }

+                }

+                

+                val options = new A4Options() => [

+                        it.symmetry = configuration.symmetry

+                        it.noOverflow = true

+                        it.solver = getSolver(configuration.getSolver, configuration)

+                        if(configuration.getSolver.externalSolver) {

+                                it.solverDirectory = configuration.solverPath

+                        }

+                        //it.inferPartialInstance

+                        //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString

+                ]

+                

+                // Transform

+                var Command command = null;

+                var CompModule compModule = null

+                

+                // Start: Alloy -> Kodkod

+                val kodkodTransformStart = System.currentTimeMillis();

+                try {

+                        compModule = CompUtil.parseEverything_fromString(reporter,alloyCode)

+                        if(compModule.allCommands.size != 1)

+                                throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''')

+                        command = compModule.allCommands.head

+                } catch (Err e){

+                        throw new AlloySolverException(e.message,warnings,e)

+                }

+                val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart

+                // Finish: Alloy -> Kodkod

+                

+                val limiter = new SimpleTimeLimiter

+                val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration)

+                var List<Pair<A4Solution, Long>> answers

+                var boolean finished

+                if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) {

+                        answers = callable.call

+                        finished = true

+                } else {

+                        try{

+                                answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true)

+                                finished = true

+                        } catch (UncheckedTimeoutException e) {

+                                answers = callable.partialAnswers

+                                finished = false

+                        }

+                }

+

+                new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished)

+                */

+        }

+        /*

+        val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap

+        def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) {

+                val config = new SolverConfiguration(backedSolver,path,options)

+                if(previousSolverConfigurations.containsKey(config)) {

+                        return previousSolverConfigurations.get(config)

+                } else {

+                        val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»'''

+                        val newSolver = A4Options.SatSolver.make(id,id,path,options)

+                        previousSolverConfigurations.put(config,newSolver)

+                        return newSolver

+                }

+        }

+        

+        def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) {

+                switch(backedSolver){

+                        case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE

+                        case SpearPIPE: return A4Options.SatSolver.SpearPIPE

+                        case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI

+                        case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI

+                        case LingelingJNI: return A4Options.SatSolver.LingelingJNI

+                        case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null)

+                        case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI

+                        case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI

+                        case SAT4J: return A4Options.SatSolver.SAT4J

+                        case CNF: return A4Options.SatSolver.CNF

+                        case KodKod: return A4Options.SatSolver.KK

+                }

+        }

+        

+        def isExternalSolver(AlloyBackendSolver backedSolver) {

+                return !(backedSolver == AlloyBackendSolver.SAT4J)

+        }

+*/

+}

+/*

+class VampireCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{

+        

+        val List<String> warnings

+        val List<String> debugs

+        val A4Reporter reporter

+        val A4Options options

+        

+        val Command command

+        val CompModule compModule

+        val AlloySolverConfiguration configuration

+        

+        val List<Pair<A4Solution,Long>> answers = new LinkedList()

+        

+        new(List<String> warnings,

+                List<String> debugs,

+                A4Reporter reporter,

+                A4Options options,

+                Command command,

+                CompModule compModule,

+                AlloySolverConfiguration configuration)

+        {

+                this.warnings = warnings

+                this.debugs = debugs

+                this.reporter = reporter

+                this.options = options

+                this.command = command

+                this.compModule = compModule

+                this.configuration = configuration

+        }

+        

+        override call() throws Exception {

+                val startTime = System.currentTimeMillis

+                

+                // Start: Execute

+                var A4Solution lastAnswer = null

+                try {

+                        if(!configuration.progressMonitor.isCancelled) {

+                                do{

+                                        if(lastAnswer == null) {

+                                                lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)

+                                        } else {

+                                                lastAnswer = lastAnswer.next

+                                        }

+                                        configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution)

+                                        

+                                        val runtime = System.currentTimeMillis -startTime

+                                        synchronized(this) {

+                                                answers += (lastAnswer->runtime)

+                                        }

+                                } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled)

+                                

+                        }

+                }catch(Exception e) {

+                        warnings +=e.message

+                }

+                // Finish: execute

+                return answers

+        }

+        

+        def hasEnoughSolution(List<?> answers) {

+                if(configuration.solutionScope.numberOfRequiredSolution < 0) return false

+                else return answers.size() == configuration.solutionScope.numberOfRequiredSolution

+        }

+        

+        public def getPartialAnswers() {

+                return answers

+        }

+

+}

+/*

+@Data class SolverConfiguration {

+        VampireBackendSolver backendSolver

+        String path

+        String[] options

+}

+*/

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend
new file mode 100644
index 00000000..66f4fb06
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend
@@ -0,0 +1,5 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+interface VampireModelInterpretation_TypeInterpretation {
+        
+}
\ No newline at end of file
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend
new file mode 100644
index 00000000..863ec783
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend
@@ -0,0 +1,5 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation {
+        //TODO
+}
\ No newline at end of file