summaryrefslogtreecommitdiff
path: root/src/api/cpp/cvc5_kind.h
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2021-06-09 00:09:26 -0700
committerGitHub <noreply@github.com>2021-06-09 09:09:26 +0200
commita0ea3701810d5af31ff3f4af75ee39233dd43301 (patch)
tree2dbb2a2f2a499b040be6740f91b0a85b9c2dce50 /src/api/cpp/cvc5_kind.h
parentccd52accc3bd19c5bc5203d091d1fc0f8d48f8a3 (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.
Diffstat (limited to 'src/api/cpp/cvc5_kind.h')
-rw-r--r--src/api/cpp/cvc5_kind.h12
1 files changed, 9 insertions, 3 deletions
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
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback