Reorganize declareDatatype unit tests. (#7767)

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 2df5de4b87e7e4cbd38a424373270b3769aa27c7..54b6dc81f8dad5ab5dbb218cc7cfca879c6118e6 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -929,22 +929,35 @@ TEST_F(TestApiBlackSolver, mkConstArray)
 
 TEST_F(TestApiBlackSolver, declareDatatype)
 {
+  DatatypeConstructorDecl lin = d_solver.mkDatatypeConstructorDecl("lin");
+  std::vector<DatatypeConstructorDecl> ctors0 = {lin};
+  ASSERT_NO_THROW(d_solver.declareDatatype(std::string(""), ctors0));
+
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors1 = {nil};
   ASSERT_NO_THROW(d_solver.declareDatatype(std::string("a"), ctors1));
+
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2};
   ASSERT_NO_THROW(d_solver.declareDatatype(std::string("b"), ctors2));
+
   DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons");
   DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3};
   ASSERT_NO_THROW(d_solver.declareDatatype(std::string(""), ctors3));
+
+  // must have at least one constructor
   std::vector<DatatypeConstructorDecl> ctors4;
   ASSERT_THROW(d_solver.declareDatatype(std::string("c"), ctors4),
                CVC5ApiException);
-  ASSERT_THROW(d_solver.declareDatatype(std::string(""), ctors4),
+  // constructors may not be reused
+  DatatypeConstructorDecl ctor1 = d_solver.mkDatatypeConstructorDecl("_x21");
+  DatatypeConstructorDecl ctor2 = d_solver.mkDatatypeConstructorDecl("_x31");
+  Sort s3 = d_solver.declareDatatype(std::string("_x17"), {ctor1, ctor2});
+  ASSERT_THROW(d_solver.declareDatatype(std::string("_x86"), {ctor1, ctor2}),
                CVC5ApiException);
+  // constructor belongs to different solver instance
   Solver slv;
   ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC5ApiException);
 }
@@ -2661,16 +2674,6 @@ TEST_F(TestApiBlackSolver, proj_issue373)
       CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, doubleUseCons)
-{
-  DatatypeConstructorDecl ctor1 = d_solver.mkDatatypeConstructorDecl("_x21");
-  DatatypeConstructorDecl ctor2 = d_solver.mkDatatypeConstructorDecl("_x31");
-  Sort s3 = d_solver.declareDatatype(std::string("_x17"), {ctor1, ctor2});
-
-  ASSERT_THROW(d_solver.declareDatatype(std::string("_x86"), {ctor1, ctor2}),
-               CVC5ApiException);
-}
-
 TEST_F(TestApiBlackSolver, proj_issue378)
 {
   DatatypeDecl dtdecl;