VAMPIRE: adapt grammar to Vampire solution + get model from text

17 files changed, 55 insertions, 72 deletions

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 a7942958..43992ea0 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/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 487f9569..19608361 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 bd61b874..791a9524 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 2e58cecd..89003c27 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 1b894303..b37d993a 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 4b7fd4bf..45afcecc 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 6626adf4..0f4dc63a 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 339baea9..ab58fcab 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 868f30e7..cf19663e 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/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index 08ffcb3b..0b2cb192 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 65f58281..58da7ccd 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
@@ -16,7 +16,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;

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

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

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal;

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

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

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

@@ -44,7 +43,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral;

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

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

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral;

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

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

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

@@ -98,7 +96,7 @@ public class Logic2VampireLanguageMapper {
   public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) {

     VLSComment _createVLSComment = this.factory.createVLSComment();

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

-      it.setComment("This is an initial Test Comment");

+      it.setComment("%This is an initial Test Comment");

     };

     final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function);

     VampireModel _createVampireModel = this.factory.createVampireModel();

@@ -202,14 +200,6 @@ public class Logic2VampireLanguageMapper {
     return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function);

   }

   

-  protected VLSTerm _transformTerm(final RealLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

-    VLSReal _createVLSReal = this.factory.createVLSReal();

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

-      it.setValue(literal.getValue().toString());

-    };

-    return ObjectExtensions.<VLSReal>operator_doubleArrow(_createVLSReal, _function);

-  }

-  

   protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

     VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

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

@@ -394,8 +384,6 @@ public class Logic2VampireLanguageMapper {
       return _transformTerm((Not)and, trace, variables);

     } else if (and instanceof Or) {

       return _transformTerm((Or)and, trace, variables);

-    } else if (and instanceof RealLiteral) {

-      return _transformTerm((RealLiteral)and, trace, variables);

     } else if (and instanceof InstanceOf) {

       return _transformTerm((InstanceOf)and, trace, variables);

     } else if (and instanceof SymbolicValue) {

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
index dd549c29..7daf1b2f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
@@ -15,6 +15,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;

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

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

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

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

 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

@@ -37,7 +38,6 @@ import org.eclipse.emf.common.util.EList;
 import org.eclipse.xtext.xbase.lib.CollectionLiterals;

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

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

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

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

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

 

@@ -123,7 +123,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

       final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {

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

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

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

         _variables.add(_duplicate);

         VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -193,10 +193,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
           it.setFofRole("axiom");

           VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

           final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> {

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

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

             VLSVariable _duplicate = this.support.duplicate(varA);

             _variables.add(_duplicate);

-            EList<VLSVariable> _variables_1 = it_1.getVariables();

+            EList<VLSVariableDeclaration> _variables_1 = it_1.getVariables();

             VLSVariable _duplicate_1 = this.support.duplicate(varB);

             _variables_1.add(_duplicate_1);

             VLSImplies _createVLSImplies = this.factory.createVLSImplies();

@@ -206,10 +206,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
               final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> {

                 VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier();

                 final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> {

-                  EList<VLSVariable> _variables_2 = it_4.getVariables();

+                  EList<VLSVariableDeclaration> _variables_2 = it_4.getVariables();

                   VLSVariable _duplicate_2 = this.support.duplicate(varC);

                   _variables_2.add(_duplicate_2);

-                  EList<VLSVariable> _variables_3 = it_4.getVariables();

+                  EList<VLSVariableDeclaration> _variables_3 = it_4.getVariables();

                   VLSVariable _duplicate_3 = this.support.duplicate(varB);

                   _variables_3.add(_duplicate_3);

                   it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB)));

@@ -234,18 +234,13 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
     Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet();

     for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) {

       {

-        VLSFunction _key = e.getKey();

-        String _plus = (_key + "   ");

-        List<VLSFunction> _value = e.getValue();

-        String _plus_1 = (_plus + _value);

-        InputOutput.<String>println(_plus_1);

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

           it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString()));

           it.setFofRole("axiom");

           VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

           final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {

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

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

             VLSVariable _duplicate = this.support.duplicate(varA);

             _variables.add(_duplicate);

             VLSImplies _createVLSImplies = this.factory.createVLSImplies();

@@ -253,7 +248,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
               it_2.setLeft(this.support.duplicate(e.getKey(), varA));

               VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

               final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> {

-                EList<VLSVariable> _variables_1 = it_3.getVariables();

+                EList<VLSVariableDeclaration> _variables_1 = it_3.getVariables();

                 VLSVariable _duplicate_1 = this.support.duplicate(varB);

                 _variables_1.add(_duplicate_1);

                 int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length;

@@ -313,9 +308,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
           final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_1) -> {

             VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

             final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_2) -> {

-              EList<VLSVariable> _variables = it_2.getVariables();

+              EList<VLSVariableDeclaration> _variables = it_2.getVariables();

               List<VLSVariable> _duplicate = this.support.duplicate(variables);

-              Iterables.<VLSVariable>addAll(_variables, _duplicate);

+              Iterables.<VLSVariableDeclaration>addAll(_variables, _duplicate);

               it_2.setOperand(this.support.unfoldAnd(conjunctionList));

             };

             VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7);

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 c6565f6a..657c3292 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
@@ -9,6 +9,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

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

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

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

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

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

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

@@ -76,7 +77,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

       final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {

         for (final VLSVariable v : relVar2VLS) {

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

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

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

           _variables.add(_duplicate);

         }

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 c2e4033b..6d4767a7 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
@@ -13,6 +13,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

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

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

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

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

 import com.google.common.base.Objects;

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

@@ -244,7 +245,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

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

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

         _variables.add(_duplicate);

         VLSImplies _createVLSImplies = this.factory.createVLSImplies();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
index f1d73bec..6cd53fae 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -13,6 +13,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

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

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

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

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

 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

@@ -323,9 +324,9 @@ public class Logic2VampireLanguageMapper_Support {
       if (isUniversal) {

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

-          EList<VLSVariable> _variables = it.getVariables();

+          EList<VLSVariableDeclaration> _variables = it.getVariables();

           Collection<VLSVariable> _values = variableMap.values();

-          Iterables.<VLSVariable>addAll(_variables, _values);

+          Iterables.<VLSVariableDeclaration>addAll(_variables, _values);

           VLSImplies _createVLSImplies = this.factory.createVLSImplies();

           final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> {

             it_1.setLeft(this.unfoldAnd(typedefs));

@@ -341,9 +342,9 @@ public class Logic2VampireLanguageMapper_Support {
           typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));

           VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

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

-            EList<VLSVariable> _variables = it.getVariables();

+            EList<VLSVariableDeclaration> _variables = it.getVariables();

             Collection<VLSVariable> _values = variableMap.values();

-            Iterables.<VLSVariable>addAll(_variables, _values);

+            Iterables.<VLSVariableDeclaration>addAll(_variables, _values);

             it.setOperand(this.unfoldAnd(typedefs));

           };

           _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2);

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
index 73e59774..7921f204 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -15,6 +15,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;

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

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

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

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

 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

@@ -143,7 +144,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
             it.setFofRole("axiom");

             VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

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

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

               _variables.add(_duplicate);

               VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -193,7 +194,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
                 it.setFofRole("axiom");

                 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

                 final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {

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

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

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

                   _variables.add(_duplicate);

                   VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -263,7 +264,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
         it.setFofRole("axiom");

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

         final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {

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

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

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

           _variables.add(_duplicate);

           VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -291,7 +292,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
         it.setFofRole("axiom");

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

         final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> {

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

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

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

           _variables.add(_duplicate);

           VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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 1479e6b7..7f6ce1c6 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
@@ -1,59 +1,55 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

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

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

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl;

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

 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.util.List;

-import java.util.Map;

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

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

 import org.eclipse.emf.ecore.EObject;

-import org.eclipse.emf.ecore.resource.Resource;

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

 

 @SuppressWarnings("all")

 public class VampireHandler {

   public EList<EObject> callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) {

     try {

-      EList<EObject> _xblockexpression = null;

-      {

-        final String CMD = "cmd /c ";

-        final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\";

-        final String VAMPNAME = "vampire.exe";

-        final String TEMPNAME = "TEMP.tptp";

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

-        final String SOLNNAME = "solution.tptp";

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

-        final URI wsURI = workspace.getWorkspaceURI();

-        final String tempLoc = (wsURI + TEMPNAME);

-        String _plus = (wsURI + SOLNNAME);

-        final String solnLoc = (_plus + " ");

-        final String vampLoc = (VAMPDIR + VAMPNAME);

-        String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString();

-        final Process p = Runtime.getRuntime().exec((((((CMD + vampLoc) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class)));

-        p.waitFor();

-        InputStream _inputStream = p.getInputStream();

-        InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream);

-        final BufferedReader reader = new BufferedReader(_inputStreamReader);

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

-        String line = "";

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

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

-        }

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

-        Map<String, Object> _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap();

-        VampireLanguageFactoryImpl _vampireLanguageFactoryImpl = new VampireLanguageFactoryImpl();

-        _extensionToFactoryMap.put("*", _vampireLanguageFactoryImpl);

-        _xblockexpression = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents();

+      final String CMD = "cmd /c ";

+      final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\";

+      final String VAMPNAME = "vampire.exe";

+      final String TEMPNAME = "TEMP.tptp";

+      final String OPTION = " --mode casc_sat ";

+      final String SOLNNAME = "solution.tptp";

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

+      final URI wsURI = workspace.getWorkspaceURI();

+      final String tempLoc = (wsURI + TEMPNAME);

+      String _plus = (wsURI + SOLNNAME);

+      final String solnLoc = (_plus + " ");

+      final String vampLoc = (VAMPDIR + VAMPNAME);

+      String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString();

+      final Process p = Runtime.getRuntime().exec((((((CMD + vampLoc) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class)));

+      p.waitFor();

+      InputStream _inputStream = p.getInputStream();

+      InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream);

+      final BufferedReader reader = new BufferedReader(_inputStreamReader);

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

+      String line = "";

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

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

       }

-      return _xblockexpression;

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

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

+      EObject _get = root.get(0);

+      InputOutput.<EList<VLSComment>>println(((VampireModelImpl) _get).getComments());

+      return root;

     } catch (Throwable _e) {

       throw Exceptions.sneakyThrow(_e);

     }