Begin handing of scope and fix type definitions.

34 files changed, 544 insertions, 401 deletions

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
index 41eb6ade..aed85a48 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties
@@ -1,4 +1,5 @@
-source.. = src/

-output.. = bin/

 bin.includes = META-INF/,\

                .

+source.. = src/,\

+           src-gen/

+output.. = bin/

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
index 27e00ccf..618980a3 100644
--- 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
@@ -4,10 +4,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 
 class VampireSolverConfiguration extends LogicSolverConfiguration {
         
-        public var int symmetry = 0 // by default
+        //public var int symmetry = 0 // by default
         //choose needed backend solver
 //      public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
-        public var boolean writeToFile = false
 }
 
 
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
index cbe53bff..ee802a99 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -7,6 +7,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
@@ -14,80 +15,81 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
 
-class VampireSolver extends LogicReasoner{
-        
+class VampireSolver extends LogicReasoner {
+
         new() {
                 VampireLanguagePackage.eINSTANCE.eClass
                 val x = new VampireLanguageStandaloneSetupGenerated
                 VampireLanguageStandaloneSetup::doSetup()
         }
-        
-         val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
-         val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
-         val VampireHandler handler = new VampireHandler
-         
-         
-         val fileName = "vampireProblem.tptp"
-         
-         override solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace) throws LogicReasonerException {
+
+        val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(
+                new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
+        val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
+        val VampireHandler handler = new VampireHandler
+
+        val fileName = "vampireProblem.tptp"
+
+        override solve(LogicProblem problem, LogicSolverConfiguration config,
+                ReasonerWorkspace workspace) throws LogicReasonerException {
                 val vampireConfig = config.asConfig
-                
+
                 // Start: Logic -> Vampire mapping
                 val transformationStart = System.currentTimeMillis
-                //TODO
-                val result = forwardMapper.transformProblem(problem,vampireConfig)
+                // TODO
+                val result = forwardMapper.transformProblem(problem, vampireConfig)
                 val vampireProblem = result.output
                 val forwardTrace = result.trace
-                
+
                 var String fileURI = null;
                 var String vampireCode = null;
-                vampireCode = workspace.writeModelToString(vampireProblem,fileName)
-                if(vampireConfig.writeToFile) {
-                        fileURI = workspace.writeModel(vampireProblem,fileName).toFileString
+                vampireCode = workspace.writeModelToString(vampireProblem, fileName)
+
+                val writeFile = (
+                        vampireConfig.documentationLevel === DocumentationLevel::NORMAL ||
+                        vampireConfig.documentationLevel === DocumentationLevel::FULL)
+                if (writeFile) {
+                        fileURI = workspace.writeModel(vampireProblem, fileName).toFileString
                 }
-                
-                //Result as String
 
-                                
+                // Result as String
                 val transformationTime = System.currentTimeMillis - transformationStart
                 // Finish: Logic -> Vampire mapping
-                
-                                
                 /*        
-                // Start: Solving Alloy problem
-                val solverStart = System.currentTimeMillis
-                //Calling Solver (Currently Manually)
-                val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode)
-//              val result2 = null
-                //TODO
-                //Backwards Mapper
-                val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
-                
-                val solverFinish = System.currentTimeMillis-solverStart
-                // Finish: Solving Alloy problem
-                                
-                if(vampireConfig.writeToFile) workspace.deactivateModel(fileName)
-                
-                return logicResult
-                
-                /*/
+                 * // Start: Solving Alloy problem
+                 * val solverStart = System.currentTimeMillis
+                 * //Calling Solver (Currently Manually)
+                 * val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode)
+                 * //           val result2 = null
+                 * //TODO
+                 * //Backwards Mapper
+                 * val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
+                 * 
+                 * val solverFinish = System.currentTimeMillis-solverStart
+                 * // Finish: Solving Alloy problem
+                 *              
+                 * if(vampireConfig.writeToFile) workspace.deactivateModel(fileName)
+                 * 
+                 * return logicResult
+                 * 
+                 /*/
                 return null // for now
-                //*/
+                // */
         }
-        
-        def asConfig(LogicSolverConfiguration configuration){
-                if(configuration instanceof VampireSolverConfiguration) {
+
+        def asConfig(LogicSolverConfiguration configuration) {
+                if (configuration instanceof VampireSolverConfiguration) {
                         return configuration
                 } else {
-                        throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''')    
+                        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 answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
 //              val sols = modelResult.representation// as List<A4Solution>
 //              //val res = answers.map 
 //              sols.map[
@@ -98,7 +100,6 @@ class VampireSolver extends LogicReasoner{
 //                              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
index cd48a032..e2c15b75 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -48,6 +48,8 @@ class Logic2VampireLanguageMapper {
                 this)
         @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(
                 this)
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(
+                this)
         @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper
 
         public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) {
@@ -72,11 +74,15 @@ class Logic2VampireLanguageMapper {
 //                      it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem))
                 ]
 
-                // call mappers
+                // TYPE MAPPER
                 if (!problem.types.isEmpty) {
                         typeMapper.transformTypes(problem.types, problem.elements, this, trace)
                 }
 
+                // SCOPE MAPPER
+                scopeMapper.transformScope(config, trace)
+                
+                
                 trace.constantDefinitions = problem.collectConstantDefinitions
                 trace.relationDefinitions = problem.collectRelationDefinitions
 
@@ -204,8 +210,9 @@ class Logic2VampireLanguageMapper {
                 ]
         }
 
-        def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
-                support.unfoldDistinctTerms(this,distinct.operands,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] }
@@ -228,12 +235,14 @@ class Logic2VampireLanguageMapper {
                 support.createExistentiallyQuantifiedExpression(this, exists, trace, variables)
         }
 
-        def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> 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.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(
@@ -253,50 +262,49 @@ class Logic2VampireLanguageMapper {
         def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,
                 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
-                        typeMapper.transformReference(referred, trace)
-                }
+                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) {
+        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) {
+        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 => [
+                // 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) {
+                        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 {
@@ -316,71 +324,68 @@ class Logic2VampireLanguageMapper {
 //                              return support.postprocessResultOfSymbolicReference(function.range,res,trace)
 //                      }
 //              }
-                                }
+        }
 
-                                // TODO
-                                def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function,
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                        Map<Variable, VLSVariable> variables) {
+        // 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) {
+        }
+
+        // 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
+                return createVLSFunction => [
+                        it.constant = support.toIDMultiple("rel", relation.name)
+                        it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
+                ]
+        }
+
+}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
new file mode 100644
index 00000000..84aa521d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -0,0 +1,74 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

+

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

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

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

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

+import java.util.List

+

+class Logic2VampireLanguageMapper_ScopeMapper {

+        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 transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {

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

+

+                

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

+                val List<VLSConstant> instances = newArrayList

+                for (var i = 0; i < config.typeScopes.minNewElements; i++) {

+                        val num = i + 1

+                        val cst = createVLSConstant => [

+                                it.name = "o" + num

+                        ]

+                        instances.add(cst)

+                }

+                

+                

+                // TODO: specify for the max

+

+

+                // 2. Create initial fof formula to specify the number of elems

+                val cstDec = createVLSFofFormula => [

+                        it.name = "typeScope"

+                        it.fofRole = "axiom"

+                        it.fofFormula = createVLSUniversalQuantifier => [

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

+                                // check below

+                                it.operand = createVLSEquivalent => [

+                                        it.left = support.topLevelTypeFunc

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

+                                                createVLSEquality => [

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

+                                                        it.right = i

+                                                ]

+                                        ])

+                                ]

+                        ]

+                ]

+                trace.specification.formulas += cstDec

+

+

+                // TODO: specify for scope per type

+

+

+

+                // 3. Specify uniqueness of elements

+                val uniqueness = createVLSFofFormula => [

+                        it.name = "typeUniqueness"

+                        it.fofRole = "axiom"

+                        it.fofFormula = support.unfoldOr(instances.map [ i |

+                                createVLSEquality => [

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

+                                        it.right = i

+                                ]

+                        ])

+                ]

+                trace.specification.formulas += cstDec

+        }

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index ab92b42f..e69f0d51 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -1,17 +1,18 @@
 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.VLSFunction
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.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.Variable
 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
@@ -25,6 +26,19 @@ class Logic2VampireLanguageMapper_Support {
                 ids.split("\\s+").join("_")
         }
 
+        def protected VLSVariable duplicate(VLSVariable vrbl) {
+                return createVLSVariable => [it.name = vrbl.name]
+        }
+
+        def protected VLSFunction topLevelTypeFunc() {
+                return createVLSFunction => [
+                        it.constant = "object"
+                        it.terms += createVLSVariable => [
+                                it.name = "A"
+                        ]
+                ]
+        }
+
         // Support Functions
         // booleans
         // AND and OR
@@ -41,7 +55,6 @@ class Logic2VampireLanguageMapper_Support {
         }
 
         def protected VLSTerm unfoldOr(List<? extends VLSTerm> operands) {
-
 //              if(operands.size == 0) {basically return true}
                 /*else*/ if (operands.size == 1) {
                         return operands.head
@@ -56,20 +69,21 @@ class Logic2VampireLanguageMapper_Support {
 
         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)
+                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!''')
+                } else
+                        throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
         }
 
         // Symbolic
@@ -105,7 +119,6 @@ class Logic2VampireLanguageMapper_Support {
                         ]
                         typedefs.add(eq)
                 }
-                
 
                 createVLSUniversalQuantifier => [
                         it.variables += variableMap.values
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
index a0f0edda..aba47edb 100644
--- 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
@@ -1,20 +1,17 @@
 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 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.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<DefinedElement, VLSFunction> element2Predicate = new HashMap
         public val Map<Type, VLSTerm> type2PossibleNot = new HashMap
         public val Map<Type, VLSTerm> type2And = new HashMap
 
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
index 41e2137c..eed10656 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -11,6 +11,8 @@ import java.util.ArrayList
 import java.util.Collection
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import java.util.List
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 
 class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {
         private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
@@ -25,50 +27,66 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                 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
+                // The variable
+                val VLSVariable variable = createVLSVariable => [it.name = "A"]
+
+                // 1. Each type (class) is a predicate with a single variable as input
                 for (type : types) {
                         val typePred = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", type.name)
-                                it.terms += createVLSVariable => [it.name = variable.name]
+                                it.constant = support.toIDMultiple("t", type.name)
+                                it.terms += support.duplicate(variable)
                         ]
                         typeTrace.type2Predicate.put(type, typePred)
                 }
 
-                // 2. Map each type definition to fof formula
+                // 2. Map each ENUM type definition to fof formula
                 for (type : types.filter(TypeDefinition)) {
+                        val List<VLSFunction> orElems = newArrayList
+                        for (e : type.elements) {
+                                val enumElemPred = createVLSFunction => [
+                                        it.constant = support.toIDMultiple("e", e.name, type.name)
+                                        it.terms += support.duplicate(variable)
+                                ]
+                                typeTrace.element2Predicate.put(e, enumElemPred)
+                                orElems.add(enumElemPred)
+                        }
 
                         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.variables += support.duplicate(variable)
                                         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.left = createVLSFunction => [
+//                                                      it.constant = type.lookup(typeTrace.type2Predicate).constant
+//                                                      it.terms += createVLSVariable => [it.name = "A"]
+//                                              ]
+                                                it.left = type.lookup(typeTrace.type2Predicate)
+
+                                                it.right = support.unfoldOr(orElems)
+
+                                        // TEMPPPPPPP
+//                                              it.right = support.unfoldOr(type.elements.map [e |
+//                                                      
+//                                                      createVLSEquality => [
+//                                                              it.left = support.duplicate(variable)
 //                                                              it.right = createVLSDoubleQuote => [
-//                                                                      it.value = "\"" + e.name + "\""
+//                                                                      it.value = "\"a" + e.name + "\""
 //                                                              ]
-                                                                it.right = createVLSDoubleQuote => [
-                                                                        it.value = "\"a" + e.name + "\""
-                                                                ]
-                                                        ]
-                                                ])
+//                                                      ]
+//                                              ])
+                                        // END TEMPPPPP
                                         ]
                                 ]
 
                         ]
                         trace.specification.formulas += res
                 }
-                // 2.5. Currently allowing duplicate types. Not problematic cuz strings are by def unique
+                
+                //HIERARCHY HANDLER
+                
+                
                 // 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
@@ -97,19 +115,17 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                 }
 
                 // 5. create fof function that is an or with all the elements in map
-                // Do this only if there are more than 1 type
+                
+                
+                
+                
                 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.left = support.topLevelTypeFunc
                                         it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
                                 ]
                         ]
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
index 5cb0198e..9c9e65b4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
@@ -4,63 +4,64 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory

 

 class Vampire2LogicMapper {

-        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE

-        

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

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

-                

-                if(!monitoredAlloySolution.finishedBeforeTimeout) {

-                        return createInsuficientResourcesResult => [

-                                it.problem = problem

-                                it.representation += models

-                                it.trace = trace

-                                it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

-                        ]

-                } else {

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

-                                return createModelResult => [

-                                        it.problem = problem

-                                        it.representation += models

-                                        it.trace = trace

-                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

-                                ]

-                        } else {

-                                return createInconsistencyResult => [

-                                        it.problem = problem

-                                        it.representation += models

-                                        it.trace = trace

-                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

-                                ]

-                        }

-                }

-        }

-        

-        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {

-                createStatistics => [

-                        it.transformationTime = transformationTime as int

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

-                                val solutionTime = solution.aswers.get(solutionIndex).value

-                                 it.entries+= createIntStatisticEntry => [

-                                        it.name = '''Answer«solutionIndex»Time'''

-                                        it.value = solutionTime.intValue

-                                ]

-                        }

-                        it.entries+= createIntStatisticEntry => [

-                                it.name = "Alloy2KodKodTransformationTime"

-                                it.value = solution.kodkodTime as int

-                        ]

-                        it.entries+= createIntStatisticEntry => [

-                                it.name = "Alloy2KodKodTransformationTime"

-                                it.value = solution.kodkodTime as int

-                        ]

-                        it.entries+= createStringStatisticEntry => [

-                                it.name = "warnings"

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

-                        ]

-                ]

-        }

-        

-        def sum(Iterable<Long> ints) {

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

-        }

 }

+//      val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE

+//      

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

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

+//              

+//              if(!monitoredAlloySolution.finishedBeforeTimeout) {

+//                      return createInsuficientResourcesResult => [

+//                              it.problem = problem

+//                              it.representation += models

+//                              it.trace = trace

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

+//                      ]

+//              } else {

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

+//                              return createModelResult => [

+//                                      it.problem = problem

+//                                      it.representation += models

+//                                      it.trace = trace

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

+//                              ]

+//                      } else {

+//                              return createInconsistencyResult => [

+//                                      it.problem = problem

+//                                      it.representation += models

+//                                      it.trace = trace

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

+//                              ]

+//                      }

+//              }

+//      }

+//      

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

+//              createStatistics => [

+//                      it.transformationTime = transformationTime as int

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

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

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

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

+//                                      it.value = solutionTime.intValue

+//                              ]

+//                      }

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

+//                              it.name = "Alloy2KodKodTransformationTime"

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

+//                      ]

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

+//                              it.name = "Alloy2KodKodTransformationTime"

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

+//                      ]

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

+//                              it.name = "warnings"

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

+//                      ]

+//              ]

+//      }

+//      

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

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

+//      }

+//}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index 462a940b..9a2a1b15 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index d8b8ca61..ce05b92c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
index e1a1ca6e..1846ba2e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
@@ -10,6 +10,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;

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

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

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

 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;

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

   }

   

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

+  private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(

+    new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes());

   

   private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper();

   

@@ -48,7 +50,9 @@ public class VampireSolver extends LogicReasoner {
     String fileURI = null;

     String vampireCode = null;

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

-    if (vampireConfig.writeToFile) {

+    final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || 

+      (vampireConfig.documentationLevel == DocumentationLevel.FULL));

+    if (writeFile) {

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

     }

     long _currentTimeMillis = System.currentTimeMillis();

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
index d392016e..1f6b3d42 100644
--- 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
@@ -4,7 +4,4 @@ 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
index d248b361..379d0683 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index d747e8ab..76dd192f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index 4dc095c0..936ab9ca 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 9a948c6f..e0f442f5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
new file mode 100644
index 00000000..493ff288
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index 4ef4809b..13281767 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index 0f4acafe..1a777880 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.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
index 7d6865bb..e8658e7b 100644
--- 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
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
index 6db26bf7..aec1688a 100644
--- 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
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index 8c96afa7..e77b9866 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index 2427721d..100a52b8 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
index d2c93ab4..231c1995 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
index 28c5d0f7..b67a307c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
index 3d29fb07..ec8107e8 100644
--- 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
@@ -37,3 +37,4 @@
 /.VampireSolverException.java._trace
 /.VampireSolutionModel.java._trace
 /.VampireCallerWithTimeout.java._trace
+/.Logic2VampireLanguageMapper_ScopeMapper.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
index a1d80e58..89c9637e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -4,6 +4,7 @@ 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_ScopeMapper;

 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;

@@ -84,6 +85,9 @@ public class Logic2VampireLanguageMapper {
   private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this);

   

   @Accessors(AccessorType.PUBLIC_GETTER)

+  private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this);

+  

+  @Accessors(AccessorType.PUBLIC_GETTER)

   private final Logic2VampireLanguageMapper_TypeMapper typeMapper;

   

   public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) {

@@ -112,6 +116,7 @@ public class Logic2VampireLanguageMapper {
     if (_not) {

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

     }

+    this.scopeMapper.transformScope(config, trace);

     trace.constantDefinitions = this.collectConstantDefinitions(problem);

     trace.relationDefinitions = this.collectRelationDefinitions(problem);

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

@@ -316,13 +321,13 @@ public class Logic2VampireLanguageMapper {
   

   /**

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

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

@@ -348,7 +353,7 @@ public class Logic2VampireLanguageMapper {
    * //                                                         rightOperand = target

    * //                                                 ]

    * //                                         }

-   * }

+   *    }

    * }

    */

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

@@ -436,6 +441,11 @@ public class Logic2VampireLanguageMapper {
   }

   

   @Pure

+  public Logic2VampireLanguageMapper_ScopeMapper getScopeMapper() {

+    return this.scopeMapper;

+  }

+  

+  @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/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
new file mode 100644
index 00000000..86d8b648
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -0,0 +1,96 @@
+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.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.VLSUniversalQuantifier;

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

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

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

+import java.util.List;

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

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

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

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

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_ScopeMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  private final Logic2VampireLanguageMapper base;

+  

+  public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) {

+    this.base = base;

+  }

+  

+  public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

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

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

+      it.setName("A");

+    };

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

+    final List<VLSConstant> instances = CollectionLiterals.<VLSConstant>newArrayList();

+    for (int i = 0; (i < config.typeScopes.minNewElements); i++) {

+      {

+        final int num = (i + 1);

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

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

+          it.setName(("o" + Integer.valueOf(num)));

+        };

+        final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1);

+        instances.add(cst);

+      }

+    }

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

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

+      it.setName("typeScope");

+      it.setFofRole("axiom");

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

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

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

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

+        _variables.add(_duplicate);

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

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

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

+          final Function1<VLSConstant, VLSEquality> _function_4 = (VLSConstant i) -> {

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

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

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

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

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

+              };

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

+              it_3.setLeft(_doubleArrow);

+              it_3.setRight(i);

+            };

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

+          };

+          it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4)));

+        };

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

+        it_1.setOperand(_doubleArrow);

+      };

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

+      it.setFofFormula(_doubleArrow);

+    };

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

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

+    _formulas.add(cstDec);

+  }

+  

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

+    _transformScope(config, trace);

+    return;

+  }

+}

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
index e1be7df5..b111732f 100644
--- 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
@@ -50,6 +50,29 @@ public class Logic2VampireLanguageMapper_Support {
     return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_");

   }

   

+  protected VLSVariable duplicate(final VLSVariable vrbl) {

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

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

+      it.setName(vrbl.getName());

+    };

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

+  }

+  

+  protected VLSFunction topLevelTypeFunc() {

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

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

+      it.setConstant("object");

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

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

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

+        it_1.setName("A");

+      };

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

+      _terms.add(_doubleArrow);

+    };

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

+  }

+  

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

     int _size = operands.size();

     boolean _equals = (_size == 1);

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
index d674ac71..f7c6cb70 100644
--- 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
@@ -1,7 +1,6 @@
 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;

@@ -13,7 +12,7 @@ import java.util.Map;
 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<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>();

   

   public final Map<Type, VLSTerm> type2PossibleNot = 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
index 0f5e4e7a..71e98871 100644
--- 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
@@ -7,7 +7,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
 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;

@@ -27,10 +26,10 @@ import java.util.ArrayList;
 import java.util.Collection;

 import java.util.List;

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

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

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

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

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

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

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

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

 

@@ -58,14 +57,10 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
       {

         VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

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

+          it.setConstant(this.support.toIDMultiple("t", 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);

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

+          _terms.add(_duplicate);

         };

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

         typeTrace.type2Predicate.put(type, typePred);

@@ -74,6 +69,22 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
     Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);

     for (final TypeDefinition type_1 : _filter) {

       {

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

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

+        for (final DefinedElement e : _elements) {

+          {

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

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

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

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

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

+              _terms.add(_duplicate);

+            };

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

+            typeTrace.element2Predicate.put(e, enumElemPred);

+            orElems.add(enumElemPred);

+          }

+        }

         VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

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

@@ -81,53 +92,15 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
           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);

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

+            _variables.add(_duplicate);

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

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

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

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

             };

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

-            it_1.setOperand(_doubleArrow_1);

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

+            it_1.setOperand(_doubleArrow);

           };

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

           it.setFofFormula(_doubleArrow);

@@ -201,19 +174,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
         _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);

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

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

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

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

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
index f4380894..f4b5a1d2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
@@ -1,59 +1,5 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

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

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

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

-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics;

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

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

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

-

 @SuppressWarnings("all")

 public class Vampire2LogicMapper {

-  @Extension

-  private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;

-  

-  public LogicResult transformOutput(final LogicProblem problem, final int requiredNumberOfSolution, final VampireSolutionModel vampireSolution, final Logic2VampireLanguageMapperTrace trace, final long transformationTime) {

-    throw new Error("Unresolved compilation problems:"

-      + "\nThe method or field aswers is undefined for the type VampireSolutionModel"

-      + "\nThe method or field key is undefined for the type Object"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution"

-      + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution"

-      + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution"

-      + "\nmap cannot be resolved"

-      + "\ntoList cannot be resolved"

-      + "\nfinishedBeforeTimeout cannot be resolved"

-      + "\n! cannot be resolved"

-      + "\nlast cannot be resolved"

-      + "\nsatisfiable cannot be resolved"

-      + "\n|| cannot be resolved");

-  }

-  

-  public Statistics transformStatistics(final /* MonitoredAlloySolution */Object solution, final long transformationTime) {

-    throw new Error("Unresolved compilation problems:"

-      + "\nCannot cast from Object to int"

-      + "\nCannot cast from Object to int"

-      + "\naswers cannot be resolved"

-      + "\nsize cannot be resolved"

-      + "\naswers cannot be resolved"

-      + "\nget cannot be resolved"

-      + "\nvalue cannot be resolved"

-      + "\nintValue cannot be resolved"

-      + "\nkodkodTime cannot be resolved"

-      + "\nkodkodTime cannot be resolved"

-      + "\nwarnings cannot be resolved");

-  }

-  

-  public Long sum(final Iterable<Long> ints) {

-    final Function2<Long, Long, Long> _function = (Long p1, Long p2) -> {

-      return Long.valueOf(((p1).longValue() + (p2).longValue()));

-    };

-    return IterableExtensions.<Long>reduce(ints, _function);

-  }

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
index c665b9a6..3c43c4ea 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
@@ -10,8 +10,7 @@ public class VampireSolutionModel {
   @Override

   @Pure

   public int hashCode() {

-    int result = 1;

-    return result;

+    return 1;

   }

   

   @Override