VAMPIRE: close #22, improve test structure for #39, .vql file trouble

18 files changed, 43 insertions, 174 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index 43e1e477..1ea7e30a 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 4e6f6ca0..ee06cb39 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 707a6089..648d9600 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 3171324f..a02821a5 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 301df7fa..b01f92a6 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 5e53ea26..7634af4b 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 b378ed09..4906adfc 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 605ac88c..e2c945e3 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 0c289e29..f465506c 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 cb72fd90..e046604a 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 cfe1e8cd..aff62dca 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 c2079147..7212cce7 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 3c70bc14..d23bacad 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 9ef20b23..be78cace 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_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 4cdc7e6a..9deab87f 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
@@ -64,12 +64,19 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
         Type _referred = ((ComplexTypeReference) _get).getReferred();

         Type pointingTo = ((Type) _referred);

         containmentListCopy.remove(pointingTo);

-        EList<Type> _subtypes = pointingTo.getSubtypes();

-        for (final Type c : _subtypes) {

+        List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList();

+        this.support.listSubtypes(pointingTo, allSubtypes);

+        for (final Type c : allSubtypes) {

           containmentListCopy.remove(c);

         }

       }

     }

+    for (final Type c : containmentListCopy) {

+      boolean _isIsAbstract = c.isIsAbstract();

+      if (_isIsAbstract) {

+        containmentListCopy.remove(c);

+      }

+    }

     final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString();

     final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate));

     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

@@ -132,7 +139,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
         final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate);

         this.addToMap(type2cont, toFunc, rel);

         EList<Type> _subtypes = toType.getSubtypes();

-        for (final Type c : _subtypes) {

+        for (final Type c_1 : _subtypes) {

           this.addToMap(type2cont, toFunc, rel);

         }

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

@@ -184,7 +191,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
       {

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

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

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

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 d5745333..c6565f6a 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
@@ -3,7 +3,6 @@ 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.VLSEquivalent;

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

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

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

@@ -17,14 +16,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition;

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

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

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

 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;

 import java.util.ArrayList;

 import java.util.Arrays;

-import java.util.Collection;

-import java.util.HashMap;

 import java.util.List;

-import java.util.Map;

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

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

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

@@ -64,10 +59,19 @@ public class Logic2VampireLanguageMapper_RelationMapper {
         relVar2TypeDecComply.add(varTypeComply);

       }

     }

+    final String[] nameArray = r.getName().split(" ");

+    String relNameVar = "";

+    int _length_1 = nameArray.length;

+    boolean _equals = (_length_1 == 3);

+    if (_equals) {

+      relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);

+    } else {

+      relNameVar = r.getName();

+    }

+    final String relName = relNameVar;

     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

-      final String[] nameArray = r.getName().split(" ");

-      it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2]));

+      it.setName(this.support.toIDMultiple("compliance", relName));

       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

@@ -80,7 +84,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
         final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {

           VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

-            it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2]));

+            it_3.setConstant(this.support.toIDMultiple("r", relName));

             for (final VLSVariable v_1 : relVar2VLS) {

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

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

@@ -104,145 +108,6 @@ public class Logic2VampireLanguageMapper_RelationMapper {
   }

   

   public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) {

-    final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>();

-    final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>();

-    final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>();

-    final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();

-    EList<Variable> _variables = reldef.getVariables();

-    for (final Variable variable : _variables) {

-      {

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

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

-          it.setName(this.support.toIDMultiple("V", variable.getName()));

-        };

-        final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);

-        relationVar2VLS.put(variable, v);

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

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

-          TypeReference _range = variable.getRange();

-          it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));

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

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

-          _terms.add(_duplicate);

-        };

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

-        relationVar2TypeDecComply.put(variable, varTypeComply);

-        relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply));

-      }

-    }

-    final String[] nameArray = reldef.getName().split(" ");

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

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

-      int _length = nameArray.length;

-      int _minus = (_length - 2);

-      int _length_1 = nameArray.length;

-      int _minus_1 = (_length_1 - 1);

-      it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], 

-        nameArray[_minus_1]));

-      it.setFofRole("axiom");

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

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

-        EList<Variable> _variables_1 = reldef.getVariables();

-        for (final Variable variable_1 : _variables_1) {

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

-          VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS));

-          _variables_2.add(_duplicate);

-        }

-        VLSImplies _createVLSImplies = this.factory.createVLSImplies();

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

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

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

-            it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName()));

-            EList<Variable> _variables_3 = reldef.getVariables();

-            for (final Variable variable_2 : _variables_3) {

-              {

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

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

-                  it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName());

-                };

-                final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);

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

-                _terms.add(v);

-              }

-            }

-          };

-          VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);

-          it_2.setLeft(_doubleArrow);

-          Collection<VLSFunction> _values = relationVar2TypeDecComply.values();

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

-          it_2.setRight(this.support.unfoldAnd(_arrayList));

-        };

-        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);

-        it_1.setOperand(_doubleArrow);

-      };

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

-      it.setFofFormula(_doubleArrow);

-    };

-    final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);

-    VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

-      int _length = nameArray.length;

-      int _minus = (_length - 2);

-      int _length_1 = nameArray.length;

-      int _minus_1 = (_length_1 - 1);

-      it.setName(this.support.toIDMultiple("relation", nameArray[_minus], 

-        nameArray[_minus_1]));

-      it.setFofRole("axiom");

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

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

-        EList<Variable> _variables_1 = reldef.getVariables();

-        for (final Variable variable_1 : _variables_1) {

-          {

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

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

-              it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName());

-            };

-            final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3);

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

-            _variables_2.add(v);

-          }

-        }

-        VLSImplies _createVLSImplies = this.factory.createVLSImplies();

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

-          Collection<VLSFunction> _values = relationVar2TypeDecRes.values();

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

-          it_2.setLeft(this.support.unfoldAnd(_arrayList));

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

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

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

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

-              it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName()));

-              EList<Variable> _variables_2 = reldef.getVariables();

-              for (final Variable variable_2 : _variables_2) {

-                {

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

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

-                    it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName());

-                  };

-                  final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6);

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

-                  _terms.add(v);

-                }

-              }

-            };

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

-            it_3.setLeft(_doubleArrow);

-            it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS));

-          };

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

-          it_2.setRight(_doubleArrow);

-        };

-        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);

-        it_1.setOperand(_doubleArrow);

-      };

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

-      it.setFofFormula(_doubleArrow);

-    };

-    final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_1);

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

-    _formulas.add(comply);

-    EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();

-    _formulas_1.add(res);

   }

   

   public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) {

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 89633ca1..f1d73bec 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
@@ -403,20 +403,14 @@ public class Logic2VampireLanguageMapper_Support {
     return _xifexpression;

   }

   

-  protected List<Type> listSubtypes(final Type t) {

-    List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList();

-    boolean _isEmpty = t.getSubtypes().isEmpty();

-    boolean _not = (!_isEmpty);

-    if (_not) {

-      EList<Type> _subtypes = t.getSubtypes();

-      for (final Type subt : _subtypes) {

-        {

-          allSubtypes.add(subt);

-          allSubtypes = this.listSubtypes(subt);

-        }

+  protected void listSubtypes(final Type t, final List<Type> allSubtypes) {

+    EList<Type> _subtypes = t.getSubtypes();

+    for (final Type subt : _subtypes) {

+      {

+        allSubtypes.add(subt);

+        this.listSubtypes(subt, allSubtypes);

       }

     }

-    return allSubtypes;

   }

   

   protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) {

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 9b8f049d..b9c1d28d 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
@@ -78,16 +78,19 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           EList<DefinedElement> _elements = type_1.getElements();

           for (final DefinedElement e : _elements) {

             {

+              final String[] nameArray = e.getName().split(" ");

+              String relNameVar = "";

+              int _length = nameArray.length;

+              boolean _equals = (_length == 3);

+              if (_equals) {

+                relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);

+              } else {

+                relNameVar = e.getName();

+              }

+              final String relName = relNameVar;

               VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

-                final String[] splitName = e.getName().split(" ");

-                int _length = splitName.length;

-                boolean _greaterThan = (_length > 2);

-                if (_greaterThan) {

-                  it.setConstant(this.support.toIDMultiple("e", splitName[0], splitName[2]));

-                } else {

-                  it.setConstant(this.support.toIDMultiple("e", splitName[0]));

-                }

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

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

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

                 _terms.add(_duplicate);

@@ -123,7 +126,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           }

           VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

-            it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0]));

+            it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString()));

             it.setFofRole("axiom");

             VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

@@ -160,10 +163,10 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2);

               final VLSConstant cst = this.support.toConstant(cstTerm);

               trace.uniqueInstances.add(cst);

-              final int index = i;

+              final int index = (i - globalCounter);

               VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

-                it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], 

+                it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), 

                   type_1.getElements().get(index).getName().split(" ")[0]));

                 it.setFofRole("axiom");

                 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();