Add to containment, add notObject case.

4 files changed, 154 insertions, 47 deletions

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 ff5a192e..820d0db2 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
@@ -1,16 +1,19 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

 

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

+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.VampireLanguageFactory

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation

-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy

-import java.util.List

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy

+import java.util.HashMap

+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.RelationDeclaration

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference

 

 class Logic2VampireLanguageMapper_ContainmentMapper {

         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

@@ -74,54 +77,121 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
                 // for each edge, if the pointedTo element exists,the edge must exist also

                 val varA = createVLSVariable => [it.name = "A"]

                 val varB = createVLSVariable => [it.name = "B"]

+                val varC = createVLSVariable => [it.name = "C"]

                 val varList = newArrayList(varB, varA)

-

+                val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap

                 for (l : relationsList) {

-                        val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString

-                        val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type

-                        val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type

+                        val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)

+//                      val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type

+                        val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type)

+                        val toFunc = toType.lookup(trace.type2Predicate)

+

+                        addToMap(type2cont, toFunc, rel)

 

-                        val listForAnd = newArrayList

-//                      listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB))

-                        listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList))

+                        for (c : toType.subtypes) {

+                                addToMap(type2cont, toFunc, rel)

+                        }

+

+//                      val listForAnd = newArrayList

+////                    listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB))

+//                      listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList))

 //                      listForAnd.add(createVLSInequality => [

 //                              it.left = support.duplicate(varA)

 //                              it.right = support.duplicate(varB)

 //                      ])

+                        // remove subtypes of elements being pointed to

+//                      var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type

+//                      containmentListCopy.remove(pointingTo)

+//                      for (c : pointingTo.subtypes) {

+//                              containmentListCopy.remove(c)

+//                      }

+                        // STEP 3

+                        // Ensure that an objct only has 1 parent

+                        val relFormula = createVLSFofFormula => [

+                                it.name = support.toIDMultiple("noDupCont", rel.constant.toString)

+                                it.fofRole = "axiom"

+                                it.fofFormula = createVLSExistentialQuantifier => [

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

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

+                                        it.operand = createVLSImplies => [

+                                                it.left = support.duplicate(rel, newArrayList(varA, varB))

+                                                it.right = createVLSUnaryNegation => [

+                                                        it.operand = createVLSExistentialQuantifier => [

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

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

+                                                                it.operand = support.duplicate(rel, newArrayList(varC, varB))

+

+                                                        ]

+                                                ]

+                                        ]

+                                ]

+                        ]

+                        trace.specification.formulas += relFormula

 

+                }

+

+// STEP  CONT'D

+                for (e : type2cont.entrySet) {

                         val relFormula = createVLSFofFormula => [

-                                it.name = support.toIDMultiple("containment", relName)

+                                it.name = support.toIDMultiple("containment", e.key.constant.toString)

                                 it.fofRole = "axiom"

 

                                 it.fofFormula = createVLSUniversalQuantifier => [

                                         it.variables += support.duplicate(varA)

                                         it.operand = createVLSImplies => [

-                                                it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA)

+                                                it.left = support.duplicate(e.key, varA)

                                                 it.right = createVLSExistentialQuantifier => [

                                                         it.variables += support.duplicate(varB)

-                                                        it.operand = support.unfoldAnd(listForAnd)

-                                                ]

+                                                        if (e.value.length > 1) {

+                                                                it.operand = makeUnique(e.value)

+                                                        } else {

+                                                                it.operand = e.value.get(0)

+                                                        }

 

-                                                createVLSEquality => [

-                                                        it.left = support.duplicate(variable)

-                                                        it.right = createVLSConstant => [

-                                                                it.name = "o1"

-                                                        ]

                                                 ]

                                         ]

                                 ]

                         ]

                         trace.specification.formulas += relFormula

-                        var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type

-                        containmentListCopy.remove(pointingTo)

-                        for (c : pointingTo.subtypes) {

-                                containmentListCopy.remove(c)

-                        }

+

                 }

 

-        // STEP 3

-        // Ensure that an objct only has 1 parent

         // STEP 4

         // Ensure that there are no cycles in the hierarchy (maybe same as for step3?)

         }

+

+        protected def VLSTerm makeUnique(List<VLSFunction> list) {

+                val List<VLSTerm> possibleNots = newArrayList

+                val List<VLSTerm> uniqueRels = newArrayList

+

+                for (t1 : list) {

+                        for (t2 : list) {

+                                if (t1 == t2) {

+                                        val fct = support.duplicate(t2)

+                                        possibleNots.add(fct)

+                                } else {

+                                        val op = support.duplicate(t2)

+                                        val negFct = createVLSUnaryNegation => [

+                                                it.operand = op

+                                        ]

+                                        possibleNots.add(negFct)

+                                }

+                        }

+                        uniqueRels.add(support.unfoldAnd(possibleNots))

+                        possibleNots.clear

+                }

+                return support.unfoldOr(uniqueRels)

+        }

+

+        protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) {

+                if (!type2cont.containsKey(toFunc)) {

+                        type2cont.put(toFunc, newArrayList(rel))

+                } else {

+                        if (!type2cont.get(toFunc).contains(rel)) {

+                                type2cont.get(toFunc).add(rel)

+                        // type2cont.replace(toFunc, newArrayList(firstRel))

+                        }

+

+                }

+        }

 }

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 548deda4..bc87d3b7 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
@@ -38,10 +38,10 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                 // Handling Minimum_General

                 if (GLOBAL_MIN != 0) {

                         getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false)

-                        for(i : trace.uniqueInstances){

+                        for (i : trace.uniqueInstances) {

                                 localInstances.add(support.duplicate(i))

                         }

-                        

+

                         makeFofFormula(localInstances, trace, true, null)

                 }

 

@@ -83,14 +83,15 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

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

+                        for (e : trace.uniqueInstances) {

+                                val uniqueness = createVLSFofFormula => [

+                                        it.name = support.toIDMultiple("t_uniqueness", e.name)

+                                        it.fofRole = "axiom"

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

+                                ]

+                                trace.specification.formulas += uniqueness

+                        }

                 }

-

         }

 

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

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 8d00d3e7..d1ea2a15 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
@@ -92,7 +92,7 @@ class Logic2VampireLanguageMapper_Support {
                         ]
                 ]
         }
-        
+
         def protected VLSFunction topLevelTypeFunc(VLSVariable v) {
                 return createVLSFunction => [
                         it.constant = "object"
@@ -108,15 +108,26 @@ class Logic2VampireLanguageMapper_Support {
         }
 
         // TODO Make more general
-        def establishUniqueness(List<VLSConstant> terms) {
+        def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) {
+//              val List<VLSInequality> eqs = newArrayList
+//              for (t1 : terms.subList(1, terms.length)) {
+//                      for (t2 : terms.subList(0, terms.indexOf(t1))) {
+//                              val eq = createVLSInequality => [
+//                                      // TEMP
+//                                      it.left = createVLSConstant => [it.name = t2.name]
+//                                      it.right = createVLSConstant => [it.name = t1.name]
+//                              // TEMP
+//                              ]
+//                              eqs.add(eq)
+//                      }
+//              }
+//              return unfoldAnd(eqs)
                 val List<VLSInequality> eqs = newArrayList
-                for (t1 : terms.subList(1, terms.length)) {
-                        for (t2 : terms.subList(0, terms.indexOf(t1))) {
+                for (t1 : terms) {
+                        if (t1 != t2) {
                                 val eq = createVLSInequality => [
-                                        // TEMP
                                         it.left = createVLSConstant => [it.name = t2.name]
                                         it.right = createVLSConstant => [it.name = t1.name]
-                                // TEMP
                                 ]
                                 eqs.add(eq)
                         }
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 4c4247ce..1719bbcc 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
@@ -91,13 +91,12 @@ class Logic2VampireLanguageMapper_TypeMapper {
                                                         it.right = support.unfoldOr(typeDefs)
                                                 ]
 //                                              it.right = support.unfoldOr((typeDefs))
-
                                         ]
                                 ]
                         ]
                         trace.specification.formulas += res
 
-                        for (var i = globalCounter; i < globalCounter+type.elements.length; i++) {
+                        for (var i = globalCounter; i < globalCounter + type.elements.length; i++) {
                                 // Create objects for the enum elements
                                 val num = i + 1
                                 val cstTerm = createVLSFunctionAsTerm => [
@@ -127,7 +126,7 @@ class Logic2VampireLanguageMapper_TypeMapper {
                                 trace.specification.formulas += enumScope
 
                         }
-                        globalCounter+=type.elements.size
+                        globalCounter += type.elements.size
                 }
 
                 // HIERARCHY HANDLER
@@ -148,9 +147,35 @@ class Logic2VampireLanguageMapper_TypeMapper {
 //                      typeTrace.type2PossibleNot.clear
                         trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values)))
                         trace.type2PossibleNot.clear
+
+                }
+
+                // 4. case where an object is not an object
+                val List<VLSTerm> type2Not = newArrayList
+                
+                for(t : types) {
+                        type2Not.add(createVLSUnaryNegation => [
+                                it.operand = support.duplicate(t.lookup(trace.type2Predicate))
+                        ])
                 }
 
-                // 5. create fof function that is an or with all the elements in map
+                val notObj = createVLSFofFormula => [
+                        it.name = "notObjectHandler"
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                it.variables += support.duplicate(variable)
+                                it.operand = createVLSEquivalent => [
+                                        it.left = createVLSUnaryNegation => [
+                                                it.operand = support.topLevelTypeFunc
+                                        ]
+                                        it.right = support.unfoldAnd(type2Not)
+                                ]
+                        ]
+                ]
+
+                trace.specification.formulas += notObj
+
+                // 4. create fof function that is an or with all the elements in map
                 val hierarch = createVLSFofFormula => [
                         it.name = "inheritanceHierarchyHandler"
                         it.fofRole = "axiom"