21 files changed, 168 insertions, 133 deletions

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 d248b361..379d0683 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 d747e8ab..76dd192f 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 4dc095c0..936ab9ca 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_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 9a948c6f..e0f442f5 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
new file mode 100644
index 00000000..493ff288
--- /dev/null
+++ 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 4ef4809b..13281767 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 0f4acafe..1a777880 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/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
index 7d6865bb..e8658e7b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
index 6db26bf7..aec1688a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.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 8c96afa7..e77b9866 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 2427721d..100a52b8 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 d2c93ab4..231c1995 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 28c5d0f7..b67a307c 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/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
index 3d29fb07..ec8107e8 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
@@ -37,3 +37,4 @@
 /.VampireSolverException.java._trace
 /.VampireSolutionModel.java._trace
 /.VampireCallerWithTimeout.java._trace
+/.Logic2VampireLanguageMapper_ScopeMapper.java._trace
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 a1d80e58..89c9637e 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
@@ -4,6 +4,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

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

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

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper;

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

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

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

@@ -84,6 +85,9 @@ public class Logic2VampireLanguageMapper {
   private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this);

   

   @Accessors(AccessorType.PUBLIC_GETTER)

+  private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this);

+  

+  @Accessors(AccessorType.PUBLIC_GETTER)

   private final Logic2VampireLanguageMapper_TypeMapper typeMapper;

   

   public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) {

@@ -112,6 +116,7 @@ public class Logic2VampireLanguageMapper {
     if (_not) {

       this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);

     }

+    this.scopeMapper.transformScope(config, trace);

     trace.constantDefinitions = this.collectConstantDefinitions(problem);

     trace.relationDefinitions = this.collectRelationDefinitions(problem);

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

@@ -316,13 +321,13 @@ public class Logic2VampireLanguageMapper {
   

   /**

    * def dispatch protected VLSTerm transformSymbolicReference(Relation relation,

-   * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,

-   * Map<Variable, VLSVariable> variables) {

-   * if (trace.relationDefinitions.containsKey(relation)) {

-   * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),

-   * parameterSubstitutions, trace, variables)

-   * }

-   * else {

+   *    List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,

+   *    Map<Variable, VLSVariable> variables) {

+   *    if (trace.relationDefinitions.containsKey(relation)) {

+   *            this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),

+   *                    parameterSubstitutions, trace, variables)

+   *    }

+   *    else {

    * //                                         if (relationMapper.transformToHostedField(relation, trace)) {

    * //                                                 val VLSRelation = relation.lookup(trace.relationDeclaration2Field)

    * //                                                 // R(a,b) =>

@@ -348,7 +353,7 @@ public class Logic2VampireLanguageMapper {
    * //                                                         rightOperand = target

    * //                                                 ]

    * //                                         }

-   * }

+   *    }

    * }

    */

   protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

@@ -436,6 +441,11 @@ public class Logic2VampireLanguageMapper {
   }

   

   @Pure

+  public Logic2VampireLanguageMapper_ScopeMapper getScopeMapper() {

+    return this.scopeMapper;

+  }

+  

+  @Pure

   public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() {

     return this.typeMapper;

   }

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
new file mode 100644
index 00000000..86d8b648
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -0,0 +1,96 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;

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

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

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

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

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

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;

+import java.util.List;

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

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

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

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

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_ScopeMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  private final Logic2VampireLanguageMapper base;

+  

+  public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) {

+    this.base = base;

+  }

+  

+  public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

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

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

+      it.setName("A");

+    };

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

+    final List<VLSConstant> instances = CollectionLiterals.<VLSConstant>newArrayList();

+    for (int i = 0; (i < config.typeScopes.minNewElements); i++) {

+      {

+        final int num = (i + 1);

+        VLSConstant _createVLSConstant = this.factory.createVLSConstant();

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

+          it.setName(("o" + Integer.valueOf(num)));

+        };

+        final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1);

+        instances.add(cst);

+      }

+    }

+    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

+      it.setName("typeScope");

+      it.setFofRole("axiom");

+      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

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

+        _variables.add(_duplicate);

+        VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

+        final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> {

+          it_2.setLeft(this.support.topLevelTypeFunc());

+          final Function1<VLSConstant, VLSEquality> _function_4 = (VLSConstant i) -> {

+            VLSEquality _createVLSEquality = this.factory.createVLSEquality();

+            final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> {

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

+              final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {

+                it_4.setName(variable.getName());

+              };

+              VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_6);

+              it_3.setLeft(_doubleArrow);

+              it_3.setRight(i);

+            };

+            return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5);

+          };

+          it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4)));

+        };

+        VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);

+        it_1.setOperand(_doubleArrow);

+      };

+      VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);

+      it.setFofFormula(_doubleArrow);

+    };

+    final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);

+    EList<VLSFofFormula> _formulas = trace.specification.getFormulas();

+    _formulas.add(cstDec);

+  }

+  

+  public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

+    _transformScope(config, trace);

+    return;

+  }

+}

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 e1be7df5..b111732f 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
@@ -50,6 +50,29 @@ public class Logic2VampireLanguageMapper_Support {
     return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_");

   }

   

+  protected VLSVariable duplicate(final VLSVariable vrbl) {

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

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

+      it.setName(vrbl.getName());

+    };

+    return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);

+  }

+  

+  protected VLSFunction topLevelTypeFunc() {

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

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

+      it.setConstant("object");

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

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

+      final Procedure1<VLSVariable> _function_1 = (VLSVariable it_1) -> {

+        it_1.setName("A");

+      };

+      VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);

+      _terms.add(_doubleArrow);

+    };

+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

+  }

+  

   protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) {

     int _size = operands.size();

     boolean _equals = (_size == 1);

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java
index d674ac71..f7c6cb70 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java
@@ -1,7 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

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

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

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

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

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

@@ -13,7 +12,7 @@ import java.util.Map;
 public class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace {

   public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();

   

-  public final Map<DefinedElement, VLSEquality> definedElement2Declaration = new HashMap<DefinedElement, VLSEquality>();

+  public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>();

   

   public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>();

   

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
index 0f5e4e7a..71e98871 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
@@ -7,7 +7,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes;

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

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

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

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

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

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

@@ -27,10 +26,10 @@ import java.util.ArrayList;
 import java.util.Collection;

 import java.util.List;

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

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

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

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

 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;

 

@@ -58,14 +57,10 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
       {

         VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

-          it.setConstant(this.support.toIDMultiple("type", type.getName()));

+          it.setConstant(this.support.toIDMultiple("t", type.getName()));

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

-          VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

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

-            it_1.setName(variable.getName());

-          };

-          VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);

-          _terms.add(_doubleArrow);

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

+          _terms.add(_duplicate);

         };

         final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

         typeTrace.type2Predicate.put(type, typePred);

@@ -74,6 +69,22 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
     Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);

     for (final TypeDefinition type_1 : _filter) {

       {

+        final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();

+        EList<DefinedElement> _elements = type_1.getElements();

+        for (final DefinedElement e : _elements) {

+          {

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

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

+              it.setConstant(this.support.toIDMultiple("e", e.getName(), type_1.getName()));

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

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

+              _terms.add(_duplicate);

+            };

+            final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

+            typeTrace.element2Predicate.put(e, enumElemPred);

+            orElems.add(enumElemPred);

+          }

+        }

         VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

           it.setName(this.support.toIDMultiple("typeDef", type_1.getName()));

@@ -81,53 +92,15 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
           VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

-            VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

-            final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> {

-              it_2.setName(variable.getName());

-            };

-            VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3);

-            _variables.add(_doubleArrow);

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

+            _variables.add(_duplicate);

             VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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

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

-              final Procedure1<VLSFunction> _function_5 = (VLSFunction it_3) -> {

-                it_3.setConstant(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate).getConstant());

-                EList<VLSTerm> _terms = it_3.getTerms();

-                VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();

-                final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {

-                  it_4.setName("A");

-                };

-                VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_6);

-                _terms.add(_doubleArrow_1);

-              };

-              VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5);

-              it_2.setLeft(_doubleArrow_1);

-              CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate);

-              final Function1<DefinedElement, VLSEquality> _function_6 = (DefinedElement e) -> {

-                VLSEquality _createVLSEquality = this.factory.createVLSEquality();

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

-                  VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();

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

-                    it_4.setName(variable.getName());

-                  };

-                  VLSVariable _doubleArrow_2 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_8);

-                  it_3.setLeft(_doubleArrow_2);

-                  VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote();

-                  final Procedure1<VLSDoubleQuote> _function_9 = (VLSDoubleQuote it_4) -> {

-                    String _name = e.getName();

-                    String _plus = ("\"a" + _name);

-                    String _plus_1 = (_plus + "\"");

-                    it_4.setValue(_plus_1);

-                  };

-                  VLSDoubleQuote _doubleArrow_3 = ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function_9);

-                  it_3.setRight(_doubleArrow_3);

-                };

-                return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7);

-              };

-              it_2.setRight(this.support.unfoldOr(ListExtensions.<DefinedElement, VLSEquality>map(type_1.getElements(), _function_6)));

+            final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> {

+              it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate));

+              it_2.setRight(this.support.unfoldOr(orElems));

             };

-            VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);

-            it_1.setOperand(_doubleArrow_1);

+            VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);

+            it_1.setOperand(_doubleArrow);

           };

           VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);

           it.setFofFormula(_doubleArrow);

@@ -201,19 +174,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
         _variables.add(_doubleArrow);

         VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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

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

-          final Procedure1<VLSFunction> _function_6 = (VLSFunction it_3) -> {

-            it_3.setConstant("object");

-            EList<VLSTerm> _terms = it_3.getTerms();

-            VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();

-            final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> {

-              it_4.setName("A");

-            };

-            VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_7);

-            _terms.add(_doubleArrow_1);

-          };

-          VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_6);

-          it_2.setLeft(_doubleArrow_1);

+          it_2.setLeft(this.support.topLevelTypeFunc());

           Collection<VLSTerm> _values = typeTrace.type2And.values();

           ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);

           it_2.setRight(this.support.unfoldOr(_arrayList));

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
index f4380894..f4b5a1d2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
@@ -1,59 +1,5 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireSolutionModel;

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

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

-import org.eclipse.xtext.xbase.lib.Functions.Function2;

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

-

 @SuppressWarnings("all")

 public class Vampire2LogicMapper {

-  @Extension

-  private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;

-  

-  public LogicResult transformOutput(final LogicProblem problem, final int requiredNumberOfSolution, final VampireSolutionModel vampireSolution, final Logic2VampireLanguageMapperTrace trace, final long transformationTime) {

-    throw new Error("Unresolved compilation problems:"

-      + "\nThe method or field aswers is undefined for the type VampireSolutionModel"

-      + "\nThe method or field key is undefined for the type Object"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution"

-      + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution"

-      + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution"

-      + "\nmap cannot be resolved"

-      + "\ntoList cannot be resolved"

-      + "\nfinishedBeforeTimeout cannot be resolved"

-      + "\n! cannot be resolved"

-      + "\nlast cannot be resolved"

-      + "\nsatisfiable cannot be resolved"

-      + "\n|| cannot be resolved");

-  }

-  

-  public Statistics transformStatistics(final /* MonitoredAlloySolution */Object solution, final long transformationTime) {

-    throw new Error("Unresolved compilation problems:"

-      + "\nCannot cast from Object to int"

-      + "\nCannot cast from Object to int"

-      + "\naswers cannot be resolved"

-      + "\nsize cannot be resolved"

-      + "\naswers cannot be resolved"

-      + "\nget cannot be resolved"

-      + "\nvalue cannot be resolved"

-      + "\nintValue cannot be resolved"

-      + "\nkodkodTime cannot be resolved"

-      + "\nkodkodTime cannot be resolved"

-      + "\nwarnings cannot be resolved");

-  }

-  

-  public Long sum(final Iterable<Long> ints) {

-    final Function2<Long, Long, Long> _function = (Long p1, Long p2) -> {

-      return Long.valueOf(((p1).longValue() + (p2).longValue()));

-    };

-    return IterableExtensions.<Long>reduce(ints, _function);

-  }

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
index c665b9a6..3c43c4ea 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
@@ -10,8 +10,7 @@ public class VampireSolutionModel {
   @Override

   @Pure

   public int hashCode() {

-    int result = 1;

-    return result;

+    return 1;

   }

   

   @Override