VAMPIRE: add to #40. I am tired

4 files changed, 71 insertions, 15 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 22bd4ab5..b9928383 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
@@ -30,6 +30,8 @@ class Logic2VampireLanguageMapperTrace {
         //Necessary containers
         public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace
         
+        public var Map<DefinedElement, String> definedElement2String = new HashMap
+        
         public val Map<Type, VLSFunction> type2Predicate = new HashMap;
         public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap
         public val Map<Type, VLSTerm> type2PossibleNot = new HashMap
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
index 8e0e0b11..c56b54be 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
@@ -14,10 +14,11 @@ import java.util.List
 import java.util.Map

 

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

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

 

 class Logic2VampireLanguageMapper_ContainmentMapper {

-        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

-        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support

+        val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

+        val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support

         val Logic2VampireLanguageMapper base

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

 

@@ -34,6 +35,8 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 

                 val containmentListCopy = hierarchy.typesOrderedInHierarchy

                 val relationsList = hierarchy.containmentRelations

+                val toRemove = newArrayList

+                

                 // STEP 1

                 // Find root element

                 for (l : relationsList) {

@@ -46,16 +49,51 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
                         }

                 }

                 

-                for (c : containmentListCopy) {

-                        if(c.isIsAbstract) {

-                                containmentListCopy.remove(c)

-                        }

-                }

-

+//              OLD

+//              for (c : containmentListCopy) {

+//                      if(c.isIsAbstract) {

+//                              toRemove.add(c)

+//                      }

+//              }

                 // State that there must exist 1 and only 1 root element

-                val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString

-                val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))

+//              val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString

+//              val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))

 

+                var topTermVar = containmentListCopy.get(0)

+                for (l : relationsList) {

+                        var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type

+                        if(containmentListCopy.contains(pointingFrom)) {

+                                //The correct topTerm will be identified

+                                topTermVar = pointingFrom

+                        }

+                }

+                

+                val topName = topTermVar.lookup(trace.type2Predicate).constant.toString

+                val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate))

+                

+                

+                

+                var topLvlIsInInitModel = false

+                var topLvlString = ""

+                for ( c : topTermVar.subtypes) {

+                        if (c.class.simpleName.equals("TypeDefinitionImpl") ) {
+                                

+                                for (d : (c as TypeDefinition).elements) {
+                                if (trace.definedElement2String.containsKey(d)) {

+                                        topLvlIsInInitModel = true

+                                        topLvlString = d.lookup(trace.definedElement2String)

+                                }

+                        }

+                        
+                        }

+                        

+                        

+                }

+                val topInIM = topLvlIsInInitModel

+                val topStr = topLvlString

+                print(topInIM)

+                print(topStr)

+                

                 val contTop = createVLSFofFormula => [

                         it.name = support.toIDMultiple("containment_topLevel", topName)

                         it.fofRole = "axiom"

@@ -67,7 +105,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
                                         it.right = createVLSEquality => [

                                                 it.left = support.duplicate(variable)

                                                 it.right = createVLSConstant => [

-                                                        it.name = "o1"

+                                                        it.name = if (topInIM) topStr else "o1"

                                                 ]

                                         ]

                                 ]

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 4a8d2827..c50aa770 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
@@ -30,6 +30,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 //              TODO HANDLE 

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

                 //These numbers do not include enums or initial model elements

+                

                 val GLOBAL_MIN = config.typeScopes.minNewElements

                 val GLOBAL_MAX = config.typeScopes.maxNewElements

 

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 2f3af593..2a121446 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
@@ -33,14 +33,24 @@ class Logic2VampireLanguageMapper_TypeMapper {
                 // 1. Each type (class) is a predicate with a single variable as input
                 for (type : types) {
                         val typePred = createVLSFunction => [
-                                it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
+                                if(type.name.split(" ").length == 3) {
+                                        it.constant = support.toIDMultiple("t", type.name.split(" ").get(0), type.name.split(" ").get(2))
+                                }
+                                else {
+                                        it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
+                                }
                                 it.terms += support.duplicate(variable)
                         ]
                         trace.type2Predicate.put(type, typePred)
                 }
 
                 // 2. Map each ENUM type definition to fof formula
+                //    This also Handles initial Model stuff
                 for (type : types.filter(TypeDefinition)) {
+                        
+                        //Detect if is an Enum
+                        //Otherwise, it is a defined element (from initial model)
+                        val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract
 
                         // Create a VLSFunction for each Enum Element
                         val List<VLSFunction> orElems = newArrayList
@@ -104,15 +114,20 @@ class Logic2VampireLanguageMapper_TypeMapper {
                         for (var i = globalCounter; i < globalCounter + type.elements.length; i++) {
                                 // Create objects for the enum elements
                                 val num = i + 1
+                                val index = i-globalCounter
+                                
                                 val cstTerm = createVLSFunctionAsTerm => [
                                         it.functor = "eo" + num
                                 ]
+                                if (isNotEnum) {
+                                        trace.definedElement2String.put(type.elements.get(index),cstTerm.functor)
+                                }
+                                
                                 val cst = support.toConstant(cstTerm)
                                 trace.uniqueInstances.add(cst)
-
-                                val index = i-globalCounter
+                                
                                 val enumScope = createVLSFofFormula => [
-                                        it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString,
+                                        it.name = support.toIDMultiple(if(isNotEnum) "definedType" else "enumScope", type.lookup(trace.type2Predicate).constant.toString,
                                                 type.elements.get(index).name.split(" ").get(0))
                                         it.fofRole = "axiom"
                                         it.fofFormula = createVLSUniversalQuantifier => [