New C++ API: Unit tests for declare* functions. (#2831)

1 files changed, 39 insertions, 0 deletions

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index fcc68d981..169a9948d 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -76,7 +76,11 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkUniverseSet();
   void testMkVar();
 
+  void testDeclareConst();
+  void testDeclareDatatype();
   void testDeclareFun();
+  void testDeclareSort();
+
   void testDefineFun();
   void testDefineFunRec();
   void testDefineFunsRec();
@@ -733,6 +737,34 @@ void SolverBlack::testMkVar()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkVar("", funSort));
 }
 
+void SolverBlack::testDeclareConst()
+{
+  Sort boolSort = d_solver->getBooleanSort();
+  Sort intSort = d_solver->getIntegerSort();
+  Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("b"), boolSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("i"), intSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("f", funSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("", funSort));
+  TS_ASSERT_THROWS(d_solver->declareConst("a", Sort()), CVC4ApiException&);
+}
+
+void SolverBlack::testDeclareDatatype()
+{
+  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl nil("nil");
+  std::vector<DatatypeConstructorDecl> ctors1 = {nil};
+  std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil};
+  std::vector<DatatypeConstructorDecl> ctors3;
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors2));
+  TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors3),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors3),
+                   CVC4ApiException&);
+}
+
 void SolverBlack::testDeclareFun()
 {
   Sort bvSort = d_solver->mkBitVectorSort(32);
@@ -748,6 +780,13 @@ void SolverBlack::testDeclareFun()
                    CVC4ApiException&);
 }
 
+void SolverBlack::testDeclareSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("s", 0));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("s", 2));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("", 2));
+}
+
 void SolverBlack::testDefineFun()
 {
   Sort bvSort = d_solver->mkBitVectorSort(32);