19 files changed, 129 insertions, 22 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 4c2f1952..1fda24d9 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
@@ -24,7 +24,8 @@ enum BackendSolver {
         IPROVER,
         PARADOX,
         VAMPIRE,
-        Z3
+        Z3,
+        LOCVAMP
         //add needed things
 }
 
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 9ec08163..042caa86 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
@@ -20,6 +20,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl
 
 class VampireSolver extends LogicReasoner {
 
@@ -128,17 +129,17 @@ class VampireSolver extends LogicReasoner {
                                                         it.name = "satOut"
                                                         it.value = satOut
                                                 ]
-                                                it.entries += createRealStatisticEntry => [
+                                                it.entries += createStringStatisticEntry => [
                                                         it.name = "satTime"
-                                                        it.value = Double.parseDouble(satTime)
+                                                        it.value = satTime
                                                 ]
                                                 it.entries += createStringStatisticEntry => [
                                                         it.name = "modOut"
                                                         it.value = modOut
                                                 ]
-                                                it.entries += createRealStatisticEntry => [
+                                                it.entries += createStringStatisticEntry => [
                                                         it.name = "modTime"
-                                                        it.value = Double.parseDouble(modTime)
+                                                        it.value = modTime
                                                 ]
 
                                         ]
@@ -148,6 +149,7 @@ class VampireSolver extends LogicReasoner {
                         } else {
 
                                 // Start: Solving .tptp problem
+                                println()
                                 val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
                                 // Finish: Solving .tptp problem
                                 // Start: Vampire -> Logic mapping
@@ -159,7 +161,44 @@ class VampireSolver extends LogicReasoner {
                                 val backTransformationTime = System.currentTimeMillis - backTransformationStart
                                 // Finish: Vampire -> Logic Mapping
 //              print(vampSol.generatedModel.tfformulas.size)
-                                return logicResult // currently only a ModelResult
+
+//                              return logicResult // currently only a ModelResult
+
+                                var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl]
+//                              
+                                var modOut = "no"
+                                if(model.length >0){
+                                        modOut = "FiniteModel"
+                                }
+                                
+                                val realModOut=modOut
+ 
+                                
+                                return createModelResult => [
+                                        it.problem = null
+                                        it.representation += createVampireModel => []
+                                        it.trace = trace
+                                        it.statistics = createStatistics => [
+                                                it.transformationTime = transformationTime as int
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "satOut"
+                                                        it.value = "-"
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "satTime"
+                                                        it.value = "-"
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "modOut"
+                                                        it.value = realModOut
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "modTime"
+                                                        it.value = (vampSol.solverTime/1000.0).toString
+                                                ]
+
+                                        ]
+                                ]
                         }
                 }
                 return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution,
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 6d301442..c277759a 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
@@ -54,7 +54,7 @@ class VampireHandler {
                 val TEMPNAME = "TEMP.tptp"

 //              val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements +

 //                      "_" + configuration.iteration + ".tptp"

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

+                val SOLNNAME = "solution" + "_" + configuration.typeScopes.minNewElements + "_" + configuration.iteration +

                         ".tptp"

                 val PATH = "C:/cygwin64/bin"

 

@@ -70,7 +70,7 @@ class VampireHandler {
                 var long startTime = -1 as long

                 var long solverTime = -1 as long

                 var Process p = null

-                if (configuration.solver == BackendSolver::VAMPIRE) {

+                if (configuration.solver == BackendSolver::LOCVAMP) {

 

                         var OPTION = " --mode casc_sat "

                         if (configuration.runtimeLimit != -1) {

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 b26c1ded..5c40d767 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 7fedcc30..2d4d0741 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 3e3bd688..4f554956 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,9 +10,11 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolut
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation;

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

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

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

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

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl;

 import com.google.common.base.Objects;

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

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

@@ -24,7 +26,6 @@ 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.ModelResult;

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

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry;

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

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry;

@@ -34,10 +35,12 @@ import java.util.List;
 import org.eclipse.emf.common.util.EList;

 import org.eclipse.xtend2.lib.StringConcatenation;

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

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

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

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

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

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

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

@@ -149,28 +152,28 @@ public class VampireSolver extends LogicReasoner {
               StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3);

               _entries.add(_doubleArrow_1);

               EList<StatisticEntry> _entries_1 = it_1.getEntries();

-              RealStatisticEntry _createRealStatisticEntry = this.resultFactory.createRealStatisticEntry();

-              final Procedure1<RealStatisticEntry> _function_4 = (RealStatisticEntry it_2) -> {

+              StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry();

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

                 it_2.setName("satTime");

-                it_2.setValue(Double.parseDouble(satTime));

+                it_2.setValue(satTime);

               };

-              RealStatisticEntry _doubleArrow_2 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry, _function_4);

+              StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_4);

               _entries_1.add(_doubleArrow_2);

               EList<StatisticEntry> _entries_2 = it_1.getEntries();

-              StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry();

+              StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry();

               final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> {

                 it_2.setName("modOut");

                 it_2.setValue(modOut);

               };

-              StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5);

+              StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_5);

               _entries_2.add(_doubleArrow_3);

               EList<StatisticEntry> _entries_3 = it_1.getEntries();

-              RealStatisticEntry _createRealStatisticEntry_1 = this.resultFactory.createRealStatisticEntry();

-              final Procedure1<RealStatisticEntry> _function_6 = (RealStatisticEntry it_2) -> {

+              StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry();

+              final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> {

                 it_2.setName("modTime");

-                it_2.setValue(Double.parseDouble(modTime));

+                it_2.setValue(modTime);

               };

-              RealStatisticEntry _doubleArrow_4 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry_1, _function_6);

+              StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_6);

               _entries_3.add(_doubleArrow_4);

             };

             Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2);

@@ -178,13 +181,77 @@ public class VampireSolver extends LogicReasoner {
           };

           return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function);

         } else {

+          InputOutput.println();

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

           final long backTransformationStart = System.currentTimeMillis();

           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;

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

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

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

+          };

+          Iterable<VLSConfirmations> model = IterableExtensions.<VLSConfirmations>filter(vampSol.getGeneratedModel().getConfirmations(), _function_1);

+          String modOut_1 = "no";

+          final Iterable<VLSConfirmations> _converted_model = (Iterable<VLSConfirmations>)model;

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

+          boolean _greaterThan = (_length > 0);

+          if (_greaterThan) {

+            modOut_1 = "FiniteModel";

+          }

+          final String realModOut = modOut_1;

+          ModelResult _createModelResult_1 = this.resultFactory.createModelResult();

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

+            it.setProblem(null);

+            EList<Object> _representation = it.getRepresentation();

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

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

+            };

+            VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_3);

+            _representation.add(_doubleArrow);

+            it.setTrace(it.getTrace());

+            Statistics _createStatistics = this.resultFactory.createStatistics();

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

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

+              EList<StatisticEntry> _entries = it_1.getEntries();

+              StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry();

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

+                it_2.setName("satOut");

+                it_2.setValue("-");

+              };

+              StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_5);

+              _entries.add(_doubleArrow_1);

+              EList<StatisticEntry> _entries_1 = it_1.getEntries();

+              StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry();

+              final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> {

+                it_2.setName("satTime");

+                it_2.setValue("-");

+              };

+              StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_6);

+              _entries_1.add(_doubleArrow_2);

+              EList<StatisticEntry> _entries_2 = it_1.getEntries();

+              StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry();

+              final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> {

+                it_2.setName("modOut");

+                it_2.setValue(realModOut);

+              };

+              StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_7);

+              _entries_2.add(_doubleArrow_3);

+              EList<StatisticEntry> _entries_3 = it_1.getEntries();

+              StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry();

+              final Procedure1<StringStatisticEntry> _function_8 = (StringStatisticEntry it_2) -> {

+                it_2.setName("modTime");

+                long _solverTime = vampSol.getSolverTime();

+                it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString());

+              };

+              StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_8);

+              _entries_3.add(_doubleArrow_4);

+            };

+            Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_4);

+            it.setStatistics(_doubleArrow_1);

+          };

+          return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_2);

         }

       }

       MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null);

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 8b7f031e..887a3a31 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 1b6e8f80..b4943b57 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 f523f1af..e3b29572 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 30ba1843..50ff7011 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 174c7362..337edcba 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 affa3754..c32ba83f 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 9caad4ea..75e60f21 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 5be67889..d69b41ea 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 192c9d1a..6b91ff7b 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 0495ab53..f23063ea 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 c438f1e5..0de59fdb 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 5fb9b455..6176aca5 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/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
index e32530cb..e9073d82 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
@@ -30,7 +30,7 @@ public class VampireHandler {
       final String CVC4LOC = (CVC4DIR + CVC4NAME);

       final String CMD = "cmd /c ";

       final String TEMPNAME = "TEMP.tptp";

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

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

         ".tptp");

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

       final URI wsURI = workspace.getWorkspaceURI();

@@ -41,7 +41,7 @@ public class VampireHandler {
       long startTime = (-((long) 1));

       long solverTime = (-((long) 1));

       Process p = null;

-      boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMPIRE);

+      boolean _equals = Objects.equal(configuration.solver, BackendSolver.LOCVAMP);

       if (_equals) {

         String OPTION = " --mode casc_sat ";

         if ((configuration.runtimeLimit != (-1))) {