Datatypes with nested recursion are not handled in TheoryDatatypes unless option is set (#3707)

Towards experimental support for non-simply recursive datatypes (https://github.com/ajreynol/CVC4/tree/dtNonSimpleRec). Builds a check for non-simple recursion in the DType class. If a term of a datatype type is registered to TheoryDatatypes for a datatype that has nested recursion, we throw a LogicException unless the option dtNestedRec is set to true. Also includes a bug discovered in the TypeMatcher utility and another in expr::getComponentTypes.

It also adds a unit test using the new API for a simple parametric datatype example as well, not related to nested recursion, as this was previously missing.

10 files changed, 281 insertions, 18 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 164df0631..2c65f1ca6 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2191,6 +2191,10 @@ bool Datatype::isRecord() const { return d_dtype->isRecord(); }
 
 bool Datatype::isFinite() const { return d_dtype->isFinite(); }
 bool Datatype::isWellFounded() const { return d_dtype->isWellFounded(); }
+bool Datatype::hasNestedRecursion() const
+{
+  return d_dtype->hasNestedRecursion();
+}
 
 std::string Datatype::toString() const { return d_dtype->getName(); }
 
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 73e3ed856..adf3691ab 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1673,6 +1673,17 @@ class CVC4_PUBLIC Datatype
   bool isWellFounded() const;
 
   /**
+   * Does this datatype have nested recursion? This method returns false if a
+   * value of this datatype includes a subterm of its type that is nested
+   * beneath a non-datatype type constructor. For example, a datatype
+   * T containing a constructor having a selector with range type (Set T) has
+   * nested recursion.
+   *
+   * @return true if this datatype has nested recursion
+   */
+  bool hasNestedRecursion() const;
+
+  /**
    * @return a string representation of this datatype
    */
   std::string toString() const;
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 3925e1434..b33580b09 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -406,6 +406,12 @@ bool Datatype::isWellFounded() const
   return d_internal->isWellFounded();
 }
 
+bool Datatype::hasNestedRecursion() const
+{
+  ExprManagerScope ems(d_self);
+  return d_internal->hasNestedRecursion();
+}
+
 Expr Datatype::mkGroundTerm(Type t) const
 {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 0f99499ce..daef7cc94 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -705,6 +705,12 @@ class CVC4_PUBLIC Datatype {
    * This datatype must be resolved or an exception is thrown.
    */
   bool isWellFounded() const;
+  /** has nested recursion
+   *
+   * Return true iff this datatype has nested recursion.
+   * This datatype must be resolved or an exception is thrown.
+   */
+  bool hasNestedRecursion() const;
 
   /** is recursive singleton
    *
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index f16b193ce..ff9880b94 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -14,6 +14,7 @@
 #include "expr/dtype.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/type_matcher.h"
 
 using namespace CVC4::kind;
 
@@ -32,7 +33,8 @@ DType::DType(std::string name, bool isCo)
       d_sygusAllowConst(false),
       d_sygusAllowAll(false),
       d_card(CardinalityUnknown()),
-      d_wellFounded(0)
+      d_wellFounded(0),
+      d_nestedRecursion(0)
 {
 }
 
@@ -49,7 +51,8 @@ DType::DType(std::string name, const std::vector<TypeNode>& params, bool isCo)
       d_sygusAllowConst(false),
       d_sygusAllowAll(false),
       d_card(CardinalityUnknown()),
-      d_wellFounded(0)
+      d_wellFounded(0),
+      d_nestedRecursion(0)
 {
 }
 
@@ -471,21 +474,26 @@ bool DType::isInterpretedFinite() const
 
 bool DType::isWellFounded() const
 {
-  Trace("datatypes-init") << "DType::isWellFounded " << std::endl;
   Assert(isResolved());
-  if (d_wellFounded == 0)
+  if (d_wellFounded != 0)
   {
-    std::vector<TypeNode> processing;
-    if (computeWellFounded(processing))
-    {
-      d_wellFounded = 1;
-    }
-    else
-    {
-      d_wellFounded = -1;
-    }
+    // already computed
+    return d_wellFounded == 1;
   }
-  return d_wellFounded == 1;
+  Trace("datatypes-init") << "DType::isWellFounded " << getName() << std::endl;
+  std::vector<TypeNode> processing;
+  if (!computeWellFounded(processing))
+  {
+    // not well-founded since no ground term can be constructed
+    Trace("datatypes-init") << "DType::isWellFounded: false for " << getName()
+                            << " due to no ground terms." << std::endl;
+    d_wellFounded = -1;
+    return false;
+  }
+  Trace("datatypes-init") << "DType::isWellFounded: true for " << getName()
+                          << std::endl;
+  d_wellFounded = 1;
+  return true;
 }
 
 bool DType::computeWellFounded(std::vector<TypeNode>& processing) const
@@ -557,6 +565,137 @@ Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const
   return groundTerm;
 }
 
+void DType::getAlienSubfieldTypes(
+    std::unordered_set<TypeNode, TypeNodeHashFunction>& types,
+    std::map<TypeNode, bool>& processed,
+    bool isAlienPos) const
+{
+  std::map<TypeNode, bool>::iterator it = processed.find(d_self);
+  if (it != processed.end())
+  {
+    if (it->second || (!isAlienPos && !it->second))
+    {
+      // already processed as an alien subfield type, or already processed
+      // as a non-alien subfield type and isAlienPos is false.
+      return;
+    }
+  }
+  processed[d_self] = isAlienPos;
+  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    for (unsigned j = 0, nargs = ctor->getNumArgs(); j < nargs; ++j)
+    {
+      TypeNode tn = ctor->getArgType(j);
+      if (tn.isDatatype())
+      {
+        // special case for datatypes, we must recurse to collect subfield types
+        if (!isAlienPos)
+        {
+          // since we aren't adding it to types below, we add its alien
+          // subfield types here.
+          const DType& dt = tn.getDType();
+          dt.getAlienSubfieldTypes(types, processed, false);
+        }
+        if (tn.isParametricDatatype() && !isAlienPos)
+        {
+          // (instantiated) parametric datatypes have an AST structure:
+          //  (PARAMETRIC_DATATYPE D T1 ... Tn)
+          // where D is the uninstantiated datatype type.  We should not view D
+          // as an alien subfield type of tn. Thus, we need a special case here
+          // which ignores the first child, when isAlienPos is false.
+          for (unsigned i = 1, nchild = tn.getNumChildren(); i < nchild; i++)
+          {
+            expr::getComponentTypes(tn[i], types);
+          }
+          continue;
+        }
+      }
+      // we are in a case where tn is not a datatype, we add all (alien)
+      // component types to types below.
+      bool hasTn = types.find(tn) != types.end();
+      Trace("datatypes-init")
+          << "Collect subfield types " << tn << ", hasTn=" << hasTn
+          << ", isAlienPos=" << isAlienPos << std::endl;
+      expr::getComponentTypes(tn, types);
+      if (!isAlienPos && !hasTn)
+      {
+        // the top-level type is added by getComponentTypes, so remove it if it
+        // was not already listed in types
+        Assert(types.find(tn) != types.end());
+        types.erase(tn);
+      }
+    }
+  }
+  // Now, go back and add all alien subfield types from datatypes if
+  // not done so already. This is because getComponentTypes does not
+  // recurse into subfield types of datatypes.
+  for (const TypeNode& sstn : types)
+  {
+    if (sstn.isDatatype())
+    {
+      const DType& dt = sstn.getDType();
+      dt.getAlienSubfieldTypes(types, processed, true);
+    }
+  }
+}
+
+bool DType::hasNestedRecursion() const
+{
+  if (d_nestedRecursion != 0)
+  {
+    return d_nestedRecursion == 1;
+  }
+  Trace("datatypes-init") << "Compute simply recursive for " << getName()
+                          << std::endl;
+  // get the alien subfield types of this datatype
+  std::unordered_set<TypeNode, TypeNodeHashFunction> types;
+  std::map<TypeNode, bool> processed;
+  getAlienSubfieldTypes(types, processed, false);
+  if (Trace.isOn("datatypes-init"))
+  {
+    Trace("datatypes-init") << "Alien subfield types: " << std::endl;
+    for (const TypeNode& t : types)
+    {
+      Trace("datatypes-init") << "- " << t << std::endl;
+    }
+  }
+  // does types contain self?
+  if (types.find(d_self) != types.end())
+  {
+    Trace("datatypes-init")
+        << "DType::hasNestedRecursion: true for " << getName()
+        << " due to alien subfield type" << std::endl;
+    // has nested recursion since it has itself as an alien subfield type.
+    d_nestedRecursion = 1;
+    return true;
+  }
+  // If it is parametric, this type may match with an alien subfield type (e.g.
+  // we may have a field (T Int) for parametric datatype (T x) where x
+  // is a type parameter). Thus, we check whether the self type matches any
+  // alien subfield type using the TypeMatcher utility.
+  if (isParametric())
+  {
+    for (const TypeNode& t : types)
+    {
+      TypeMatcher m(d_self);
+      Trace("datatypes-init") << "  " << t << std::endl;
+      if (m.doMatching(d_self, t))
+      {
+        Trace("datatypes-init")
+            << "DType::hasNestedRecursion: true for " << getName()
+            << " due to parametric strict component type, " << d_self
+            << " matching " << t << std::endl;
+        d_nestedRecursion = 1;
+        return true;
+      }
+    }
+  }
+  Trace("datatypes-init") << "DType::hasNestedRecursion: false for "
+                          << getName() << std::endl;
+  d_nestedRecursion = -1;
+  return false;
+}
+
 Node getSubtermWithType(Node e, TypeNode t, bool isTop)
 {
   if (!isTop && e.getType() == t)
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index 08fe9965b..f9c4eff9c 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -287,6 +287,16 @@ class DType
    * violated.
    */
   bool isWellFounded() const;
+  /**
+   * Does this datatype have nested recursion? This is true if this datatype
+   * definition contains itself as an alien subfield type, or a variant
+   * of itself as an alien subfield type (if this datatype is parametric).
+   * For details see getAlienSubfieldTypes below.
+   *
+   * Notice that a type having no nested recursion may have a subfield type that
+   * has nested recursion.
+   */
+  bool hasNestedRecursion() const;
 
   /** is recursive singleton
    *
@@ -489,6 +499,51 @@ class DType
    * Helper for mkGroundTerm and mkGroundValue above.
    */
   Node mkGroundTermInternal(TypeNode t, bool isValue) const;
+  /**
+   * This method is used to get alien subfield types of this datatype.
+   *
+   * A subfield type T of a datatype type D is a type such that a value of
+   * type T may appear as a subterm of a value of type D.
+   *
+   * An *alien* subfield type T of a datatype type D is a type such that a
+   * value v of type T may appear as a subterm of a value of D, and moreover
+   * v occurs as a strict subterm of a non-datatype term in that value.
+   *
+   * For example, the alien subfield types of T in:
+   *   T -> Emp | Container(s : (Set List))
+   *   List -> nil | cons( head : Int, tail: List)
+   * are { List, Int }. Notice that Int is an alien subfield type since it
+   * appears as a subfield type of List, and List is an alien subfield type
+   * of T. In other words, Int is an alien subfield type due to the above
+   * definition due to the term (Container (singleton (cons 0 nil))), where
+   * 0 occurs as a subterm of (singleton (cons 0 nil)). The non-strict
+   * subfield types of T in this example are { (Set List) }.
+   *
+   * For example, the alien subfield types of T in:
+   *   T -> Emp | Container(s : List)
+   *   List -> nil | cons( head : (Set T), tail: List)
+   * are { T, List, (Set T) }. Notice that T is an alien subfield type of itself
+   * since List is a subfield type of T and T is an alien subfield type of List.
+   * Furthermore, List and (Set T) are also alien subfield types of T since
+   * List is a subfield type of T and T is an alien subfield type of itself.
+   *
+   * For example, the alien subfield types of T in:
+   *   T -> Emp | Container(s : (Array Int T))
+   * are { T, Int }, where we assume that values of (Array U1 U2) are
+   * constructed from values of U1 and U2, for all types U1, U2. The non-strict
+   * subfield types of T in this example are { (Array Int T) }.
+   *
+   * @param types The set of types to append the alien subfield types to,
+   * @param processed The datatypes (cached using d_self) we have processed. If
+   * the range of this map is true, we have processed the datatype with
+   * isAlienPos = true.
+   * @param isAlienPos Whether we are in an alien subfield type position. This
+   * flag is true if we have traversed beneath a non-datatype type constructor.
+   */
+  void getAlienSubfieldTypes(
+      std::unordered_set<TypeNode, TypeNodeHashFunction>& types,
+      std::map<TypeNode, bool>& processed,
+      bool isAlienPos) const;
   /** name of this datatype */
   std::string d_name;
   /** the type parameters of this datatype (if this is a parametric datatype)
@@ -543,6 +598,12 @@ class DType
    * not.
    */
   mutable int d_wellFounded;
+  /**
+   * Cache of whether this datatype has nested recursion, where 0 means we have
+   * not computed this information, 1 means it has nested recursion, -1 means it
+   * does not.
+   */
+  mutable int d_nestedRecursion;
   /** cache of ground term for this datatype */
   mutable std::map<TypeNode, Node> d_groundTerm;
   /** cache of ground values for this datatype */
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 44430f072..358023647 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -622,13 +622,13 @@ void getComponentTypes(
     TypeNode curr = toProcess.back();
     toProcess.pop_back();
     // if not already visited
-    if (types.find(t) == types.end())
+    if (types.find(curr) == types.end())
     {
-      types.insert(t);
+      types.insert(curr);
       // get component types from the children
-      for (unsigned i = 0, nchild = t.getNumChildren(); i < nchild; i++)
+      for (unsigned i = 0, nchild = curr.getNumChildren(); i < nchild; i++)
       {
-        toProcess.push_back(t[i]);
+        toProcess.push_back(curr[i]);
       }
     }
   } while (!toProcess.empty());
diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp
index f99c8a2da..479d2127f 100644
--- a/src/expr/type_matcher.cpp
+++ b/src/expr/type_matcher.cpp
@@ -86,6 +86,11 @@ bool TypeMatcher::doMatching(TypeNode pattern, TypeNode tn)
   {
     return false;
   }
+  else if (pattern.getNumChildren() == 0)
+  {
+    // fail if the type parameter or type constructors are different
+    return pattern == tn;
+  }
   for (size_t j = 0, nchild = pattern.getNumChildren(); j < nchild; j++)
   {
     if (!doMatching(pattern[j], tn[j]))
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index ac371efeb..19434fa33 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -68,6 +68,15 @@ header = "options/datatypes_options.h"
   help       = "when applicable, blast splitting lemmas for all variables at once"
 
 [[option]]
+  name       = "dtNestedRec"
+  category   = "regular"
+  long       = "dt-nested-rec"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "allow nested recursion in datatype definitions"
+
+[[option]]
   name       = "dtSharedSelectors"
   category   = "regular"
   long       = "dt-share-sel"
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9c8e9e2fa..6e5b028a7 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -561,6 +561,28 @@ void TheoryDatatypes::finishInit() {
 Node TheoryDatatypes::expandDefinition(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
+  // must ensure the type is well founded and has no nested recursion if
+  // the option dtNestedRec is not set to true.
+  TypeNode tn = n.getType();
+  if (tn.isDatatype())
+  {
+    const DType& dt = tn.getDType();
+    if (!dt.isWellFounded())
+    {
+      std::stringstream ss;
+      ss << "Cannot handle non-well-founded datatype " << dt.getName();
+      throw LogicException(ss.str());
+    }
+    if (!options::dtNestedRec())
+    {
+      if (dt.hasNestedRecursion())
+      {
+        std::stringstream ss;
+        ss << "Cannot handle nested-recursive datatype " << dt.getName();
+        throw LogicException(ss.str());
+      }
+    }
+  }
   switch (n.getKind())
   {
     case kind::APPLY_SELECTOR: