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.

1 files changed, 11 insertions, 0 deletions

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;