14 files changed, 94 insertions, 75 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 80a74b4c..f312e3a8 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 2dc1ce19..88960abc 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 3c14aa6c..580eb165 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 b51b8ceb..adc1b1cf 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 02b4f393..57f21798 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 1feb9930..355315f8 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 fbc106a5..77a5ce95 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 77ffdd4b..5eef76af 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 070afd3c..b042022e 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.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index f04bd7dc..65f58281 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
@@ -117,13 +117,13 @@ public class Logic2VampireLanguageMapper {
     if (_not) {

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

     }

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

     trace.relationDefinitions = this.collectRelationDefinitions(problem);

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

       this.relationMapper.transformRelation(it, trace);

     };

     problem.getRelations().forEach(_function_3);

     this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace);

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

     trace.constantDefinitions = this.collectConstantDefinitions(problem);

     final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> {

       this.constantMapper.transformConstantDefinitionSpecification(it, trace);

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
index 621a6e58..f1600087 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
@@ -31,6 +31,8 @@ public class Logic2VampireLanguageMapperTrace {
   

   public Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>();

   

+  public Object topLvlElementIsInInitialModel = null;

+  

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

   

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

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 855d7637..07677b7a 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
@@ -25,6 +25,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy;

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

 import java.util.ArrayList;

@@ -36,7 +37,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;

 

@@ -91,10 +91,17 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
     final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate));

     boolean topLvlIsInInitModel = false;

     String topLvlString = "";

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

-    for (final Type c : _subtypes) {

-      boolean _equals = c.getClass().getSimpleName().equals("TypeDefinitionImpl");

+    ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar);

+    listToCheck.addAll(topTermVar.getSubtypes());

+    for (final Type c : listToCheck) {

+      Class<? extends Type> _class = c.getClass();

+      boolean _equals = Objects.equal(_class, TypeDefinitionImpl.class);

       if (_equals) {

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

+        boolean _greaterThan = (_length > 1);

+        if (_greaterThan) {

+          throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model");

+        }

         EList<DefinedElement> _elements = ((TypeDefinition) c).getElements();

         for (final DefinedElement d : _elements) {

           boolean _containsKey = trace.definedElement2String.containsKey(d);

@@ -105,10 +112,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
         }

       }

     }

+    trace.topLvlElementIsInInitialModel = Boolean.valueOf(topLvlIsInInitModel);

     final boolean topInIM = topLvlIsInInitModel;

     final String topStr = topLvlString;

-    InputOutput.<Boolean>print(Boolean.valueOf(topInIM));

-    InputOutput.<String>print(topStr);

     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

       it.setName(this.support.toIDMultiple("containment_topLevel", topName));

@@ -174,8 +180,8 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
         final Type toType = ((Type) _referred);

         final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate);

         this.addToMap(type2cont, toFunc, rel);

-        EList<Type> _subtypes_1 = toType.getSubtypes();

-        for (final Type c_1 : _subtypes_1) {

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

+        for (final Type c_1 : _subtypes) {

           this.addToMap(type2cont, toFunc, rel);

         }

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

@@ -242,9 +248,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
                 EList<VLSVariable> _variables_1 = it_3.getVariables();

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

                 _variables_1.add(_duplicate_1);

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

-                boolean _greaterThan = (_length > 1);

-                if (_greaterThan) {

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

+                boolean _greaterThan_1 = (_length_1 > 1);

+                if (_greaterThan_1) {

                   it_3.setOperand(this.makeUnique(e.getValue()));

                 } else {

                   it_3.setOperand(e.getValue().get(0));

@@ -282,7 +288,8 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
           {

             for (final Relation l_3 : relationsList) {

               {

-                final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i))));

+                final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), 

+                  CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i))));

                 disjunctionList.add(rel);

               }

             }

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 f5d35b28..bf7b70d0 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
@@ -47,11 +47,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     this.base = base;

   }

   

-  public void _transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

+  public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

     final int ABSOLUTE_MIN = 0;

     final int ABSOLUTE_MAX = Integer.MAX_VALUE;

-    final int GLOBAL_MIN = config.typeScopes.minNewElements;

-    final int GLOBAL_MAX = config.typeScopes.maxNewElements;

+    int elemsInIM = trace.definedElement2String.size();

+    final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM);

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

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

     final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN);

     if ((GLOBAL_MIN != ABSOLUTE_MIN)) {

@@ -74,34 +75,37 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       }

     }

     int i_1 = 1;

+    if ((((Boolean) trace.topLvlElementIsInInitialModel)).booleanValue()) {

+      i_1 = 0;

+    }

     int minNum = (-1);

     Map<Type, Integer> startPoints = new HashMap<Type, Integer>();

     Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet();

-    for (final Type t : _keySet) {

+    for (final Type tConfig : _keySet) {

       {

-        minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue();

+        minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig, config.typeScopes.minNewElementsByType)).intValue();

         if ((minNum != 0)) {

           this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false);

-          startPoints.put(t, Integer.valueOf(i_1));

+          startPoints.put(tConfig, Integer.valueOf(i_1));

           int _i = i_1;

           i_1 = (_i + minNum);

-          this.makeFofFormula(localInstances, trace, true, t);

+          this.makeFofFormula(localInstances, trace, true, tConfig);

         }

       }

     }

     Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet();

-    for (final Type t_1 : _keySet_1) {

+    for (final Type tConfig_1 : _keySet_1) {

       {

-        Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType);

-        minNum = (CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType)).intValue();

-        Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints);

+        Integer maxNum = CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.maxNewElementsByType);

+        minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.minNewElementsByType)).intValue();

+        Integer startpoint = CollectionsUtil.<Type, Integer>lookup(tConfig_1, startPoints);

         if ((minNum != 0)) {

           this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false);

         }

         if (((maxNum).intValue() != minNum)) {

           int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum));

           this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false);

-          this.makeFofFormula(localInstances, trace, false, t_1);

+          this.makeFofFormula(localInstances, trace, false, tConfig_1);

         }

       }

     }

@@ -246,8 +250,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     _formulas.add(cstDec);

   }

   

-  public void transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

-    _transformScope(config, trace);

+  public void transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

+    _transformScope(types, 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_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 2d9d566d..73e59774 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
@@ -77,10 +77,16 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           trace.type2Predicate.put(type, typePred);

         }

       }

-      Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);

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

+        boolean _isIsAbstract = it.isIsAbstract();

+        return Boolean.valueOf((!_isIsAbstract));

+      };

+      Iterable<TypeDefinition> _filter = IterableExtensions.<TypeDefinition>filter(Iterables.<TypeDefinition>filter(types, TypeDefinition.class), _function_1);

       for (final TypeDefinition type_1 : _filter) {

         {

-          final boolean isNotEnum = ((((Object[])Conversions.unwrapArray(type_1.getSupertypes(), Object.class)).length == 1) && type_1.getSupertypes().get(0).isIsAbstract());

+          final int len = type_1.getName().length();

+          boolean _equals = type_1.getName().substring((len - 4), len).equals("enum");

+          final boolean isNotEnum = (!_equals);

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

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

           for (final DefinedElement e : _elements) {

@@ -88,21 +94,21 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               final String[] nameArray = e.getName().split(" ");

               String relNameVar = "";

               int _length = nameArray.length;

-              boolean _equals = (_length == 3);

-              if (_equals) {

+              boolean _equals_1 = (_length == 3);

+              if (_equals_1) {

                 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 Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> {

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

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

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

                 _terms.add(_duplicate);

               };

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

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

               trace.element2Predicate.put(e, enumElemPred);

             }

           }

@@ -113,17 +119,17 @@ public class Logic2VampireLanguageMapper_TypeMapper {
             {

               EList<DefinedElement> _elements_2 = type_1.getElements();

               for (final DefinedElement t2 : _elements_2) {

-                boolean _equals = Objects.equal(t1, t2);

-                if (_equals) {

+                boolean _equals_1 = Objects.equal(t1, t2);

+                if (_equals_1) {

                   final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);

                   possibleNots.add(fct);

                 } else {

                   final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);

                   VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

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

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

                     it.setOperand(op);

                   };

-                  final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_1);

+                  final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);

                   possibleNots.add(negFct);

                 }

               }

@@ -132,32 +138,32 @@ public class Logic2VampireLanguageMapper_TypeMapper {
             }

           }

           VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

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

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

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

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

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

                 VLSAnd _createVLSAnd = this.factory.createVLSAnd();

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

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

                   it_3.setLeft(this.support.topLevelTypeFunc(variable));

                   it_3.setRight(this.support.unfoldOr(typeDefs));

                 };

-                VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_4);

+                VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_5);

                 it_2.setRight(_doubleArrow);

               };

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

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

               it_1.setOperand(_doubleArrow);

             };

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

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

             it.setFofFormula(_doubleArrow);

           };

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

+          final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);

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

           _formulas.add(res);

           for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) {

@@ -165,17 +171,17 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               final int num = (i + 1);

               final int index = (i - globalCounter);

               VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();

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

+              final Procedure1<VLSFunctionAsTerm> _function_3 = (VLSFunctionAsTerm it) -> {

                 it.setFunctor(("eo" + Integer.valueOf(num)));

               };

-              final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2);

+              final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3);

               if (isNotEnum) {

                 trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor());

               }

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

               trace.uniqueInstances.add(cst);

               VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

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

                 String _xifexpression = null;

                 if (isNotEnum) {

                   _xifexpression = "definedType";

@@ -186,28 +192,28 @@ public class Logic2VampireLanguageMapper_TypeMapper {
                   type_1.getElements().get(index).getName().split(" ")[0]));

                 it.setFofRole("axiom");

                 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

+                final Procedure1<VLSUniversalQuantifier> _function_5 = (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_5 = (VLSEquivalent it_2) -> {

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

                     VLSEquality _createVLSEquality = this.factory.createVLSEquality();

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

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

                       it_3.setLeft(this.support.duplicate(variable));

                       it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm)));

                     };

-                    VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6);

+                    VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7);

                     it_2.setLeft(_doubleArrow);

                     it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable));

                   };

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

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

                   it_1.setOperand(_doubleArrow);

                 };

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

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

                 it.setFofFormula(_doubleArrow);

               };

-              final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3);

+              final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4);

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

               _formulas_1.add(enumScope);

             }

@@ -217,11 +223,11 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           globalCounter = (_globalCounter + _size);

         }

       }

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

+      final Function1<Type, Boolean> _function_2 = (Type it) -> {

         boolean _isIsAbstract = it.isIsAbstract();

         return Boolean.valueOf((!_isIsAbstract));

       };

-      Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);

+      Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_2);

       for (final Type t1 : _filter_1) {

         {

           for (final Type t2 : types) {

@@ -229,10 +235,10 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));

             } else {

               VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

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

+              final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {

                 it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));

               };

-              VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);

+              VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);

               trace.type2PossibleNot.put(t2, _doubleArrow);

             }

           }

@@ -245,63 +251,63 @@ public class Logic2VampireLanguageMapper_TypeMapper {
       final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList();

       for (final Type t : types) {

         VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

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

+        final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {

           it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate)));

         };

-        VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);

+        VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);

         type2Not.add(_doubleArrow);

       }

       VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

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

         it.setName("notObjectHandler");

         it.setFofRole("axiom");

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

+        final Procedure1<VLSUniversalQuantifier> _function_5 = (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_5 = (VLSEquivalent it_2) -> {

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

             VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation();

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

+            final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> {

               it_3.setOperand(this.support.topLevelTypeFunc());

             };

-            VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_6);

+            VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_7);

             it_2.setLeft(_doubleArrow_1);

             it_2.setRight(this.support.unfoldAnd(type2Not));

           };

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

+          VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6);

           it_1.setOperand(_doubleArrow_1);

         };

-        VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4);

+        VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);

         it.setFofFormula(_doubleArrow_1);

       };

-      final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_3);

+      final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_4);

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

       _formulas.add(notObj);

       VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

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

         it.setName("inheritanceHierarchyHandler");

         it.setFofRole("axiom");

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

+        final Procedure1<VLSUniversalQuantifier> _function_6 = (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_6 = (VLSEquivalent it_2) -> {

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

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

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

             final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values);

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

           };

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

+          VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_7);

           it_1.setOperand(_doubleArrow_1);

         };

-        VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);

+        VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_6);

         it.setFofFormula(_doubleArrow_1);

       };

-      final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4);

+      final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5);

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

       _xblockexpression = _formulas_1.add(hierarch);

     }