From 21b15a0464bc6bbee801385c86930af3c63804bc Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 17 Nov 2021 11:40:49 -0800 Subject: [PATCH] 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. --- docs/api/api.rst | 6 +-- docs/api/python/CMakeLists.txt | 13 +++++- docs/api/python/python.rst | 32 ++++++++------- docs/api/python/{ => regular}/datatype.rst | 0 .../{ => regular}/datatypeconstructor.rst | 0 .../{ => regular}/datatypeconstructordecl.rst | 0 .../api/python/{ => regular}/datatypedecl.rst | 0 .../python/{ => regular}/datatypeselector.rst | 0 docs/api/python/{ => regular}/grammar.rst | 0 docs/api/python/{ => regular}/op.rst | 0 docs/api/python/regular/python.rst | 25 ++++++++++++ docs/api/python/{ => regular}/quickstart.rst | 40 +++++++++---------- docs/api/python/{ => regular}/result.rst | 0 .../api/python/{ => regular}/roundingmode.rst | 0 docs/api/python/{ => regular}/solver.rst | 0 docs/api/python/{ => regular}/sort.rst | 0 .../{ => regular}/unknownexplanation.rst | 0 docs/api/python/z3compat/z3compat.rst | 14 +++++++ docs/conf.py.in | 1 + 19 files changed, 92 insertions(+), 39 deletions(-) rename docs/api/python/{ => regular}/datatype.rst (100%) rename docs/api/python/{ => regular}/datatypeconstructor.rst (100%) rename docs/api/python/{ => regular}/datatypeconstructordecl.rst (100%) rename docs/api/python/{ => regular}/datatypedecl.rst (100%) rename docs/api/python/{ => regular}/datatypeselector.rst (100%) rename docs/api/python/{ => regular}/grammar.rst (100%) rename docs/api/python/{ => regular}/op.rst (100%) create mode 100644 docs/api/python/regular/python.rst rename docs/api/python/{ => regular}/quickstart.rst (75%) rename docs/api/python/{ => regular}/result.rst (100%) rename docs/api/python/{ => regular}/roundingmode.rst (100%) rename docs/api/python/{ => regular}/solver.rst (100%) rename docs/api/python/{ => regular}/sort.rst (100%) rename docs/api/python/{ => regular}/unknownexplanation.rst (100%) create mode 100644 docs/api/python/z3compat/z3compat.rst 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/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/datatype.rst b/docs/api/python/regular/datatype.rst similarity index 100% rename from docs/api/python/datatype.rst rename to docs/api/python/regular/datatype.rst diff --git a/docs/api/python/datatypeconstructor.rst b/docs/api/python/regular/datatypeconstructor.rst similarity index 100% rename from docs/api/python/datatypeconstructor.rst rename to docs/api/python/regular/datatypeconstructor.rst diff --git a/docs/api/python/datatypeconstructordecl.rst b/docs/api/python/regular/datatypeconstructordecl.rst similarity index 100% rename from docs/api/python/datatypeconstructordecl.rst rename to docs/api/python/regular/datatypeconstructordecl.rst diff --git a/docs/api/python/datatypedecl.rst b/docs/api/python/regular/datatypedecl.rst similarity index 100% rename from docs/api/python/datatypedecl.rst rename to docs/api/python/regular/datatypedecl.rst diff --git a/docs/api/python/datatypeselector.rst b/docs/api/python/regular/datatypeselector.rst similarity index 100% rename from docs/api/python/datatypeselector.rst rename to docs/api/python/regular/datatypeselector.rst diff --git a/docs/api/python/grammar.rst b/docs/api/python/regular/grammar.rst similarity index 100% rename from docs/api/python/grammar.rst rename to docs/api/python/regular/grammar.rst diff --git a/docs/api/python/op.rst b/docs/api/python/regular/op.rst similarity index 100% rename from docs/api/python/op.rst rename to docs/api/python/regular/op.rst 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/quickstart.rst b/docs/api/python/regular/quickstart.rst similarity index 75% rename from docs/api/python/quickstart.rst rename to docs/api/python/regular/quickstart.rst index 22a947010..bf8773ce8 100644 --- a/docs/api/python/quickstart.rst +++ b/docs/api/python/regular/quickstart.rst @@ -3,14 +3,14 @@ Quickstart Guide First, create a cvc5 solver instance: -.. literalinclude:: ../../../examples/api/python/quickstart.py +.. 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 +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 26-27 @@ -21,14 +21,14 @@ 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 +.. 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 +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 40-41 @@ -36,7 +36,7 @@ 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 +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 46-49 @@ -48,7 +48,7 @@ We define the following constraints regarding ``x`` and ``y``: We construct the required terms and assert them as follows: -.. literalinclude:: ../../../examples/api/python/quickstart.py +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 59-81 @@ -56,7 +56,7 @@ 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 +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 85 @@ -65,7 +65,7 @@ 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 +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 89-90 @@ -79,20 +79,20 @@ This will print: Now, we query the solver for the values for ``x`` and ``y`` that satisfy the constraints. -.. literalinclude:: ../../../examples/api/python/quickstart.py +.. 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 +.. 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 +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 102-108 @@ -109,7 +109,7 @@ 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 +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 114-118 @@ -123,7 +123,7 @@ 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 +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 130 @@ -131,13 +131,13 @@ 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 +.. 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 +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 142, 145-146 @@ -151,7 +151,7 @@ This time the asserted formula is unsatisfiable: 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 +.. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python :lines: 150-152 @@ -169,7 +169,7 @@ Example | 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 + ../../../../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/result.rst b/docs/api/python/regular/result.rst similarity index 100% rename from docs/api/python/result.rst rename to docs/api/python/regular/result.rst diff --git a/docs/api/python/roundingmode.rst b/docs/api/python/regular/roundingmode.rst similarity index 100% rename from docs/api/python/roundingmode.rst rename to docs/api/python/regular/roundingmode.rst diff --git a/docs/api/python/solver.rst b/docs/api/python/regular/solver.rst similarity index 100% rename from docs/api/python/solver.rst rename to docs/api/python/regular/solver.rst diff --git a/docs/api/python/sort.rst b/docs/api/python/regular/sort.rst similarity index 100% rename from docs/api/python/sort.rst rename to docs/api/python/regular/sort.rst diff --git a/docs/api/python/unknownexplanation.rst b/docs/api/python/regular/unknownexplanation.rst similarity index 100% rename from docs/api/python/unknownexplanation.rst rename to docs/api/python/regular/unknownexplanation.rst 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') -- 2.30.2