From 2bd404249035c03063ac464d4bace855975bbbd7 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 16 Mar 2022 13:26:09 -0700
Subject: [PATCH] unit: Add test for api::Kind. (#8322)

---
 test/unit/api/cpp/CMakeLists.txt     |  7 ++--
 test/unit/api/cpp/api_kind_black.cpp | 57 ++++++++++++++++++++++++++++
 2 files changed, 61 insertions(+), 3 deletions(-)
 create mode 100644 test/unit/api/cpp/api_kind_black.cpp

diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt
index 0125d6962..919f2eafb 100644
--- 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
index 000000000..d9078a98c
--- /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
+
-- 
2.30.2