From: Gereon Kremer <gkremer@stanford.edu>
Date: Tue, 23 Nov 2021 20:59:26 +0000 (-0800)
Subject: Add kinds to python docs (#7672)
X-Git-Tag: cvc5-1.0.0~781
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=38e4cf3fe6dd8f171657943155e875c180649e15;p=cvc5.git

Add kinds to python docs (#7672)

This PR adds the kinds to the documentation for the regular python docs.
---

diff --git a/docs/api/python/regular/kind.rst b/docs/api/python/regular/kind.rst
new file mode 100644
index 000000000..f2dd8550b
--- /dev/null
+++ b/docs/api/python/regular/kind.rst
@@ -0,0 +1,12 @@
+Kind
+================
+
+Every :py:class:`Term <pycvc5.Term>` has a kind which represents its type, for
+example whether it is an equality (:py:obj:`Equal <pycvc5.kinds.Equal>`), a
+conjunction (:py:obj:`And <pycvc5.kinds.And>`), or a bit-vector addtion
+(:py:obj:`BVAdd <pycvc5.kinds.BVAdd>`).
+The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind <cvc5::api::Kind>` enum.
+
+.. autoclass:: pycvc5.kinds
+    :members:
+    :undoc-members:
diff --git a/docs/api/python/regular/python.rst b/docs/api/python/regular/python.rst
index 2e50f2d68..b054cbe16 100644
--- a/docs/api/python/regular/python.rst
+++ b/docs/api/python/regular/python.rst
@@ -17,6 +17,7 @@ Python API Documentation
     datatypedecl
     datatypeselector
     grammar
+    kind
     op
     result
     roundingmode