diff options
Diffstat (limited to 'docs/api/python')
| -rw-r--r-- | docs/api/python/python.rst | 17 | ||||
| -rw-r--r-- | docs/api/python/regular/kind.rst | 8 | ||||
| -rw-r--r-- | docs/api/python/regular/python.rst | 4 | ||||
| -rw-r--r-- | docs/api/python/regular/quickstart.rst | 2 | ||||
| -rw-r--r-- | docs/api/python/z3compat/z3compat.rst | 2 |
5 files changed, 16 insertions, 17 deletions
diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index 3697cf579..b3bd865be 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -1,13 +1,6 @@ -Python API Documentation +Python API ======================== -.. toctree:: - :maxdepth: 1 - :hidden: - - z3py compatibility API <z3compat/z3compat> - regular Python API <regular/python> - .. only:: not bindings_python .. warning:: @@ -16,7 +9,13 @@ Python API Documentation cvc5 offers two separate APIs for Python users. The :doc:`regular Python API <regular/python>` is an almost exact copy of the :doc:`C++ API <../cpp/cpp>`. -Alternatively, the :doc:`z3py compatibility API <z3compat/z3compat>` is a more pythonic API that aims to be fully compatible with `Z3s Python API <https://z3prover.github.io/api/html/namespacez3py.html>`_ while adding functionality that Z3 does not support. +Alternatively, the :doc:`z3py compatibility Python API <z3compat/z3compat>` is a more pythonic API that aims to be fully compatible with `Z3s Python API <https://z3prover.github.io/api/html/namespacez3py.html>`_ while adding functionality that Z3 does not support. + +.. toctree:: + :maxdepth: 1 + + z3compat/z3compat + regular/python Which Python API should I use? diff --git a/docs/api/python/regular/kind.rst b/docs/api/python/regular/kind.rst index f2dd8550b..b4be797e0 100644 --- a/docs/api/python/regular/kind.rst +++ b/docs/api/python/regular/kind.rst @@ -2,11 +2,11 @@ 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>`). +example whether it is an equality (:py:obj:`Equal <pycvc5.Kind.Equal>`), a +conjunction (:py:obj:`And <pycvc5.Kind.And>`), or a bit-vector addtion +(:py:obj:`BVAdd <pycvc5.Kind.BVAdd>`). The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind <cvc5::api::Kind>` enum. -.. autoclass:: pycvc5.kinds +.. autoclass:: pycvc5.Kind :members: :undoc-members: diff --git a/docs/api/python/regular/python.rst b/docs/api/python/regular/python.rst index b054cbe16..84593b17f 100644 --- a/docs/api/python/regular/python.rst +++ b/docs/api/python/regular/python.rst @@ -1,4 +1,4 @@ -Python API Documentation +Regular Python API ======================== .. only:: not bindings_python @@ -8,7 +8,7 @@ Python API Documentation This documentation was built while python bindings were disabled. This part of the documentation is likely either empty or outdated. Please enable :code:`BUILD_BINDINGS_PYTHON` in :code:`cmake` and build the documentation again. .. toctree:: - :maxdepth: 1 + :maxdepth: 2 quickstart datatype diff --git a/docs/api/python/regular/quickstart.rst b/docs/api/python/regular/quickstart.rst index 783bcfd1f..ba3360db8 100644 --- a/docs/api/python/regular/quickstart.rst +++ b/docs/api/python/regular/quickstart.rst @@ -166,7 +166,7 @@ Example ------- | The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_. -| The source code for this example can be found at `examples/api/python/quickstart.py <https://github.com/cvc5/cvc5/blob/master/examples/api/python/quickstart.cpp>`_. +| The source code for this example can be found at `examples/api/python/quickstart.py <https://github.com/cvc5/cvc5/blob/master/examples/api/python/quickstart.py>`_. .. api-examples:: <examples>/api/cpp/quickstart.cpp diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/z3compat/z3compat.rst index ad7c8524b..d5a06195d 100644 --- a/docs/api/python/z3compat/z3compat.rst +++ b/docs/api/python/z3compat/z3compat.rst @@ -1,4 +1,4 @@ -z3py compatibility API +z3py compatibility Python API ========================================= .. only:: not bindings_python |