New C++ Api: Clean up usage of internal kind. (#6087)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index fbbaeee2433e8e90d23ce860765a41a8f19437b3..0ce3ee0580a49007c586749ee03a425767e808a8 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -659,13 +659,37 @@ const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds(
 
 namespace {
 
+/** Convert a CVC4::Kind (internal) to a CVC4::api::Kind (external). */
+CVC4::api::Kind intToExtKind(CVC4::Kind k)
+{
+  auto it = api::s_kinds_internal.find(k);
+  if (it == api::s_kinds_internal.end())
+  {
+    return api::INTERNAL_KIND;
+  }
+  return it->second;
+}
+
+/** Convert a CVC4::api::Kind (external) to a CVC4::Kind (internal). */
+CVC4::Kind extToIntKind(CVC4::api::Kind k)
+{
+  auto it = api::s_kinds.find(k);
+  if (it == api::s_kinds.end())
+  {
+    return CVC4::Kind::UNDEFINED_KIND;
+  }
+  return it->second;
+}
+
+/** Return true if given kind is a defined external kind. */
 bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
 
-/** Returns true if the internal kind is one where the API term structure
- *  differs from internal structure. This happens for APPLY_* kinds.
- *  The API takes a "higher-order" perspective and treats functions as well
- *  as datatype constructors/selectors/testers as terms
- *  but interally they are not
+/**
+ * Return true if the internal kind is one where the API term structure
+ * differs from internal structure. This happens for APPLY_* kinds.
+ * The API takes a "higher-order" perspective and treats functions as well
+ * as datatype constructors/selectors/testers as terms
+ * but interally they are not
  */
 bool isApplyKind(CVC4::Kind k)
 {
@@ -674,12 +698,14 @@ bool isApplyKind(CVC4::Kind k)
 }
 
 #ifdef CVC4_ASSERTIONS
+/** Return true if given kind is a defined internal kind. */
 bool isDefinedIntKind(CVC4::Kind k)
 {
   return k != CVC4::Kind::UNDEFINED_KIND && k != CVC4::Kind::LAST_KIND;
 }
 #endif
 
+/** Return the minimum arity of given kind. */
 uint32_t minArity(Kind k)
 {
   Assert(isDefinedKind(k));
@@ -695,6 +721,7 @@ uint32_t minArity(Kind k)
   return min;
 }
 
+/** Return the maximum arity of given kind. */
 uint32_t maxArity(Kind k)
 {
   Assert(isDefinedKind(k));
@@ -5969,28 +5996,4 @@ Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); }
 
 }  // namespace api
 
-/* -------------------------------------------------------------------------- */
-/* Kind Conversions                                                           */
-/* -------------------------------------------------------------------------- */
-
-CVC4::api::Kind intToExtKind(CVC4::Kind k)
-{
-  auto it = api::s_kinds_internal.find(k);
-  if (it == api::s_kinds_internal.end())
-  {
-    return api::INTERNAL_KIND;
-  }
-  return it->second;
-}
-
-CVC4::Kind extToIntKind(CVC4::api::Kind k)
-{
-  auto it = api::s_kinds.find(k);
-  if (it == api::s_kinds.end())
-  {
-    return CVC4::Kind::UNDEFINED_KIND;
-  }
-  return it->second;
-}
-
 }  // namespace CVC4

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 1d6367b31576d71e5ec9be433c49e63620cc9b46..3d26f5c7bb7f473176ee7a0a24503be9d774ee59 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -20,10 +20,6 @@
 #define CVC4__API__CVC4CPP_H
 
 #include "api/cvc4cppkind.h"
-// !!! Only temporarily public until the parser is fully migrated to the new
-// API. !!!
-#include "expr/kind.h"
-// !!!
 
 #include <map>
 #include <memory>
@@ -3639,11 +3635,5 @@ class CVC4_PUBLIC Solver
 };
 
 }  // namespace api
-
-// !!! Only temporarily public until the parser is fully migrated to the
-// new API. !!!
-CVC4::api::Kind intToExtKind(CVC4::Kind k);
-CVC4::Kind extToIntKind(CVC4::api::Kind k);
-
 }  // namespace CVC4
 #endif