Improve TypeScope handling

47 files changed, 268 insertions, 130 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) -> {

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi
new file mode 100644
index 00000000..cef17e1b
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi
@@ -0,0 +1,7 @@
+<?xml version="1.0" encoding="UTF-8"?>

+<functionalarchitecture:FunctionalArchitectureModel

+    xmi:version="2.0"

+    xmlns:xmi="http://www.omg.org/XMI"

+    xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"

+    xmlns:functionalarchitecture="http://www.inf.mit.bme.hu/viatrasolver/example/fam"

+    xsi:schemaLocation="http://www.inf.mit.bme.hu/viatrasolver/example/fam FAM/FamMetamodel.ecore"/>

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
index a3b9c865..f55667e4 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
@@ -1,9 +1,10 @@
 % This is an initial Test Comment

 fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) .

 fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( ~ e_Intermediate_FunctionType ( eo1 ) & ( ~ e_Leaf_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & ( ~ e_Root_FunctionType ( eo2 ) & ( ~ e_Leaf_FunctionType ( eo2 ) & ( e_Leaf_FunctionType ( eo3 ) & ( ~ e_Root_FunctionType ( eo3 ) & ~ e_Intermediate_FunctionType ( eo3 ) ) ) ) ) ) ) ) ) .

-fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalData ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & t_Function ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

-fof ( typeScope , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) => object ( A ) ) ) .

-fof ( typeUniqueness , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo2 != eo3 & ( eo1 != o1 & ( eo2 != o1 & ( eo3 != o1 & ( eo1 != o2 & ( eo2 != o2 & ( eo3 != o2 & ( o1 != o2 & ( eo1 != o3 & ( eo2 != o3 & ( eo3 != o3 & ( o1 != o3 & ( o2 != o3 & ( eo1 != o4 & ( eo2 != o4 & ( eo3 != o4 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( eo1 != o5 & ( eo2 != o5 & ( eo3 != o5 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

+fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( ~ t_FunctionType ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

+fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | A = o3 ) ) => object ( A ) ) ) .

+fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | A = o6 ) ) ) ) ) ) ) .

+fof ( typeUniqueness , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo2 != eo3 & ( eo1 != o1 & ( eo2 != o1 & ( eo3 != o1 & ( eo1 != o2 & ( eo2 != o2 & ( eo3 != o2 & ( o1 != o2 & ( eo1 != o3 & ( eo2 != o3 & ( eo3 != o3 & ( o1 != o3 & ( o2 != o3 & ( eo1 != o4 & ( eo2 != o4 & ( eo3 != o4 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( eo1 != o5 & ( eo2 != o5 & ( eo3 != o5 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & ( o4 != o5 & ( eo1 != o6 & ( eo2 != o6 & ( eo3 != o6 & ( o1 != o6 & ( o2 != o6 & ( o3 != o6 & ( o4 != o6 & o5 != o6 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

 fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .

 fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) .

 fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) .

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
index 95bfd87a..a9314376 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
@@ -23,12 +23,12 @@ class FAMTest {
                 println("Input and output workspaces are created")

 

                 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)

-                val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel2.xmi")

+                val partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi")

                 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)

 

                 println("DSL loaded")

                 

-                GeneralTest.createAndSolveProblem(metamodel, new LinkedList<EObject>, queries, workspace)       

+                GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace)  

         }

         

         

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
index 20ad6119..40e305aa 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
@@ -2,19 +2,23 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse
 

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration

-import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns

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

+import functionalarchitecture.Function

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration

+import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace

 import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel

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

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

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult

 import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic

-import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration

 import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic

 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace

 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace

+import java.util.HashMap

 import java.util.List

 import org.eclipse.emf.ecore.EAttribute

 import org.eclipse.emf.ecore.EClass

@@ -26,13 +30,12 @@ import org.eclipse.emf.ecore.EReference
 import org.eclipse.emf.ecore.resource.Resource

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl

 import org.eclipse.viatra.query.runtime.api.IQueryGroup

-import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver

-import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration

-import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel

+import org.eclipse.emf.ecore.EClassifier

 

 class GeneralTest {

         def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel,

                 ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) {

+                val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

                 val Ecore2Logic ecore2Logic = new Ecore2Logic

                 val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)

                 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)

@@ -52,10 +55,17 @@ class GeneralTest {
                 

                 //*

                 reasoner = new VampireSolver

+//              val typeMap = new HashMap<Type, Integer>

+//              val n = Function.simpleName

+//              val classif = factory.vampireLanguagePackage.getEClassifier(n) as EClass

+//              val x = ecore2Logic.TypeofEClass(modelGenerationProblem.trace, classif)

+//              typeMap.put(x, 3)

                 val vampireConfig = new VampireSolverConfiguration => [

                         // add configuration things, in config file first

                         it.documentationLevel = DocumentationLevel::FULL

-                        it.typeScopes.minNewElements = 5

+                        it.typeScopes.minNewElements = 3

+                        it.typeScopes.maxNewElements = 6

+//                      it.typeScopes.minNewElementsByType = typeMap

                 ]

                 solution = reasoner.solve(problem, vampireConfig, workspace)

                 

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
index c9fd4467..620541af 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
index 9ded2f72..38c38fcd 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
index 2c84c402..dbe2934c 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
index 120f7cbb..86f98ad3 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
index 8364a369..91e71b1b 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
index dd061008..7b4bb578 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
@@ -6,7 +6,6 @@ import functionalarchitecture.FunctionalarchitecturePackage;
 import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;

 import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor;

 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;

-import java.util.LinkedList;

 import java.util.Map;

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

 import org.eclipse.emf.ecore.EObject;

@@ -31,10 +30,9 @@ public class FAMTest {
     map.put("logicproblem", _xMIResourceFactoryImpl);

     InputOutput.<String>println("Input and output workspaces are created");

     final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE);

-    final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel2.xmi");

+    final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi");

     final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance());

     InputOutput.<String>println("DSL loaded");

-    LinkedList<EObject> _linkedList = new LinkedList<EObject>();

-    GeneralTest.createAndSolveProblem(metamodel, _linkedList, queries, workspace);

+    GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace);

   }

 }

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
index 5e4df399..c902bd10 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
@@ -2,6 +2,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse;
 

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

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

 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;

@@ -39,6 +40,7 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
 import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation;

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

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

+import org.eclipse.xtext.xbase.lib.Extension;

 import org.eclipse.xtext.xbase.lib.Functions.Function1;

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

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

@@ -52,6 +54,8 @@ public class GeneralTest {
     try {

       String _xblockexpression = null;

       {

+        @Extension

+        final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

         final Ecore2Logic ecore2Logic = new Ecore2Logic();

         final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic);

         final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);

@@ -68,7 +72,8 @@ public class GeneralTest {
         VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

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

           it.documentationLevel = DocumentationLevel.FULL;

-          it.typeScopes.minNewElements = 5;

+          it.typeScopes.minNewElements = 3;

+          it.typeScopes.maxNewElements = 6;

         };

         final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);

         solution = reasoner.solve(problem, vampireConfig, workspace);

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
index 3669124b..2fac977d 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
index a6a6e1b8..1c3ec2f4 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
index 71eec0ad..d479a2aa 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin