Improve TypeScope handling

33 files changed, 231 insertions, 114 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
index 059cb511..a357265a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
index 3c6361f3..d51853b3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
index e00e853c..ac749133 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
index 6f5209e7..c4d049d4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
index 4ff50857..6c21f595 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
index bce7ab42..be25b151 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
index b6c23926..ce399e1c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
index 19d1d4f6..e279fc45 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
index 834a13c3..9abf8fdb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
index 279b2fbb..2b114f57 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
index 6895f687..5f2366b0 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
index 66b7827f..d0414079 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
index 5bac2912..56e0771f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
index 7cafc3c7..8ac45333 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml
index 95881b26..2381b84f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml
@@ -1,18 +1 @@
-<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.4"?><plugin>

-  <extension id="ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries" point="org.eclipse.viatra.query.runtime.queryspecification">

-    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries" id="ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries">

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSComment"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSFofFormula"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSAnnotation"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSOr"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSAnd"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSEquivalent"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSFunction"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSExistentialQuantifier"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSUniversalQuantifier"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSUnaryNegation"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSInequality"/>

-      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSFunctionFof"/>

-    </group>

-  </extension>

-</plugin>

+<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.4"?><plugin/>

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index deb24778..0ae06bc3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -7,6 +7,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
 import java.util.ArrayList
 import java.util.HashMap
@@ -43,7 +44,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
                 }
 
-                val comply = createVLSFofFormula => [
+                val comply = createVLSFofFormula=> [
                         val nameArray = r.name.split(" ")
                         it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2))
                         it.fofRole = "axiom"
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 e5dfbf08..2da4cfd7 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
@@ -5,60 +5,124 @@ 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 java.util.ArrayList

+

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

 

 class Logic2VampireLanguageMapper_ScopeMapper {

         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

         private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support

         val Logic2VampireLanguageMapper base

+        private val VLSVariable variable = createVLSVariable => [it.name = "A"]

 

         public new(Logic2VampireLanguageMapper base) {

                 this.base = base

         }

 

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

-                val VLSVariable variable = createVLSVariable => [it.name = "A"]

 

+//              HANDLE ERRORS RELATED TO MAX > MIN

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

+//              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

+

                 val localInstances = newArrayList

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

+

+                // Handling Minimum_General

+                if (GLOBAL_MIN != 0) {

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

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

+                }

+

+                // Handling Maximum_General

+                if (GLOBAL_MAX != 0) {

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

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

+                }

+

+                // Handling Minimum_Specific

+                var i = 0

+                var minNum = -1

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

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

+                        if (minNum != 0) {

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

+                                i += minNum

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

+                        }

+                }

+

+                //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

+                        }

+                }

+

+                // 3. Specify uniqueness of elements

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

+                        val uniqueness = createVLSFofFormula => [

+                                it.name = "typeUniqueness"

+                                it.fofRole = "axiom"

+                                it.fofFormula = support.establishUniqueness(trace.uniqueInstances)

+                        ]

+                        trace.specification.formulas += uniqueness

+                }

+

+        }

+

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

+                Logic2VampireLanguageMapperTrace trace, boolean addToTrace) {

+                list.clear

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

                         val num = i + 1

                         val cst = createVLSConstant => [

                                 it.name = "o" + num

                         ]

-                        trace.uniqueInstances.add(cst)

-                        localInstances.add(cst)

+                        if (addToTrace) {

+                                trace.uniqueInstances.add(cst)

+                        }

+                        list.add(cst)

                 }

+        }

 

-                // TODO: specify for the max

-                if (config.typeScopes.minNewElements != 0) {

-                        // 2. Create initial fof formula to specify the number of elems

-                        val cstDec = createVLSFofFormula => [

-                                it.name = "typeScope"

-                                it.fofRole = "axiom"

-                                it.fofFormula = createVLSUniversalQuantifier => [

-                                        it.variables += support.duplicate(variable)

-                                        // check below

-                                        it.operand = createVLSImplies => [

-                                                it.left = support.unfoldOr(localInstances.map [ i |

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

+                val cstDec = createVLSFofFormula => [

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

+                        it.fofRole = "axiom"

+                        it.fofFormula = createVLSUniversalQuantifier => [

+                                it.variables += support.duplicate(variable)

+                                // check below

+                                it.operand = createVLSImplies => [

+                                        if (minimum) {

+                                                it.left = support.unfoldOr(list.map [ i |

                                                         createVLSEquality => [

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

                                                                 it.right = i

                                                         ]

                                                 ])

                                                 it.right = support.topLevelTypeFunc

-                                        ]

+                                        } else {

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

+                                                        createVLSEquality => [

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

+                                                                it.right = i

+                                                        ]

+                                                ])

+                                                it.left = support.topLevelTypeFunc

+                                        }

                                 ]

                         ]

-                        trace.specification.formulas += cstDec

-

-                        // TODO: specify for scope per type

-                        // 3. Specify uniqueness of elements

-                        val uniqueness = createVLSFofFormula => [

-                                it.name = "typeUniqueness"

-                                it.fofRole = "axiom"

-                                it.fofFormula = support.establishUniqueness(trace.uniqueInstances)

-                        ]

-                        trace.specification.formulas += uniqueness

-                }

+                ]

+                trace.specification.formulas += cstDec

         }

+

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
index ee6365dd..e12180fa 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
@@ -48,7 +48,13 @@ class Logic2VampireLanguageMapper_TypeMapper {
                         val List<VLSFunction> orElems = newArrayList
                         for (e : type.elements) {
                                 val enumElemPred = createVLSFunction => [
-                                        it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2))
+                                        val splitName = e.name.split(" ")
+                                        if( splitName.length > 2) {
+                                                it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2))
+                                        }
+                                        else {
+                                                it.constant = support.toIDMultiple("e", splitName.get(0))
+                                        }
                                         it.terms += support.duplicate(variable)
                                 ]
 //                              typeTrace.element2Predicate.put(e, enumElemPred)
@@ -63,26 +69,8 @@ class Logic2VampireLanguageMapper_TypeMapper {
                                 it.fofFormula = createVLSUniversalQuantifier => [
                                         it.variables += support.duplicate(variable)
                                         it.operand = createVLSEquivalent => [
-//                                              it.left = createVLSFunction => [
-//                                                      it.constant = type.lookup(typeTrace.type2Predicate).constant
-//                                                      it.terms += createVLSVariable => [it.name = "A"]
-//                                              ]
-//                                              it.left = type.lookup(typeTrace.type2Predicate)
                                                 it.left = type.lookup(trace.type2Predicate)
-
                                                 it.right = support.unfoldOr(orElems)
-
-                                        // TEMPPPPPPP
-//                                              it.right = support.unfoldOr(type.elements.map [e |
-//                                                      
-//                                                      createVLSEquality => [
-//                                                              it.left = support.duplicate(variable)
-//                                                              it.right = createVLSDoubleQuote => [
-//                                                                      it.value = "\"a" + e.name + "\""
-//                                                              ]
-//                                                      ]
-//                                              ])
-                                        // END TEMPPPPP
                                         ]
                                 ]
 
@@ -152,7 +140,7 @@ class Logic2VampireLanguageMapper_TypeMapper {
 
                 // 5. create fof function that is an or with all the elements in map
                 val hierarch = createVLSFofFormula => [
-                        it.name = "hierarchyHandler"
+                        it.name = "inheritanceHierarchyHandler"
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
                                 it.variables += support.duplicate(variable)
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 3f204913..5c634ba0 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 10983f27..19d48790 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 00ebca4b..2db39cf0 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 9641858d..1fba7ac4 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 2b51fe5d..9ef3a39c 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 75482abc..687f4889 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 c394f878..d59b2e98 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 1ec5da80..eb12e24a 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 8a6f30f9..70eb3434 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 c000d128..0077e151 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 5eb63977..62de24fc 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 501dbfb4..d00ac8ca 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 621c888a..b86330dc 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 15ba78c9..a412241a 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
@@ -12,9 +12,13 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

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

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

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

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

 import java.util.ArrayList;

+import java.util.Set;

 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.Functions.Function1;

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

@@ -30,76 +34,146 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
   

   private final Logic2VampireLanguageMapper base;

   

+  private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> {

+    it.setName("A");

+  }));

+  

   public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) {

     this.base = base;

   }

   

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

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

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

-      it.setName("A");

-    };

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

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

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

+    final int GLOBAL_MIN = config.typeScopes.minNewElements;

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

+    }

+    if ((GLOBAL_MAX != 0)) {

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

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

+    }

+    int i = 0;

+    int minNum = (-1);

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

+          int _i = i;

+          i = (_i + minNum);

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

+        }

+      }

+    }

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

+    for (final Type t_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();

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

+        }

+      }

+    }

+    int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length;

+    boolean _notEquals = (_length != 0);

+    if (_notEquals) {

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

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

+        it.setName("typeUniqueness");

+        it.setFofRole("axiom");

+        it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances));

+      };

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

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

+      _formulas.add(uniqueness);

+    }

+  }

+  

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

       {

         final int num = (i + 1);

         VLSConstant _createVLSConstant = this.factory.createVLSConstant();

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

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

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

         };

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

-        trace.uniqueInstances.add(cst);

-        localInstances.add(cst);

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

+        if (addToTrace) {

+          trace.uniqueInstances.add(cst);

+        }

+        list.add(cst);

       }

     }

-    if ((config.typeScopes.minNewElements != 0)) {

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

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

-        it.setName("typeScope");

-        it.setFofRole("axiom");

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

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

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

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

-          _variables.add(_duplicate);

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

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

+  }

+  

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

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

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

+      String _xifexpression = null;

+      if (minimum) {

+        _xifexpression = "min";

+      } else {

+        _xifexpression = "max";

+      }

+      it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name));

+      it.setFofRole("axiom");

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

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

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

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

+        _variables.add(_duplicate);

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

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

+          if (minimum) {

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

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

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

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

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

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

+                };

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

+                it_3.setLeft(_doubleArrow);

+                it_3.setRight(i);

+              };

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

+          } else {

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

               VLSEquality _createVLSEquality = this.factory.createVLSEquality();

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

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

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

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

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

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

                 };

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

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

                 it_3.setLeft(_doubleArrow);

                 it_3.setRight(i);

               };

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

             };

-            it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(localInstances, _function_4)));

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

-          };

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

-          it_1.setOperand(_doubleArrow);

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

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

+          }

         };

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

-        it.setFofFormula(_doubleArrow);

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

+        it_1.setOperand(_doubleArrow);

       };

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

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

-      _formulas.add(cstDec);

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

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

-        it.setName("typeUniqueness");

-        it.setFofRole("axiom");

-        it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances));

-      };

-      final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2);

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

-      _formulas_1.add(uniqueness);

-    }

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

+      it.setFofFormula(_doubleArrow);

+    };

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

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

+    _formulas.add(cstDec);

   }

   

   public void transformScope(final LogicSolverConfiguration config, 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_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 c101aa4c..b8d74f36 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,7 +78,14 @@ public class Logic2VampireLanguageMapper_TypeMapper {
             {

               VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

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

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

+                }

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

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

                 _terms.add(_duplicate);

@@ -175,7 +182,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
       }

       VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

-        it.setName("hierarchyHandler");

+        it.setName("inheritanceHierarchyHandler");

         it.setFofRole("axiom");

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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