VAMPIRE: post-submission push

20 files changed, 63 insertions, 72 deletions

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 042caa86..59084843 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
@@ -153,21 +153,21 @@ class VampireSolver extends LogicReasoner {
                                 val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
                                 // Finish: Solving .tptp problem
                                 // Start: Vampire -> Logic mapping
-                                val backTransformationStart = System.currentTimeMillis
-                                // Backwards Mapper
-                                val logicResult = backwardMapper.transformOutput(problem,
-                                        vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime)
-
-                                val backTransformationTime = System.currentTimeMillis - backTransformationStart
+//                              val backTransformationStart = System.currentTimeMillis
+//                              // Backwards Mapper
+//                              val logicResult = backwardMapper.transformOutput(problem,
+//                                      vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime)
+//
+//                              val backTransformationTime = System.currentTimeMillis - backTransformationStart
                                 // Finish: Vampire -> Logic Mapping
 //              print(vampSol.generatedModel.tfformulas.size)
 
 //                              return logicResult // currently only a ModelResult
 
-                                var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl]
+//                              var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl]
 //                              
                                 var modOut = "no"
-                                if(model.length >0){
+                                if(vampSol.finiteModelGenerated){
                                         modOut = "FiniteModel"
                                 }
                                 
@@ -201,8 +201,8 @@ class VampireSolver extends LogicReasoner {
                                 ]
                         }
                 }
-                return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution,
-                        new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime)
+//              return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution,
+//                      new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime)
         }
 
         def asConfig(LogicSolverConfiguration configuration) {
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
index a9516cc4..96c2da48 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -56,11 +56,11 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

                 val localInstances = newArrayList

 

-                val consistant = GLOBAL_MAX > GLOBAL_MIN

+                val consistant = GLOBAL_MAX >= GLOBAL_MIN

 

                 // Handling Minimum_General

                 if (GLOBAL_MIN != ABSOLUTE_MIN) {

-                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant)//may make not consistent here 

+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant)//may make not consistent here 

                         if (consistant) {

                                 for (i : trace.uniqueInstances) {

                                         localInstances.add(support.duplicate(i))

@@ -73,7 +73,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

                 // Handling Maximum_General

                 if (GLOBAL_MAX != ABSOLUTE_MAX) {

-                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, !consistant)

+                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant)

                         if (consistant) {

                                 makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)

                         } else {

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 c277759a..d7dd53f0 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
@@ -11,6 +11,7 @@ import org.eclipse.xtend.lib.annotations.Data
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver

+import java.io.FileReader

 

 class VampireSolverException extends Exception {

         new(String s) {

@@ -33,6 +34,7 @@ class VampireSolverException extends Exception {
 //      val List<Pair<A4Solution, Long>> aswers

         val VampireModel generatedModel

 //      val boolean finishedBeforeTimeout

+        val boolean finiteModelGenerated

 }

 

 class VampireHandler {

@@ -92,28 +94,38 @@ class VampireHandler {
                         p.waitFor

                         solverTime = System.currentTimeMillis - startTime

                 }

+                

 

                 // 2.1 determine time left

                 // 2.2 store output into local variable

-                val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream()));

+                val BufferedReader reader = new BufferedReader(new FileReader(solnLoc));

                 val List<String> output = newArrayList

 

                 var line = "";

                 while ((line = reader.readLine()) != null) {

-                        output.add(line + "\n");

+                        if (line == "Finite Model Found!") {

+                                return new MonitoredVampireSolution(solverTime, null, true)

+                        }

                 }

+                return new MonitoredVampireSolution(solverTime, null, false)

 

-//      println(output.toString())

-                // 4. delete temp file

-                workspace.getFile(TEMPNAME).delete

+        /*              var line = "";

+         *              while ((line = reader.readLine()) != null) {

+         *                      output.add(line + "\n");

+         *              }

 

-                // 5. determine and return whether or not finite model was found

-                // 6. save solution as a .tptp model

-                val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents

+         * //           println(output.toString())

+         *              // 4. delete temp file

+         *              workspace.getFile(TEMPNAME).delete

 

-//              println((root.get(0) as VampireModel ).comments)

-                return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel)

+         *              // 5. determine and return whether or not finite model was found

+         *              // 6. save solution as a .tptp model

+         *              val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents

 

+         * //           println((root.get(0) as VampireModel ).comments)

+         *              return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel)

+         * 

+         */

         /*

          * //Prepare

          * val warnings = new LinkedList<String>

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 5c40d767..88e234fc 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 2d4d0741..8f9c0397 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 4f554956..eb6007ec 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,11 +10,9 @@ 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;

@@ -35,12 +33,10 @@ 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;

@@ -183,79 +179,66 @@ public class VampireSolver extends LogicReasoner {
         } 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);

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

+          boolean _isFiniteModelGenerated = vampSol.isFiniteModelGenerated();

+          if (_isFiniteModelGenerated) {

             modOut_1 = "FiniteModel";

           }

           final String realModOut = modOut_1;

           ModelResult _createModelResult_1 = this.resultFactory.createModelResult();

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

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

             it.setProblem(null);

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

             VampireModel _createVampireModel = this.factory.createVampireModel();

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

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

             };

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

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

             _representation.add(_doubleArrow);

             it.setTrace(it.getTrace());

             Statistics _createStatistics = this.resultFactory.createStatistics();

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

+            final Procedure1<Statistics> _function_3 = (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) -> {

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

                 it_2.setName("satOut");

                 it_2.setValue("-");

               };

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

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

               _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) -> {

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

                 it_2.setName("satTime");

                 it_2.setValue("-");

               };

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

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

               _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) -> {

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

                 it_2.setName("modOut");

                 it_2.setValue(realModOut);

               };

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

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

               _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) -> {

+              final Procedure1<StringStatisticEntry> _function_7 = (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);

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

               _entries_3.add(_doubleArrow_4);

             };

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

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

             it.setStatistics(_doubleArrow_1);

           };

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

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

         }

       }

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

-      return this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime);

+      return null;

     } catch (Throwable _e) {

       throw Exceptions.sneakyThrow(_e);

     }

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 887a3a31..07b7d4c3 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 b4943b57..04a3303b 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 e3b29572..dbd48bbb 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 50ff7011..4f4710d4 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 337edcba..19ff819d 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 c32ba83f..2774bb57 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 75e60f21..9b636247 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 d69b41ea..739f0cd5 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 6b91ff7b..96506230 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 f23063ea..b7d9060d 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 0de59fdb..d8bc6614 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 6176aca5..512e8a06 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/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index c09d929e..d6c90484 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -59,9 +59,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM);

     final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM);

     final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();

-    final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN);

+    final boolean consistant = (GLOBAL_MAX >= GLOBAL_MIN);

     if ((GLOBAL_MIN != ABSOLUTE_MIN)) {

-      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant);

+      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant));

       if (consistant) {

         for (final VLSConstant i : trace.uniqueInstances) {

           localInstances.add(this.support.duplicate(i));

@@ -72,7 +72,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       }

     }

     if ((GLOBAL_MAX != ABSOLUTE_MAX)) {

-      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, (!consistant));

+      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant);

       if (consistant) {

         this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);

       } else {

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 e9073d82..39773357 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
@@ -7,12 +7,9 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
 import com.google.common.base.Objects;

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

 import java.io.BufferedReader;

-import java.io.InputStream;

-import java.io.InputStreamReader;

+import java.io.FileReader;

 import java.util.List;

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

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

-import org.eclipse.emf.ecore.EObject;

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

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

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

@@ -67,18 +64,17 @@ public class VampireHandler {
         long _minus_1 = (_currentTimeMillis_1 - startTime);

         solverTime = _minus_1;

       }

-      InputStream _inputStream = p.getInputStream();

-      InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream);

-      final BufferedReader reader = new BufferedReader(_inputStreamReader);

+      FileReader _fileReader = new FileReader(solnLoc);

+      final BufferedReader reader = new BufferedReader(_fileReader);

       final List<String> output = CollectionLiterals.<String>newArrayList();

       String line = "";

       while ((!Objects.equal((line = reader.readLine()), null))) {

-        output.add((line + "\n"));

+        boolean _equals_2 = Objects.equal(line, "Finite Model Found!");

+        if (_equals_2) {

+          return new MonitoredVampireSolution(solverTime, null, true);

+        }

       }

-      workspace.getFile(TEMPNAME).delete();

-      final EList<EObject> root = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents();

-      EObject _get = root.get(0);

-      return new MonitoredVampireSolution(solverTime, ((VampireModel) _get));

+      return new MonitoredVampireSolution(solverTime, null, false);

     } catch (Throwable _e) {

       throw Exceptions.sneakyThrow(_e);

     }