Smt2 parsing support for nested recursive datatypes (#4575)

Also includes some minor improvement to expand definitions in TheoryDatatypes leftover from the branch.

Adds 3 regressions using the option --dt-nested-rec.

1 files changed, 9 insertions, 0 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index b24f9ae9d..5ad773c9c 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -387,6 +387,15 @@ api::Sort Parser::mkUnresolvedTypeConstructor(
   return unresolved;
 }
 
+api::Sort Parser::mkUnresolvedType(const std::string& name, size_t arity)
+{
+  if (arity == 0)
+  {
+    return mkUnresolvedType(name);
+  }
+  return mkUnresolvedTypeConstructor(name, arity);
+}
+
 bool Parser::isUnresolvedType(const std::string& name) {
   if (!isDeclared(name, SYM_SORT)) {
     return false;