mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
21b15a0464
This PR includes documentation for the z3py compatibility API into our general API. It does so by adding the z3py compatibility API as an external project to download it and then have sphinx document it via the autodoc extension that we already use for our regular python API. Right now we simply show everything on one page, which should be refactored in the future.
28 lines
1.2 KiB
ReStructuredText
28 lines
1.2 KiB
ReStructuredText
Python API Documentation
|
|
========================
|
|
|
|
.. toctree::
|
|
:maxdepth: 1
|
|
:hidden:
|
|
|
|
z3py compatibility API <z3compat/z3compat>
|
|
regular Python API <regular/python>
|
|
|
|
.. 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 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.
|
|
|
|
|
|
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>`.
|