From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 9 Jun 2021 07:09:26 +0000 (-0700)
Subject: docs: Fix `Kind` description (#6712)
X-Git-Tag: cvc5-1.0.0~1625
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a0ea3701810d5af31ff3f4af75ee39233dd43301;p=cvc5.git

docs: Fix `Kind` description (#6712)

This commit changes the Kind description not to include C/C++
preprocessor statements and updates the kind of bit-vector addtion.
It also marks some of the information as internal to exclude it from the
public documentation.
---

diff --git a/docs/api/cpp/kind.rst b/docs/api/cpp/kind.rst
index 579407c85..4c07804a4 100644
--- a/docs/api/cpp/kind.rst
+++ b/docs/api/cpp/kind.rst
@@ -4,14 +4,8 @@ Kind
 Every :cpp:class:`Term <cvc5::api::Term>` has a kind which represents its type,
 for example whether it is an equality (:cpp:enumerator:`EQUAL
 <cvc5::api::Kind::EQUAL>`), a conjunction (:cpp:enumerator:`AND
-<cvc5::api::Kind::AND>`), or a bitvector addition
-(:cpp:enumerator:`BITVECTOR_PLUS <cvc5::api::Kind::BITVECTOR_PLUS>`).
-#ifndef DOXYGEN_SKIP
-Note that the API type :cpp:enum:`cvc5::api::Kind` roughly corresponds to
-:cpp:enum:`cvc5::Kind`, but is a different type. It hides internal kinds that
-should not be exported to the API, and maps all kinds that we want to export
-to its corresponding internal kinds.
-#endif
+<cvc5::api::Kind::AND>`), or a bit-vector addition
+(:cpp:enumerator:`BITVECTOR_ADD <cvc5::api::Kind::BITVECTOR_ADD>`).
 
 .. doxygenenum:: cvc5::api::Kind
     :project: cvc5
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index b4596e977..be9083960 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -33,9 +33,15 @@ namespace api {
 /**
  * The kind of a cvc5 term.
  *
- * Note that the underlying type of Kind must be signed (to enable range
- * checks for validity). The size of this type depends on the size of
- * cvc5::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h).
+ * \internal
+ *
+ * Note that the API type `cvc5::api::Kind` roughly corresponds to
+ * `cvc5::Kind`, but is a different type. It hides internal kinds that should
+ * not be exported to the API, and maps all kinds that we want to export to its
+ * corresponding internal kinds. The underlying type of `cvc5::api::Kind` must
+ * be signed (to enable range checks for validity). The size of this type
+ * depends on the size of `cvc5::Kind` (`NodeValue::NBITS_KIND`, currently 10
+ * bits, see expr/node_value.h).
  */
 enum CVC5_EXPORT Kind : int32_t
 {