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.
.. toctree::
:maxdepth: 1
- cpp/cpp
- java/index
- python/python
+ C++ API <cpp/cpp>
+ Java API <java/index>
+ Python API <python/python>
if (BUILD_BINDINGS_PYTHON)
# Python API docs are generated from built python API
- add_dependencies(docs-python pycvc5)
+ ExternalProject_Add(
+ z3pycompat-EP
+ ${COMMON_EP_CONFIG}
+ GIT_REPOSITORY https://github.com/cvc5/cvc5_z3py_compat.git
+ GIT_TAG main
+ CONFIGURE_COMMAND ""
+ BUILD_COMMAND ""
+ INSTALL_COMMAND ""
+ DEPENDS pycvc5
+ )
+
+ add_dependencies(docs-python pycvc5 z3pycompat-EP)
endif()
+++ /dev/null
-Datatype
-========
-
-.. autoclass:: pycvc5.Datatype
- :members:
- :undoc-members:
+++ /dev/null
-DatatypeConstructor
-===================
-
-.. autoclass:: pycvc5.DatatypeConstructor
- :members:
- :undoc-members:
+++ /dev/null
-DatatypeConstructorDecl
-=======================
-
-.. autoclass:: pycvc5.DatatypeConstructorDecl
- :members:
- :undoc-members:
+++ /dev/null
-DatatypeDecl
-============
-
-.. autoclass:: pycvc5.DatatypeDecl
- :members:
- :undoc-members:
+++ /dev/null
-DatatypeSelector
-================
-
-.. autoclass:: pycvc5.DatatypeSelector
- :members:
- :undoc-members:
+++ /dev/null
-Grammar
-================
-
-.. autoclass:: pycvc5.Grammar
- :members:
- :undoc-members:
+++ /dev/null
-Op
-================
-
-.. autoclass:: pycvc5.Op
- :members:
- :undoc-members:
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.
-.. toctree::
- :maxdepth: 1
+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>`.
- quickstart
- datatype
- datatypeconstructor
- datatypeconstructordecl
- datatypedecl
- datatypeselector
- grammar
- op
- result
- roundingmode
- solver
- sort
- unknownexplanation
+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>`.
+++ /dev/null
-Quickstart Guide
-================
-
-First, create a cvc5 solver instance:
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 22
-
-We will ask the solver to produce models and unsat cores in the following,
-and for this we have to enable the following options.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 26-27
-
-Next we set the logic.
-The simplest way to set a logic for the solver is to choose ``"ALL"``.
-This enables all logics in the solver.
-Alternatively, ``"QF_ALL"`` enables all logics without quantifiers.
-To optimize the solver's behavior for a more specific logic,
-use the logic name, e.g. ``"QF_BV"`` or ``"QF_AUFBV"``.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 36
-
-In the following, we will define constraints of reals and integers.
-For this, we first query the solver for the corresponding sorts.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 40-41
-
-Now, we create two constants ``x`` and ``y`` of sort ``Real``,
-and two constants ``a`` and ``b`` of sort ``Integer``.
-Notice that these are *symbolic* constants, but not actual values.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 46-49
-
-We define the following constraints regarding ``x`` and ``y``:
-
-.. math::
-
- (0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y)
-
-We construct the required terms and assert them as follows:
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 59-81
-
-Now we check if the asserted formula is satisfiable, that is, we check if
-there exist values of sort ``Real`` for ``x`` and ``y`` that satisfy all
-the constraints.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 85
-
-The result we get from this satisfiability check is either ``sat``, ``unsat``
-or ``unknown``.
-It's status can be queried via `isSat`, `isUnsat` and `isSatUnknown` functions.
-Alternatively, it can also be printed.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 89-90
-
-This will print:
-
-.. code:: text
-
- expected: sat
- result: sat
-
-Now, we query the solver for the values for ``x`` and ``y`` that satisfy
-the constraints.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 93-94
-
-It is also possible to get values for terms that do not appear in the original
-formula.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 98-99
-
-We can retrieve the Python representation of these values as follows.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 102-108
-
-This will print the following:
-
-.. code:: text
-
- value for x: 1/6
- value for y: 1/6
- value for x - y: 0
-
-Another way to independently compute the value of ``x - y`` would be to
-use the Python minus operator instead of asking the solver.
-However, for more complex terms, it is easier to let the solver do the
-evaluation.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 114-118
-
-This will print:
-
-.. code:: text
-
- computed correctly
-
-Next, we will check satisfiability of the same formula,
-only this time over integer variables ``a`` and ``b``.
-For this, we first reset the assertions added to the solver.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 130
-
-Next, we assert the same assertions as above, but with integers.
-This time, we inline the construction of terms
-to the assertion command.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 135-139
-
-Now, we check whether the revised assertion is satisfiable.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 142, 145-146
-
-This time the asserted formula is unsatisfiable:
-
-.. code:: text
-
- expected: unsat
- result: unsat
-
-We can query the solver for an unsatisfiable core, that is, a subset
-of the assertions that is already unsatisfiable.
-
-.. literalinclude:: ../../../examples/api/python/quickstart.py
- :language: python
- :lines: 150-152
-
-This will print:
-
-.. code:: text
-
- unsat core size: 3
- unsat core: [(< 0 a), (< 0 b), (< (+ a b) 1)]
-
-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>`_.
-
-.. api-examples::
- ../../../examples/api/cpp/quickstart.cpp
- ../../../examples/api/java/QuickStart.java
- ../../../examples/api/python/quickstart.py
- ../../../examples/api/smtlib/quickstart.smt2
--- /dev/null
+Datatype
+========
+
+.. autoclass:: pycvc5.Datatype
+ :members:
+ :undoc-members:
--- /dev/null
+DatatypeConstructor
+===================
+
+.. autoclass:: pycvc5.DatatypeConstructor
+ :members:
+ :undoc-members:
--- /dev/null
+DatatypeConstructorDecl
+=======================
+
+.. autoclass:: pycvc5.DatatypeConstructorDecl
+ :members:
+ :undoc-members:
--- /dev/null
+DatatypeDecl
+============
+
+.. autoclass:: pycvc5.DatatypeDecl
+ :members:
+ :undoc-members:
--- /dev/null
+DatatypeSelector
+================
+
+.. autoclass:: pycvc5.DatatypeSelector
+ :members:
+ :undoc-members:
--- /dev/null
+Grammar
+================
+
+.. autoclass:: pycvc5.Grammar
+ :members:
+ :undoc-members:
--- /dev/null
+Op
+================
+
+.. autoclass:: pycvc5.Op
+ :members:
+ :undoc-members:
--- /dev/null
+Python API Documentation
+========================
+
+.. 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.
+
+.. toctree::
+ :maxdepth: 1
+
+ quickstart
+ datatype
+ datatypeconstructor
+ datatypeconstructordecl
+ datatypedecl
+ datatypeselector
+ grammar
+ op
+ result
+ roundingmode
+ solver
+ sort
+ unknownexplanation
--- /dev/null
+Quickstart Guide
+================
+
+First, create a cvc5 solver instance:
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 22
+
+We will ask the solver to produce models and unsat cores in the following,
+and for this we have to enable the following options.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 26-27
+
+Next we set the logic.
+The simplest way to set a logic for the solver is to choose ``"ALL"``.
+This enables all logics in the solver.
+Alternatively, ``"QF_ALL"`` enables all logics without quantifiers.
+To optimize the solver's behavior for a more specific logic,
+use the logic name, e.g. ``"QF_BV"`` or ``"QF_AUFBV"``.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 36
+
+In the following, we will define constraints of reals and integers.
+For this, we first query the solver for the corresponding sorts.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 40-41
+
+Now, we create two constants ``x`` and ``y`` of sort ``Real``,
+and two constants ``a`` and ``b`` of sort ``Integer``.
+Notice that these are *symbolic* constants, but not actual values.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 46-49
+
+We define the following constraints regarding ``x`` and ``y``:
+
+.. math::
+
+ (0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y)
+
+We construct the required terms and assert them as follows:
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 59-81
+
+Now we check if the asserted formula is satisfiable, that is, we check if
+there exist values of sort ``Real`` for ``x`` and ``y`` that satisfy all
+the constraints.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 85
+
+The result we get from this satisfiability check is either ``sat``, ``unsat``
+or ``unknown``.
+It's status can be queried via `isSat`, `isUnsat` and `isSatUnknown` functions.
+Alternatively, it can also be printed.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 89-90
+
+This will print:
+
+.. code:: text
+
+ expected: sat
+ result: sat
+
+Now, we query the solver for the values for ``x`` and ``y`` that satisfy
+the constraints.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 93-94
+
+It is also possible to get values for terms that do not appear in the original
+formula.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 98-99
+
+We can retrieve the Python representation of these values as follows.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 102-108
+
+This will print the following:
+
+.. code:: text
+
+ value for x: 1/6
+ value for y: 1/6
+ value for x - y: 0
+
+Another way to independently compute the value of ``x - y`` would be to
+use the Python minus operator instead of asking the solver.
+However, for more complex terms, it is easier to let the solver do the
+evaluation.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 114-118
+
+This will print:
+
+.. code:: text
+
+ computed correctly
+
+Next, we will check satisfiability of the same formula,
+only this time over integer variables ``a`` and ``b``.
+For this, we first reset the assertions added to the solver.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 130
+
+Next, we assert the same assertions as above, but with integers.
+This time, we inline the construction of terms
+to the assertion command.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 135-139
+
+Now, we check whether the revised assertion is satisfiable.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 142, 145-146
+
+This time the asserted formula is unsatisfiable:
+
+.. code:: text
+
+ expected: unsat
+ result: unsat
+
+We can query the solver for an unsatisfiable core, that is, a subset
+of the assertions that is already unsatisfiable.
+
+.. literalinclude:: ../../../../examples/api/python/quickstart.py
+ :language: python
+ :lines: 150-152
+
+This will print:
+
+.. code:: text
+
+ unsat core size: 3
+ unsat core: [(< 0 a), (< 0 b), (< (+ a b) 1)]
+
+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>`_.
+
+.. api-examples::
+ ../../../../examples/api/cpp/quickstart.cpp
+ ../../../../examples/api/java/QuickStart.java
+ ../../../../examples/api/python/quickstart.py
+ ../../../../examples/api/smtlib/quickstart.smt2
--- /dev/null
+Result
+================
+
+.. autoclass:: pycvc5.Result
+ :members:
+ :undoc-members:
--- /dev/null
+RoundingMode
+================
+
+.. autoclass:: pycvc5.RoundingMode
+ :members:
+ :undoc-members:
--- /dev/null
+Solver
+========
+
+.. autoclass:: pycvc5.Solver
+ :members:
+ :undoc-members:
--- /dev/null
+Sort
+================
+
+.. autoclass:: pycvc5.Sort
+ :members:
+ :undoc-members:
--- /dev/null
+UnknownExplanation
+==================
+
+.. autoclass:: pycvc5.UnknownExplanation
+ :members:
+ :undoc-members:
+++ /dev/null
-Result
-================
-
-.. autoclass:: pycvc5.Result
- :members:
- :undoc-members:
+++ /dev/null
-RoundingMode
-================
-
-.. autoclass:: pycvc5.RoundingMode
- :members:
- :undoc-members:
+++ /dev/null
-Solver
-========
-
-.. autoclass:: pycvc5.Solver
- :members:
- :undoc-members:
+++ /dev/null
-Sort
-================
-
-.. autoclass:: pycvc5.Sort
- :members:
- :undoc-members:
+++ /dev/null
-UnknownExplanation
-==================
-
-.. autoclass:: pycvc5.UnknownExplanation
- :members:
- :undoc-members:
--- /dev/null
+z3py compatibility 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.
+
+
+.. automodule:: cvc5_z3py_compat
+ :members:
+ :private-members:
+ :imported-members:
# path to python api
sys.path.insert(0, '${CMAKE_BINARY_DIR}/src/api/python')
+sys.path.insert(0, '${CMAKE_BINARY_DIR}/deps/src/z3pycompat-EP')
if("${BUILD_BINDINGS_PYTHON}" == "ON"):
tags.add('bindings_python')
projects / cvc5.git / commitdiff