From: Gereon Kremer Date: Wed, 17 Nov 2021 19:40:49 +0000 (-0800) Subject: Add documentation for z3py compatibility API (#7652) X-Git-Tag: cvc5-1.0.0~804 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=21b15a0464bc6bbee801385c86930af3c63804bc;p=cvc5.git Add documentation for z3py compatibility API (#7652) 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. --- diff --git a/docs/api/api.rst b/docs/api/api.rst index 4a1fb7202..727caea4d 100644 --- a/docs/api/api.rst +++ b/docs/api/api.rst @@ -9,6 +9,6 @@ Additionally, a more pythonic Python API is availble at https://github.com/cvc5/ .. toctree:: :maxdepth: 1 - cpp/cpp - java/index - python/python + C++ API + Java API + Python API diff --git a/docs/api/python/CMakeLists.txt b/docs/api/python/CMakeLists.txt index cdac14de0..a6e46752a 100644 --- a/docs/api/python/CMakeLists.txt +++ b/docs/api/python/CMakeLists.txt @@ -17,5 +17,16 @@ add_custom_target(docs-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() diff --git a/docs/api/python/datatype.rst b/docs/api/python/datatype.rst deleted file mode 100644 index a6052b1f5..000000000 --- a/docs/api/python/datatype.rst +++ /dev/null @@ -1,6 +0,0 @@ -Datatype -======== - -.. autoclass:: pycvc5.Datatype - :members: - :undoc-members: diff --git a/docs/api/python/datatypeconstructor.rst b/docs/api/python/datatypeconstructor.rst deleted file mode 100644 index ed457562b..000000000 --- a/docs/api/python/datatypeconstructor.rst +++ /dev/null @@ -1,6 +0,0 @@ -DatatypeConstructor -=================== - -.. autoclass:: pycvc5.DatatypeConstructor - :members: - :undoc-members: diff --git a/docs/api/python/datatypeconstructordecl.rst b/docs/api/python/datatypeconstructordecl.rst deleted file mode 100644 index 77b1ea3f3..000000000 --- a/docs/api/python/datatypeconstructordecl.rst +++ /dev/null @@ -1,6 +0,0 @@ -DatatypeConstructorDecl -======================= - -.. autoclass:: pycvc5.DatatypeConstructorDecl - :members: - :undoc-members: diff --git a/docs/api/python/datatypedecl.rst b/docs/api/python/datatypedecl.rst deleted file mode 100644 index 0f61471f4..000000000 --- a/docs/api/python/datatypedecl.rst +++ /dev/null @@ -1,6 +0,0 @@ -DatatypeDecl -============ - -.. autoclass:: pycvc5.DatatypeDecl - :members: - :undoc-members: diff --git a/docs/api/python/datatypeselector.rst b/docs/api/python/datatypeselector.rst deleted file mode 100644 index 9c2ae22fe..000000000 --- a/docs/api/python/datatypeselector.rst +++ /dev/null @@ -1,6 +0,0 @@ -DatatypeSelector -================ - -.. autoclass:: pycvc5.DatatypeSelector - :members: - :undoc-members: diff --git a/docs/api/python/grammar.rst b/docs/api/python/grammar.rst deleted file mode 100644 index a2059fa93..000000000 --- a/docs/api/python/grammar.rst +++ /dev/null @@ -1,6 +0,0 @@ -Grammar -================ - -.. autoclass:: pycvc5.Grammar - :members: - :undoc-members: diff --git a/docs/api/python/op.rst b/docs/api/python/op.rst deleted file mode 100644 index 7769b33f0..000000000 --- a/docs/api/python/op.rst +++ /dev/null @@ -1,6 +0,0 @@ -Op -================ - -.. autoclass:: pycvc5.Op - :members: - :undoc-members: diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index 0cf78d0ce..3697cf579 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -1,25 +1,27 @@ Python API Documentation ======================== +.. toctree:: + :maxdepth: 1 + :hidden: + + z3py compatibility API + regular 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. -.. toctree:: - :maxdepth: 1 +cvc5 offers two separate APIs for Python users. +The :doc:`regular Python API ` is an almost exact copy of the :doc:`C++ API <../cpp/cpp>`. +Alternatively, the :doc:`z3py compatibility API ` is a more pythonic API that aims to be fully compatible with `Z3s Python API `_ 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 `. - 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 `. diff --git a/docs/api/python/quickstart.rst b/docs/api/python/quickstart.rst deleted file mode 100644 index 22a947010..000000000 --- a/docs/api/python/quickstart.rst +++ /dev/null @@ -1,175 +0,0 @@ -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 `_. -| The source code for this example can be found at `examples/api/python/quickstart.py `_. - -.. api-examples:: - ../../../examples/api/cpp/quickstart.cpp - ../../../examples/api/java/QuickStart.java - ../../../examples/api/python/quickstart.py - ../../../examples/api/smtlib/quickstart.smt2 diff --git a/docs/api/python/regular/datatype.rst b/docs/api/python/regular/datatype.rst new file mode 100644 index 000000000..a6052b1f5 --- /dev/null +++ b/docs/api/python/regular/datatype.rst @@ -0,0 +1,6 @@ +Datatype +======== + +.. autoclass:: pycvc5.Datatype + :members: + :undoc-members: diff --git a/docs/api/python/regular/datatypeconstructor.rst b/docs/api/python/regular/datatypeconstructor.rst new file mode 100644 index 000000000..ed457562b --- /dev/null +++ b/docs/api/python/regular/datatypeconstructor.rst @@ -0,0 +1,6 @@ +DatatypeConstructor +=================== + +.. autoclass:: pycvc5.DatatypeConstructor + :members: + :undoc-members: diff --git a/docs/api/python/regular/datatypeconstructordecl.rst b/docs/api/python/regular/datatypeconstructordecl.rst new file mode 100644 index 000000000..77b1ea3f3 --- /dev/null +++ b/docs/api/python/regular/datatypeconstructordecl.rst @@ -0,0 +1,6 @@ +DatatypeConstructorDecl +======================= + +.. autoclass:: pycvc5.DatatypeConstructorDecl + :members: + :undoc-members: diff --git a/docs/api/python/regular/datatypedecl.rst b/docs/api/python/regular/datatypedecl.rst new file mode 100644 index 000000000..0f61471f4 --- /dev/null +++ b/docs/api/python/regular/datatypedecl.rst @@ -0,0 +1,6 @@ +DatatypeDecl +============ + +.. autoclass:: pycvc5.DatatypeDecl + :members: + :undoc-members: diff --git a/docs/api/python/regular/datatypeselector.rst b/docs/api/python/regular/datatypeselector.rst new file mode 100644 index 000000000..9c2ae22fe --- /dev/null +++ b/docs/api/python/regular/datatypeselector.rst @@ -0,0 +1,6 @@ +DatatypeSelector +================ + +.. autoclass:: pycvc5.DatatypeSelector + :members: + :undoc-members: diff --git a/docs/api/python/regular/grammar.rst b/docs/api/python/regular/grammar.rst new file mode 100644 index 000000000..a2059fa93 --- /dev/null +++ b/docs/api/python/regular/grammar.rst @@ -0,0 +1,6 @@ +Grammar +================ + +.. autoclass:: pycvc5.Grammar + :members: + :undoc-members: diff --git a/docs/api/python/regular/op.rst b/docs/api/python/regular/op.rst new file mode 100644 index 000000000..7769b33f0 --- /dev/null +++ b/docs/api/python/regular/op.rst @@ -0,0 +1,6 @@ +Op +================ + +.. autoclass:: pycvc5.Op + :members: + :undoc-members: diff --git a/docs/api/python/regular/python.rst b/docs/api/python/regular/python.rst new file mode 100644 index 000000000..0cf78d0ce --- /dev/null +++ b/docs/api/python/regular/python.rst @@ -0,0 +1,25 @@ +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 diff --git a/docs/api/python/regular/quickstart.rst b/docs/api/python/regular/quickstart.rst new file mode 100644 index 000000000..bf8773ce8 --- /dev/null +++ b/docs/api/python/regular/quickstart.rst @@ -0,0 +1,175 @@ +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 `_. +| The source code for this example can be found at `examples/api/python/quickstart.py `_. + +.. api-examples:: + ../../../../examples/api/cpp/quickstart.cpp + ../../../../examples/api/java/QuickStart.java + ../../../../examples/api/python/quickstart.py + ../../../../examples/api/smtlib/quickstart.smt2 diff --git a/docs/api/python/regular/result.rst b/docs/api/python/regular/result.rst new file mode 100644 index 000000000..9edb12b92 --- /dev/null +++ b/docs/api/python/regular/result.rst @@ -0,0 +1,6 @@ +Result +================ + +.. autoclass:: pycvc5.Result + :members: + :undoc-members: diff --git a/docs/api/python/regular/roundingmode.rst b/docs/api/python/regular/roundingmode.rst new file mode 100644 index 000000000..0c226082e --- /dev/null +++ b/docs/api/python/regular/roundingmode.rst @@ -0,0 +1,6 @@ +RoundingMode +================ + +.. autoclass:: pycvc5.RoundingMode + :members: + :undoc-members: diff --git a/docs/api/python/regular/solver.rst b/docs/api/python/regular/solver.rst new file mode 100644 index 000000000..2147a1f76 --- /dev/null +++ b/docs/api/python/regular/solver.rst @@ -0,0 +1,6 @@ +Solver +======== + +.. autoclass:: pycvc5.Solver + :members: + :undoc-members: diff --git a/docs/api/python/regular/sort.rst b/docs/api/python/regular/sort.rst new file mode 100644 index 000000000..270113e0c --- /dev/null +++ b/docs/api/python/regular/sort.rst @@ -0,0 +1,6 @@ +Sort +================ + +.. autoclass:: pycvc5.Sort + :members: + :undoc-members: diff --git a/docs/api/python/regular/unknownexplanation.rst b/docs/api/python/regular/unknownexplanation.rst new file mode 100644 index 000000000..aee134582 --- /dev/null +++ b/docs/api/python/regular/unknownexplanation.rst @@ -0,0 +1,6 @@ +UnknownExplanation +================== + +.. autoclass:: pycvc5.UnknownExplanation + :members: + :undoc-members: diff --git a/docs/api/python/result.rst b/docs/api/python/result.rst deleted file mode 100644 index 9edb12b92..000000000 --- a/docs/api/python/result.rst +++ /dev/null @@ -1,6 +0,0 @@ -Result -================ - -.. autoclass:: pycvc5.Result - :members: - :undoc-members: diff --git a/docs/api/python/roundingmode.rst b/docs/api/python/roundingmode.rst deleted file mode 100644 index 0c226082e..000000000 --- a/docs/api/python/roundingmode.rst +++ /dev/null @@ -1,6 +0,0 @@ -RoundingMode -================ - -.. autoclass:: pycvc5.RoundingMode - :members: - :undoc-members: diff --git a/docs/api/python/solver.rst b/docs/api/python/solver.rst deleted file mode 100644 index 2147a1f76..000000000 --- a/docs/api/python/solver.rst +++ /dev/null @@ -1,6 +0,0 @@ -Solver -======== - -.. autoclass:: pycvc5.Solver - :members: - :undoc-members: diff --git a/docs/api/python/sort.rst b/docs/api/python/sort.rst deleted file mode 100644 index 270113e0c..000000000 --- a/docs/api/python/sort.rst +++ /dev/null @@ -1,6 +0,0 @@ -Sort -================ - -.. autoclass:: pycvc5.Sort - :members: - :undoc-members: diff --git a/docs/api/python/unknownexplanation.rst b/docs/api/python/unknownexplanation.rst deleted file mode 100644 index aee134582..000000000 --- a/docs/api/python/unknownexplanation.rst +++ /dev/null @@ -1,6 +0,0 @@ -UnknownExplanation -================== - -.. autoclass:: pycvc5.UnknownExplanation - :members: - :undoc-members: diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/z3compat/z3compat.rst new file mode 100644 index 000000000..a9db13d49 --- /dev/null +++ b/docs/api/python/z3compat/z3compat.rst @@ -0,0 +1,14 @@ +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: diff --git a/docs/conf.py.in b/docs/conf.py.in index f91997646..b8aacf129 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -18,6 +18,7 @@ sys.path.insert(0, '${CMAKE_CURRENT_SOURCE_DIR}/ext/') # 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')