4 files changed, 79 insertions, 16 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
index 3c672f4b..22bd4ab5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
@@ -1,5 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
@@ -13,6 +14,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
 import java.util.HashMap
+import java.util.List
 import java.util.Map
 
 interface Logic2VampireLanguageMapper_TypeMapperTrace {}
@@ -32,6 +34,9 @@ class Logic2VampireLanguageMapperTrace {
         public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap
         public val Map<Type, VLSTerm> type2PossibleNot = new HashMap
         public val Map<Type, VLSTerm> type2And = new HashMap
+        //Uniqueness
+        public val List<VLSConstant> uniqueInstances = newArrayList
+        
         
         public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions
         public var Map<RelationDeclaration, RelationDefinition> relationDefinitions
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 4b7ea3d0..e5dfbf08 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
@@ -19,13 +19,14 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                 val VLSVariable variable = createVLSVariable => [it.name = "A"]

 

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

-                val List<VLSConstant> instances = newArrayList

+                val localInstances = newArrayList

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

                         val num = i + 1

                         val cst = createVLSConstant => [

                                 it.name = "o" + num

                         ]

-                        instances.add(cst)

+                        trace.uniqueInstances.add(cst)

+                        localInstances.add(cst)

                 }

 

                 // TODO: specify for the max

@@ -37,14 +38,14 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                                 it.fofFormula = createVLSUniversalQuantifier => [

                                         it.variables += support.duplicate(variable)

                                         // check below

-                                        it.operand = createVLSEquivalent => [

-                                                it.left = support.topLevelTypeFunc

-                                                it.right = support.unfoldOr(instances.map [ i |

+                                        it.operand = createVLSImplies => [

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

                                                         createVLSEquality => [

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

                                                                 it.right = i

                                                         ]

                                                 ])

+                                                it.right = support.topLevelTypeFunc

                                         ]

                                 ]

                         ]

@@ -55,7 +56,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                         val uniqueness = createVLSFofFormula => [

                                 it.name = "typeUniqueness"

                                 it.fofRole = "axiom"

-                                it.fofFormula = support.establishUniqueness(instances)

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

                         ]

                         trace.specification.formulas += uniqueness

                 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index d3595a73..021cb0ea 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -2,6 +2,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
@@ -36,6 +37,14 @@ class Logic2VampireLanguageMapper_Support {
         def protected VLSVariable duplicate(VLSVariable term) {
                 return createVLSVariable => [it.name = term.name]
         }
+        
+        def protected VLSFunctionAsTerm duplicate(VLSFunctionAsTerm term) {
+                return createVLSFunctionAsTerm => [it.functor = term.functor]
+        }
+        
+        def protected VLSConstant duplicate(VLSConstant term) {
+                return createVLSConstant => [it.name = term.name]
+        }
 
         def protected VLSFunction duplicate(VLSFunction term) {
                 return createVLSFunction => [
@@ -52,6 +61,19 @@ class Logic2VampireLanguageMapper_Support {
                         it.terms += duplicate(v)
                 ]
         }
+        
+        def protected VLSFunction duplicate(VLSFunction term, VLSFunctionAsTerm v) {
+                return createVLSFunction => [
+                        it.constant = term.constant
+                        it.terms += duplicate(v)
+                ]
+        }
+        
+        def protected VLSConstant toConstant(VLSFunctionAsTerm term) {
+                return createVLSConstant => [
+                        it.name = term.functor
+                ]
+        }
 
         def protected VLSFunction topLevelTypeFunc() {
                 return createVLSFunction => [
@@ -61,6 +83,13 @@ class Logic2VampireLanguageMapper_Support {
                         ]
                 ]
         }
+        
+        def protected VLSFunction topLevelTypeFunc(VLSFunctionAsTerm v) {
+                return createVLSFunction => [
+                        it.constant = "object"
+                        it.terms += duplicate(v)
+                ]
+        }
 
         // TODO Make more general
         def establishUniqueness(List<VLSConstant> terms) {
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 bc0b3e23..f2a7b3f2 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
@@ -14,8 +14,9 @@ import java.util.Collection
 import java.util.List
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import java.util.Collections
 
-class Logic2VampireLanguageMapper_TypeMapper  {
+class Logic2VampireLanguageMapper_TypeMapper {
         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
         private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
         val Logic2VampireLanguageMapper base
@@ -25,8 +26,9 @@ class Logic2VampireLanguageMapper_TypeMapper  {
                 this.base = base
         }
 
-        def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
-                
+        def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements,
+                Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
+
 //              val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
 //              trace.typeMapperTrace = typeTrace
                 val VLSVariable variable = createVLSVariable => [it.name = "A"]
@@ -86,14 +88,38 @@ class Logic2VampireLanguageMapper_TypeMapper  {
 
                         ]
                         trace.specification.formulas += res
+
+                        // Create objects for the enum elements
+                        val List<VLSFunction> enumScopeElems = newArrayList
+                        for (var i = 0; i < type.elements.length; i++) {
+                                val num = i + 1
+                                val cstTerm = createVLSFunctionAsTerm => [
+                                        it.functor = "eo" + num
+                                ]
+                                val cst = support.toConstant(cstTerm)
+                                trace.uniqueInstances.add(cst)
+                                val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm)
+                                enumScopeElems.add(fct)
+//                              enumScopeElems.add(support.topLevelTypeFunc(cstTerm))
+                        }
+                        
+                        
+                        
+                        val enumScope = createVLSFofFormula => [
+                                it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0))
+                                // below is temporary solution
+                                it.fofRole = "axiom"                    
+                                it.fofFormula = support.unfoldAnd(enumScopeElems)
+                        ]
+                        
+                        trace.specification.formulas += enumScope
                 }
-                
-                //HIERARCHY HANDLER
-                
-                
+
+                // HIERARCHY HANDLER
                 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
                 // and store in a map
-                for (t1 : types.filter[!isIsAbstract]) {
+//              println(types.filter[!isIsAbstract])
+                for (t1 : types.filter[!isIsAbstract].filter(TypeDeclaration)) {
                         for (t2 : types) {
                                 // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
                                 if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
@@ -121,7 +147,9 @@ class Logic2VampireLanguageMapper_TypeMapper  {
                                 it.operand = createVLSEquivalent => [
                                         it.left = support.topLevelTypeFunc
 //                                      it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
-                                        it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values))
+                                        val reversedList = new ArrayList<VLSTerm>(trace.type2And.values)
+//                                      Collections.reverse(reversedList)
+                                        it.right = support.unfoldOr(reversedList)
                                 ]
                         ]
                 ]
@@ -130,7 +158,7 @@ class Logic2VampireLanguageMapper_TypeMapper  {
 
         }
 
-        //below are from previous interface
+        // below are from previous interface
         def protected transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
                 Logic2VampireLanguageMapperTrace trace) {
                 throw new UnsupportedOperationException("TODO: auto-generated method stub")