mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
881464ade1
This PR does multiple things: - the kinds are changed from custom objects to a proper enum.Enum class (including according changes to the cython code and the kind generation scripts) - all examples and tests are modified to account for the change how to use kinds (Kind instead of kinds) - add docstrings to the kind enum values - add a custom documenter that properly renders enums via autodoc - extend doxygen setup so that we can write comments as rst (allowing us to copy the documentation for kinds from the cpp api to the other apis)
27 lines
1.2 KiB
ReStructuredText
27 lines
1.2 KiB
ReStructuredText
Python API
|
|
========================
|
|
|
|
.. only:: not bindings_python
|
|
|
|
.. warning::
|
|
|
|
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.
|
|
|
|
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 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?
|
|
------------------------------
|
|
|
|
If you are a new user, or already have an application that uses Z3's python API, use the :doc:`z3py compatibility API <z3compat/z3compat>`.
|
|
|
|
If you would like a more feature-complete python API, with the ability to do almost everything that the cpp API allows, use the :doc:`regular Python API <regular/python>`.
|