12 files changed, 1130 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..27e00ccf
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
@@ -0,0 +1,22 @@
+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
+        public var boolean writeToFile = false
+}
+
+
+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..64484b88
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -0,0 +1,102 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner
+
+import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated
+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 ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import java.io.PrintWriter
+import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes
+
+class VampireSolver extends LogicReasoner{
+        
+        new() {
+                VampireLanguagePackage.eINSTANCE.eClass
+                val x = new VampireLanguageStandaloneSetupGenerated
+                VampireLanguageStandaloneSetup::doSetup()
+        }
+        
+         val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
+//       //not for now
+//       val VampireHandler handler = new VampireHandler
+//       val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
+         
+         val fileName = "problem.tptp"
+         
+         override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
+                val vampireConfig = configuration.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;
+                if(vampireConfig.writeToFile) {
+                        fileURI = workspace.writeModel(vampireProblem,fileName).toFileString
+                } else {
+                        vampireCode = workspace.writeModelToString(vampireProblem,fileName)
+                } 
+                val transformationTime = System.currentTimeMillis - transformationStart
+                // Finish: Logic -> Vampire mapping
+                
+                //Creates a file containing the tptp code after transformation
+                val out = new PrintWriter("output/files/vampireCode.tptp")
+                out.println(vampireCode)
+                out.close()
+                
+                
+                /*      
+                 * not for now -> Start: Solving Alloy problem
+                 *  
+                // Start: Solving Alloy problem
+                val solverStart = System.currentTimeMillis
+                val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode)
+                val logicResult = backwardMapper.transformOutput(problem,configuration.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
+//                      )
+//              ]
+        }       
+//      */
+        
+}
\ 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.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..5ec15541
--- /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,386 @@
+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.*
+
+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_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(
+                this)
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper
+
+        public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) {
+                this.typeMapper = typeMapper
+        }
+
+        public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem,
+                VampireSolverConfiguration configuration) {
+                // create model bases
+                // TODO
+                val initialComment = createVLSComment => [
+                        it.comment = "%This is an initial Test Comment \r"
+                ]
+
+                val specification = createVampireModel => [
+                        it.comments += initialComment
+                ]
+
+                val trace = new Logic2VampireLanguageMapperTrace => [
+                        it.specification = specification
+
+//                      it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem))
+                ]
+
+                // call mappers
+                if (!problem.types.isEmpty) {
+                        typeMapper.transformTypes(problem.types, problem.elements, this, trace)
+                }
+
+                trace.constantDefinitions = problem.collectConstantDefinitions
+                trace.relationDefinitions = problem.collectRelationDefinitions
+
+                problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
+
+                // only transforms definitions
+                // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)]
+                problem.constants.filter(ConstantDefinition).forEach [
+                        this.constantMapper.transformConstantDefinitionSpecification(it, trace)
+                ]
+
+                // //////////////////
+                // Transform Assertions
+                // //////////////////
+                for (assertion : problem.assertions) {
+                        transformAssertion(assertion, trace)
+                }
+
+                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.createUniversallyQuantifiedExpression(this, forall, trace, variables)
+        }
+
+        def dispatch protected VLSTerm transformTerm(Exists exists, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                support.createExistentiallyQuantifiedExpression(this, exists, trace, variables)
+        }
+
+        def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+                return createVLSFunction => [
+                        it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name )
+                        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
+                                        // below does not work
+                                        val res = createVLSVariable => [
+//                                              it.name = support.toIDMultiple("Var", variable.lookup(variables).name)
+                                                it.name = support.toID(variable.lookup(variables).name)
+                                        ]
+                                        // no need for potprocessing cuz booleans are supported
+                                        return res
+                                }
+
+                                // 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 = support.toIDMultiple("rel", relation.name)
+                                                it.terms += parameterSubstitutions.map[p | p.transformTerm(trace,variables)]
+                                        ]
+                                }
+
+                        }
+                        
\ 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/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..135b3f07
--- /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,39 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
+import java.util.HashMap
+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
+//NOT NEEDED    //public var VLSFunction constantDec
+        
+        public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace
+        
+        
+//NOT NEEDED    //public val Map<ConstantDeclaration, VLSFunctionDeclaration> constantDeclaration2LanguageField = new HashMap
+        //public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap
+        
+        public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions
+        
+        public var Map<RelationDeclaration, RelationDefinition> relationDefinitions
+        public val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
+        public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap
+                
+}
\ 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_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..60653a42
--- /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,183 @@
+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.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(RelationDefinition r, Logic2VampireLanguageMapperTrace trace) {
+
+                // 1. store all variables in support wrt their name
+                // 1.1 if variable has type, creating list of type declarations
+                val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
+                val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
+                val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
+                val typedefs = new ArrayList<VLSTerm>
+                for (variable : r.variables) {
+                        val v = createVLSVariable => [
+                                it.name = support.toIDMultiple("Var", variable.name)
+                        ]
+                        relationVar2VLS.put(variable, v)
+
+                        val varTypeComply = createVLSFunction => [
+                                it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.terms += createVLSVariable => [
+                                        it.name = support.toIDMultiple("Var", variable.name)
+                                ]
+                        ]
+                        relationVar2TypeDecComply.put(variable, varTypeComply)
+                        
+                        val varTypeRes = createVLSFunction => [
+                                it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.terms += createVLSVariable => [
+                                        it.name = support.toIDMultiple("Var", variable.name)
+                                ]
+                        ]                       
+                        relationVar2TypeDecRes.put(variable, varTypeRes)
+                }
+
+                val comply = createVLSFofFormula => [
+                        it.name = support.toIDMultiple("compliance", r.name)
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                for (variable : r.variables) {
+                                        val v = createVLSVariable => [
+                                                it.name = variable.lookup(relationVar2VLS).name
+                                        ]
+                                        it.variables += v
+
+                                }
+                                it.operand = createVLSImplies => [
+                                        it.left = createVLSFunction => [
+                                                it.constant = support.toIDMultiple("rel", r.name)
+                                                for (variable : r.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", r.name)
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                for (variable : r.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", r.name)
+                                                        for (variable : r.variables) {
+                                                                val v = createVLSVariable => [
+                                                                        it.name = variable.lookup(relationVar2VLS).name
+                                                                ]
+                                                                it.terms += v
+
+                                                        }
+                                                ]
+                                                it.right = base.transformTerm(r.value, trace, relationVar2VLS)
+                                        ]
+
+                                ]
+
+                        ]
+
+                ]
+
+                // trace.relationDefinition2Predicate.put(r,res)
+                trace.specification.formulas += comply;
+                trace.specification.formulas += res;
+
+        }
+        
+        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) {
+
+                // 1. store all variables in support wrt their name
+                // 1.1 if variable has type, creating list of type declarations
+                val List<VLSVariable> relationVar2VLS = new ArrayList
+                val List<VLSFunction> relationVar2TypeDecComply = new ArrayList
+                val typedefs = new ArrayList<VLSTerm>
+                
+                for (i : 0..<r.parameters.length) {
+                        
+                        val v = createVLSVariable => [
+                                it.name = support.toIDMultiple("Var", i.toString)
+                        ]
+                        relationVar2VLS.add(v)
+
+                        val varTypeComply = createVLSFunction => [
+                                it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name)
+                                it.terms += createVLSVariable => [
+                                        it.name = support.toIDMultiple("Var", i.toString)
+                                ]
+                        ]
+                        relationVar2TypeDecComply.add(varTypeComply)
+
+                }
+                
+
+                val comply = createVLSFofFormula => [
+                        it.name = support.toIDMultiple("compliance", r.name)
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                
+                                for (i : 0..<r.parameters.length) {
+                                        val v = createVLSVariable => [
+                                                it.name = relationVar2VLS.get(i).name
+                                        ]
+                                        it.variables += v
+
+                                }
+                                
+                                it.operand = createVLSImplies => [
+                                        it.left = createVLSFunction => [
+                                                it.constant = support.toIDMultiple("rel", r.name)
+                                                
+                                                for (i : 0..<r.parameters.length) {
+                                                        val v = createVLSVariable => [
+                                                                it.name = relationVar2VLS.get(i).name
+                                                        ]
+                                                        it.terms += v
+                                                }
+                                                
+                                        ]
+                                        it.right = support.unfoldAnd(relationVar2TypeDecComply)
+                                ]
+                        ]
+                ]
+
+                // trace.relationDefinition2Predicate.put(r,res)
+                trace.specification.formulas += comply
+        }
+
+}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
new file mode 100644
index 00000000..ab92b42f
--- /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,148 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import org.eclipse.emf.common.util.EList
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+
+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("_")
+        }
+
+        // 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
+        }
+
+        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 createUniversallyQuantifiedExpression(Logic2VampireLanguageMapper mapper,
+                QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+                val variableMap = expression.quantifiedVariables.toInvertedMap [ v |
+                        createVLSVariable => [it.name = toIDMultiple("Var", v.name)]
+                ]
+
+                val typedefs = new ArrayList<VLSTerm>
+                for (variable : expression.quantifiedVariables) {
+                        val eq = createVLSFunction => [
+                                it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.terms += createVLSVariable => [
+                                        it.name = toIDMultiple("Var", variable.name)
+                                ]
+
+                        ]
+                        typedefs.add(eq)
+                }
+                
+
+                createVLSUniversalQuantifier => [
+                        it.variables += variableMap.values
+                        it.operand = createVLSImplies => [
+                                it.left = unfoldAnd(typedefs)
+                                it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))
+                        ]
+                ]
+        }
+
+        def protected VLSTerm createExistentiallyQuantifiedExpression(Logic2VampireLanguageMapper mapper,
+                QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+                val variableMap = expression.quantifiedVariables.toInvertedMap [ v |
+                        createVLSVariable => [it.name = toIDMultiple("Var", v.name)]
+                ]
+
+                val typedefs = new ArrayList<VLSTerm>
+                for (variable : expression.quantifiedVariables) {
+                        val eq = createVLSFunction => [
+                                it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.terms += createVLSVariable => [
+                                        it.name = toIDMultiple("Var", variable.name)
+                                ]
+                        ]
+                        typedefs.add(eq)
+                }
+
+                typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)))
+                createVLSExistentialQuantifier => [
+                        it.variables += variableMap.values
+                        it.operand = unfoldAnd(typedefs)
+
+                ]
+        }
+
+        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..1f071635
--- /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,19 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import java.util.Collection
+import java.util.List
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+
+interface Logic2VampireLanguageMapper_TypeMapper {
+        def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace);
+        //samples below 2 lines
+        def List<VLSTerm> transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace)
+        def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace)
+        
+        def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace)
+        def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace)
+        
+        def VampireModelInterpretation_TypeInterpretation getTypeInterpreter()
+}
\ No newline at end of file
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..a0f0edda
--- /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,21 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.List
+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, VLSEquality> definedElement2Declaration = new HashMap //Not Yet Used
+        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/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
new file mode 100644
index 00000000..7221f3ff
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -0,0 +1,158 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+import java.util.ArrayList
+import java.util.Collection
+
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+
+class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {
+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
+
+        new() {
+                LogicproblemPackage.eINSTANCE.class
+        }
+
+        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements,
+                Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
+                val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
+                trace.typeMapperTrace = typeTrace
+
+                val VLSVariable variable = createVLSVariable => [it.name = "A"] // did not work
+                // 1. store predicates for declarations in trace
+                for (type : types) {
+                        val typePred = createVLSFunction => [
+                                it.constant = support.toIDMultiple("type", type.name)
+                                it.terms += createVLSVariable => [it.name = variable.name]
+                        ]
+                        typeTrace.type2Predicate.put(type, typePred)
+                }
+
+                // 2. Map each type definition to fof formula
+                for (type : types.filter(TypeDefinition)) {
+
+                        val res = createVLSFofFormula => [
+                                it.name = support.toIDMultiple("typeDef", type.name)
+                                // below is temporary solution
+                                it.fofRole = "axiom"
+                                it.fofFormula = createVLSUniversalQuantifier => [
+                                        it.variables += createVLSVariable => [it.name = variable.name]
+                                        it.operand = createVLSEquivalent => [
+                                                it.left = createVLSFunction => [
+                                                        it.constant = type.lookup(typeTrace.type2Predicate).constant
+                                                        it.terms += createVLSVariable => [it.name = "A"]
+                                                ]
+
+                                                type.lookup(typeTrace.type2Predicate)
+                                                it.right = support.unfoldOr(type.elements.map [ e |
+                                                        createVLSEquality => [
+                                                                it.left = createVLSVariable => [it.name = variable.name]
+//                                                              it.right = createVLSDoubleQuote => [
+//                                                                      it.value = "\"" + e.name + "\""
+//                                                              ]
+                                                                it.right = createVLSDoubleQuote => [
+                                                                        it.value = "\"a" + e.name + "\""
+                                                                ]
+                                                        ]
+                                                ])
+                                        ]
+                                ]
+
+                        ]
+                        trace.specification.formulas += res
+                }
+                // 2.5. Currently allowing duplicate types. Not problematic cuz strings are by def unique
+                // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
+                // and store in a map
+//              val List<VLSTerm> type2PossibleNot = new ArrayList
+//              val List<VLSTerm> type2And = new ArrayList
+                for (type : types.filter[!isIsAbstract]) {
+                        for (type2 : types) {
+                                // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
+                                if (type == type2 || dfsSupertypeCheck(type, type2)) {
+                                        typeTrace.type2PossibleNot.put(type2, createVLSFunction => [
+                                                it.constant = type2.lookup(typeTrace.type2Predicate).constant
+                                                it.terms += createVLSVariable => [it.name = "A"]
+                                        ])
+                                } else {
+                                        typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [
+                                                it.operand = createVLSFunction => [
+                                                        it.constant = type2.lookup(typeTrace.type2Predicate).constant
+                                                        it.terms += createVLSVariable => [it.name = "A"]
+                                                ]
+                                        ])
+                                }
+//                              typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate))
+                        }
+                        typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
+//                      typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) )
+                        typeTrace.type2PossibleNot.clear
+                }
+
+                // 5. create fof function that is an or with all the elements in map
+                val hierarch = createVLSFofFormula => [
+                        it.name = "hierarchyHandler"
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                it.variables += createVLSVariable => [it.name = "A"]
+                                it.operand = createVLSEquivalent => [
+                                        it.left = createVLSFunction => [
+                                                it.constant = "Object"
+                                                it.terms += createVLSVariable => [
+                                                        it.name = "A"
+                                                ]
+                                        ]
+                                        it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
+                                ]
+                        ]
+                ]
+
+                trace.specification.formulas += hierarch
+        }
+
+        def boolean dfsSupertypeCheck(Type type, Type type2) {
+                // There is surely a better way to do this
+                if (type.supertypes.isEmpty)
+                        return false
+                else {
+                        if (type.supertypes.contains(type2))
+                                return true
+                        else {
+                                for (supertype : type.supertypes) {
+                                        if(dfsSupertypeCheck(supertype, type2)) return true
+                                }
+                        }
+                }
+        }
+
+        override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
+                Logic2VampireLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+        override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+        override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+        override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) {
+                createVLSDoubleQuote => [
+                        it.value = "\"a" + referred.name + "\""
+                ]
+        }
+
+        override getTypeInterpreter() {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/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