diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-09 00:09:26 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-09 09:09:26 +0200 |
| commit | a0ea3701810d5af31ff3f4af75ee39233dd43301 (patch) | |
| tree | 2dbb2a2f2a499b040be6740f91b0a85b9c2dce50 | |
| parent | ccd52accc3bd19c5bc5203d091d1fc0f8d48f8a3 (diff) | |
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.
| -rw-r--r-- | docs/api/cpp/kind.rst | 10 | ||||
| -rw-r--r-- | src/api/cpp/cvc5_kind.h | 12 |
2 files changed, 11 insertions, 11 deletions
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 { |