VAMPIRE: fixed MANY bugs in containment and scope. #40 is good for now

12 files changed, 103 insertions, 37 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 f312e3a8..677cb718 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 88960abc..d071aa8a 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 580eb165..48090814 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 adc1b1cf..154e42a2 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 57f21798..61774e26 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 355315f8..2798d324 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 77a5ce95..5f3f349b 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 5eef76af..787c44a2 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 b042022e..b6e94088 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/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
index f1600087..c2ae099e 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
@@ -33,6 +33,8 @@ public class Logic2VampireLanguageMapperTrace {
   

   public Object topLvlElementIsInInitialModel = null;

   

+  public Object topLevelType = 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 07677b7a..dd549c29 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
@@ -37,6 +37,7 @@ 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;

 

@@ -89,6 +90,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
     }

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

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

+    trace.topLevelType = topTermVar;

     boolean topLvlIsInInitModel = false;

     String topLvlString = "";

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

@@ -174,15 +176,16 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
     final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>();

     for (final Relation l_2 : relationsList) {

       {

-        final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), varList);

+        final VLSFunction rel = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate);

         TypeReference _get = l_2.getParameters().get(1);

         Type _referred = ((ComplexTypeReference) _get).getReferred();

         final Type toType = ((Type) _referred);

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

-        this.addToMap(type2cont, toFunc, rel);

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

-        for (final Type c_1 : _subtypes) {

-          this.addToMap(type2cont, toFunc, rel);

+        this.addToMap(type2cont, this.support.duplicate(toFunc), this.support.duplicate(rel, varList));

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

+        this.support.listSubtypes(toType, subTypes);

+        for (final Type c_1 : subTypes) {

+          this.addToMap(type2cont, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(c_1, trace.type2Predicate)), this.support.duplicate(rel, varList));

         }

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

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

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

       {

+        VLSFunction _key = e.getKey();

+        String _plus = (_key + "   ");

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

+        String _plus_1 = (_plus + _value);

+        InputOutput.<String>println(_plus_1);

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

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

@@ -352,20 +360,32 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
   }

   

   protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) {

-    Object _xifexpression = null;

-    boolean _containsKey = type2cont.containsKey(toFunc);

-    boolean _not = (!_containsKey);

-    if (_not) {

-      _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel));

-    } else {

-      boolean _xifexpression_1 = false;

-      boolean _contains = type2cont.get(toFunc).contains(rel);

-      boolean _not_1 = (!_contains);

-      if (_not_1) {

-        _xifexpression_1 = type2cont.get(toFunc).add(rel);

+    Object _xblockexpression = null;

+    {

+      boolean keyInMap = false;

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

+      Set<VLSFunction> _keySet = type2cont.keySet();

+      for (final VLSFunction k : _keySet) {

+        boolean _equals = k.getConstant().equals(toFunc.getConstant());

+        if (_equals) {

+          keyInMap = true;

+          existingKey = k;

+        }

+      }

+      Object _xifexpression = null;

+      if ((!keyInMap)) {

+        _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel));

+      } else {

+        boolean _xifexpression_1 = false;

+        boolean _contains = type2cont.get(existingKey).contains(rel);

+        boolean _not = (!_contains);

+        if (_not) {

+          _xifexpression_1 = type2cont.get(existingKey).add(rel);

+        }

+        _xifexpression = Boolean.valueOf(_xifexpression_1);

       }

-      _xifexpression = Boolean.valueOf(_xifexpression_1);

+      _xblockexpression = _xifexpression;

     }

-    return _xifexpression;

+    return _xblockexpression;

   }

 }

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 bf7b70d0..c2e4033b 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
@@ -14,7 +14,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

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

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

+import com.google.common.base.Objects;

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

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

 import java.util.ArrayList;

 import java.util.HashMap;

@@ -26,6 +29,7 @@ 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.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;

@@ -80,33 +84,73 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     }

     int minNum = (-1);

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

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

-    for (final Type tConfig : _keySet) {

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

+      boolean _equals = it.equals(trace.topLevelType);

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

+    };

+    Iterable<Type> _filter = IterableExtensions.<Type>filter(config.typeScopes.minNewElementsByType.keySet(), _function);

+    for (final Type t : _filter) {

       {

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

+        int numIniIntModel = 0;

+        Set<DefinedElement> _keySet = trace.definedElement2String.keySet();

+        for (final DefinedElement elem : _keySet) {

+          EList<TypeDefinition> _definedInType = elem.getDefinedInType();

+          for (final TypeDefinition tDefined : _definedInType) {

+            boolean _dfsSubtypeCheck = this.support.dfsSubtypeCheck(t, tDefined);

+            if (_dfsSubtypeCheck) {

+              int _numIniIntModel = numIniIntModel;

+              numIniIntModel = (_numIniIntModel + 1);

+            }

+          }

+        }

+        Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType);

+        int _minus = ((_lookup).intValue() - numIniIntModel);

+        minNum = _minus;

         if ((minNum != 0)) {

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

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

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

           int _i = i_1;

           i_1 = (_i + minNum);

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

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

         }

       }

     }

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

-    for (final Type tConfig_1 : _keySet_1) {

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

+      boolean _equals = it.equals(trace.topLevelType);

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

+    };

+    Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(config.typeScopes.maxNewElementsByType.keySet(), _function_1);

+    for (final Type t_1 : _filter_1) {

       {

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

+        int numIniIntModel = 0;

+        Set<DefinedElement> _keySet = trace.definedElement2String.keySet();

+        for (final DefinedElement elem : _keySet) {

+          EList<TypeDefinition> _definedInType = elem.getDefinedInType();

+          boolean _equals = Objects.equal(_definedInType, t_1);

+          if (_equals) {

+            int _numIniIntModel = numIniIntModel;

+            numIniIntModel = (_numIniIntModel + 1);

+          }

+        }

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

+        int maxNum = ((_lookup).intValue() - numIniIntModel);

+        boolean _contains = config.typeScopes.minNewElementsByType.keySet().contains(t_1);

+        if (_contains) {

+          Integer _lookup_1 = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType);

+          int _minus = ((_lookup_1).intValue() - numIniIntModel);

+          minNum = _minus;

+        } else {

+          minNum = 0;

+        }

         if ((minNum != 0)) {

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

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

+        } else {

+          localInstances.clear();

         }

-        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, tConfig_1);

-        }

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

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

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

       }

     }

     final boolean DUPLICATES = config.uniquenessDuplicates;

@@ -118,12 +162,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
           {

             final int x = ind;

             VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

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

               it.setName(this.support.toIDMultiple("t_uniqueness", e.getName()));

               it.setFofRole("axiom");

               it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e));

             };

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

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

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

             _formulas.add(uniqueness);

             ind++;

@@ -135,12 +179,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
           {

             final int x = ind;

             VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

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

               it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName()));

               it.setFofRole("axiom");

               it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1));

             };

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

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

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

             _formulas.add(uniqueness);

             ind++;