diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-14 23:10:11 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-14 21:10:11 +0000 |
commit | 9894b5fca418879ec472e5efbb43be26995e4045 (patch) | |
tree | d71642d46d9a43fddf09cb306263f06982f11ef5 /docs/cpp | |
parent | 485b3db20d182b0d621c002bb355c9d1ec2429e9 (diff) |
Improve documentation of API kinds (#6341)
This PR improves the documentation of the api::Kind enum. Note that the docs for many of the enum values should still be improved. This PR merely makes sure that everything that is already there is actually output (/* vs /**) and properly rendered (missing spacing between lists, some formulas, etc).
Diffstat (limited to 'docs/cpp')
-rw-r--r-- | docs/cpp/kind.rst | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/docs/cpp/kind.rst b/docs/cpp/kind.rst index 23421905e..2f74ee5fe 100644 --- a/docs/cpp/kind.rst +++ b/docs/cpp/kind.rst @@ -1,10 +1,22 @@ 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 + +.. doxygenenum:: cvc5::api::Kind + :project: cvc5 + .. doxygenstruct:: cvc5::api::KindHashFunction :project: cvc5 :members: :undoc-members: - -.. doxygenenum:: cvc5::api::Kind - :project: cvc5 |