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.

12 files changed, 571 insertions, 19 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:
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h
index c9eaf103e..180db8f32 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.h
@@ -32,6 +32,10 @@ class DatatypeBlack : public CxxTest::TestSuite
   void testDatatypeStructs();
   void testDatatypeNames();
 
+  void testParametricDatatype();
+
+  void testDatatypeSimplyRec();
+
  private:
   Solver d_solver;
 };
@@ -233,3 +237,285 @@ void DatatypeBlack::testDatatypeNames()
   // possible to construct null datatype declarations if not using solver
   TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&);
 }
+
+void DatatypeBlack::testParametricDatatype()
+{
+  std::vector<Sort> v;
+  Sort t1 = d_solver.mkParamSort("T1");
+  Sort t2 = d_solver.mkParamSort("T2");
+  v.push_back(t1);
+  v.push_back(t2);
+  DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v);
+
+  DatatypeConstructorDecl mkpair =
+      d_solver.mkDatatypeConstructorDecl("mk-pair");
+  mkpair.addSelector("first", t1);
+  mkpair.addSelector("second", t2);
+  pairSpec.addConstructor(mkpair);
+
+  Sort pairType = d_solver.mkDatatypeSort(pairSpec);
+
+  TS_ASSERT(pairType.getDatatype().isParametric());
+
+  v.clear();
+  v.push_back(d_solver.getIntegerSort());
+  v.push_back(d_solver.getIntegerSort());
+  Sort pairIntInt = pairType.instantiate(v);
+  v.clear();
+  v.push_back(d_solver.getRealSort());
+  v.push_back(d_solver.getRealSort());
+  Sort pairRealReal = pairType.instantiate(v);
+  v.clear();
+  v.push_back(d_solver.getRealSort());
+  v.push_back(d_solver.getIntegerSort());
+  Sort pairRealInt = pairType.instantiate(v);
+  v.clear();
+  v.push_back(d_solver.getIntegerSort());
+  v.push_back(d_solver.getRealSort());
+  Sort pairIntReal = pairType.instantiate(v);
+
+  TS_ASSERT_DIFFERS(pairIntInt, pairRealReal);
+  TS_ASSERT_DIFFERS(pairIntReal, pairRealReal);
+  TS_ASSERT_DIFFERS(pairRealInt, pairRealReal);
+  TS_ASSERT_DIFFERS(pairIntInt, pairIntReal);
+  TS_ASSERT_DIFFERS(pairIntInt, pairRealInt);
+  TS_ASSERT_DIFFERS(pairIntReal, pairRealInt);
+
+  TS_ASSERT(pairRealReal.isComparableTo(pairRealReal));
+  TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal));
+  TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal));
+  TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal));
+  TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt));
+  TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt));
+  TS_ASSERT(pairRealInt.isComparableTo(pairRealInt));
+  TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt));
+  TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal));
+  TS_ASSERT(pairIntReal.isComparableTo(pairIntReal));
+  TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal));
+  TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal));
+  TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt));
+  TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt));
+  TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt));
+  TS_ASSERT(pairIntInt.isComparableTo(pairIntInt));
+
+  TS_ASSERT(pairRealReal.isSubsortOf(pairRealReal));
+  TS_ASSERT(!pairIntReal.isSubsortOf(pairRealReal));
+  TS_ASSERT(!pairRealInt.isSubsortOf(pairRealReal));
+  TS_ASSERT(!pairIntInt.isSubsortOf(pairRealReal));
+  TS_ASSERT(!pairRealReal.isSubsortOf(pairRealInt));
+  TS_ASSERT(!pairIntReal.isSubsortOf(pairRealInt));
+  TS_ASSERT(pairRealInt.isSubsortOf(pairRealInt));
+  TS_ASSERT(!pairIntInt.isSubsortOf(pairRealInt));
+  TS_ASSERT(!pairRealReal.isSubsortOf(pairIntReal));
+  TS_ASSERT(pairIntReal.isSubsortOf(pairIntReal));
+  TS_ASSERT(!pairRealInt.isSubsortOf(pairIntReal));
+  TS_ASSERT(!pairIntInt.isSubsortOf(pairIntReal));
+  TS_ASSERT(!pairRealReal.isSubsortOf(pairIntInt));
+  TS_ASSERT(!pairIntReal.isSubsortOf(pairIntInt));
+  TS_ASSERT(!pairRealInt.isSubsortOf(pairIntInt));
+  TS_ASSERT(pairIntInt.isSubsortOf(pairIntInt));
+}
+
+void DatatypeBlack::testDatatypeSimplyRec()
+{
+  /* Create mutual datatypes corresponding to this definition block:
+   *
+   *   DATATYPE
+   *     wlist = leaf(data: list),
+   *     list = cons(car: wlist, cdr: list) | nil,
+   *     ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list))
+   *   END;
+   */
+  // Make unresolved types as placeholders
+  std::set<Sort> unresTypes;
+  Sort unresWList = d_solver.mkUninterpretedSort("wlist");
+  Sort unresList = d_solver.mkUninterpretedSort("list");
+  Sort unresNs = d_solver.mkUninterpretedSort("ns");
+  unresTypes.insert(unresWList);
+  unresTypes.insert(unresList);
+  unresTypes.insert(unresNs);
+
+  DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist");
+  DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
+  leaf.addSelector("data", unresList);
+  wlist.addConstructor(leaf);
+
+  DatatypeDecl list = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  cons.addSelector("car", unresWList);
+  cons.addSelector("cdr", unresList);
+  list.addConstructor(cons);
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+  list.addConstructor(nil);
+
+  DatatypeDecl ns = d_solver.mkDatatypeDecl("ns");
+  DatatypeConstructorDecl elem = d_solver.mkDatatypeConstructorDecl("elem");
+  elem.addSelector("ndata", d_solver.mkSetSort(unresWList));
+  ns.addConstructor(elem);
+  DatatypeConstructorDecl elemArray =
+      d_solver.mkDatatypeConstructorDecl("elemArray");
+  elemArray.addSelector("ndata", d_solver.mkArraySort(unresList, unresList));
+  ns.addConstructor(elemArray);
+
+  std::vector<DatatypeDecl> dtdecls;
+  dtdecls.push_back(wlist);
+  dtdecls.push_back(list);
+  dtdecls.push_back(ns);
+  // this is well-founded and has no nested recursion
+  std::vector<Sort> dtsorts;
+  TS_ASSERT_THROWS_NOTHING(dtsorts =
+                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  TS_ASSERT(dtsorts.size() == 3);
+  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
+  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
+  TS_ASSERT(dtsorts[2].getDatatype().isWellFounded());
+  TS_ASSERT(!dtsorts[0].getDatatype().hasNestedRecursion());
+  TS_ASSERT(!dtsorts[1].getDatatype().hasNestedRecursion());
+  TS_ASSERT(!dtsorts[2].getDatatype().hasNestedRecursion());
+
+  /* Create mutual datatypes corresponding to this definition block:
+   *   DATATYPE
+   *     ns2 = elem2(ndata: array(int,ns2)) | nil2
+   *   END;
+   */
+  unresTypes.clear();
+  Sort unresNs2 = d_solver.mkUninterpretedSort("ns2");
+  unresTypes.insert(unresNs2);
+
+  DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2");
+  DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2");
+  elem2.addSelector("ndata",
+                    d_solver.mkArraySort(d_solver.getIntegerSort(), unresNs2));
+  ns2.addConstructor(elem2);
+  DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2");
+  ns2.addConstructor(nil2);
+
+  dtdecls.clear();
+  dtdecls.push_back(ns2);
+
+  dtsorts.clear();
+  // this is not well-founded due to non-simple recursion
+  TS_ASSERT_THROWS_NOTHING(dtsorts =
+                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  TS_ASSERT(dtsorts.size() == 1);
+  TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray());
+  TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort()
+            == dtsorts[0]);
+  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
+  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
+
+  /* Create mutual datatypes corresponding to this definition block:
+   *   DATATYPE
+   *     list3 = cons3(car: ns3, cdr: list3) | nil3,
+   *     ns3 = elem3(ndata: set(list3))
+   *   END;
+   */
+  unresTypes.clear();
+  Sort unresNs3 = d_solver.mkUninterpretedSort("ns3");
+  unresTypes.insert(unresNs3);
+  Sort unresList3 = d_solver.mkUninterpretedSort("list3");
+  unresTypes.insert(unresList3);
+
+  DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3");
+  DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3");
+  cons3.addSelector("car", unresNs3);
+  cons3.addSelector("cdr", unresList3);
+  list3.addConstructor(cons3);
+  DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil3");
+  list3.addConstructor(nil3);
+
+  DatatypeDecl ns3 = d_solver.mkDatatypeDecl("ns3");
+  DatatypeConstructorDecl elem3 = d_solver.mkDatatypeConstructorDecl("elem3");
+  elem3.addSelector("ndata", d_solver.mkSetSort(unresList3));
+  ns3.addConstructor(elem3);
+
+  dtdecls.clear();
+  dtdecls.push_back(list3);
+  dtdecls.push_back(ns3);
+
+  dtsorts.clear();
+  // both are well-founded and have nested recursion
+  TS_ASSERT_THROWS_NOTHING(dtsorts =
+                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  TS_ASSERT(dtsorts.size() == 2);
+  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
+  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
+  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
+  TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion());
+
+  /* Create mutual datatypes corresponding to this definition block:
+   *   DATATYPE
+   *     list4 = cons(car: set(ns4), cdr: list4) | nil,
+   *     ns4 = elem(ndata: list4)
+   *   END;
+   */
+  unresTypes.clear();
+  Sort unresNs4 = d_solver.mkUninterpretedSort("ns4");
+  unresTypes.insert(unresNs4);
+  Sort unresList4 = d_solver.mkUninterpretedSort("list4");
+  unresTypes.insert(unresList4);
+
+  DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4");
+  DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4");
+  cons4.addSelector("car", d_solver.mkSetSort(unresNs4));
+  cons4.addSelector("cdr", unresList4);
+  list4.addConstructor(cons4);
+  DatatypeConstructorDecl nil4 = d_solver.mkDatatypeConstructorDecl("nil4");
+  list4.addConstructor(nil4);
+
+  DatatypeDecl ns4 = d_solver.mkDatatypeDecl("ns4");
+  DatatypeConstructorDecl elem4 = d_solver.mkDatatypeConstructorDecl("elem3");
+  elem4.addSelector("ndata", unresList4);
+  ns4.addConstructor(elem4);
+
+  dtdecls.clear();
+  dtdecls.push_back(list4);
+  dtdecls.push_back(ns4);
+
+  dtsorts.clear();
+  // both are well-founded and have nested recursion
+  TS_ASSERT_THROWS_NOTHING(dtsorts =
+                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  TS_ASSERT(dtsorts.size() == 2);
+  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
+  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
+  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
+  TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion());
+
+  /* Create mutual datatypes corresponding to this definition block:
+   *   DATATYPE
+   *     list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil
+   *   END;
+   */
+  unresTypes.clear();
+  Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1);
+  unresTypes.insert(unresList5);
+
+  std::vector<Sort> v;
+  Sort x = d_solver.mkParamSort("X");
+  v.push_back(x);
+  DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v);
+
+  std::vector<Sort> args;
+  args.push_back(x);
+  Sort urListX = unresList5.instantiate(args);
+  args[0] = urListX;
+  Sort urListListX = unresList5.instantiate(args);
+
+  DatatypeConstructorDecl cons5 = d_solver.mkDatatypeConstructorDecl("cons5");
+  cons5.addSelector("car", x);
+  cons5.addSelector("cdr", urListListX);
+  list5.addConstructor(cons5);
+  DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("nil5");
+  list5.addConstructor(nil5);
+
+  dtdecls.clear();
+  dtdecls.push_back(list5);
+
+  // well-founded and has nested recursion
+  TS_ASSERT_THROWS_NOTHING(dtsorts =
+                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  TS_ASSERT(dtsorts.size() == 1);
+  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
+  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
+}
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index a829d9a8d..f1691edd4 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -254,7 +254,10 @@ public:
     tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;");
     tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil END;");
     //tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
-    tryGoodInput("DATATYPE trex = Foo | Bar END; DATATYPE tree = node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
+    tryGoodInput(
+        "DATATYPE trex = Foo | Bar END; DATATYPE tree = "
+        "node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list "
+        "OF tree,cdr:BITVECTOR(32)) END;");
   }
 
   void testBadCvc4Inputs() {