Closes #34, adds code to test cases where minScope>maxScope.

4 files changed, 60 insertions, 19 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 820d0db2..48ee8789 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
@@ -27,7 +27,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 

         def public void transformContainment(List<ContainmentHierarchy> hierarchies,

                 Logic2VampireLanguageMapperTrace trace) {

-

+                //TODO throw error is there exists a circular containment that does not involve hierarchy

                 // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST

                 // TEMP

                 val hierarchy = hierarchies.get(0)

@@ -91,6 +91,9 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
                         for (c : toType.subtypes) {

                                 addToMap(type2cont, toFunc, rel)

                         }

+//                      for (c : support.listSubtypes(toType)) {

+//                              addToMap(type2cont, toFunc, rel)

+//                      }

 

 //                      val listForAnd = newArrayList

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

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 bc87d3b7..54fcdc86 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
@@ -24,11 +24,12 @@ class Logic2VampireLanguageMapper_ScopeMapper {
         }

 

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

+                val ABSOLUTE_MIN = 0

+                val ABSOLUTE_MAX = Integer.MAX_VALUE

 

 //              TODO HANDLE ERRORS RELATED TO MAX > MIN

 //              TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS

 //              TODO HANDLE 

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

@@ -36,19 +37,30 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                 val localInstances = newArrayList

 

                 // Handling Minimum_General

-                if (GLOBAL_MIN != 0) {

+                if (GLOBAL_MIN != ABSOLUTE_MIN) {

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

                         for (i : trace.uniqueInstances) {

                                 localInstances.add(support.duplicate(i))

                         }

 

                         makeFofFormula(localInstances, trace, true, null)

+

+//                      //For testing Min>Max scope

+//                      getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, true)

+//                      makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null)

+//                      //end for testing

+

                 }

 

                 // Handling Maximum_General

-                if (GLOBAL_MAX != 0) {

+                if (GLOBAL_MAX != ABSOLUTE_MAX) {

                         getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true)

                         makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)

+

+//                      //For testing Min>Max scope

+//                      getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, false)

+//                      makeFofFormula(localInstances, trace, false, null)

+//                      //end for testing

                 }

 

                 // Handling Minimum_Specific

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 d1ea2a15..b00dad42 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
@@ -23,7 +23,7 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 class Logic2VampireLanguageMapper_Support {
         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
 
-        // ID Handler
+// ID Handler
         def protected String toIDMultiple(String... ids) {
                 ids.map[it.split("\\s+").join("_")].join("_")
         }
@@ -32,8 +32,8 @@ class Logic2VampireLanguageMapper_Support {
                 ids.split("\\s+").join("_")
         }
 
-        // Term Handling
-        // TODO Make more general
+// Term Handling
+// TODO Make more general
         def protected VLSVariable duplicate(VLSVariable term) {
                 return createVLSVariable => [it.name = term.name]
         }
@@ -107,7 +107,7 @@ class Logic2VampireLanguageMapper_Support {
                 ]
         }
 
-        // TODO Make more general
+// TODO Make more general
         def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) {
 //              val List<VLSInequality> eqs = newArrayList
 //              for (t1 : terms.subList(1, terms.length)) {
@@ -135,9 +135,9 @@ class Logic2VampireLanguageMapper_Support {
                 return unfoldAnd(eqs)
         }
 
-        // Support Functions
-        // booleans
-        // AND and OR
+// Support Functions
+// booleans
+// AND and OR
         def protected VLSTerm unfoldAnd(List<? extends VLSTerm> operands) {
                 if (operands.size == 1) {
                         return operands.head
@@ -163,7 +163,7 @@ class Logic2VampireLanguageMapper_Support {
                         throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP
         }
 
-        // can delete below
+// can delete below
         def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands,
                 Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
                 if (operands.size == 1) {
@@ -183,8 +183,8 @@ class Logic2VampireLanguageMapper_Support {
                         throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
         }
 
-        // Symbolic
-        // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) {
+// Symbolic
+// def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) {
 //              if(type instanceof BoolTypeReference) {
 //                      return booleanToLogicValue(term ,trace)
 //              }
@@ -198,7 +198,7 @@ class Logic2VampireLanguageMapper_Support {
          *      ids.map[it.split("\\s+").join("'")].join("'")
          * }
          */
-        // QUANTIFIERS + VARIABLES
+// QUANTIFIERS + VARIABLES
         def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper,
                 QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables,
                 boolean isUniversal) {
@@ -245,6 +245,32 @@ class Logic2VampireLanguageMapper_Support {
                         }
                 }
         }
+        //TODO rewrite such that it uses "listSubTypes"
+        def protected boolean dfsSubtypeCheck(Type type, Type type2) {
+                // There is surely a better way to do this
+                if (type.subtypes.isEmpty)
+                        return false
+                else {
+                        if (type.subtypes.contains(type2))
+                                return true
+                        else {
+                                for (subtype : type.subtypes) {
+                                        if(dfsSubtypeCheck(subtype, type2)) return true
+                                }
+                        }
+                }
+        }
+
+        def protected List<Type> listSubtypes(Type t) {
+                var List<Type> allSubtypes = newArrayList
+                if (!t.subtypes.isEmpty) {
+                        for (subt : t.subtypes) {
+                                allSubtypes.add(subt)
+                                allSubtypes = listSubtypes(subt)
+                        }
+                }
+                return allSubtypes
+        }
 
         def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) {
                 new HashMap(map1) => [putAll(map2)]
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 1719bbcc..3bc945df 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
@@ -150,10 +150,10 @@ class Logic2VampireLanguageMapper_TypeMapper {
 
                 }
 
-                // 4. case where an object is not an object
+                // 3.5: case where an object is not an object
                 val List<VLSTerm> type2Not = newArrayList
-                
-                for(t : types) {
+
+                for (t : types) {
                         type2Not.add(createVLSUnaryNegation => [
                                 it.operand = support.duplicate(t.lookup(trace.type2Predicate))
                         ])
@@ -174,7 +174,7 @@ class Logic2VampireLanguageMapper_TypeMapper {
                 ]
 
                 trace.specification.formulas += notObj
-
+                // End 3.5
                 // 4. create fof function that is an or with all the elements in map
                 val hierarch = createVLSFofFormula => [
                         it.name = "inheritanceHierarchyHandler"