Initial workspace setup

49 files changed, 2718 insertions, 0 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath
new file mode 100644
index 00000000..a1e0140b
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath
@@ -0,0 +1,9 @@
+<?xml version="1.0" encoding="UTF-8"?>

+<classpath>

+        <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>

+        <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>

+        <classpathentry kind="src" path="src"/>

+        <classpathentry kind="src" path="xtend-gen"/>

+        <classpathentry kind="src" path="queries"/>

+        <classpathentry kind="output" path="bin"/>

+</classpath>

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.gitignore
new file mode 100644
index 00000000..ae3c1726
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.gitignore
@@ -0,0 +1 @@
+/bin/
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project
new file mode 100644
index 00000000..2221f39c
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project
@@ -0,0 +1,34 @@
+<?xml version="1.0" encoding="UTF-8"?>

+<projectDescription>

+        <name>ca.mcgill.ecse.dslreasoner.vampire.reasoner</name>

+        <comment></comment>

+        <projects>

+        </projects>

+        <buildSpec>

+                <buildCommand>

+                        <name>org.eclipse.xtext.ui.shared.xtextBuilder</name>

+                        <arguments>

+                        </arguments>

+                </buildCommand>

+                <buildCommand>

+                        <name>org.eclipse.jdt.core.javabuilder</name>

+                        <arguments>

+                        </arguments>

+                </buildCommand>

+                <buildCommand>

+                        <name>org.eclipse.pde.ManifestBuilder</name>

+                        <arguments>

+                        </arguments>

+                </buildCommand>

+                <buildCommand>

+                        <name>org.eclipse.pde.SchemaBuilder</name>

+                        <arguments>

+                        </arguments>

+                </buildCommand>

+        </buildSpec>

+        <natures>

+                <nature>org.eclipse.pde.PluginNature</nature>

+                <nature>org.eclipse.jdt.core.javanature</nature>

+                <nature>org.eclipse.xtext.ui.shared.xtextNature</nature>

+        </natures>

+</projectDescription>

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.settings/org.eclipse.jdt.core.prefs b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.settings/org.eclipse.jdt.core.prefs
new file mode 100644
index 00000000..295926d9
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.settings/org.eclipse.jdt.core.prefs
@@ -0,0 +1,7 @@
+eclipse.preferences.version=1

+org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled

+org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8

+org.eclipse.jdt.core.compiler.compliance=1.8

+org.eclipse.jdt.core.compiler.problem.assertIdentifier=error

+org.eclipse.jdt.core.compiler.problem.enumIdentifier=error

+org.eclipse.jdt.core.compiler.source=1.8

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF
new file mode 100644
index 00000000..2eb4f151
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF
@@ -0,0 +1,17 @@
+Manifest-Version: 1.0

+Bundle-ManifestVersion: 2

+Bundle-Name: Reasoner

+Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.reasoner;singleton:=true

+Bundle-Version: 1.0.0.qualifier

+Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.reasoner

+Bundle-RequiredExecutionEnvironment: JavaSE-1.8

+Require-Bundle: org.eclipse.xtend.lib,

+ hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",

+ hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",

+ ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0",

+ org.eclipse.viatra.query.runtime;bundle-version="2.1.0",

+ org.eclipse.viatra.query.runtime.base.itc;bundle-version="2.1.0"

+Export-Package: ca.mcgill.ecse.dslreasoner.vampire.reasoner,

+ ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

+ 

+

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties
new file mode 100644
index 00000000..41eb6ade
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties
@@ -0,0 +1,4 @@
+source.. = src/

+output.. = bin/

+bin.includes = META-INF/,\

+               .

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/signatureQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/signatureQueries.vql
new file mode 100644
index 00000000..754b5ac7
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/signatureQueries.vql
@@ -0,0 +1 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries
\ No newline at end of file
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/typeQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/typeQueries.vql
new file mode 100644
index 00000000..754b5ac7
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/typeQueries.vql
@@ -0,0 +1 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries
\ 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/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
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
new file mode 100644
index 00000000..e8e82269
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
new file mode 100644
index 00000000..dee2a0a8
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore
new file mode 100644
index 00000000..9efd2ac5
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore
@@ -0,0 +1,4 @@
+/.VampireSolver.java._trace
+/.TypeMappingTechnique.java._trace
+/.VampireBackendSolver.java._trace
+/.VampireSolverConfiguration.java._trace
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java
new file mode 100644
index 00000000..8ffba2f1
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java
@@ -0,0 +1,6 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner;

+

+@SuppressWarnings("all")

+public enum TypeMappingTechnique {

+  FilteredTypes;

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java
new file mode 100644
index 00000000..91e9bed0
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java
@@ -0,0 +1,5 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner;

+

+@SuppressWarnings("all")

+public enum VampireBackendSolver {

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
new file mode 100644
index 00000000..81cae109
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
@@ -0,0 +1,80 @@
+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.VampireSolverConfiguration;

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

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

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

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation;

+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.builder.TracedOutput;

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

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;

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

+import java.io.PrintWriter;

+import java.util.List;

+import org.eclipse.xtend2.lib.StringConcatenation;

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

+

+@SuppressWarnings("all")

+public class VampireSolver extends LogicReasoner {

+  public VampireSolver() {

+    VampireLanguagePackage.eINSTANCE.eClass();

+    final VampireLanguageStandaloneSetupGenerated x = new VampireLanguageStandaloneSetupGenerated();

+    VampireLanguageStandaloneSetup.doSetup();

+  }

+  

+  private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes());

+  

+  private final String fileName = "problem.tptp";

+  

+  @Override

+  public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration configuration, final ReasonerWorkspace workspace) throws LogicReasonerException {

+    try {

+      final VampireSolverConfiguration vampireConfig = this.asConfig(configuration);

+      final long transformationStart = System.currentTimeMillis();

+      final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig);

+      final VampireModel vampireProblem = result.getOutput();

+      final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();

+      String fileURI = null;

+      String vampireCode = null;

+      if (vampireConfig.writeToFile) {

+        fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString();

+      } else {

+        vampireCode = workspace.writeModelToString(vampireProblem, this.fileName);

+      }

+      long _currentTimeMillis = System.currentTimeMillis();

+      final long transformationTime = (_currentTimeMillis - transformationStart);

+      final PrintWriter out = new PrintWriter("output/files/vampireCode.tptp");

+      out.println(vampireCode);

+      out.close();

+      return null;

+    } catch (Throwable _e) {

+      throw Exceptions.sneakyThrow(_e);

+    }

+  }

+  

+  public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) {

+    if ((configuration instanceof VampireSolverConfiguration)) {

+      return ((VampireSolverConfiguration)configuration);

+    } else {

+      StringConcatenation _builder = new StringConcatenation();

+      _builder.append("The configuration have to be an ");

+      String _simpleName = VampireSolverConfiguration.class.getSimpleName();

+      _builder.append(_simpleName);

+      _builder.append("!");

+      throw new IllegalArgumentException(_builder.toString());

+    }

+  }

+  

+  @Override

+  public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) {

+    return null;

+  }

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
new file mode 100644
index 00000000..d392016e
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
@@ -0,0 +1,10 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner;

+

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

+

+@SuppressWarnings("all")

+public class VampireSolverConfiguration extends LogicSolverConfiguration {

+  public int symmetry = 0;

+  

+  public boolean writeToFile = false;

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
new file mode 100644
index 00000000..10edee94
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
new file mode 100644
index 00000000..50c1d625
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
new file mode 100644
index 00000000..f331beac
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
new file mode 100644
index 00000000..e929e637
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
new file mode 100644
index 00000000..cc7aea7c
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
new file mode 100644
index 00000000..1b6cf5d1
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
new file mode 100644
index 00000000..7a4d5bc7
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
new file mode 100644
index 00000000..7b6b2f9a
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
new file mode 100644
index 00000000..f8b3c54e
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
new file mode 100644
index 00000000..52b870a3
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
new file mode 100644
index 00000000..d27ff186
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
@@ -0,0 +1,11 @@
+/.Logic2VampireLanguageMapper_ConstantMapper.java._trace
+/.Logic2VampireLanguageMapper.java._trace
+/.Logic2VampireLanguageMapperTrace.java._trace
+/.Logic2VampireLanguageMapper_TypeMapperTrace.java._trace
+/.VampireModelInterpretation_TypeInterpretation.java._trace
+/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.java._trace
+/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java._trace
+/.Logic2VampireLanguageMapper_TypeMapper.java._trace
+/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java._trace
+/.Logic2VampireLanguageMapper_Support.java._trace
+/.Logic2VampireLanguageMapper_RelationMapper.java._trace
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
new file mode 100644
index 00000000..390a6b10
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -0,0 +1,442 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+import java.util.Arrays;

+import java.util.Collections;

+import java.util.HashMap;

+import java.util.List;

+import java.util.Map;

+import java.util.function.Consumer;

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

+import org.eclipse.xtend.lib.annotations.AccessorType;

+import org.eclipse.xtend.lib.annotations.Accessors;

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

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

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

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

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  @Accessors(AccessorType.PUBLIC_GETTER)

+  private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this);

+  

+  @Accessors(AccessorType.PUBLIC_GETTER)

+  private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this);

+  

+  @Accessors(AccessorType.PUBLIC_GETTER)

+  private final Logic2VampireLanguageMapper_TypeMapper typeMapper;

+  

+  public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) {

+    this.typeMapper = typeMapper;

+  }

+  

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

+    VLSComment _createVLSComment = this.factory.createVLSComment();

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

+      it.setComment("%This is an initial Test Comment \r");

+    };

+    final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function);

+    VampireModel _createVampireModel = this.factory.createVampireModel();

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

+      EList<VLSComment> _comments = it.getComments();

+      _comments.add(initialComment);

+    };

+    final VampireModel specification = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1);

+    Logic2VampireLanguageMapperTrace _logic2VampireLanguageMapperTrace = new Logic2VampireLanguageMapperTrace();

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

+      it.specification = specification;

+    };

+    final Logic2VampireLanguageMapperTrace trace = ObjectExtensions.<Logic2VampireLanguageMapperTrace>operator_doubleArrow(_logic2VampireLanguageMapperTrace, _function_2);

+    boolean _isEmpty = problem.getTypes().isEmpty();

+    boolean _not = (!_isEmpty);

+    if (_not) {

+      this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);

+    }

+    trace.constantDefinitions = this.collectConstantDefinitions(problem);

+    trace.relationDefinitions = this.collectRelationDefinitions(problem);

+    final Consumer<Relation> _function_3 = (Relation it) -> {

+      this.relationMapper.transformRelation(it, trace);

+    };

+    problem.getRelations().forEach(_function_3);

+    final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> {

+      this.constantMapper.transformConstantDefinitionSpecification(it, trace);

+    };

+    Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_4);

+    EList<Assertion> _assertions = problem.getAssertions();

+    for (final Assertion assertion : _assertions) {

+      this.transformAssertion(assertion, trace);

+    }

+    return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace);

+  }

+  

+  protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) {

+    return null;

+  }

+  

+  private HashMap<ConstantDeclaration, ConstantDefinition> collectConstantDefinitions(final LogicProblem problem) {

+    final HashMap<ConstantDeclaration, ConstantDefinition> res = new HashMap<ConstantDeclaration, ConstantDefinition>();

+    final Function1<ConstantDefinition, Boolean> _function = (ConstantDefinition it) -> {

+      ConstantDeclaration _defines = it.getDefines();

+      return Boolean.valueOf((_defines != null));

+    };

+    final Consumer<ConstantDefinition> _function_1 = (ConstantDefinition it) -> {

+      res.put(it.getDefines(), it);

+    };

+    IterableExtensions.<ConstantDefinition>filter(Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class), _function).forEach(_function_1);

+    return res;

+  }

+  

+  private HashMap<RelationDeclaration, RelationDefinition> collectRelationDefinitions(final LogicProblem problem) {

+    final HashMap<RelationDeclaration, RelationDefinition> res = new HashMap<RelationDeclaration, RelationDefinition>();

+    final Function1<RelationDefinition, Boolean> _function = (RelationDefinition it) -> {

+      RelationDeclaration _defines = it.getDefines();

+      return Boolean.valueOf((_defines != null));

+    };

+    final Consumer<RelationDefinition> _function_1 = (RelationDefinition it) -> {

+      res.put(it.getDefines(), it);

+    };

+    IterableExtensions.<RelationDefinition>filter(Iterables.<RelationDefinition>filter(problem.getRelations(), RelationDefinition.class), _function).forEach(_function_1);

+    return res;

+  }

+  

+  protected boolean transformAssertion(final Assertion assertion, final Logic2VampireLanguageMapperTrace trace) {

+    boolean _xblockexpression = false;

+    {

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

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

+        it.setName(this.support.toID(assertion.getName()));

+        it.setFofRole("axiom");

+        it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP));

+      };

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

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

+      _xblockexpression = _formulas.add(res);

+    }

+    return _xblockexpression;

+  }

+  

+  protected VLSTerm _transformTerm(final BoolLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSTerm _xifexpression = null;

+    boolean _isValue = literal.isValue();

+    boolean _equals = (_isValue == true);

+    if (_equals) {

+      _xifexpression = this.factory.createVLSTrue();

+    } else {

+      _xifexpression = this.factory.createVLSFalse();

+    }

+    return _xifexpression;

+  }

+  

+  protected VLSTerm _transformTerm(final IntLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSInt _createVLSInt = this.factory.createVLSInt();

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

+      it.setValue(Integer.valueOf(literal.getValue()).toString());

+    };

+    return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final RealLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSReal _createVLSReal = this.factory.createVLSReal();

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

+      it.setValue(literal.getValue().toString());

+    };

+    return ObjectExtensions.<VLSReal>operator_doubleArrow(_createVLSReal, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      it.setOperand(this.transformTerm(not.getOperand(), trace, variables));

+    };

+    return ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final And and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    final Function1<Term, VLSTerm> _function = (Term it) -> {

+      return this.transformTerm(it, trace, variables);

+    };

+    return this.support.unfoldAnd(ListExtensions.<Term, VLSTerm>map(and.getOperands(), _function));

+  }

+  

+  protected VLSTerm _transformTerm(final Or or, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    final Function1<Term, VLSTerm> _function = (Term it) -> {

+      return this.transformTerm(it, trace, variables);

+    };

+    return this.support.unfoldOr(ListExtensions.<Term, VLSTerm>map(or.getOperands(), _function));

+  }

+  

+  protected VLSTerm _transformTerm(final Impl impl, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSImplies _createVLSImplies = this.factory.createVLSImplies();

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

+      it.setLeft(this.transformTerm(impl.getLeftOperand(), trace, variables));

+      it.setRight(this.transformTerm(impl.getRightOperand(), trace, variables));

+    };

+    return ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final Iff iff, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      it.setLeft(this.transformTerm(iff.getLeftOperand(), trace, variables));

+      it.setRight(this.transformTerm(iff.getRightOperand(), trace, variables));

+    };

+    return ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final Equals equals, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSEquality _createVLSEquality = this.factory.createVLSEquality();

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

+      it.setLeft(this.transformTerm(equals.getLeftOperand(), trace, variables));

+      it.setRight(this.transformTerm(equals.getRightOperand(), trace, variables));

+    };

+    return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final Distinct distinct, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.support.unfoldDistinctTerms(this, distinct.getOperands(), trace, variables);

+  }

+  

+  protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.support.createUniversallyQuantifiedExpression(this, forall, trace, variables);

+  }

+  

+  protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.support.createExistentiallyQuantifiedExpression(this, exists, trace, variables);

+  }

+  

+  protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      TypeReference _range = instanceOf.getRange();

+      it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName()));

+      EList<VLSTerm> _terms = it.getTerms();

+      VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables);

+      _terms.add(_transformTerm);

+    };

+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final SymbolicValue symbolicValue, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.transformSymbolicReference(symbolicValue.getSymbolicReference(), symbolicValue.getParameterSubstitutions(), trace, variables);

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.typeMapper.transformReference(referred, trace);

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSConstant _createVLSConstant = this.factory.createVLSConstant();

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

+      it.setName(this.support.toID(constant.getName()));

+    };

+    final VLSConstant res = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);

+    return res;

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final ConstantDefinition constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return null;

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      it.setName(this.support.toID(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables).getName()));

+    };

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

+    return res;

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return null;

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final FunctionDefinition function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return null;

+  }

+  

+  /**

+   * 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

+   * //                                                 ]

+   * //                                         }

+   * }

+   * }

+   */

+  protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      it.setConstant(this.support.toIDMultiple("rel", relation.getName()));

+      EList<VLSTerm> _terms = it.getTerms();

+      final Function1<Term, VLSTerm> _function_1 = (Term p) -> {

+        return this.transformTerm(p, trace, variables);

+      };

+      List<VLSTerm> _map = ListExtensions.<Term, VLSTerm>map(parameterSubstitutions, _function_1);

+      Iterables.<VLSTerm>addAll(_terms, _map);

+    };

+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

+  }

+  

+  protected VLSTerm transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) {

+    return _transformTypeReference(boolTypeReference, trace);

+  }

+  

+  protected VLSTerm transformTerm(final Term and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    if (and instanceof And) {

+      return _transformTerm((And)and, trace, variables);

+    } else if (and instanceof BoolLiteral) {

+      return _transformTerm((BoolLiteral)and, trace, variables);

+    } else if (and instanceof Distinct) {

+      return _transformTerm((Distinct)and, trace, variables);

+    } else if (and instanceof Equals) {

+      return _transformTerm((Equals)and, trace, variables);

+    } else if (and instanceof Exists) {

+      return _transformTerm((Exists)and, trace, variables);

+    } else if (and instanceof Forall) {

+      return _transformTerm((Forall)and, trace, variables);

+    } else if (and instanceof Iff) {

+      return _transformTerm((Iff)and, trace, variables);

+    } else if (and instanceof Impl) {

+      return _transformTerm((Impl)and, trace, variables);

+    } else if (and instanceof IntLiteral) {

+      return _transformTerm((IntLiteral)and, trace, variables);

+    } else if (and instanceof Not) {

+      return _transformTerm((Not)and, trace, variables);

+    } else if (and instanceof Or) {

+      return _transformTerm((Or)and, trace, variables);

+    } else if (and instanceof RealLiteral) {

+      return _transformTerm((RealLiteral)and, trace, variables);

+    } else if (and instanceof InstanceOf) {

+      return _transformTerm((InstanceOf)and, trace, variables);

+    } else if (and instanceof SymbolicValue) {

+      return _transformTerm((SymbolicValue)and, trace, variables);

+    } else {

+      throw new IllegalArgumentException("Unhandled parameter types: " +

+        Arrays.<Object>asList(and, trace, variables).toString());

+    }

+  }

+  

+  protected VLSTerm transformSymbolicReference(final SymbolicDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    if (constant instanceof ConstantDeclaration) {

+      return _transformSymbolicReference((ConstantDeclaration)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof ConstantDefinition) {

+      return _transformSymbolicReference((ConstantDefinition)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof FunctionDeclaration) {

+      return _transformSymbolicReference((FunctionDeclaration)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof FunctionDefinition) {

+      return _transformSymbolicReference((FunctionDefinition)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof DefinedElement) {

+      return _transformSymbolicReference((DefinedElement)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof Relation) {

+      return _transformSymbolicReference((Relation)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof Variable) {

+      return _transformSymbolicReference((Variable)constant, parameterSubstitutions, trace, variables);

+    } else {

+      throw new IllegalArgumentException("Unhandled parameter types: " +

+        Arrays.<Object>asList(constant, parameterSubstitutions, trace, variables).toString());

+    }

+  }

+  

+  @Pure

+  public Logic2VampireLanguageMapper_ConstantMapper getConstantMapper() {

+    return this.constantMapper;

+  }

+  

+  @Pure

+  public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() {

+    return this.relationMapper;

+  }

+  

+  @Pure

+  public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() {

+    return this.typeMapper;

+  }

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
new file mode 100644
index 00000000..855815f8
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
@@ -0,0 +1,34 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

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

+import java.util.HashMap;

+import java.util.Map;

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapperTrace {

+  public VampireModel specification;

+  

+  public VLSFofFormula logicLanguageBody;

+  

+  public VLSTerm formula;

+  

+  public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace;

+  

+  public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions;

+  

+  public Map<RelationDeclaration, RelationDefinition> relationDefinitions;

+  

+  public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>();

+  

+  public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>();

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java
new file mode 100644
index 00000000..e5f42e73
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java
@@ -0,0 +1,34 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_ConstantMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  private final Logic2VampireLanguageMapper base;

+  

+  public Logic2VampireLanguageMapper_ConstantMapper(final Logic2VampireLanguageMapper base) {

+    this.base = base;

+  }

+  

+  protected Object _transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) {

+    return null;

+  }

+  

+  protected Object transformConstantDefinitionSpecification(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) {

+    return null;

+  }

+  

+  protected Object transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) {

+    return _transformConstant(constant, trace);

+  }

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
new file mode 100644
index 00000000..561402a7
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -0,0 +1,296 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+import java.util.ArrayList;

+import java.util.Arrays;

+import java.util.Collection;

+import java.util.HashMap;

+import java.util.List;

+import java.util.Map;

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

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

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

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_RelationMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  private final Logic2VampireLanguageMapper base;

+  

+  public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) {

+    this.base = base;

+  }

+  

+  public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace) {

+    final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>();

+    final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>();

+    final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>();

+    final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();

+    EList<Variable> _variables = r.getVariables();

+    for (final Variable variable : _variables) {

+      {

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

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

+          it.setName(this.support.toIDMultiple("Var", variable.getName()));

+        };

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

+        relationVar2VLS.put(variable, v);

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

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

+          TypeReference _range = variable.getRange();

+          it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName()));

+          EList<VLSTerm> _terms = it.getTerms();

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

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

+            it_1.setName(this.support.toIDMultiple("Var", variable.getName()));

+          };

+          VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);

+          _terms.add(_doubleArrow);

+        };

+        final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

+        relationVar2TypeDecComply.put(variable, varTypeComply);

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

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

+          TypeReference _range = variable.getRange();

+          it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName()));

+          EList<VLSTerm> _terms = it.getTerms();

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

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

+            it_1.setName(this.support.toIDMultiple("Var", variable.getName()));

+          };

+          VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3);

+          _terms.add(_doubleArrow);

+        };

+        final VLSFunction varTypeRes = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_2);

+        relationVar2TypeDecRes.put(variable, varTypeRes);

+      }

+    }

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

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

+      it.setName(this.support.toIDMultiple("compliance", r.getName()));

+      it.setFofRole("axiom");

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

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

+        EList<Variable> _variables_1 = r.getVariables();

+        for (final Variable variable_1 : _variables_1) {

+          {

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

+            final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> {

+              it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName());

+            };

+            final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2);

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

+            _variables_2.add(v);

+          }

+        }

+        VLSImplies _createVLSImplies = this.factory.createVLSImplies();

+        final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {

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

+          final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {

+            it_3.setConstant(this.support.toIDMultiple("rel", r.getName()));

+            EList<Variable> _variables_2 = r.getVariables();

+            for (final Variable variable_2 : _variables_2) {

+              {

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

+                final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> {

+                  it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName());

+                };

+                final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);

+                EList<VLSTerm> _terms = it_3.getTerms();

+                _terms.add(v);

+              }

+            }

+          };

+          VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);

+          it_2.setLeft(_doubleArrow);

+          Collection<VLSFunction> _values = relationVar2TypeDecComply.values();

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

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

+        };

+        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);

+        it_1.setOperand(_doubleArrow);

+      };

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

+      it.setFofFormula(_doubleArrow);

+    };

+    final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);

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

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

+      it.setName(this.support.toIDMultiple("relation", r.getName()));

+      it.setFofRole("axiom");

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

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

+        EList<Variable> _variables_1 = r.getVariables();

+        for (final Variable variable_1 : _variables_1) {

+          {

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

+            final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> {

+              it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName());

+            };

+            final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3);

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

+            _variables_2.add(v);

+          }

+        }

+        VLSImplies _createVLSImplies = this.factory.createVLSImplies();

+        final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {

+          Collection<VLSFunction> _values = relationVar2TypeDecRes.values();

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

+          it_2.setLeft(this.support.unfoldAnd(_arrayList));

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

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

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

+            final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> {

+              it_4.setConstant(this.support.toIDMultiple("rel", r.getName()));

+              EList<Variable> _variables_2 = r.getVariables();

+              for (final Variable variable_2 : _variables_2) {

+                {

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

+                  final Procedure1<VLSVariable> _function_6 = (VLSVariable it_5) -> {

+                    it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName());

+                  };

+                  final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6);

+                  EList<VLSTerm> _terms = it_4.getTerms();

+                  _terms.add(v);

+                }

+              }

+            };

+            VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5);

+            it_3.setLeft(_doubleArrow);

+            it_3.setRight(this.base.transformTerm(r.getValue(), trace, relationVar2VLS));

+          };

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

+          it_2.setRight(_doubleArrow);

+        };

+        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);

+        it_1.setOperand(_doubleArrow);

+      };

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

+      it.setFofFormula(_doubleArrow);

+    };

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

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

+    _formulas.add(comply);

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

+    _formulas_1.add(res);

+  }

+  

+  public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) {

+    final List<VLSVariable> relationVar2VLS = new ArrayList<VLSVariable>();

+    final List<VLSFunction> relationVar2TypeDecComply = new ArrayList<VLSFunction>();

+    final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();

+    int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;

+    ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true);

+    for (final Integer i : _doubleDotLessThan) {

+      {

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

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

+          it.setName(this.support.toIDMultiple("Var", i.toString()));

+        };

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

+        relationVar2VLS.add(v);

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

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

+          TypeReference _get = r.getParameters().get((i).intValue());

+          it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _get).getReferred().getName()));

+          EList<VLSTerm> _terms = it.getTerms();

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

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

+            it_1.setName(this.support.toIDMultiple("Var", i.toString()));

+          };

+          VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);

+          _terms.add(_doubleArrow);

+        };

+        final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

+        relationVar2TypeDecComply.add(varTypeComply);

+      }

+    }

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

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

+      it.setName(this.support.toIDMultiple("compliance", r.getName()));

+      it.setFofRole("axiom");

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

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

+        int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;

+        ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true);

+        for (final Integer i_1 : _doubleDotLessThan_1) {

+          {

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

+            final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> {

+              it_2.setName(relationVar2VLS.get((i_1).intValue()).getName());

+            };

+            final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2);

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

+            _variables.add(v);

+          }

+        }

+        VLSImplies _createVLSImplies = this.factory.createVLSImplies();

+        final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {

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

+          final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {

+            it_3.setConstant(this.support.toIDMultiple("rel", r.getName()));

+            int _length_2 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;

+            ExclusiveRange _doubleDotLessThan_2 = new ExclusiveRange(0, _length_2, true);

+            for (final Integer i_2 : _doubleDotLessThan_2) {

+              {

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

+                final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> {

+                  it_4.setName(relationVar2VLS.get((i_2).intValue()).getName());

+                };

+                final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);

+                EList<VLSTerm> _terms = it_3.getTerms();

+                _terms.add(v);

+              }

+            }

+          };

+          VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);

+          it_2.setLeft(_doubleArrow);

+          it_2.setRight(this.support.unfoldAnd(relationVar2TypeDecComply));

+        };

+        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);

+        it_1.setOperand(_doubleArrow);

+      };

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

+      it.setFofFormula(_doubleArrow);

+    };

+    final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);

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

+    _formulas.add(comply);

+  }

+  

+  public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) {

+    if (r instanceof RelationDeclaration) {

+      _transformRelation((RelationDeclaration)r, trace);

+      return;

+    } else if (r instanceof RelationDefinition) {

+      _transformRelation((RelationDefinition)r, trace);

+      return;

+    } else {

+      throw new IllegalArgumentException("Unhandled parameter types: " +

+        Arrays.<Object>asList(r, trace).toString());

+    }

+  }

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
new file mode 100644
index 00000000..e1be7df5
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -0,0 +1,242 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+import java.util.ArrayList;

+import java.util.Collection;

+import java.util.HashMap;

+import java.util.List;

+import java.util.Map;

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

+import org.eclipse.xtend2.lib.StringConcatenation;

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

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

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

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

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

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_Support {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  protected String toIDMultiple(final String... ids) {

+    final Function1<String, String> _function = (String it) -> {

+      return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(it.split("\\s+"))), "_");

+    };

+    return IterableExtensions.join(ListExtensions.<String, String>map(((List<String>)Conversions.doWrapArray(ids)), _function), "_");

+  }

+  

+  protected String toID(final String ids) {

+    return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_");

+  }

+  

+  protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) {

+    int _size = operands.size();

+    boolean _equals = (_size == 1);

+    if (_equals) {

+      return IterableExtensions.head(operands);

+    } else {

+      int _size_1 = operands.size();

+      boolean _greaterThan = (_size_1 > 1);

+      if (_greaterThan) {

+        VLSAnd _createVLSAnd = this.factory.createVLSAnd();

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

+          it.setLeft(IterableExtensions.head(operands));

+          it.setRight(this.unfoldAnd(operands.subList(1, operands.size())));

+        };

+        return ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function);

+      } else {

+        StringConcatenation _builder = new StringConcatenation();

+        _builder.append("Logic operator with 0 operands!");

+        throw new UnsupportedOperationException(_builder.toString());

+      }

+    }

+  }

+  

+  protected VLSTerm unfoldOr(final List<? extends VLSTerm> operands) {

+    int _size = operands.size();

+    boolean _equals = (_size == 1);

+    if (_equals) {

+      return IterableExtensions.head(operands);

+    } else {

+      int _size_1 = operands.size();

+      boolean _greaterThan = (_size_1 > 1);

+      if (_greaterThan) {

+        VLSOr _createVLSOr = this.factory.createVLSOr();

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

+          it.setLeft(IterableExtensions.head(operands));

+          it.setRight(this.unfoldOr(operands.subList(1, operands.size())));

+        };

+        return ObjectExtensions.<VLSOr>operator_doubleArrow(_createVLSOr, _function);

+      } else {

+        StringConcatenation _builder = new StringConcatenation();

+        _builder.append("Logic operator with 0 operands!");

+        throw new UnsupportedOperationException(_builder.toString());

+      }

+    }

+  }

+  

+  protected VLSTerm unfoldDistinctTerms(final Logic2VampireLanguageMapper m, final EList<Term> operands, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    int _size = operands.size();

+    boolean _equals = (_size == 1);

+    if (_equals) {

+      return m.transformTerm(IterableExtensions.<Term>head(operands), trace, variables);

+    } else {

+      int _size_1 = operands.size();

+      boolean _greaterThan = (_size_1 > 1);

+      if (_greaterThan) {

+        int _size_2 = operands.size();

+        int _size_3 = operands.size();

+        int _multiply = (_size_2 * _size_3);

+        int _divide = (_multiply / 2);

+        final ArrayList<VLSTerm> notEquals = new ArrayList<VLSTerm>(_divide);

+        int _size_4 = operands.size();

+        ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _size_4, true);

+        for (final Integer i : _doubleDotLessThan) {

+          int _size_5 = operands.size();

+          ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(((i).intValue() + 1), _size_5, true);

+          for (final Integer j : _doubleDotLessThan_1) {

+            VLSInequality _createVLSInequality = this.factory.createVLSInequality();

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

+              it.setLeft(m.transformTerm(operands.get((i).intValue()), trace, variables));

+              it.setRight(m.transformTerm(operands.get((j).intValue()), trace, variables));

+            };

+            VLSInequality _doubleArrow = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function);

+            notEquals.add(_doubleArrow);

+          }

+        }

+        return this.unfoldAnd(notEquals);

+      } else {

+        StringConcatenation _builder = new StringConcatenation();

+        _builder.append("Logic operator with 0 operands!");

+        throw new UnsupportedOperationException(_builder.toString());

+      }

+    }

+  }

+  

+  /**

+   * def protected  String toID(List<String> ids) {

+   *    ids.map[it.split("\\s+").join("'")].join("'")

+   * }

+   */

+  protected VLSTerm createUniversallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSUniversalQuantifier _xblockexpression = null;

+    {

+      final Function1<Variable, VLSVariable> _function = (Variable v) -> {

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

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

+          it.setName(this.toIDMultiple("Var", v.getName()));

+        };

+        return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);

+      };

+      final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function);

+      final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();

+      EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables();

+      for (final Variable variable : _quantifiedVariables) {

+        {

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

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

+            TypeReference _range = variable.getRange();

+            it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName()));

+            EList<VLSTerm> _terms = it.getTerms();

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

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

+              it_1.setName(this.toIDMultiple("Var", variable.getName()));

+            };

+            VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2);

+            _terms.add(_doubleArrow);

+          };

+          final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

+          typedefs.add(eq);

+        }

+      }

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

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

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

+        Collection<VLSVariable> _values = variableMap.values();

+        Iterables.<VLSVariable>addAll(_variables, _values);

+        VLSImplies _createVLSImplies = this.factory.createVLSImplies();

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

+          it_1.setLeft(this.unfoldAnd(typedefs));

+          it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));

+        };

+        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);

+        it.setOperand(_doubleArrow);

+      };

+      _xblockexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);

+    }

+    return _xblockexpression;

+  }

+  

+  protected VLSTerm createExistentiallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSExistentialQuantifier _xblockexpression = null;

+    {

+      final Function1<Variable, VLSVariable> _function = (Variable v) -> {

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

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

+          it.setName(this.toIDMultiple("Var", v.getName()));

+        };

+        return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);

+      };

+      final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function);

+      final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();

+      EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables();

+      for (final Variable variable : _quantifiedVariables) {

+        {

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

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

+            TypeReference _range = variable.getRange();

+            it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName()));

+            EList<VLSTerm> _terms = it.getTerms();

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

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

+              it_1.setName(this.toIDMultiple("Var", variable.getName()));

+            };

+            VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2);

+            _terms.add(_doubleArrow);

+          };

+          final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

+          typedefs.add(eq);

+        }

+      }

+      typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));

+      VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

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

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

+        Collection<VLSVariable> _values = variableMap.values();

+        Iterables.<VLSVariable>addAll(_variables, _values);

+        it.setOperand(this.unfoldAnd(typedefs));

+      };

+      _xblockexpression = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_1);

+    }

+    return _xblockexpression;

+  }

+  

+  protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) {

+    HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1);

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

+      it.putAll(map2);

+    };

+    return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function);

+  }

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
new file mode 100644
index 00000000..c55e2421
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -0,0 +1,25 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

+import ca.mcgill.ecse.dslreasoner.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.Collection;

+import java.util.List;

+

+@SuppressWarnings("all")

+public interface Logic2VampireLanguageMapper_TypeMapper {

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

+  

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

+  

+  public abstract VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace);

+  

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

+  

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

+  

+  public abstract VampireModelInterpretation_TypeInterpretation getTypeInterpreter();

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java
new file mode 100644
index 00000000..1e08c8ad
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java
@@ -0,0 +1,5 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

+@SuppressWarnings("all")

+public interface Logic2VampireLanguageMapper_TypeMapperTrace {

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java
new file mode 100644
index 00000000..d674ac71
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java
@@ -0,0 +1,21 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace {

+  public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();

+  

+  public final Map<DefinedElement, VLSEquality> definedElement2Declaration = new HashMap<DefinedElement, VLSEquality>();

+  

+  public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>();

+  

+  public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>();

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
new file mode 100644
index 00000000..38ff37cd
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
@@ -0,0 +1,287 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+import java.util.ArrayList;

+import java.util.Collection;

+import java.util.List;

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

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

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

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

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  public Logic2VampireLanguageMapper_TypeMapper_FilteredTypes() {

+    LogicproblemPackage.eINSTANCE.getClass();

+  }

+  

+  @Override

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

+    final Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes();

+    trace.typeMapperTrace = typeTrace;

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

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

+      it.setName("A");

+    };

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

+    for (final Type type : types) {

+      {

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

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

+          it.setConstant(this.support.toIDMultiple("type", type.getName()));

+          EList<VLSTerm> _terms = it.getTerms();

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

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

+            it_1.setName(variable.getName());

+          };

+          VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);

+          _terms.add(_doubleArrow);

+        };

+        final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

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

+      }

+    }

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

+    for (final TypeDefinition type_1 : _filter) {

+      {

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

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

+          it.setName(this.support.toIDMultiple("typeDef", type_1.getName()));

+          it.setFofRole("axiom");

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

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

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

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

+            final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> {

+              it_2.setName(variable.getName());

+            };

+            VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3);

+            _variables.add(_doubleArrow);

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

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

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

+              final Procedure1<VLSFunction> _function_5 = (VLSFunction it_3) -> {

+                it_3.setConstant(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate).getConstant());

+                EList<VLSTerm> _terms = it_3.getTerms();

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

+                final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {

+                  it_4.setName("A");

+                };

+                VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_6);

+                _terms.add(_doubleArrow_1);

+              };

+              VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5);

+              it_2.setLeft(_doubleArrow_1);

+              CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate);

+              final Function1<DefinedElement, VLSEquality> _function_6 = (DefinedElement e) -> {

+                VLSEquality _createVLSEquality = this.factory.createVLSEquality();

+                final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> {

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

+                  final Procedure1<VLSVariable> _function_8 = (VLSVariable it_4) -> {

+                    it_4.setName(variable.getName());

+                  };

+                  VLSVariable _doubleArrow_2 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_8);

+                  it_3.setLeft(_doubleArrow_2);

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

+                  final Procedure1<VLSDoubleQuote> _function_9 = (VLSDoubleQuote it_4) -> {

+                    String _name = e.getName();

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

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

+                    it_4.setValue(_plus_1);

+                  };

+                  VLSDoubleQuote _doubleArrow_3 = ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function_9);

+                  it_3.setRight(_doubleArrow_3);

+                };

+                return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7);

+              };

+              it_2.setRight(this.support.unfoldOr(ListExtensions.<DefinedElement, VLSEquality>map(type_1.getElements(), _function_6)));

+            };

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

+            it_1.setOperand(_doubleArrow_1);

+          };

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

+          it.setFofFormula(_doubleArrow);

+        };

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

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

+        _formulas.add(res);

+      }

+    }

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

+      boolean _isIsAbstract = it.isIsAbstract();

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

+    };

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

+    for (final Type type_2 : _filter_1) {

+      {

+        for (final Type type2 : types) {

+          if ((Objects.equal(type_2, type2) || this.dfsSupertypeCheck(type_2, type2))) {

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

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

+              it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant());

+              EList<VLSTerm> _terms = it.getTerms();

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

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

+                it_1.setName("A");

+              };

+              VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3);

+              _terms.add(_doubleArrow);

+            };

+            VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2);

+            typeTrace.type2PossibleNot.put(type2, _doubleArrow);

+          } else {

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

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

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

+              final Procedure1<VLSFunction> _function_4 = (VLSFunction it_1) -> {

+                it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant());

+                EList<VLSTerm> _terms = it_1.getTerms();

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

+                final Procedure1<VLSVariable> _function_5 = (VLSVariable it_2) -> {

+                  it_2.setName("A");

+                };

+                VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_5);

+                _terms.add(_doubleArrow_1);

+              };

+              VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_4);

+              it.setOperand(_doubleArrow_1);

+            };

+            VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);

+            typeTrace.type2PossibleNot.put(type2, _doubleArrow_1);

+          }

+        }

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

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

+        typeTrace.type2And.put(type_2, this.support.unfoldAnd(_arrayList));

+        typeTrace.type2PossibleNot.clear();

+      }

+    }

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

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

+      it.setName("hierarchyHandler");

+      it.setFofRole("axiom");

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

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

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

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

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

+          it_2.setName("A");

+        };

+        VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_4);

+        _variables.add(_doubleArrow);

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

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

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

+          final Procedure1<VLSFunction> _function_6 = (VLSFunction it_3) -> {

+            it_3.setConstant("Object");

+            EList<VLSTerm> _terms = it_3.getTerms();

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

+            final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> {

+              it_4.setName("A");

+            };

+            VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_7);

+            _terms.add(_doubleArrow_1);

+          };

+          VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_6);

+          it_2.setLeft(_doubleArrow_1);

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

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

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

+        };

+        VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5);

+        it_1.setOperand(_doubleArrow_1);

+      };

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

+      it.setFofFormula(_doubleArrow);

+    };

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

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

+    _formulas.add(hierarch);

+  }

+  

+  public boolean dfsSupertypeCheck(final Type type, final Type type2) {

+    boolean _xifexpression = false;

+    boolean _isEmpty = type.getSupertypes().isEmpty();

+    if (_isEmpty) {

+      return false;

+    } else {

+      boolean _xifexpression_1 = false;

+      boolean _contains = type.getSupertypes().contains(type2);

+      if (_contains) {

+        return true;

+      } else {

+        EList<Type> _supertypes = type.getSupertypes();

+        for (final Type supertype : _supertypes) {

+          boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2);

+          if (_dfsSupertypeCheck) {

+            return true;

+          }

+        }

+      }

+      _xifexpression = _xifexpression_1;

+    }

+    return _xifexpression;

+  }

+  

+  @Override

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

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

+  }

+  

+  @Override

+  public VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) {

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

+  }

+  

+  @Override

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

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

+  }

+  

+  @Override

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

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

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

+      String _name = referred.getName();

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

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

+      it.setValue(_plus_1);

+    };

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

+  }

+  

+  @Override

+  public VampireModelInterpretation_TypeInterpretation getTypeInterpreter() {

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

+  }

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java
new file mode 100644
index 00000000..507831fa
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java
@@ -0,0 +1,5 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

+@SuppressWarnings("all")

+public interface VampireModelInterpretation_TypeInterpretation {

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java
new file mode 100644
index 00000000..aff0dc9d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java
@@ -0,0 +1,7 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

+

+@SuppressWarnings("all")

+public class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation {

+}