23 files changed, 141 insertions, 62 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
index 98967181..fc8d3e99 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
@@ -6,6 +6,7 @@ class VampireSolverConfiguration extends LogicSolverConfiguration {
         
         public var int contCycleLevel = 0
         public var boolean uniquenessDuplicates = false
+        public var int iteration = -1
         //choose needed backend solver
 //      public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
 }
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 3b5cec0a..3281a196 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
@@ -46,6 +46,8 @@ class VampireSolver extends LogicReasoner {
                 val transformationStart = System.currentTimeMillis
                 // TODO
                 val result = forwardMapper.transformProblem(problem, vampireConfig)
+                val transformationTime = System.currentTimeMillis - transformationStart
+                
                 val vampireProblem = result.output
                 val forwardTrace = result.trace
 
@@ -71,19 +73,17 @@ class VampireSolver extends LogicReasoner {
                 
 
                 // Result as String
-                val transformationTime = System.currentTimeMillis - transformationStart
+                
                 // Finish: Logic -> Vampire mapping
                 
                 // Start: Solving .tptp problem
-                val solverStart = System.currentTimeMillis
                 val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
-                val solvingTime = System.currentTimeMillis - solverStart
                 // Finish: Solving .tptp problem
                 
                 // Start: Vampire -> Logic mapping
                 val backTransformationStart = System.currentTimeMillis
                 // Backwards Mapper
-                val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,solvingTime)
+                val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime)
 
                 val backTransformationTime = System.currentTimeMillis - backTransformationStart
                 // Finish: Vampire -> Logic Mapping
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 b617912d..60309f2d 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
@@ -79,14 +79,15 @@ class Logic2VampireLanguageMapper {
                 if (!problem.types.isEmpty) {
                         typeMapper.transformTypes(problem.types, problem.elements, this, trace)
                 }
-                
+
                 // RELATION MAPPER
                 trace.relationDefinitions = problem.collectRelationDefinitions
 //              println(problem.relations.filter[class == RelationDefinitionImpl])
+                toTrace(problem.relations.filter[class == RelationDefinitionImpl], trace)
                 problem.relations.forEach[this.relationMapper.transformRelation(it, trace, new Logic2VampireLanguageMapper)]
-                
+
                 // CONTAINMENT MAPPER
-                containmentMapper.transformContainment(config,problem.containmentHierarchies, trace)
+                containmentMapper.transformContainment(config, problem.containmentHierarchies, trace)
 
                 // SCOPE MAPPER
                 scopeMapper.transformScope(problem.types, config, trace)
@@ -107,6 +108,39 @@ class Logic2VampireLanguageMapper {
                 return new TracedOutput(specification, trace)
         }
 
+        def toTrace(Iterable<Relation> relations, Logic2VampireLanguageMapperTrace trace) {
+                val List<VLSVariable> vars = newArrayList
+                for (rel : relations) {
+                        //decide name
+                        val nameArray = rel.name.split(" ")
+                        var relNameVar = ""
+                        if (nameArray.length == 3) {
+                                relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
+                        } else {
+                                relNameVar = rel.name
+                        }
+                        val relName = relNameVar
+                        
+                        val relDef = rel as RelationDefinition
+                        for (i : 0 ..< rel.parameters.length) {
+
+                                val v = createVLSVariable => [
+                                        it.name = support.toIDMultiple("V", i.toString)
+                                ]
+                                vars.add(v)
+                        }
+
+                        val relFunc = createVLSFunction => [
+                                it.constant = support.toIDMultiple("r", relName)
+                                for (v : vars) {
+                                        it.terms += support.duplicate(v)
+                                }
+                        ]
+                        trace.relDef2Predicate.put(relDef, relFunc)
+                        trace.predicate2RelDef.put(relFunc, relDef)
+                }
+        }
+
         // End of transformProblem
         // ////////////
         // Type References
@@ -169,7 +203,6 @@ class Logic2VampireLanguageMapper {
 //              Map<Variable, VLSVariable> variables) {
 //              createVLSReal => [it.value = literal.value.toString()]
 //      }
-
         def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
                 createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)]
@@ -265,10 +298,10 @@ class Logic2VampireLanguageMapper {
         def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,
                 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
-                        val name = referred.lookup(trace.definedElement2String)
-                        return createVLSConstant => [
-                                it.name = name
-                        ]
+                val name = referred.lookup(trace.definedElement2String)
+                return createVLSConstant => [
+                        it.name = name
+                ]
 //              typeMapper.transformReference(referred, trace)
         }
 
@@ -390,12 +423,11 @@ class Logic2VampireLanguageMapper {
 //              }
                 return createVLSFunction => [
                         if (relation.class == RelationDeclarationImpl) {
-                                                        it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
-                        }
-                        else {
+                                it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
+                        } else {
                                 it.constant = (relation as RelationDefinition).lookup(trace.relDef2Predicate).constant
                         }
-                        
+
                         it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
                 ]
         }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index 181c59ca..efedf6dc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -23,7 +23,8 @@ class Logic2VampireLanguageMapper_RelationMapper {
                 this.base = base
         }
 
-        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) {
+        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace,
+                Logic2VampireLanguageMapper mapper) {
 
                 // 1. store all variables in support wrt their name
                 // 1.1 if variable has type, creating list of type declarations
@@ -42,19 +43,18 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
                 }
 
-                //deciding name of relation
+                // deciding name of relation
                 val nameArray = r.name.split(" ")
                 var relNameVar = ""
                 if (nameArray.length == 3) {
                         relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
-                }
-                else {
+                } else {
                         relNameVar = r.name
                 }
                 val relName = relNameVar
-                
-                val comply = createVLSFofFormula=> [
-                        
+
+                val comply = createVLSFofFormula => [
+
                         it.name = support.toIDMultiple("compliance", relName)
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
@@ -79,10 +79,10 @@ class Logic2VampireLanguageMapper_RelationMapper {
                 trace.specification.formulas += comply
         }
 
-        def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) {
-                
-//              println("XXXXXXXXXXXXXXXXX")
+        def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace,
+                Logic2VampireLanguageMapper mapper) {
 
+//              println("XXXXXXXXXXXXXXXXX")
 // 1. store all variables in support wrt their name
                 // 1.1 if variable has type, creating list of type declarations
                 val Map<Variable, VLSVariable> relVar2VLS = new HashMap
@@ -102,34 +102,30 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
                 }
 
-                //deciding name of relation
+                // deciding name of relation
                 val nameArray = r.name.split(" ")
                 var relNameVar = ""
                 if (nameArray.length == 3) {
                         relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
-                }
-                else {
+                } else {
                         relNameVar = r.name
                 }
                 val relName = relNameVar
-                
-                //define logic for pattern
+
+                // define logic for pattern
 //              val map = new HashMap
 //              map.put(r.variables.get(0), createVLSVariable)
                 val definition = mapper.transformTerm(r.value, trace, relVar2VLS)
-                
-                
-                
-                
-                //get entire contents of and
+
+                // get entire contents of and
                 val compliance = support.unfoldAnd(relVar2TypeDecComply)
-                val compDefn = createVLSAnd=> [
+                val compDefn = createVLSAnd => [
                         it.left = compliance
                         it.right = definition
                 ]
-                
-                val relDef = createVLSFofFormula=> [
-                        
+
+                val relDef = createVLSFofFormula => [
+
                         it.name = support.toID(relName)
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
@@ -143,14 +139,13 @@ class Logic2VampireLanguageMapper_RelationMapper {
                                                         it.terms += support.duplicate(v)
                                                 }
                                         ]
-                                        trace.relDef2Predicate.put(r, rel)
-                                        trace.predicate2RelDef.put(rel, r)
+//                                      trace.relDef2Predicate.put(r, rel)
+//                                      trace.predicate2RelDef.put(rel, r)
                                         it.left = support.duplicate(rel)
                                         it.right = compDefn
                                 ]
                         ]
                 ]
-
                 trace.specification.formulas += relDef
 
         }
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 489bf423..e136d1c6 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
@@ -8,7 +8,7 @@ class Vampire2LogicMapper {
 

 //      

         public def transformOutput(LogicProblem problem, int requiredNumberOfSolution,

-                MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace,

+                MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace, 

                 long transformationTime) {

 

                 // ModelRsult implements LogicResult

@@ -22,7 +22,8 @@ class Vampire2LogicMapper {
 

         def transformStatistics(MonitoredVampireSolution solution, long transformationTime) {

                 return createStatistics => [

-                        it.transformationTime = solution.solverTime as int

+                        it.solverTime = solution.solverTime as int

+                        it.transformationTime = transformationTime as int

                 ]

 //              createStatistics => [

 //                      it.transformationTime = transformationTime as int

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
index 74532ee5..c5cfb1c7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
@@ -44,7 +44,7 @@ class VampireHandler {
                 val VAMPNAME = "vampire.exe"

                 val TEMPNAME = "TEMP.tptp"

                 val OPTION = " --mode casc_sat -t 300 "

-                val SOLNNAME = "_solution" + configuration.typeScopes.maxNewElements + ".tptp"

+                val SOLNNAME = "solution" + configuration.typeScopes.maxNewElements +"_" + configuration.iteration + ".tptp"

                 val PATH = "C:/cygwin64/bin"

 

                 val wsURI = workspace.workspaceURI

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 600187ca..2c203d6e 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 9517185f..f2461efc 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 1241dcb2..c3e185f5 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
@@ -62,6 +62,8 @@ public class VampireSolver extends LogicReasoner {
     final VampireSolverConfiguration vampireConfig = this.asConfig(config);

     final long transformationStart = System.currentTimeMillis();

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

+    long _currentTimeMillis = System.currentTimeMillis();

+    final long transformationTime = (_currentTimeMillis - transformationStart);

     final VampireModel vampireProblem = result.getOutput();

     final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();

     String fileURI = null;

@@ -72,16 +74,11 @@ public class VampireSolver extends LogicReasoner {
     if (writeFile) {

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

     }

-    long _currentTimeMillis = System.currentTimeMillis();

-    final long transformationTime = (_currentTimeMillis - transformationStart);

-    final long solverStart = System.currentTimeMillis();

     final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);

-    long _currentTimeMillis_1 = System.currentTimeMillis();

-    final long solvingTime = (_currentTimeMillis_1 - solverStart);

     final long backTransformationStart = System.currentTimeMillis();

-    final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, solvingTime);

-    long _currentTimeMillis_2 = System.currentTimeMillis();

-    final long backTransformationTime = (_currentTimeMillis_2 - backTransformationStart);

+    final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime);

+    long _currentTimeMillis_1 = System.currentTimeMillis();

+    final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart);

     return logicResult;

   }

   

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 ac55ebd7..5086d15a 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
@@ -7,4 +7,6 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration {
   public int contCycleLevel = 0;

   

   public boolean uniquenessDuplicates = false;

+  

+  public int iteration = (-1);

 }

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 3ebc907b..f537b830 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/.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 c9ae6c62..14a639ad 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_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index ec8fae35..ba5dbd89 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.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 5e770b94..f5e4ca8c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 1d3cd01c..6c06a366 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index 72067608..1ee73cd6 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 a9228720..edda9f05 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index 3697ed87..8edf2fe9 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 c489bf07..18c788c6 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/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index c8961c6e..dc5ec788 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
@@ -54,6 +54,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;

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

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl;

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

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

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

 import java.util.Arrays;

@@ -65,6 +66,9 @@ import java.util.function.Consumer;
 import org.eclipse.emf.common.util.EList;

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

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

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

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

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

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

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

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

@@ -118,18 +122,23 @@ public class Logic2VampireLanguageMapper {
       this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);

     }

     trace.relationDefinitions = this.collectRelationDefinitions(problem);

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

+    final Function1<Relation, Boolean> _function_3 = (Relation it) -> {

+      Class<? extends Relation> _class = it.getClass();

+      return Boolean.valueOf(Objects.equal(_class, RelationDefinitionImpl.class));

+    };

+    this.toTrace(IterableExtensions.<Relation>filter(problem.getRelations(), _function_3), trace);

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

       Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper();

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

     };

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

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

     this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace);

     this.scopeMapper.transformScope(problem.getTypes(), config, trace);

     trace.constantDefinitions = this.collectConstantDefinitions(problem);

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

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

       this.constantMapper.transformConstantDefinitionSpecification(it, trace);

     };

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

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

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

     for (final Assertion assertion : _assertions) {

       this.transformAssertion(assertion, trace);

@@ -137,6 +146,49 @@ public class Logic2VampireLanguageMapper {
     return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace);

   }

   

+  public void toTrace(final Iterable<Relation> relations, final Logic2VampireLanguageMapperTrace trace) {

+    final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList();

+    for (final Relation rel : relations) {

+      {

+        final String[] nameArray = rel.getName().split(" ");

+        String relNameVar = "";

+        int _length = nameArray.length;

+        boolean _equals = (_length == 3);

+        if (_equals) {

+          relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);

+        } else {

+          relNameVar = rel.getName();

+        }

+        final String relName = relNameVar;

+        final RelationDefinition relDef = ((RelationDefinition) rel);

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

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

+        for (final Integer i : _doubleDotLessThan) {

+          {

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

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

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

+            };

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

+            vars.add(v);

+          }

+        }

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

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

+          it.setConstant(this.support.toIDMultiple("r", relName));

+          for (final VLSVariable v : vars) {

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

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

+            _terms.add(_duplicate);

+          }

+        };

+        final VLSFunction relFunc = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

+        trace.relDef2Predicate.put(relDef, relFunc);

+        trace.predicate2RelDef.put(relFunc, relDef);

+      }

+    }

+  }

+  

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

     return null;

   }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
index c175c72a..4c14e93e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -176,8 +176,6 @@ public class Logic2VampireLanguageMapper_RelationMapper {
             }

           };

           final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_4);

-          trace.relDef2Predicate.put(r, rel);

-          trace.predicate2RelDef.put(rel, r);

           it_2.setLeft(this.support.duplicate(rel));

           it_2.setRight(compDefn);

         };

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 4fbf7291..9fb23c71 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
@@ -34,7 +34,8 @@ public class Vampire2LogicMapper {
     Statistics _createStatistics = this.resultFactory.createStatistics();

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

       long _solverTime = solution.getSolverTime();

-      it.setTransformationTime(((int) _solverTime));

+      it.setSolverTime(((int) _solverTime));

+      it.setTransformationTime(((int) transformationTime));

     };

     return ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function);

   }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
index 0c8b0013..a1f19410 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
@@ -25,7 +25,7 @@ public class VampireHandler {
       final String VAMPNAME = "vampire.exe";

       final String TEMPNAME = "TEMP.tptp";

       final String OPTION = " --mode casc_sat -t 300 ";

-      final String SOLNNAME = (("_solution" + Integer.valueOf(configuration.typeScopes.maxNewElements)) + ".tptp");

+      final String SOLNNAME = (((("solution" + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + ".tptp");

       final String PATH = "C:/cygwin64/bin";

       final URI wsURI = workspace.getWorkspaceURI();

       final String tempLoc = (wsURI + TEMPNAME);