Add missing datatype functions to new API (#3930)

This is in preparation for migrating the parser to use the Term-level API for datatypes.

Notably, this adds the function mkDatatypeSorts for making mutually recursive datatypes. I've added a unit test that demonstrates this method (which mirrors the Expr-level datatype API).

1 files changed, 78 insertions, 0 deletions

diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h
index dcccd2628..f25282624 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.h
@@ -27,6 +27,7 @@ class DatatypeBlack : public CxxTest::TestSuite
   void tearDown() override;
 
   void testMkDatatypeSort();
+  void testMkDatatypeSorts();
 
   void testDatatypeStructs();
   void testDatatypeNames();
@@ -57,6 +58,77 @@ void DatatypeBlack::testMkDatatypeSort()
   TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm());
 }
 
+void DatatypeBlack::testMkDatatypeSorts()
+{
+  /* Create two mutual datatypes corresponding to this definition
+   * block:
+   *
+   *   DATATYPE
+   *     tree = node(left: tree, right: tree) | leaf(data: list),
+   *     list = cons(car: tree, cdr: list) | nil
+   *   END;
+   */
+  // Make unresolved types as placeholders
+  std::set<Sort> unresTypes;
+  Sort unresTree = d_solver.mkUninterpretedSort("tree");
+  Sort unresList = d_solver.mkUninterpretedSort("list");
+  unresTypes.insert(unresTree);
+  unresTypes.insert(unresList);
+
+  DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
+  DatatypeConstructorDecl node("node");
+  DatatypeSelectorDecl left("left", unresTree);
+  node.addSelector(left);
+  DatatypeSelectorDecl right("right", unresTree);
+  node.addSelector(right);
+  tree.addConstructor(node);
+
+  DatatypeConstructorDecl leaf("leaf");
+  DatatypeSelectorDecl data("data", unresList);
+  leaf.addSelector(data);
+  tree.addConstructor(leaf);
+
+  DatatypeDecl list = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl car("car", unresTree);
+  cons.addSelector(car);
+  DatatypeSelectorDecl cdr("cdr", unresTree);
+  cons.addSelector(cdr);
+  list.addConstructor(cons);
+
+  DatatypeConstructorDecl nil("nil");
+  list.addConstructor(nil);
+
+  std::vector<DatatypeDecl> dtdecls;
+  dtdecls.push_back(tree);
+  dtdecls.push_back(list);
+  std::vector<Sort> dtsorts;
+  TS_ASSERT_THROWS_NOTHING(dtsorts =
+                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  TS_ASSERT(dtsorts.size() == dtdecls.size());
+  for (unsigned i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
+  {
+    TS_ASSERT(dtsorts[i].isDatatype());
+    TS_ASSERT(!dtsorts[i].getDatatype().isFinite());
+    TS_ASSERT(dtsorts[i].getDatatype().getName() == dtdecls[i].getName());
+  }
+  // verify the resolution was correct
+  Datatype dtTree = dtsorts[0].getDatatype();
+  DatatypeConstructor dtcTreeNode = dtTree[0];
+  TS_ASSERT(dtcTreeNode.getName() == "node");
+  DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0];
+  TS_ASSERT(dtsTreeNodeLeft.getName() == "left");
+  // argument type should have resolved to be recursive
+  TS_ASSERT(dtsTreeNodeLeft.getRangeSort().isDatatype());
+  TS_ASSERT(dtsTreeNodeLeft.getRangeSort() == dtsorts[0]);
+
+  // fails due to empty datatype
+  std::vector<DatatypeDecl> dtdeclsBad;
+  DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD");
+  dtdeclsBad.push_back(emptyD);
+  TS_ASSERT_THROWS(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException&);
+}
+
 void DatatypeBlack::testDatatypeStructs()
 {
   Sort intSort = d_solver.getIntegerSort();
@@ -138,6 +210,8 @@ void DatatypeBlack::testDatatypeNames()
 
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+  TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName());
+  TS_ASSERT(dtypeSpec.getName() == std::string("list"));
   DatatypeConstructorDecl cons("cons");
   DatatypeSelectorDecl head("head", intSort);
   cons.addSelector(head);
@@ -163,4 +237,8 @@ void DatatypeBlack::testDatatypeNames()
   // get selector
   DatatypeSelector dselTail = dcons[1];
   TS_ASSERT(dselTail.getName() == std::string("tail"));
+  TS_ASSERT(dselTail.getRangeSort() == dtypeSort);
+
+  // possible to construct null datatype declarations if not using solver
+  TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&);
 }