VAMPIRE: fix bug in transformation, further implement measurement code

17 files changed, 66 insertions, 16 deletions

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