unit: Add test for api::Kind. (#8322)

diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt
index 0125d69623c91b12d4329f4f9fa3aef33601ef5f..919f2eafbeac39ec48cbeb7d0b54d2048ac3c951 100644 (file)
--- a/test/unit/api/cpp/CMakeLists.txt
+++ b/test/unit/api/cpp/CMakeLists.txt
@@ -14,14 +14,15 @@
 ##
 cvc5_add_unit_test_black(datatype_api_black api)
 cvc5_add_unit_test_black(grammar_black api)
+cvc5_add_unit_test_black(api_kind_black api)
 cvc5_add_unit_test_black(op_black api)
-cvc5_add_unit_test_white(op_white api)
 cvc5_add_unit_test_black(parametric_datatype_black api)
 cvc5_add_unit_test_black(result_black api)
 cvc5_add_unit_test_black(solver_black api)
-cvc5_add_unit_test_white(solver_white api)
 cvc5_add_unit_test_black(sort_black api)
 cvc5_add_unit_test_black(term_black api)
-cvc5_add_unit_test_white(term_white api)
 cvc5_add_unit_test_black(theory_arith_nl_black api)
 cvc5_add_unit_test_black(theory_uf_ho_black api)
+cvc5_add_unit_test_white(op_white api)
+cvc5_add_unit_test_white(solver_white api)
+cvc5_add_unit_test_white(term_white api)

diff --git a/test/unit/api/cpp/api_kind_black.cpp b/test/unit/api/cpp/api_kind_black.cpp
new file mode 100644 (file)
index 0000000..d9078a9
--- /dev/null
+++ b/test/unit/api/cpp/api_kind_black.cpp
@@ -0,0 +1,57 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Black box testing of the Kind enum of the  C++ API.
+ */
+
+#include <algorithm>
+
+#include "gtest/gtest.h"
+
+#include "api/cpp/cvc5.h"
+#include "base/output.h"
+
+namespace cvc5 {
+
+using namespace api;
+
+namespace test {
+
+class TestApiKind : public ::testing::Test
+{
+};
+
+TEST_F(TestApiKind, kindToString)
+{
+  for (int32_t k = INTERNAL_KIND; k < LAST_KIND; ++k)
+  {
+    auto kindstr = kindToString(static_cast<Kind>(k));
+    if (k == INTERNAL_KIND)
+    {
+      ASSERT_EQ(kindstr, "INTERNAL_KIND");
+    }
+    else if (k == UNDEFINED_KIND)
+    {
+      ASSERT_EQ(kindstr, "UNDEFINED_KIND");
+    }
+    else
+    {
+      // If this assertion fails, s_kinds in cvc5.cpp is missing kind k.
+      ASSERT_NE(kindstr, "UNDEFINED_KIND");
+      ASSERT_NE(kindstr, "INTERNAL_KIND");
+    }
+  }
+}
+
+}  // namespace test
+}  // namespace cvc5
+