From 082ffeaffc2975da6da574e0f0ed65a007691a18 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 14 Jan 2022 13:45:19 -0800 Subject: [PATCH] Rename python APIs (#7950) Rename python APIs to "base" and "pythonic" --- docs/api/api.rst | 5 +++-- docs/api/python/{regular => base}/datatype.rst | 0 .../{regular => base}/datatypeconstructor.rst | 0 .../{regular => base}/datatypeconstructordecl.rst | 0 docs/api/python/{regular => base}/datatypedecl.rst | 0 .../python/{regular => base}/datatypeselector.rst | 0 docs/api/python/{regular => base}/grammar.rst | 0 docs/api/python/{regular => base}/kind.rst | 0 docs/api/python/{regular => base}/op.rst | 0 docs/api/python/{regular => base}/python.rst | 7 ++++++- docs/api/python/{regular => base}/quickstart.rst | 0 docs/api/python/{regular => base}/result.rst | 0 docs/api/python/{regular => base}/roundingmode.rst | 0 docs/api/python/{regular => base}/solver.rst | 0 docs/api/python/{regular => base}/sort.rst | 0 docs/api/python/{regular => base}/term.rst | 0 .../{regular => base}/unknownexplanation.rst | 0 docs/api/python/python.rst | 14 ++++++++------ docs/api/python/{z3compat => pythonic}/arith.rst | 0 docs/api/python/{z3compat => pythonic}/array.rst | 0 docs/api/python/{z3compat => pythonic}/bitvec.rst | 0 docs/api/python/{z3compat => pythonic}/boolean.rst | 0 docs/api/python/{z3compat => pythonic}/dt.rst | 0 docs/api/python/{z3compat => pythonic}/fp.rst | 0 .../python/{z3compat => pythonic}/internals.rst | 0 .../z3compat.rst => pythonic/pythonic.rst} | 4 ++-- docs/api/python/{z3compat => pythonic}/quant.rst | 0 .../python/{z3compat => pythonic}/quickstart.rst | 0 docs/api/python/{z3compat => pythonic}/set.rst | 0 docs/api/python/{z3compat => pythonic}/solver.rst | 0 docs/conf.py.in | 4 ++-- 31 files changed, 21 insertions(+), 13 deletions(-) rename docs/api/python/{regular => base}/datatype.rst (100%) rename docs/api/python/{regular => base}/datatypeconstructor.rst (100%) rename docs/api/python/{regular => base}/datatypeconstructordecl.rst (100%) rename docs/api/python/{regular => base}/datatypedecl.rst (100%) rename docs/api/python/{regular => base}/datatypeselector.rst (100%) rename docs/api/python/{regular => base}/grammar.rst (100%) rename docs/api/python/{regular => base}/kind.rst (100%) rename docs/api/python/{regular => base}/op.rst (100%) rename docs/api/python/{regular => base}/python.rst (73%) rename docs/api/python/{regular => base}/quickstart.rst (100%) rename docs/api/python/{regular => base}/result.rst (100%) rename docs/api/python/{regular => base}/roundingmode.rst (100%) rename docs/api/python/{regular => base}/solver.rst (100%) rename docs/api/python/{regular => base}/sort.rst (100%) rename docs/api/python/{regular => base}/term.rst (100%) rename docs/api/python/{regular => base}/unknownexplanation.rst (100%) rename docs/api/python/{z3compat => pythonic}/arith.rst (100%) rename docs/api/python/{z3compat => pythonic}/array.rst (100%) rename docs/api/python/{z3compat => pythonic}/bitvec.rst (100%) rename docs/api/python/{z3compat => pythonic}/boolean.rst (100%) rename docs/api/python/{z3compat => pythonic}/dt.rst (100%) rename docs/api/python/{z3compat => pythonic}/fp.rst (100%) rename docs/api/python/{z3compat => pythonic}/internals.rst (100%) rename docs/api/python/{z3compat/z3compat.rst => pythonic/pythonic.rst} (92%) rename docs/api/python/{z3compat => pythonic}/quant.rst (100%) rename docs/api/python/{z3compat => pythonic}/quickstart.rst (100%) rename docs/api/python/{z3compat => pythonic}/set.rst (100%) rename docs/api/python/{z3compat => pythonic}/solver.rst (100%) diff --git a/docs/api/api.rst b/docs/api/api.rst index 3eff4bd1c..63533855c 100644 --- a/docs/api/api.rst +++ b/docs/api/api.rst @@ -3,8 +3,9 @@ API Documentation In addition to using cvc5 :doc:`as a binary <../binary/binary>`, cvc5 features APIs for several different programming languages. -While the :doc:`C++ API ` is considered the primary interface to cvc5, both the :doc:`Java API ` and the :doc:`Python API ` implement a thin wrapper around it. -Additionally, a more pythonic Python API is available at https://github.com/cvc5/cvc5_z3py_compat. +While the :doc:`C++ API ` is considered the primary interface to cvc5, both the :doc:`Java API ` and the :doc:`base Python API ` implement a thin wrapper around it. +Additionally, a more pythonic Python API is available at https://github.com/cvc5/cvc5_z3py_compat +and documented :doc:`here `. .. toctree:: :maxdepth: 1 diff --git a/docs/api/python/regular/datatype.rst b/docs/api/python/base/datatype.rst similarity index 100% rename from docs/api/python/regular/datatype.rst rename to docs/api/python/base/datatype.rst diff --git a/docs/api/python/regular/datatypeconstructor.rst b/docs/api/python/base/datatypeconstructor.rst similarity index 100% rename from docs/api/python/regular/datatypeconstructor.rst rename to docs/api/python/base/datatypeconstructor.rst diff --git a/docs/api/python/regular/datatypeconstructordecl.rst b/docs/api/python/base/datatypeconstructordecl.rst similarity index 100% rename from docs/api/python/regular/datatypeconstructordecl.rst rename to docs/api/python/base/datatypeconstructordecl.rst diff --git a/docs/api/python/regular/datatypedecl.rst b/docs/api/python/base/datatypedecl.rst similarity index 100% rename from docs/api/python/regular/datatypedecl.rst rename to docs/api/python/base/datatypedecl.rst diff --git a/docs/api/python/regular/datatypeselector.rst b/docs/api/python/base/datatypeselector.rst similarity index 100% rename from docs/api/python/regular/datatypeselector.rst rename to docs/api/python/base/datatypeselector.rst diff --git a/docs/api/python/regular/grammar.rst b/docs/api/python/base/grammar.rst similarity index 100% rename from docs/api/python/regular/grammar.rst rename to docs/api/python/base/grammar.rst diff --git a/docs/api/python/regular/kind.rst b/docs/api/python/base/kind.rst similarity index 100% rename from docs/api/python/regular/kind.rst rename to docs/api/python/base/kind.rst diff --git a/docs/api/python/regular/op.rst b/docs/api/python/base/op.rst similarity index 100% rename from docs/api/python/regular/op.rst rename to docs/api/python/base/op.rst diff --git a/docs/api/python/regular/python.rst b/docs/api/python/base/python.rst similarity index 73% rename from docs/api/python/regular/python.rst rename to docs/api/python/base/python.rst index 84593b17f..5036fa081 100644 --- a/docs/api/python/regular/python.rst +++ b/docs/api/python/base/python.rst @@ -1,4 +1,4 @@ -Regular Python API +Base Python API ======================== .. only:: not bindings_python @@ -7,6 +7,11 @@ Regular Python API 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. +This is the base Python API. +It is an almost exact copy of the :doc:`C++ API <../../cpp/cpp>`. + +See the :doc:`pythonic API <../pythonic/pythonic>` for a higher-level programming experience. + .. toctree:: :maxdepth: 2 diff --git a/docs/api/python/regular/quickstart.rst b/docs/api/python/base/quickstart.rst similarity index 100% rename from docs/api/python/regular/quickstart.rst rename to docs/api/python/base/quickstart.rst diff --git a/docs/api/python/regular/result.rst b/docs/api/python/base/result.rst similarity index 100% rename from docs/api/python/regular/result.rst rename to docs/api/python/base/result.rst diff --git a/docs/api/python/regular/roundingmode.rst b/docs/api/python/base/roundingmode.rst similarity index 100% rename from docs/api/python/regular/roundingmode.rst rename to docs/api/python/base/roundingmode.rst diff --git a/docs/api/python/regular/solver.rst b/docs/api/python/base/solver.rst similarity index 100% rename from docs/api/python/regular/solver.rst rename to docs/api/python/base/solver.rst diff --git a/docs/api/python/regular/sort.rst b/docs/api/python/base/sort.rst similarity index 100% rename from docs/api/python/regular/sort.rst rename to docs/api/python/base/sort.rst diff --git a/docs/api/python/regular/term.rst b/docs/api/python/base/term.rst similarity index 100% rename from docs/api/python/regular/term.rst rename to docs/api/python/base/term.rst diff --git a/docs/api/python/regular/unknownexplanation.rst b/docs/api/python/base/unknownexplanation.rst similarity index 100% rename from docs/api/python/regular/unknownexplanation.rst rename to docs/api/python/base/unknownexplanation.rst diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index b3bd865be..9763b45aa 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -8,19 +8,21 @@ Python API 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 ` is an almost exact copy of the :doc:`C++ API <../cpp/cpp>`. -Alternatively, the :doc:`z3py compatibility Python API ` is a more pythonic API that aims to be fully compatible with `Z3s Python API `_ while adding functionality that Z3 does not support. +The :doc:`base Python API ` is an almost exact copy of the :doc:`C++ API <../cpp/cpp>`. +Alternatively, the :doc:`pythonic API ` is a more pythonic API that aims to be fully compatible with `Z3s Python API `_ while adding functionality that Z3 does not support. .. toctree:: :maxdepth: 1 - z3compat/z3compat - regular/python + pythonic/pythonic + base/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 `. +If you are a new user, or already have an application that uses Z3's python API, use the :doc:`pythonic API `. -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 `. +If you would like a more feature-complete---yet verbose---python API, with the ability to do almost everything that the cpp API allows, use the :doc:`base Python API `. + +You can compare examples using the two APIs by visiting the :doc:`examples page <../../examples/quickstart>`. diff --git a/docs/api/python/z3compat/arith.rst b/docs/api/python/pythonic/arith.rst similarity index 100% rename from docs/api/python/z3compat/arith.rst rename to docs/api/python/pythonic/arith.rst diff --git a/docs/api/python/z3compat/array.rst b/docs/api/python/pythonic/array.rst similarity index 100% rename from docs/api/python/z3compat/array.rst rename to docs/api/python/pythonic/array.rst diff --git a/docs/api/python/z3compat/bitvec.rst b/docs/api/python/pythonic/bitvec.rst similarity index 100% rename from docs/api/python/z3compat/bitvec.rst rename to docs/api/python/pythonic/bitvec.rst diff --git a/docs/api/python/z3compat/boolean.rst b/docs/api/python/pythonic/boolean.rst similarity index 100% rename from docs/api/python/z3compat/boolean.rst rename to docs/api/python/pythonic/boolean.rst diff --git a/docs/api/python/z3compat/dt.rst b/docs/api/python/pythonic/dt.rst similarity index 100% rename from docs/api/python/z3compat/dt.rst rename to docs/api/python/pythonic/dt.rst diff --git a/docs/api/python/z3compat/fp.rst b/docs/api/python/pythonic/fp.rst similarity index 100% rename from docs/api/python/z3compat/fp.rst rename to docs/api/python/pythonic/fp.rst diff --git a/docs/api/python/z3compat/internals.rst b/docs/api/python/pythonic/internals.rst similarity index 100% rename from docs/api/python/z3compat/internals.rst rename to docs/api/python/pythonic/internals.rst diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/pythonic/pythonic.rst similarity index 92% rename from docs/api/python/z3compat/z3compat.rst rename to docs/api/python/pythonic/pythonic.rst index 8d1312907..d5a31a939 100644 --- a/docs/api/python/z3compat/z3compat.rst +++ b/docs/api/python/pythonic/pythonic.rst @@ -1,4 +1,4 @@ -z3py compatibility Python API +Pythonic API ========================================= .. only:: not bindings_python @@ -16,7 +16,7 @@ It does not (currently) support these cvc5 features: * unsatisfiable cores * syntax-guided synthesis (SyGuS) -It does not support the following features of Z3Py: +It does not (currently) support the following features of Z3Py: * Patterns for quantifier instantiation * Pseudo-boolean counting constraints: AtMost, AtLeast, ... diff --git a/docs/api/python/z3compat/quant.rst b/docs/api/python/pythonic/quant.rst similarity index 100% rename from docs/api/python/z3compat/quant.rst rename to docs/api/python/pythonic/quant.rst diff --git a/docs/api/python/z3compat/quickstart.rst b/docs/api/python/pythonic/quickstart.rst similarity index 100% rename from docs/api/python/z3compat/quickstart.rst rename to docs/api/python/pythonic/quickstart.rst diff --git a/docs/api/python/z3compat/set.rst b/docs/api/python/pythonic/set.rst similarity index 100% rename from docs/api/python/z3compat/set.rst rename to docs/api/python/pythonic/set.rst diff --git a/docs/api/python/z3compat/solver.rst b/docs/api/python/pythonic/solver.rst similarity index 100% rename from docs/api/python/z3compat/solver.rst rename to docs/api/python/pythonic/solver.rst diff --git a/docs/conf.py.in b/docs/conf.py.in index 23ef5da12..28c64d555 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -94,12 +94,12 @@ examples_types = { 'group': 'java' }, '^.*\.py$': { - 'title': 'Python', + 'title': 'Python (base)', 'lang': 'python', 'group': 'py-regular' }, '^.*\.py$': { - 'title': 'Python z3py', + 'title': 'Python (pythonic)', 'lang': 'python', 'group': 'py-z3pycompat' }, -- 2.30.2