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.

9 files changed, 115 insertions, 13 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;
diff --git a/src/parser/parser.h b/src/parser/parser.h
index b5dc83902..681404efa 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -589,6 +589,13 @@ public:
                                         const std::vector<api::Sort>& params);
 
   /**
+   * Creates a new unresolved (parameterized) type constructor of the given
+   * arity. Calls either mkUnresolvedType or mkUnresolvedTypeConstructor
+   * depending on the arity.
+   */
+  api::Sort mkUnresolvedType(const std::string& name, size_t arity);
+
+  /**
    * Returns true IFF name is an unresolved type.
    */
   bool isUnresolvedType(const std::string& name);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ec3e874df..436700826 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1530,7 +1530,10 @@ datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
 /**
  * Read a list of datatype definitions for datatypes with names dnames and
  * parametric arities arities. A negative value in arities indicates that the
- * arity for the corresponding datatype has not been fixed.
+ * arity for the corresponding datatype has not been fixed: notice that we do
+ * not know the arity of datatypes in the declare-datatype command prior to
+ * parsing their body, whereas the arity of datatypes in declare-datatypes is
+ * given in the preamble of that command and thus is known prior to this call.
  */
 datatypesDef[bool isCo,
              const std::vector<std::string>& dnames,
@@ -1541,7 +1544,26 @@ datatypesDef[bool isCo,
   std::string name;
   std::vector<api::Sort> params;
 }
-  : { PARSER_STATE->pushScope(true); }
+  : { PARSER_STATE->pushScope(true);
+      // Declare the datatypes that are currently being defined as unresolved
+      // types. If we do not know the arity of the datatype yet, we wait to
+      // define it until parsing the preamble of its body, which may optionally
+      // involve `par`. This is limited to the case of single datatypes defined
+      // via declare-datatype, and hence no datatype body is parsed without
+      // having all types declared. This ensures we can parse datatypes with
+      // nested recursion, e.g. datatypes D having a subfield type
+      // (Array Int D).
+      for (unsigned i=0, dsize=dnames.size(); i<dsize; i++)
+      {
+        if( arities[i]<0 )
+        {
+          // do not know the arity yet
+          continue;
+        }
+        unsigned arity = static_cast<unsigned>(arities[i]);
+        PARSER_STATE->mkUnresolvedType(dnames[i], arity);
+      }
+    }
     ( LPAREN_TOK {
       params.clear();
       Debug("parser-dt") << "Processing datatype #" << dts.size() << std::endl;
@@ -1559,6 +1581,11 @@ datatypesDef[bool isCo,
         if( arities[dts.size()]>=0 && static_cast<int>(params.size())!=arities[dts.size()] ){
           PARSER_STATE->parseError("Wrong number of parameters for datatype.");
         }
+        if (arities[dts.size()]<0)
+        {
+          // now declare it as an unresolved type
+          PARSER_STATE->mkUnresolvedType(dnames[dts.size()], params.size());
+        }
         Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
         dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()], params, isCo));
       }
@@ -1569,6 +1596,11 @@ datatypesDef[bool isCo,
         if( arities[dts.size()]>0 ){
           PARSER_STATE->parseError("No parameters given for datatype.");
         }
+        else if (arities[dts.size()]<0)
+        {
+          // now declare it as an unresolved type
+          PARSER_STATE->mkUnresolvedType(dnames[dts.size()], 0);
+        }
         Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
         dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()],
                                              params,
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 6e5b028a7..b0164265d 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -587,7 +587,6 @@ Node TheoryDatatypes::expandDefinition(Node n)
   {
     case kind::APPLY_SELECTOR:
     {
-      Trace("dt-expand") << "Dt Expand definition : " << n << std::endl;
       Node selector = n.getOperator();
       // APPLY_SELECTOR always applies to an external selector, cindexOf is
       // legal here
@@ -643,30 +642,28 @@ Node TheoryDatatypes::expandDefinition(Node n)
     case TUPLE_UPDATE:
     case RECORD_UPDATE:
     {
-      TypeNode t = n.getType();
-      Assert(t.isDatatype());
-      const DType& dt = t.getDType();
+      Assert(tn.isDatatype());
+      const DType& dt = tn.getDType();
       NodeBuilder<> b(APPLY_CONSTRUCTOR);
       b << dt[0].getConstructor();
       size_t size, updateIndex;
       if (n.getKind() == TUPLE_UPDATE)
       {
-        Assert(t.isTuple());
-        size = t.getTupleLength();
+        Assert(tn.isTuple());
+        size = tn.getTupleLength();
         updateIndex = n.getOperator().getConst<TupleUpdate>().getIndex();
       }
       else
       {
-        Assert(t.toType().isRecord());
-        const Record& record =
-            DatatypeType(t.toType()).getRecord();
+        Assert(tn.toType().isRecord());
+        const Record& record = DatatypeType(tn.toType()).getRecord();
         size = record.getNumFields();
         updateIndex = record.getIndex(
             n.getOperator().getConst<RecordUpdate>().getField());
       }
       Debug("tuprec") << "expr is " << n << std::endl;
       Debug("tuprec") << "updateIndex is " << updateIndex << std::endl;
-      Debug("tuprec") << "t is " << t << std::endl;
+      Debug("tuprec") << "t is " << tn << std::endl;
       Debug("tuprec") << "t has arity " << size << std::endl;
       for (size_t i = 0; i < size; ++i)
       {
@@ -679,7 +676,7 @@ Node TheoryDatatypes::expandDefinition(Node n)
         else
         {
           b << nm->mkNode(
-              APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(t, i), n[0]);
+              APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, i), n[0]);
           Debug("tuprec") << "arg " << i << " copies "
                           << b[b.getNumChildren() - 1] << std::endl;
         }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f6bc70cd0..4bc9d2705 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1275,6 +1275,9 @@ set(regress_1_tests
   regress1/datatypes/issue3266-small.smt2
   regress1/datatypes/issue-variant-dt-zero.smt2
   regress1/datatypes/manos-model.smt2
+  regress1/datatypes/non-simple-rec.smt2
+  regress1/datatypes/non-simple-rec-mut-unsat.smt2
+  regress1/datatypes/non-simple-rec-param.smt2
   regress1/decision/error3.smtv1.smt2
   regress1/decision/quant-Arrays_Q1-noinfer.smt2
   regress1/decision/quant-symmetric_unsat_7.smt2
diff --git a/test/regress/regress1/datatypes/non-simple-rec-mut-unsat.smt2 b/test/regress/regress1/datatypes/non-simple-rec-mut-unsat.smt2
new file mode 100644
index 000000000..35e06a0d3
--- /dev/null
+++ b/test/regress/regress1/datatypes/non-simple-rec-mut-unsat.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --dt-nested-rec
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((E 0)(T 0)) (
+((Yes) (No))
+((FMap (m (Array E E))) (Map (mm (Array E T))) (None) )
+))
+(declare-fun a () T)
+(declare-fun b () T)
+(declare-fun c () T)
+(assert (distinct a b c))
+(assert ((_ is FMap) a))
+(assert ((_ is FMap) b))
+(assert ((_ is FMap) c))
+(assert (= (select (m a) Yes) (select (m b) Yes)))
+(assert (= (select (m b) Yes) (select (m c) Yes)))
+(check-sat)
diff --git a/test/regress/regress1/datatypes/non-simple-rec-param.smt2 b/test/regress/regress1/datatypes/non-simple-rec-param.smt2
new file mode 100644
index 000000000..8db92b0fd
--- /dev/null
+++ b/test/regress/regress1/datatypes/non-simple-rec-param.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --dt-nested-rec
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((T 1)) (
+(par (x) ((Data (s x)) (Map (m (Array Int (T (T Int)))) ) ) ))
+)
+(declare-fun a () (T Int))
+(declare-fun b () (T Int))
+(declare-fun c () (T Int))
+(declare-fun d () (T Int))
+(assert (distinct a b c d))
+(assert (= (select (m a) 5) (Data b)))
+(assert (not (= (s b) 0)))
+(check-sat)
diff --git a/test/regress/regress1/datatypes/non-simple-rec-set.smt2 b/test/regress/regress1/datatypes/non-simple-rec-set.smt2
new file mode 100644
index 000000000..a6c4f6695
--- /dev/null
+++ b/test/regress/regress1/datatypes/non-simple-rec-set.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --dt-nested-rec
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatype T
+((Emp) (Container (s (Set T)) )
+))
+(declare-fun a () T)
+(assert (not ((_ is Emp) a)))
+(assert (= (s a) (singleton a)))
+(check-sat)
diff --git a/test/regress/regress1/datatypes/non-simple-rec.smt2 b/test/regress/regress1/datatypes/non-simple-rec.smt2
new file mode 100644
index 000000000..f6b8ede3f
--- /dev/null
+++ b/test/regress/regress1/datatypes/non-simple-rec.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --dt-nested-rec
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((T 0)) (((Nil) (Map (m (Array Int T)) ) ) ))
+(declare-fun a () T)
+(declare-fun b () T)
+(declare-fun c () T)
+(declare-fun d () T)
+(assert (distinct a b c d))
+(check-sat)