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.

2 files changed, 290 insertions, 1 deletions

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() {