summaryrefslogtreecommitdiff
path: root/docs/cpp
diff options
context:
space:
mode:
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>2021-04-14 23:10:11 +0200
committerGitHub <noreply@github.com>2021-04-14 21:10:11 +0000
commit9894b5fca418879ec472e5efbb43be26995e4045 (patch)
treed71642d46d9a43fddf09cb306263f06982f11ef5 /docs/cpp
parent485b3db20d182b0d621c002bb355c9d1ec2429e9 (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.rst18
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback