15 files changed, 86 insertions, 41 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
index 2da4cfd7..5c5eaff3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -1,13 +1,15 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

 

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant

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

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

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

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

-import java.util.List

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

 import java.util.ArrayList

+import java.util.Map

 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

+import java.util.HashMap

 

 class Logic2VampireLanguageMapper_ScopeMapper {

         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

@@ -21,9 +23,9 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

         def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {

 

-//              HANDLE ERRORS RELATED TO MAX > MIN

-//              HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS

-//              NOT SPECIFIED MEANS =0 ?

+//              TODO HANDLE ERRORS RELATED TO MAX > MIN

+//              TODO HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS

+//              TODO NOT SPECIFIED MEANS =0 ?

                 // 1. make a list of constants equaling the min number of specified objects

                 val GLOBAL_MIN = config.typeScopes.minNewElements

                 val GLOBAL_MAX = config.typeScopes.maxNewElements

@@ -32,42 +34,47 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

                 // Handling Minimum_General

                 if (GLOBAL_MIN != 0) {

-                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false) // fix last param

-                        makeFofFormula(localInstances, trace, true, "object")

+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) // fix last param

+                        makeFofFormula(localInstances, trace, true, null)

                 }

 

                 // Handling Maximum_General

                 if (GLOBAL_MAX != 0) {

-                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true) // fix last param

-                        makeFofFormula(localInstances, trace, false, "object")

+                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) // fix last param

+                        makeFofFormula(localInstances, trace, false, null)

                 }

 

                 // Handling Minimum_Specific

                 var i = 0

                 var minNum = -1

+                var Map<Type, Integer> startPoints = new HashMap

                 for (t : config.typeScopes.minNewElementsByType.keySet) {

                         minNum = t.lookup(config.typeScopes.minNewElementsByType)

                         if (minNum != 0) {

-                                getInstanceConstants(i+minNum, i, localInstances, trace, false)

+                                getInstanceConstants(i + minNum, i, localInstances, trace, true, false)

+                                startPoints.put(t, i)

                                 i += minNum

-                                makeFofFormula(localInstances, trace, true, t.toString)//fix last param

+                                makeFofFormula(localInstances, trace, true, t)

                         }

                 }

 

-                //TODO: calc sum of mins, compare to current value of i

-                

+                // TODO: calc sum of mins, compare to current value of i

                 // Handling Maximum_Specific

                 for (t : config.typeScopes.maxNewElementsByType.keySet) {

                         var maxNum = t.lookup(config.typeScopes.maxNewElementsByType)

                         minNum = t.lookup(config.typeScopes.minNewElementsByType)

-                        if (maxNum != 0) {

-                                var forLimit = Math.min(GLOBAL_MAX, i+maxNum-minNum)

-                                getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false)

-                                makeFofFormula(localInstances, trace, false, t.toString)//fix last param

+                        var startpoint = t.lookup(startPoints)

+                        if (minNum != 0) {

+                                getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false)

+                        }

+                        if (maxNum != minNum) {

+                                var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum)

+                                getInstanceConstants(instEndInd, i, localInstances, trace, false, false)

+                                makeFofFormula(localInstances, trace, false, t)

                         }

                 }

 

-                // 3. Specify uniqueness of elements

+// 3. Specify uniqueness of elements

                 if (trace.uniqueInstances.length != 0) {

                         val uniqueness = createVLSFofFormula => [

                                 it.name = "typeUniqueness"

@@ -79,10 +86,12 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

         }

 

-        def protected void getInstanceConstants(int numElems, int init, ArrayList list,

-                Logic2VampireLanguageMapperTrace trace, boolean addToTrace) {

-                list.clear

-                for (var i = init; i < numElems; i++) {

+        def protected void getInstanceConstants(int endInd, int startInd, ArrayList list,

+                Logic2VampireLanguageMapperTrace trace, boolean clear, boolean addToTrace) {

+                if (clear) {

+                        list.clear

+                }

+                for (var i = startInd; i < endInd; i++) {

                         val num = i + 1

                         val cst = createVLSConstant => [

                                 it.name = "o" + num

@@ -94,7 +103,20 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                 }

         }

 

-        def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, String name) {

+        def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum,

+                Type type) {

+                var nm = ""

+                var VLSFunction tm = null

+                if (type === null) {

+                        nm = "object"

+                        tm = support.topLevelTypeFunc

+                } else {

+                        nm = type.lookup(trace.type2Predicate).constant.toString

+                        tm = support.duplicate(type.lookup(trace.type2Predicate))

+                }

+                val name = nm

+                val term = tm

+

                 val cstDec = createVLSFofFormula => [

                         it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name)

                         it.fofRole = "axiom"

@@ -109,15 +131,16 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                                                                 it.right = i

                                                         ]

                                                 ])

-                                                it.right = support.topLevelTypeFunc

+                                                it.right = term

                                         } else {

+                                                it.left = term

                                                 it.right = support.unfoldOr(list.map [ i |

                                                         createVLSEquality => [

                                                                 it.left = createVLSVariable => [it.name = variable.name]

                                                                 it.right = i

                                                         ]

                                                 ])

-                                                it.left = support.topLevelTypeFunc

+

                                         }

                                 ]

                         ]

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 5c634ba0..b86e8068 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 19d48790..052e0175 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 2db39cf0..1296bf9e 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 1fba7ac4..0210a300 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 9ef3a39c..fd625384 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 687f4889..978571d2 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 d59b2e98..b98f0332 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 eb12e24a..8238a89e 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 70eb3434..f64a218b 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 0077e151..cf8e4acd 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 62de24fc..07d5b7b4 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 d00ac8ca..983108a2 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 b86330dc..4442cdea 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_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 a412241a..1950cad0 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
@@ -6,6 +6,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;

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

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

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

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

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

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

@@ -15,6 +16,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;

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

 import java.util.ArrayList;

+import java.util.HashMap;

+import java.util.Map;

 import java.util.Set;

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

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

@@ -47,24 +50,26 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     final int GLOBAL_MAX = config.typeScopes.maxNewElements;

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

     if ((GLOBAL_MIN != 0)) {

-      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false);

-      this.makeFofFormula(localInstances, trace, true, "object");

+      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false);

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

     }

     if ((GLOBAL_MAX != 0)) {

-      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true);

-      this.makeFofFormula(localInstances, trace, false, "object");

+      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true);

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

     }

     int i = 0;

     int minNum = (-1);

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

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

     for (final Type t : _keySet) {

       {

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

         if ((minNum != 0)) {

-          this.getInstanceConstants((i + minNum), i, localInstances, trace, false);

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

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

           int _i = i;

           i = (_i + minNum);

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

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

         }

       }

     }

@@ -73,10 +78,14 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       {

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

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

-        if (((maxNum).intValue() != 0)) {

-          int forLimit = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum));

-          this.getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false);

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

+        Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_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 + (maxNum).intValue()) - minNum));

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

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

         }

       }

     }

@@ -95,9 +104,11 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     }

   }

   

-  protected void getInstanceConstants(final int numElems, final int init, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean addToTrace) {

-    list.clear();

-    for (int i = init; (i < numElems); i++) {

+  protected void getInstanceConstants(final int endInd, final int startInd, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean clear, final boolean addToTrace) {

+    if (clear) {

+      list.clear();

+    }

+    for (int i = startInd; (i < endInd); i++) {

       {

         final int num = (i + 1);

         VLSConstant _createVLSConstant = this.factory.createVLSConstant();

@@ -113,7 +124,18 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     }

   }

   

-  protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final String name) {

+  protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) {

+    String nm = "";

+    VLSFunction tm = null;

+    if ((type == null)) {

+      nm = "object";

+      tm = this.support.topLevelTypeFunc();

+    } else {

+      nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString();

+      tm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate));

+    }

+    final String name = nm;

+    final VLSFunction term = tm;

     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

       String _xifexpression = null;

@@ -146,8 +168,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
               return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_4);

             };

             it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_3)));

-            it_2.setRight(this.support.topLevelTypeFunc());

+            it_2.setRight(term);

           } else {

+            it_2.setLeft(term);

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

               VLSEquality _createVLSEquality = this.factory.createVLSEquality();

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

@@ -162,7 +185,6 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
               return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5);

             };

             it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4)));

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

           }

         };

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