Rename python APIs (#7950)

Rename python APIs to "base" and "pythonic"

diff --git a/docs/api/api.rst b/docs/api/api.rst
index 3eff4bd1cd4b2c194514de8934d7a7f00ebdc2cc..63533855c8c94ce0ce33ef0e58b730e8fc12cf20 100644 (file)
--- 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 <cpp/cpp>` is considered the primary interface to cvc5, both the :doc:`Java API <java/java>` and the :doc:`Python API <python/python>` 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 <cpp/cpp>` is considered the primary interface to cvc5, both the :doc:`Java API <java/java>` and the :doc:`base Python API <python/base/python>` 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 <python/pythonic/pythonic>`.
 
 .. toctree::
    :maxdepth: 1

diff --git a/docs/api/python/base/datatype.rst b/docs/api/python/base/datatype.rst
new file mode 100644 (file)
index 0000000..a6052b1
--- /dev/null
+++ b/docs/api/python/base/datatype.rst
@@ -0,0 +1,6 @@
+Datatype
+========
+
+.. autoclass:: pycvc5.Datatype
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/datatypeconstructor.rst b/docs/api/python/base/datatypeconstructor.rst
new file mode 100644 (file)
index 0000000..ed45756
--- /dev/null
+++ b/docs/api/python/base/datatypeconstructor.rst
@@ -0,0 +1,6 @@
+DatatypeConstructor
+===================
+
+.. autoclass:: pycvc5.DatatypeConstructor
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/datatypeconstructordecl.rst b/docs/api/python/base/datatypeconstructordecl.rst
new file mode 100644 (file)
index 0000000..77b1ea3
--- /dev/null
+++ b/docs/api/python/base/datatypeconstructordecl.rst
@@ -0,0 +1,6 @@
+DatatypeConstructorDecl
+=======================
+
+.. autoclass:: pycvc5.DatatypeConstructorDecl
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/datatypedecl.rst b/docs/api/python/base/datatypedecl.rst
new file mode 100644 (file)
index 0000000..0f61471
--- /dev/null
+++ b/docs/api/python/base/datatypedecl.rst
@@ -0,0 +1,6 @@
+DatatypeDecl
+============
+
+.. autoclass:: pycvc5.DatatypeDecl
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/datatypeselector.rst b/docs/api/python/base/datatypeselector.rst
new file mode 100644 (file)
index 0000000..9c2ae22
--- /dev/null
+++ b/docs/api/python/base/datatypeselector.rst
@@ -0,0 +1,6 @@
+DatatypeSelector
+================
+
+.. autoclass:: pycvc5.DatatypeSelector
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/grammar.rst b/docs/api/python/base/grammar.rst
new file mode 100644 (file)
index 0000000..a2059fa
--- /dev/null
+++ b/docs/api/python/base/grammar.rst
@@ -0,0 +1,6 @@
+Grammar
+================
+
+.. autoclass:: pycvc5.Grammar
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/kind.rst b/docs/api/python/base/kind.rst
new file mode 100644 (file)
index 0000000..b4be797
--- /dev/null
+++ b/docs/api/python/base/kind.rst
@@ -0,0 +1,12 @@
+Kind
+================
+
+Every :py:class:`Term <pycvc5.Term>` has a kind which represents its type, for
+example whether it is an equality (:py:obj:`Equal <pycvc5.Kind.Equal>`), a
+conjunction (:py:obj:`And <pycvc5.Kind.And>`), or a bit-vector addtion
+(:py:obj:`BVAdd <pycvc5.Kind.BVAdd>`).
+The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind <cvc5::api::Kind>` enum.
+
+.. autoclass:: pycvc5.Kind
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/op.rst b/docs/api/python/base/op.rst
new file mode 100644 (file)
index 0000000..7769b33
--- /dev/null
+++ b/docs/api/python/base/op.rst
@@ -0,0 +1,6 @@
+Op
+================
+
+.. autoclass:: pycvc5.Op
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/python.rst b/docs/api/python/base/python.rst
new file mode 100644 (file)
index 0000000..5036fa0
--- /dev/null
+++ b/docs/api/python/base/python.rst
@@ -0,0 +1,32 @@
+Base 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.
+
+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
+
+    quickstart
+    datatype
+    datatypeconstructor
+    datatypeconstructordecl
+    datatypedecl
+    datatypeselector
+    grammar
+    kind
+    op
+    result
+    roundingmode
+    solver
+    sort
+    term 
+    unknownexplanation

diff --git a/docs/api/python/base/quickstart.rst b/docs/api/python/base/quickstart.rst
new file mode 100644 (file)
index 0000000..ba3360d
--- /dev/null
+++ b/docs/api/python/base/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 <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.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/base/result.rst b/docs/api/python/base/result.rst
new file mode 100644 (file)
index 0000000..9edb12b
--- /dev/null
+++ b/docs/api/python/base/result.rst
@@ -0,0 +1,6 @@
+Result
+================
+
+.. autoclass:: pycvc5.Result
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/roundingmode.rst b/docs/api/python/base/roundingmode.rst
new file mode 100644 (file)
index 0000000..0c22608
--- /dev/null
+++ b/docs/api/python/base/roundingmode.rst
@@ -0,0 +1,6 @@
+RoundingMode
+================
+
+.. autoclass:: pycvc5.RoundingMode
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/solver.rst b/docs/api/python/base/solver.rst
new file mode 100644 (file)
index 0000000..2147a1f
--- /dev/null
+++ b/docs/api/python/base/solver.rst
@@ -0,0 +1,6 @@
+Solver
+========
+
+.. autoclass:: pycvc5.Solver
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/sort.rst b/docs/api/python/base/sort.rst
new file mode 100644 (file)
index 0000000..270113e
--- /dev/null
+++ b/docs/api/python/base/sort.rst
@@ -0,0 +1,6 @@
+Sort
+================
+
+.. autoclass:: pycvc5.Sort
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/term.rst b/docs/api/python/base/term.rst
new file mode 100644 (file)
index 0000000..0099220
--- /dev/null
+++ b/docs/api/python/base/term.rst
@@ -0,0 +1,6 @@
+Term
+================
+
+.. autoclass:: pycvc5.Term
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/base/unknownexplanation.rst b/docs/api/python/base/unknownexplanation.rst
new file mode 100644 (file)
index 0000000..aee1345
--- /dev/null
+++ b/docs/api/python/base/unknownexplanation.rst
@@ -0,0 +1,6 @@
+UnknownExplanation
+==================
+
+.. autoclass:: pycvc5.UnknownExplanation
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst
index b3bd865bef8bb4e7957794bfd58a3ff75af6d94c..9763b45aaf8de0ef537e63b5b1fc18a4c7e2aa32 100644 (file)
--- 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 <regular/python>` is an almost exact copy of the :doc:`C++ API <../cpp/cpp>`.
-Alternatively, the :doc:`z3py compatibility Python 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.
+The :doc:`base Python API <base/python>` is an almost exact copy of the :doc:`C++ API <../cpp/cpp>`.
+Alternatively, the :doc:`pythonic API <pythonic/pythonic>` 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.
 
 .. 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 <z3compat/z3compat>`.
+If you are a new user, or already have an application that uses Z3's python API, use the :doc:`pythonic API <pythonic/pythonic>`.
 
-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>`.
+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 <base/python>`.
+
+You can compare examples using the two APIs by visiting the :doc:`examples page <../../examples/quickstart>`.

diff --git a/docs/api/python/pythonic/arith.rst b/docs/api/python/pythonic/arith.rst
new file mode 100644 (file)
index 0000000..38ecf4e
--- /dev/null
+++ b/docs/api/python/pythonic/arith.rst
@@ -0,0 +1,122 @@
+Arithmetic
+============
+
+
+Basic Arithmetic Term Builders
+-------------------------------
+.. autofunction:: cvc5_z3py_compat.Int
+.. autofunction:: cvc5_z3py_compat.Real
+.. autofunction:: cvc5_z3py_compat.IntVal
+.. autofunction:: cvc5_z3py_compat.RealVal
+.. autofunction:: cvc5_z3py_compat.RatVal
+.. autofunction:: cvc5_z3py_compat.Q
+.. autofunction:: cvc5_z3py_compat.IntSort
+.. autofunction:: cvc5_z3py_compat.RealSort
+.. autofunction:: cvc5_z3py_compat.FreshInt
+.. autofunction:: cvc5_z3py_compat.Ints
+.. autofunction:: cvc5_z3py_compat.IntVector
+.. autofunction:: cvc5_z3py_compat.FreshReal
+.. autofunction:: cvc5_z3py_compat.Reals
+.. autofunction:: cvc5_z3py_compat.RealVector
+
+
+Arithmetic Overloads
+--------------------
+
+See the following operator overloads for building arithmetic terms. These terms
+can also be built with builder functions listed below.
+
+addition (``+``)
+  :py:meth:`cvc5_z3py_compat.ArithRef.__add__`
+
+subtraction (``-``)
+  :py:meth:`cvc5_z3py_compat.ArithRef.__sub__`
+
+multiplication (``*``)
+  :py:meth:`cvc5_z3py_compat.ArithRef.__mul__`
+
+division (``/``)
+  :py:meth:`cvc5_z3py_compat.ArithRef.__div__`
+
+power (``**``)
+  :py:meth:`cvc5_z3py_compat.ArithRef.__pow__`
+
+negation (``-``)
+  :py:meth:`cvc5_z3py_compat.ArithRef.__neg__`
+
+greater than (``>``)
+  :py:meth:`cvc5_z3py_compat.ArithRef.__gt__`
+
+less than (``<``)
+  :py:meth:`cvc5_z3py_compat.ArithRef.__lt__`
+
+greater than or equal to (``>=``)
+  :py:meth:`cvc5_z3py_compat.ArithRef.__ge__`
+
+less than or equal to (``<=``)
+  :py:meth:`cvc5_z3py_compat.ArithRef.__le__`
+
+equal (``==``)
+  :py:meth:`cvc5_z3py_compat.ExprRef.__eq__`
+
+not equal (``!=``)
+  :py:meth:`cvc5_z3py_compat.ExprRef.__ne__`
+
+.. autofunction:: cvc5_z3py_compat.Plus
+.. autofunction:: cvc5_z3py_compat.Mult
+.. autofunction:: cvc5_z3py_compat.Sub
+.. autofunction:: cvc5_z3py_compat.UMinus
+.. autofunction:: cvc5_z3py_compat.Div
+.. autofunction:: cvc5_z3py_compat.Pow
+.. autofunction:: cvc5_z3py_compat.IntsModulus
+.. autofunction:: cvc5_z3py_compat.Leq
+.. autofunction:: cvc5_z3py_compat.Geq
+.. autofunction:: cvc5_z3py_compat.Lt
+.. autofunction:: cvc5_z3py_compat.Gt
+
+Other Arithmetic Operators
+--------------------------
+
+.. autofunction:: cvc5_z3py_compat.ToReal
+.. autofunction:: cvc5_z3py_compat.ToInt
+.. autofunction:: cvc5_z3py_compat.IsInt
+.. autofunction:: cvc5_z3py_compat.Sqrt
+.. autofunction:: cvc5_z3py_compat.Cbrt
+
+Testers
+-------------------
+.. autofunction:: cvc5_z3py_compat.is_arith
+.. autofunction:: cvc5_z3py_compat.is_int
+.. autofunction:: cvc5_z3py_compat.is_real
+.. autofunction:: cvc5_z3py_compat.is_int_value
+.. autofunction:: cvc5_z3py_compat.is_rational_value
+.. autofunction:: cvc5_z3py_compat.is_arith_sort
+.. autofunction:: cvc5_z3py_compat.is_add
+.. autofunction:: cvc5_z3py_compat.is_mul
+.. autofunction:: cvc5_z3py_compat.is_sub
+.. autofunction:: cvc5_z3py_compat.is_div
+.. autofunction:: cvc5_z3py_compat.is_idiv
+.. autofunction:: cvc5_z3py_compat.is_mod
+.. autofunction:: cvc5_z3py_compat.is_le
+.. autofunction:: cvc5_z3py_compat.is_lt
+.. autofunction:: cvc5_z3py_compat.is_ge
+.. autofunction:: cvc5_z3py_compat.is_gt
+.. autofunction:: cvc5_z3py_compat.is_is_int
+.. autofunction:: cvc5_z3py_compat.is_to_real
+.. autofunction:: cvc5_z3py_compat.is_to_int
+
+Classes (with overloads)
+-------------------------
+
+.. autoclass:: cvc5_z3py_compat.ArithSortRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.ArithRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.IntNumRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.RatNumRef
+   :members:
+   :special-members:

diff --git a/docs/api/python/pythonic/array.rst b/docs/api/python/pythonic/array.rst
new file mode 100644 (file)
index 0000000..5991894
--- /dev/null
+++ b/docs/api/python/pythonic/array.rst
@@ -0,0 +1,45 @@
+Arrays
+============
+
+
+Basic Array Term Builders
+-------------------------
+
+.. autofunction:: cvc5_z3py_compat.Array
+.. autofunction:: cvc5_z3py_compat.ConstArray
+.. autofunction:: cvc5_z3py_compat.K
+.. autofunction:: cvc5_z3py_compat.ArraySort
+
+Array Operators
+-------------------
+
+.. autofunction:: cvc5_z3py_compat.Select
+.. autofunction:: cvc5_z3py_compat.Store
+.. autofunction:: cvc5_z3py_compat.Update
+
+See the following operator overloads for building other kinds of array
+terms:
+
+* ``select``: :py:meth:`cvc5_z3py_compat.ArrayRef.__getitem__`
+
+
+Testers
+-------------------
+.. autofunction:: cvc5_z3py_compat.is_array_sort
+.. autofunction:: cvc5_z3py_compat.is_array
+.. autofunction:: cvc5_z3py_compat.is_const_array
+.. autofunction:: cvc5_z3py_compat.is_K
+.. autofunction:: cvc5_z3py_compat.is_select
+.. autofunction:: cvc5_z3py_compat.is_store
+.. autofunction:: cvc5_z3py_compat.is_update
+
+
+Classes (with overloads)
+------------------------
+
+.. autoclass:: cvc5_z3py_compat.ArraySortRef
+  :members:
+  :special-members:
+.. autoclass:: cvc5_z3py_compat.ArrayRef
+  :members:
+  :special-members:

diff --git a/docs/api/python/pythonic/bitvec.rst b/docs/api/python/pythonic/bitvec.rst
new file mode 100644 (file)
index 0000000..d8eea48
--- /dev/null
+++ b/docs/api/python/pythonic/bitvec.rst
@@ -0,0 +1,130 @@
+Bit-Vectors
+============
+
+
+Basic Bit-Vector Term Builders
+----------------------------------
+.. autofunction:: cvc5_z3py_compat.BitVec
+.. autofunction:: cvc5_z3py_compat.BitVecVal
+.. autofunction:: cvc5_z3py_compat.BitVecSort
+.. autofunction:: cvc5_z3py_compat.BitVecs
+
+Bit-Vector Overloads
+--------------------
+
+See the following operator overloads for building bit-vector terms.
+Each kind of term can also be built with a builder function below.
+
+* arithmetic
+
+  addition (``+``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__add__`
+
+  subtraction (``-``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__sub__`
+
+  multiplication (``*``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__mul__`
+
+  division (``/``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__div__`
+
+* bit-wise
+
+  or (``|``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__or__`
+
+  and (``&``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__and__`
+
+  xor (``^``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__xor__`
+
+  bit complement (``~``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__invert__`
+
+  negation (``-``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__neg__`
+
+  left shift (``<<``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__lshift__`
+
+  right shift (``>>``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__rshift__`
+
+* comparisons
+
+  signed greater than (``>``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__gt__`
+
+  signed less than (``<``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__lt__`
+
+  signed greater than or equal to (``>=``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__ge__`
+
+  signed less than or equal to (``<=``)
+    :py:meth:`cvc5_z3py_compat.BitVecRef.__le__`
+
+  equal (``==``)
+    :py:meth:`cvc5_z3py_compat.ExprRef.__eq__`
+
+  not equal (``!=``)
+    :py:meth:`cvc5_z3py_compat.ExprRef.__ne__`
+
+Bit-Vector Term Builders
+------------------------
+
+.. autofunction:: cvc5_z3py_compat.BV2Int
+.. autofunction:: cvc5_z3py_compat.Int2BV
+.. autofunction:: cvc5_z3py_compat.Concat
+.. autofunction:: cvc5_z3py_compat.Extract
+.. autofunction:: cvc5_z3py_compat.ULE
+.. autofunction:: cvc5_z3py_compat.ULT
+.. autofunction:: cvc5_z3py_compat.UGE
+.. autofunction:: cvc5_z3py_compat.UGT
+.. autofunction:: cvc5_z3py_compat.SLE
+.. autofunction:: cvc5_z3py_compat.SLT
+.. autofunction:: cvc5_z3py_compat.SGE
+.. autofunction:: cvc5_z3py_compat.SGT
+.. autofunction:: cvc5_z3py_compat.UDiv
+.. autofunction:: cvc5_z3py_compat.URem
+.. autofunction:: cvc5_z3py_compat.SDiv
+.. autofunction:: cvc5_z3py_compat.SMod
+.. autofunction:: cvc5_z3py_compat.SRem
+.. autofunction:: cvc5_z3py_compat.LShR
+.. autofunction:: cvc5_z3py_compat.RotateLeft
+.. autofunction:: cvc5_z3py_compat.RotateRight
+.. autofunction:: cvc5_z3py_compat.SignExt
+.. autofunction:: cvc5_z3py_compat.ZeroExt
+.. autofunction:: cvc5_z3py_compat.RepeatBitVec
+.. autofunction:: cvc5_z3py_compat.BVRedAnd
+.. autofunction:: cvc5_z3py_compat.BVRedOr
+.. autofunction:: cvc5_z3py_compat.BVAdd
+.. autofunction:: cvc5_z3py_compat.BVMult
+.. autofunction:: cvc5_z3py_compat.BVSub
+.. autofunction:: cvc5_z3py_compat.BVOr
+.. autofunction:: cvc5_z3py_compat.BVAnd
+.. autofunction:: cvc5_z3py_compat.BVXor
+.. autofunction:: cvc5_z3py_compat.BVNeg
+.. autofunction:: cvc5_z3py_compat.BVNot
+
+
+Testers
+-------------------
+.. autofunction:: cvc5_z3py_compat.is_bv_sort
+.. autofunction:: cvc5_z3py_compat.is_bv
+.. autofunction:: cvc5_z3py_compat.is_bv_value
+
+Classes (with overloads)
+-----------------------------
+
+.. autoclass:: cvc5_z3py_compat.BitVecSortRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.BitVecRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.BitVecNumRef
+   :members:
+   :special-members:

diff --git a/docs/api/python/pythonic/boolean.rst b/docs/api/python/pythonic/boolean.rst
new file mode 100644 (file)
index 0000000..57ef4e6
--- /dev/null
+++ b/docs/api/python/pythonic/boolean.rst
@@ -0,0 +1,77 @@
+Core & Booleans
+================
+
+Basic Boolean Term Builders
+---------------------------
+.. autofunction:: cvc5_z3py_compat.Bool
+.. autofunction:: cvc5_z3py_compat.BoolVal
+.. autofunction:: cvc5_z3py_compat.BoolSort
+.. autofunction:: cvc5_z3py_compat.FreshBool
+.. autofunction:: cvc5_z3py_compat.Bools
+.. autofunction:: cvc5_z3py_compat.BoolVector
+
+Basic Generic Term Builders
+---------------------------
+.. autofunction:: cvc5_z3py_compat.Const
+.. autofunction:: cvc5_z3py_compat.Consts
+.. autofunction:: cvc5_z3py_compat.FreshConst
+.. autofunction:: cvc5_z3py_compat.Function
+.. autofunction:: cvc5_z3py_compat.FreshFunction
+
+Boolean Operators
+-----------------
+.. autofunction:: cvc5_z3py_compat.And
+.. autofunction:: cvc5_z3py_compat.Or
+.. autofunction:: cvc5_z3py_compat.Not
+.. autofunction:: cvc5_z3py_compat.mk_not
+.. autofunction:: cvc5_z3py_compat.Implies
+.. autofunction:: cvc5_z3py_compat.Xor
+
+Generic Operators
+-----------------
+.. autofunction:: cvc5_z3py_compat.If
+.. autofunction:: cvc5_z3py_compat.Distinct
+
+Equality
+~~~~~~~~
+
+See
+:py:meth:`cvc5_z3py_compat.ExprRef.__eq__`
+and
+:py:meth:`cvc5_z3py_compat.ExprRef.__ne__`
+for building equality and disequality terms.
+
+
+Testers
+-------
+.. autofunction:: cvc5_z3py_compat.is_bool
+.. autofunction:: cvc5_z3py_compat.is_bool_value
+.. autofunction:: cvc5_z3py_compat.is_true
+.. autofunction:: cvc5_z3py_compat.is_false
+.. autofunction:: cvc5_z3py_compat.is_and
+.. autofunction:: cvc5_z3py_compat.is_or
+.. autofunction:: cvc5_z3py_compat.is_implies
+.. autofunction:: cvc5_z3py_compat.is_not
+.. autofunction:: cvc5_z3py_compat.is_eq
+.. autofunction:: cvc5_z3py_compat.is_distinct
+.. autofunction:: cvc5_z3py_compat.is_const
+.. autofunction:: cvc5_z3py_compat.is_func_decl
+
+
+Classes (with overloads)
+----------------------------
+.. autoclass:: cvc5_z3py_compat.ExprRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.SortRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.BoolRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.BoolSortRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.FuncDeclRef
+   :members:
+   :special-members:

diff --git a/docs/api/python/pythonic/dt.rst b/docs/api/python/pythonic/dt.rst
new file mode 100644 (file)
index 0000000..6a29347
--- /dev/null
+++ b/docs/api/python/pythonic/dt.rst
@@ -0,0 +1,79 @@
+Datatypes
+============
+
+Overview
+----------
+
+To manipulate instances of a datatype, one must first *declare* the datatype itself.
+Declaration happens in three phases. Let's consider declaring a cons-list of
+integers.
+
+First, we initialize the datatype with its *name*
+
+    >>> IntList = Datatype('IntList')
+
+Second, we declare constructors for the datatype, giving the *constructor name*
+and *field names and sorts*. Here is the empty list constructor:
+
+    >>> IntList.declare('nil', ())
+
+Here is the cons constructor:
+
+    >>> IntList.declare('cons', ('val', IntSort()), ('tail', IntList))
+
+Third, after all constructors are declared, we can *create* the datatype,
+finishing its declaration.
+
+    >>> IntList = IntList.create()
+
+Now, one has access to a number of tools for interacting with integer lists.
+
+* ``IntList.nil`` refers to the SMT term that is an empty list,
+  and ``IntList.cons`` refers to the cons constructor.
+* ``IntList.is_nil`` and ``IntList.is_cons`` are testors (a.k.a.,
+  recognizers) for those constructors.
+* ``IntList.val`` and ``IntList.tail`` are selectors (a.k.a. accessors)
+  for the cons constructor.
+
+If constructor, accessor, or selector names are ambiguous (e.g., if different
+constructors have selectors of the same name), then see the methods on
+:py:class:`cvc5_z3py_compat.DatatypeSortRef` to unambiguously access a specific
+function.
+
+To create mutually recursive datatypes, see
+:py:func:`cvc5_z3py_compat.CreateDatatypes`.
+
+To create a codataype (e.g., a possibly infinite stream of integers), pass the
+``isCoDatatype=True`` argument to the :py:class:`cvc5_z3py_compat.Datatype`
+constructor.
+
+    >>> IntStream = Datatype('IntStream', isCoDatatype=True)
+
+Declaration Utilities
+---------------------
+
+.. autofunction:: cvc5_z3py_compat.CreateDatatypes
+.. autofunction:: cvc5_z3py_compat.TupleSort
+.. autofunction:: cvc5_z3py_compat.DisjointSum
+
+
+Classes
+------------------------
+.. autoclass:: cvc5_z3py_compat.Datatype
+  :members:
+  :special-members:
+.. autoclass:: cvc5_z3py_compat.DatatypeSortRef
+  :members:
+  :special-members:
+.. autoclass:: cvc5_z3py_compat.DatatypeConstructorRef
+  :members:
+  :special-members:
+.. autoclass:: cvc5_z3py_compat.DatatypeSelectorRef
+  :members:
+  :special-members:
+.. autoclass:: cvc5_z3py_compat.DatatypeRecognizerRef
+  :members:
+  :special-members:
+.. autoclass:: cvc5_z3py_compat.DatatypeRef
+  :members:
+  :special-members:

diff --git a/docs/api/python/pythonic/fp.rst b/docs/api/python/pythonic/fp.rst
new file mode 100644 (file)
index 0000000..d8a72bf
--- /dev/null
+++ b/docs/api/python/pythonic/fp.rst
@@ -0,0 +1,126 @@
+Floating Point
+==============
+
+Basic FP Term Builders
+-------------------------
+
+.. autofunction:: cvc5_z3py_compat.FP
+.. autofunction:: cvc5_z3py_compat.FPs
+.. autofunction:: cvc5_z3py_compat.FPVal
+.. autofunction:: cvc5_z3py_compat.fpNaN
+.. autofunction:: cvc5_z3py_compat.fpPlusInfinity
+.. autofunction:: cvc5_z3py_compat.fpMinusInfinity
+.. autofunction:: cvc5_z3py_compat.fpInfinity
+.. autofunction:: cvc5_z3py_compat.fpPlusZero
+.. autofunction:: cvc5_z3py_compat.fpMinusZero
+.. autofunction:: cvc5_z3py_compat.fpZero
+.. autofunction:: cvc5_z3py_compat.FPSort
+.. autofunction:: cvc5_z3py_compat.Float16
+.. autofunction:: cvc5_z3py_compat.FloatHalf
+.. autofunction:: cvc5_z3py_compat.Float32
+.. autofunction:: cvc5_z3py_compat.FloatSingle
+.. autofunction:: cvc5_z3py_compat.Float64
+.. autofunction:: cvc5_z3py_compat.FloatDouble
+.. autofunction:: cvc5_z3py_compat.Float128
+.. autofunction:: cvc5_z3py_compat.FloatQuadruple
+
+FP Operators
+-------------------
+
+See the following operator overloads for building basic floating-point terms:
+
+* ``+``: :py:meth:`cvc5_z3py_compat.FPRef.__add__`
+* ``-``: :py:meth:`cvc5_z3py_compat.FPRef.__sub__`
+* ``*``: :py:meth:`cvc5_z3py_compat.FPRef.__mul__`
+* unary ``-``: :py:meth:`cvc5_z3py_compat.FPRef.__neg__`
+* ``/``: :py:meth:`cvc5_z3py_compat.FPRef.__div__`
+* ``%``: :py:meth:`cvc5_z3py_compat.FPRef.__mod__`
+* ``<=``: :py:meth:`cvc5_z3py_compat.FPRef.__le__`
+* ``<``: :py:meth:`cvc5_z3py_compat.FPRef.__lt__`
+* ``>=``: :py:meth:`cvc5_z3py_compat.FPRef.__ge__`
+* ``>``: :py:meth:`cvc5_z3py_compat.FPRef.__gt__`
+
+.. autofunction:: cvc5_z3py_compat.fpAbs
+.. autofunction:: cvc5_z3py_compat.fpNeg
+.. autofunction:: cvc5_z3py_compat.fpAdd
+.. autofunction:: cvc5_z3py_compat.fpSub
+.. autofunction:: cvc5_z3py_compat.fpMul
+.. autofunction:: cvc5_z3py_compat.fpDiv
+.. autofunction:: cvc5_z3py_compat.fpRem
+.. autofunction:: cvc5_z3py_compat.fpMin
+.. autofunction:: cvc5_z3py_compat.fpMax
+.. autofunction:: cvc5_z3py_compat.fpFMA
+.. autofunction:: cvc5_z3py_compat.fpSqrt
+.. autofunction:: cvc5_z3py_compat.fpRoundToIntegral
+.. autofunction:: cvc5_z3py_compat.fpIsNaN
+.. autofunction:: cvc5_z3py_compat.fpIsInf
+.. autofunction:: cvc5_z3py_compat.fpIsZero
+.. autofunction:: cvc5_z3py_compat.fpIsNormal
+.. autofunction:: cvc5_z3py_compat.fpIsSubnormal
+.. autofunction:: cvc5_z3py_compat.fpIsNegative
+.. autofunction:: cvc5_z3py_compat.fpIsPositive
+.. autofunction:: cvc5_z3py_compat.fpLT
+.. autofunction:: cvc5_z3py_compat.fpLEQ
+.. autofunction:: cvc5_z3py_compat.fpGT
+.. autofunction:: cvc5_z3py_compat.fpGEQ
+.. autofunction:: cvc5_z3py_compat.fpEQ
+.. autofunction:: cvc5_z3py_compat.fpNEQ
+.. autofunction:: cvc5_z3py_compat.fpFP
+.. autofunction:: cvc5_z3py_compat.fpToFP
+.. autofunction:: cvc5_z3py_compat.fpBVToFP
+.. autofunction:: cvc5_z3py_compat.fpFPToFP
+.. autofunction:: cvc5_z3py_compat.fpRealToFP
+.. autofunction:: cvc5_z3py_compat.fpSignedToFP
+.. autofunction:: cvc5_z3py_compat.fpUnsignedToFP
+.. autofunction:: cvc5_z3py_compat.fpToFPUnsigned
+.. autofunction:: cvc5_z3py_compat.fpToSBV
+.. autofunction:: cvc5_z3py_compat.fpToUBV
+.. autofunction:: cvc5_z3py_compat.fpToReal
+
+
+
+Testers
+-------------------
+.. autofunction:: cvc5_z3py_compat.is_fp_sort
+.. autofunction:: cvc5_z3py_compat.is_fp
+.. autofunction:: cvc5_z3py_compat.is_fp_value
+.. autofunction:: cvc5_z3py_compat.is_fprm_sort
+.. autofunction:: cvc5_z3py_compat.is_fprm
+.. autofunction:: cvc5_z3py_compat.is_fprm_value
+
+
+FP Rounding Modes
+-------------------------
+.. autofunction:: cvc5_z3py_compat.RoundNearestTiesToEven
+.. autofunction:: cvc5_z3py_compat.RNE
+.. autofunction:: cvc5_z3py_compat.RoundNearestTiesToAway
+.. autofunction:: cvc5_z3py_compat.RNA
+.. autofunction:: cvc5_z3py_compat.RoundTowardPositive
+.. autofunction:: cvc5_z3py_compat.RTP
+.. autofunction:: cvc5_z3py_compat.RoundTowardNegative
+.. autofunction:: cvc5_z3py_compat.RTN
+.. autofunction:: cvc5_z3py_compat.RoundTowardZero
+.. autofunction:: cvc5_z3py_compat.RTZ
+.. autofunction:: cvc5_z3py_compat.get_default_rounding_mode
+.. autofunction:: cvc5_z3py_compat.set_default_rounding_mode
+.. autofunction:: cvc5_z3py_compat.get_default_fp_sort
+.. autofunction:: cvc5_z3py_compat.set_default_fp_sort
+
+
+Classes (with overloads)
+------------------------
+
+.. autoclass:: cvc5_z3py_compat.FPSortRef
+  :members:
+  :special-members:
+.. autoclass:: cvc5_z3py_compat.FPRef
+  :members:
+  :special-members:
+.. autoclass:: cvc5_z3py_compat.FPNumRef
+  :members:
+  :special-members:
+.. autoclass:: cvc5_z3py_compat.FPRMRef
+  :members:
+  :special-members:
+
+

diff --git a/docs/api/python/pythonic/internals.rst b/docs/api/python/pythonic/internals.rst
new file mode 100644 (file)
index 0000000..f555d3e
--- /dev/null
+++ b/docs/api/python/pythonic/internals.rst
@@ -0,0 +1,17 @@
+Internals
+============
+
+
+Testers
+-------------------
+.. autofunction:: cvc5_z3py_compat.is_expr
+.. autofunction:: cvc5_z3py_compat.is_sort
+.. autofunction:: cvc5_z3py_compat.is_app
+.. autofunction:: cvc5_z3py_compat.is_app_of
+
+Exceptions
+-------------------
+
+.. autoclass:: cvc5_z3py_compat.SMTException
+   :members:
+   :special-members:

diff --git a/docs/api/python/pythonic/pythonic.rst b/docs/api/python/pythonic/pythonic.rst
new file mode 100644 (file)
index 0000000..d5a31a9
--- /dev/null
+++ b/docs/api/python/pythonic/pythonic.rst
@@ -0,0 +1,43 @@
+Pythonic 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.
+
+
+This API is missing some features from cvc5 and Z3Py.
+
+It does not (currently) support these cvc5 features:
+
+* The theories of strings and sequences
+* unsatisfiable cores
+* syntax-guided synthesis (SyGuS)
+
+It does not (currently) support the following features of Z3Py:
+
+* Patterns for quantifier instantiation
+* Pseudo-boolean counting constraints: AtMost, AtLeast, ...
+* Special relation classes: PartialOrder, LinearOrder, ...
+* HTML integration
+* Hooks for user-defined propagation and probing
+* Fixedpoint API
+* Finite domains
+* SMT2 file parsing
+
+.. toctree::
+    :maxdepth: 2
+
+    quickstart
+    boolean
+    arith
+    array
+    bitvec
+    dt
+    fp
+    set
+    quant
+    solver
+    internals

diff --git a/docs/api/python/pythonic/quant.rst b/docs/api/python/pythonic/quant.rst
new file mode 100644 (file)
index 0000000..ecf8544
--- /dev/null
+++ b/docs/api/python/pythonic/quant.rst
@@ -0,0 +1,20 @@
+Quantifiers
+============
+
+Builders
+------------------
+.. autofunction:: cvc5_z3py_compat.ForAll
+.. autofunction:: cvc5_z3py_compat.Exists
+.. autofunction:: cvc5_z3py_compat.Lambda
+
+Testers
+-------------------
+.. autofunction:: cvc5_z3py_compat.is_var
+.. autofunction:: cvc5_z3py_compat.is_quantifier
+
+Classes
+-------
+.. autoclass:: cvc5_z3py_compat.QuantifierRef
+   :members:
+   :special-members:
+

diff --git a/docs/api/python/pythonic/quickstart.rst b/docs/api/python/pythonic/quickstart.rst
new file mode 100644 (file)
index 0000000..764b157
--- /dev/null
+++ b/docs/api/python/pythonic/quickstart.rst
@@ -0,0 +1,2 @@
+Quickstart
+==========

diff --git a/docs/api/python/pythonic/set.rst b/docs/api/python/pythonic/set.rst
new file mode 100644 (file)
index 0000000..96c83c6
--- /dev/null
+++ b/docs/api/python/pythonic/set.rst
@@ -0,0 +1,40 @@
+Sets
+============
+
+
+Basic Set Term Builders
+-------------------------
+
+.. autofunction:: cvc5_z3py_compat.SetSort
+.. autofunction:: cvc5_z3py_compat.Set
+.. autofunction:: cvc5_z3py_compat.EmptySet
+.. autofunction:: cvc5_z3py_compat.Singleton
+.. autofunction:: cvc5_z3py_compat.FullSet
+
+Set Operators
+-------------------
+
+.. autofunction:: cvc5_z3py_compat.SetUnion
+.. autofunction:: cvc5_z3py_compat.SetIntersect
+.. autofunction:: cvc5_z3py_compat.SetAdd
+.. autofunction:: cvc5_z3py_compat.SetDel
+.. autofunction:: cvc5_z3py_compat.SetComplement
+.. autofunction:: cvc5_z3py_compat.SetDifference
+.. autofunction:: cvc5_z3py_compat.SetMinus
+.. autofunction:: cvc5_z3py_compat.IsMember
+.. autofunction:: cvc5_z3py_compat.IsSubset
+
+See the following operator overload for set terms:
+
+* is member: :py:meth:`cvc5_z3py_compat.SetRef.__getitem__`
+
+
+Classes (with overloads)
+------------------------
+
+.. autoclass:: cvc5_z3py_compat.SetSortRef
+  :members:
+  :special-members:
+.. autoclass:: cvc5_z3py_compat.SetRef
+  :members:
+  :special-members:

diff --git a/docs/api/python/pythonic/solver.rst b/docs/api/python/pythonic/solver.rst
new file mode 100644 (file)
index 0000000..c268ec3
--- /dev/null
+++ b/docs/api/python/pythonic/solver.rst
@@ -0,0 +1,52 @@
+Solvers & Results
+===========================
+
+Simple Solving
+----------------
+
+.. autofunction:: cvc5_z3py_compat.solve
+.. autofunction:: cvc5_z3py_compat.solve_using
+.. autofunction:: cvc5_z3py_compat.prove
+
+
+The Solver Class
+----------------
+
+.. autofunction:: cvc5_z3py_compat.SolverFor
+
+.. autofunction:: cvc5_z3py_compat.SimpleSolver
+
+.. autoclass:: cvc5_z3py_compat.Solver
+  :members:
+  :special-members:
+
+Results & Models
+----------------
+.. data:: cvc5_z3py_compat.unsat
+
+  An *UNSAT* result.
+
+.. data:: cvc5_z3py_compat.sat
+
+  A *SAT* result.
+
+.. data:: cvc5_z3py_compat.unknown
+
+  The satisfiability could not be determined.
+
+.. autoclass:: cvc5_z3py_compat.CheckSatResult
+  :members:
+  :special-members:
+
+.. autoclass:: cvc5_z3py_compat.ModelRef
+  :members:
+  :special-members:
+
+Utilities
+--------------
+
+.. autofunction:: cvc5_z3py_compat.evaluate
+.. autofunction:: cvc5_z3py_compat.simplify
+.. autofunction:: cvc5_z3py_compat.substitute
+.. autofunction:: cvc5_z3py_compat.Sum
+.. autofunction:: cvc5_z3py_compat.Product

diff --git a/docs/api/python/regular/datatype.rst b/docs/api/python/regular/datatype.rst
deleted file mode 100644 (file)
index a6052b1..0000000
--- a/docs/api/python/regular/datatype.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-Datatype
-========
-
-.. autoclass:: pycvc5.Datatype
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/datatypeconstructor.rst b/docs/api/python/regular/datatypeconstructor.rst
deleted file mode 100644 (file)
index ed45756..0000000
--- a/docs/api/python/regular/datatypeconstructor.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-DatatypeConstructor
-===================
-
-.. autoclass:: pycvc5.DatatypeConstructor
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/datatypeconstructordecl.rst b/docs/api/python/regular/datatypeconstructordecl.rst
deleted file mode 100644 (file)
index 77b1ea3..0000000
--- a/docs/api/python/regular/datatypeconstructordecl.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-DatatypeConstructorDecl
-=======================
-
-.. autoclass:: pycvc5.DatatypeConstructorDecl
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/datatypedecl.rst b/docs/api/python/regular/datatypedecl.rst
deleted file mode 100644 (file)
index 0f61471..0000000
--- a/docs/api/python/regular/datatypedecl.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-DatatypeDecl
-============
-
-.. autoclass:: pycvc5.DatatypeDecl
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/datatypeselector.rst b/docs/api/python/regular/datatypeselector.rst
deleted file mode 100644 (file)
index 9c2ae22..0000000
--- a/docs/api/python/regular/datatypeselector.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-DatatypeSelector
-================
-
-.. autoclass:: pycvc5.DatatypeSelector
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/grammar.rst b/docs/api/python/regular/grammar.rst
deleted file mode 100644 (file)
index a2059fa..0000000
--- a/docs/api/python/regular/grammar.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-Grammar
-================
-
-.. autoclass:: pycvc5.Grammar
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/kind.rst b/docs/api/python/regular/kind.rst
deleted file mode 100644 (file)
index b4be797..0000000
--- a/docs/api/python/regular/kind.rst
+++ /dev/null
@@ -1,12 +0,0 @@
-Kind
-================
-
-Every :py:class:`Term <pycvc5.Term>` has a kind which represents its type, for
-example whether it is an equality (:py:obj:`Equal <pycvc5.Kind.Equal>`), a
-conjunction (:py:obj:`And <pycvc5.Kind.And>`), or a bit-vector addtion
-(:py:obj:`BVAdd <pycvc5.Kind.BVAdd>`).
-The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind <cvc5::api::Kind>` enum.
-
-.. autoclass:: pycvc5.Kind
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/op.rst b/docs/api/python/regular/op.rst
deleted file mode 100644 (file)
index 7769b33..0000000
--- a/docs/api/python/regular/op.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-Op
-================
-
-.. autoclass:: pycvc5.Op
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/python.rst b/docs/api/python/regular/python.rst
deleted file mode 100644 (file)
index 84593b1..0000000
--- a/docs/api/python/regular/python.rst
+++ /dev/null
@@ -1,27 +0,0 @@
-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: 2
-
-    quickstart
-    datatype
-    datatypeconstructor
-    datatypeconstructordecl
-    datatypedecl
-    datatypeselector
-    grammar
-    kind
-    op
-    result
-    roundingmode
-    solver
-    sort
-    term 
-    unknownexplanation

diff --git a/docs/api/python/regular/quickstart.rst b/docs/api/python/regular/quickstart.rst
deleted file mode 100644 (file)
index ba3360d..0000000
--- a/docs/api/python/regular/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 <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.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
deleted file mode 100644 (file)
index 9edb12b..0000000
--- a/docs/api/python/regular/result.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-Result
-================
-
-.. autoclass:: pycvc5.Result
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/roundingmode.rst b/docs/api/python/regular/roundingmode.rst
deleted file mode 100644 (file)
index 0c22608..0000000
--- a/docs/api/python/regular/roundingmode.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-RoundingMode
-================
-
-.. autoclass:: pycvc5.RoundingMode
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/solver.rst b/docs/api/python/regular/solver.rst
deleted file mode 100644 (file)
index 2147a1f..0000000
--- a/docs/api/python/regular/solver.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-Solver
-========
-
-.. autoclass:: pycvc5.Solver
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/sort.rst b/docs/api/python/regular/sort.rst
deleted file mode 100644 (file)
index 270113e..0000000
--- a/docs/api/python/regular/sort.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-Sort
-================
-
-.. autoclass:: pycvc5.Sort
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/term.rst b/docs/api/python/regular/term.rst
deleted file mode 100644 (file)
index 0099220..0000000
--- a/docs/api/python/regular/term.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-Term
-================
-
-.. autoclass:: pycvc5.Term
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/regular/unknownexplanation.rst b/docs/api/python/regular/unknownexplanation.rst
deleted file mode 100644 (file)
index aee1345..0000000
--- a/docs/api/python/regular/unknownexplanation.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-UnknownExplanation
-==================
-
-.. autoclass:: pycvc5.UnknownExplanation
-    :members:
-    :undoc-members:

diff --git a/docs/api/python/z3compat/arith.rst b/docs/api/python/z3compat/arith.rst
deleted file mode 100644 (file)
index 38ecf4e..0000000
--- a/docs/api/python/z3compat/arith.rst
+++ /dev/null
@@ -1,122 +0,0 @@
-Arithmetic
-============
-
-
-Basic Arithmetic Term Builders
--------------------------------
-.. autofunction:: cvc5_z3py_compat.Int
-.. autofunction:: cvc5_z3py_compat.Real
-.. autofunction:: cvc5_z3py_compat.IntVal
-.. autofunction:: cvc5_z3py_compat.RealVal
-.. autofunction:: cvc5_z3py_compat.RatVal
-.. autofunction:: cvc5_z3py_compat.Q
-.. autofunction:: cvc5_z3py_compat.IntSort
-.. autofunction:: cvc5_z3py_compat.RealSort
-.. autofunction:: cvc5_z3py_compat.FreshInt
-.. autofunction:: cvc5_z3py_compat.Ints
-.. autofunction:: cvc5_z3py_compat.IntVector
-.. autofunction:: cvc5_z3py_compat.FreshReal
-.. autofunction:: cvc5_z3py_compat.Reals
-.. autofunction:: cvc5_z3py_compat.RealVector
-
-
-Arithmetic Overloads
---------------------
-
-See the following operator overloads for building arithmetic terms. These terms
-can also be built with builder functions listed below.
-
-addition (``+``)
-  :py:meth:`cvc5_z3py_compat.ArithRef.__add__`
-
-subtraction (``-``)
-  :py:meth:`cvc5_z3py_compat.ArithRef.__sub__`
-
-multiplication (``*``)
-  :py:meth:`cvc5_z3py_compat.ArithRef.__mul__`
-
-division (``/``)
-  :py:meth:`cvc5_z3py_compat.ArithRef.__div__`
-
-power (``**``)
-  :py:meth:`cvc5_z3py_compat.ArithRef.__pow__`
-
-negation (``-``)
-  :py:meth:`cvc5_z3py_compat.ArithRef.__neg__`
-
-greater than (``>``)
-  :py:meth:`cvc5_z3py_compat.ArithRef.__gt__`
-
-less than (``<``)
-  :py:meth:`cvc5_z3py_compat.ArithRef.__lt__`
-
-greater than or equal to (``>=``)
-  :py:meth:`cvc5_z3py_compat.ArithRef.__ge__`
-
-less than or equal to (``<=``)
-  :py:meth:`cvc5_z3py_compat.ArithRef.__le__`
-
-equal (``==``)
-  :py:meth:`cvc5_z3py_compat.ExprRef.__eq__`
-
-not equal (``!=``)
-  :py:meth:`cvc5_z3py_compat.ExprRef.__ne__`
-
-.. autofunction:: cvc5_z3py_compat.Plus
-.. autofunction:: cvc5_z3py_compat.Mult
-.. autofunction:: cvc5_z3py_compat.Sub
-.. autofunction:: cvc5_z3py_compat.UMinus
-.. autofunction:: cvc5_z3py_compat.Div
-.. autofunction:: cvc5_z3py_compat.Pow
-.. autofunction:: cvc5_z3py_compat.IntsModulus
-.. autofunction:: cvc5_z3py_compat.Leq
-.. autofunction:: cvc5_z3py_compat.Geq
-.. autofunction:: cvc5_z3py_compat.Lt
-.. autofunction:: cvc5_z3py_compat.Gt
-
-Other Arithmetic Operators
---------------------------
-
-.. autofunction:: cvc5_z3py_compat.ToReal
-.. autofunction:: cvc5_z3py_compat.ToInt
-.. autofunction:: cvc5_z3py_compat.IsInt
-.. autofunction:: cvc5_z3py_compat.Sqrt
-.. autofunction:: cvc5_z3py_compat.Cbrt
-
-Testers
--------------------
-.. autofunction:: cvc5_z3py_compat.is_arith
-.. autofunction:: cvc5_z3py_compat.is_int
-.. autofunction:: cvc5_z3py_compat.is_real
-.. autofunction:: cvc5_z3py_compat.is_int_value
-.. autofunction:: cvc5_z3py_compat.is_rational_value
-.. autofunction:: cvc5_z3py_compat.is_arith_sort
-.. autofunction:: cvc5_z3py_compat.is_add
-.. autofunction:: cvc5_z3py_compat.is_mul
-.. autofunction:: cvc5_z3py_compat.is_sub
-.. autofunction:: cvc5_z3py_compat.is_div
-.. autofunction:: cvc5_z3py_compat.is_idiv
-.. autofunction:: cvc5_z3py_compat.is_mod
-.. autofunction:: cvc5_z3py_compat.is_le
-.. autofunction:: cvc5_z3py_compat.is_lt
-.. autofunction:: cvc5_z3py_compat.is_ge
-.. autofunction:: cvc5_z3py_compat.is_gt
-.. autofunction:: cvc5_z3py_compat.is_is_int
-.. autofunction:: cvc5_z3py_compat.is_to_real
-.. autofunction:: cvc5_z3py_compat.is_to_int
-
-Classes (with overloads)
--------------------------
-
-.. autoclass:: cvc5_z3py_compat.ArithSortRef
-   :members:
-   :special-members:
-.. autoclass:: cvc5_z3py_compat.ArithRef
-   :members:
-   :special-members:
-.. autoclass:: cvc5_z3py_compat.IntNumRef
-   :members:
-   :special-members:
-.. autoclass:: cvc5_z3py_compat.RatNumRef
-   :members:
-   :special-members:

diff --git a/docs/api/python/z3compat/array.rst b/docs/api/python/z3compat/array.rst
deleted file mode 100644 (file)
index 5991894..0000000
--- a/docs/api/python/z3compat/array.rst
+++ /dev/null
@@ -1,45 +0,0 @@
-Arrays
-============
-
-
-Basic Array Term Builders
--------------------------
-
-.. autofunction:: cvc5_z3py_compat.Array
-.. autofunction:: cvc5_z3py_compat.ConstArray
-.. autofunction:: cvc5_z3py_compat.K
-.. autofunction:: cvc5_z3py_compat.ArraySort
-
-Array Operators
--------------------
-
-.. autofunction:: cvc5_z3py_compat.Select
-.. autofunction:: cvc5_z3py_compat.Store
-.. autofunction:: cvc5_z3py_compat.Update
-
-See the following operator overloads for building other kinds of array
-terms:
-
-* ``select``: :py:meth:`cvc5_z3py_compat.ArrayRef.__getitem__`
-
-
-Testers
--------------------
-.. autofunction:: cvc5_z3py_compat.is_array_sort
-.. autofunction:: cvc5_z3py_compat.is_array
-.. autofunction:: cvc5_z3py_compat.is_const_array
-.. autofunction:: cvc5_z3py_compat.is_K
-.. autofunction:: cvc5_z3py_compat.is_select
-.. autofunction:: cvc5_z3py_compat.is_store
-.. autofunction:: cvc5_z3py_compat.is_update
-
-
-Classes (with overloads)
-------------------------
-
-.. autoclass:: cvc5_z3py_compat.ArraySortRef
-  :members:
-  :special-members:
-.. autoclass:: cvc5_z3py_compat.ArrayRef
-  :members:
-  :special-members:

diff --git a/docs/api/python/z3compat/bitvec.rst b/docs/api/python/z3compat/bitvec.rst
deleted file mode 100644 (file)
index d8eea48..0000000
--- a/docs/api/python/z3compat/bitvec.rst
+++ /dev/null
@@ -1,130 +0,0 @@
-Bit-Vectors
-============
-
-
-Basic Bit-Vector Term Builders
-----------------------------------
-.. autofunction:: cvc5_z3py_compat.BitVec
-.. autofunction:: cvc5_z3py_compat.BitVecVal
-.. autofunction:: cvc5_z3py_compat.BitVecSort
-.. autofunction:: cvc5_z3py_compat.BitVecs
-
-Bit-Vector Overloads
---------------------
-
-See the following operator overloads for building bit-vector terms.
-Each kind of term can also be built with a builder function below.
-
-* arithmetic
-
-  addition (``+``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__add__`
-
-  subtraction (``-``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__sub__`
-
-  multiplication (``*``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__mul__`
-
-  division (``/``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__div__`
-
-* bit-wise
-
-  or (``|``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__or__`
-
-  and (``&``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__and__`
-
-  xor (``^``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__xor__`
-
-  bit complement (``~``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__invert__`
-
-  negation (``-``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__neg__`
-
-  left shift (``<<``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__lshift__`
-
-  right shift (``>>``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__rshift__`
-
-* comparisons
-
-  signed greater than (``>``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__gt__`
-
-  signed less than (``<``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__lt__`
-
-  signed greater than or equal to (``>=``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__ge__`
-
-  signed less than or equal to (``<=``)
-    :py:meth:`cvc5_z3py_compat.BitVecRef.__le__`
-
-  equal (``==``)
-    :py:meth:`cvc5_z3py_compat.ExprRef.__eq__`
-
-  not equal (``!=``)
-    :py:meth:`cvc5_z3py_compat.ExprRef.__ne__`
-
-Bit-Vector Term Builders
-------------------------
-
-.. autofunction:: cvc5_z3py_compat.BV2Int
-.. autofunction:: cvc5_z3py_compat.Int2BV
-.. autofunction:: cvc5_z3py_compat.Concat
-.. autofunction:: cvc5_z3py_compat.Extract
-.. autofunction:: cvc5_z3py_compat.ULE
-.. autofunction:: cvc5_z3py_compat.ULT
-.. autofunction:: cvc5_z3py_compat.UGE
-.. autofunction:: cvc5_z3py_compat.UGT
-.. autofunction:: cvc5_z3py_compat.SLE
-.. autofunction:: cvc5_z3py_compat.SLT
-.. autofunction:: cvc5_z3py_compat.SGE
-.. autofunction:: cvc5_z3py_compat.SGT
-.. autofunction:: cvc5_z3py_compat.UDiv
-.. autofunction:: cvc5_z3py_compat.URem
-.. autofunction:: cvc5_z3py_compat.SDiv
-.. autofunction:: cvc5_z3py_compat.SMod
-.. autofunction:: cvc5_z3py_compat.SRem
-.. autofunction:: cvc5_z3py_compat.LShR
-.. autofunction:: cvc5_z3py_compat.RotateLeft
-.. autofunction:: cvc5_z3py_compat.RotateRight
-.. autofunction:: cvc5_z3py_compat.SignExt
-.. autofunction:: cvc5_z3py_compat.ZeroExt
-.. autofunction:: cvc5_z3py_compat.RepeatBitVec
-.. autofunction:: cvc5_z3py_compat.BVRedAnd
-.. autofunction:: cvc5_z3py_compat.BVRedOr
-.. autofunction:: cvc5_z3py_compat.BVAdd
-.. autofunction:: cvc5_z3py_compat.BVMult
-.. autofunction:: cvc5_z3py_compat.BVSub
-.. autofunction:: cvc5_z3py_compat.BVOr
-.. autofunction:: cvc5_z3py_compat.BVAnd
-.. autofunction:: cvc5_z3py_compat.BVXor
-.. autofunction:: cvc5_z3py_compat.BVNeg
-.. autofunction:: cvc5_z3py_compat.BVNot
-
-
-Testers
--------------------
-.. autofunction:: cvc5_z3py_compat.is_bv_sort
-.. autofunction:: cvc5_z3py_compat.is_bv
-.. autofunction:: cvc5_z3py_compat.is_bv_value
-
-Classes (with overloads)
------------------------------
-
-.. autoclass:: cvc5_z3py_compat.BitVecSortRef
-   :members:
-   :special-members:
-.. autoclass:: cvc5_z3py_compat.BitVecRef
-   :members:
-   :special-members:
-.. autoclass:: cvc5_z3py_compat.BitVecNumRef
-   :members:
-   :special-members:

diff --git a/docs/api/python/z3compat/boolean.rst b/docs/api/python/z3compat/boolean.rst
deleted file mode 100644 (file)
index 57ef4e6..0000000
--- a/docs/api/python/z3compat/boolean.rst
+++ /dev/null
@@ -1,77 +0,0 @@
-Core & Booleans
-================
-
-Basic Boolean Term Builders
----------------------------
-.. autofunction:: cvc5_z3py_compat.Bool
-.. autofunction:: cvc5_z3py_compat.BoolVal
-.. autofunction:: cvc5_z3py_compat.BoolSort
-.. autofunction:: cvc5_z3py_compat.FreshBool
-.. autofunction:: cvc5_z3py_compat.Bools
-.. autofunction:: cvc5_z3py_compat.BoolVector
-
-Basic Generic Term Builders
----------------------------
-.. autofunction:: cvc5_z3py_compat.Const
-.. autofunction:: cvc5_z3py_compat.Consts
-.. autofunction:: cvc5_z3py_compat.FreshConst
-.. autofunction:: cvc5_z3py_compat.Function
-.. autofunction:: cvc5_z3py_compat.FreshFunction
-
-Boolean Operators
------------------
-.. autofunction:: cvc5_z3py_compat.And
-.. autofunction:: cvc5_z3py_compat.Or
-.. autofunction:: cvc5_z3py_compat.Not
-.. autofunction:: cvc5_z3py_compat.mk_not
-.. autofunction:: cvc5_z3py_compat.Implies
-.. autofunction:: cvc5_z3py_compat.Xor
-
-Generic Operators
------------------
-.. autofunction:: cvc5_z3py_compat.If
-.. autofunction:: cvc5_z3py_compat.Distinct
-
-Equality
-~~~~~~~~
-
-See
-:py:meth:`cvc5_z3py_compat.ExprRef.__eq__`
-and
-:py:meth:`cvc5_z3py_compat.ExprRef.__ne__`
-for building equality and disequality terms.
-
-
-Testers
--------
-.. autofunction:: cvc5_z3py_compat.is_bool
-.. autofunction:: cvc5_z3py_compat.is_bool_value
-.. autofunction:: cvc5_z3py_compat.is_true
-.. autofunction:: cvc5_z3py_compat.is_false
-.. autofunction:: cvc5_z3py_compat.is_and
-.. autofunction:: cvc5_z3py_compat.is_or
-.. autofunction:: cvc5_z3py_compat.is_implies
-.. autofunction:: cvc5_z3py_compat.is_not
-.. autofunction:: cvc5_z3py_compat.is_eq
-.. autofunction:: cvc5_z3py_compat.is_distinct
-.. autofunction:: cvc5_z3py_compat.is_const
-.. autofunction:: cvc5_z3py_compat.is_func_decl
-
-
-Classes (with overloads)
-----------------------------
-.. autoclass:: cvc5_z3py_compat.ExprRef
-   :members:
-   :special-members:
-.. autoclass:: cvc5_z3py_compat.SortRef
-   :members:
-   :special-members:
-.. autoclass:: cvc5_z3py_compat.BoolRef
-   :members:
-   :special-members:
-.. autoclass:: cvc5_z3py_compat.BoolSortRef
-   :members:
-   :special-members:
-.. autoclass:: cvc5_z3py_compat.FuncDeclRef
-   :members:
-   :special-members:

diff --git a/docs/api/python/z3compat/dt.rst b/docs/api/python/z3compat/dt.rst
deleted file mode 100644 (file)
index 6a29347..0000000
--- a/docs/api/python/z3compat/dt.rst
+++ /dev/null
@@ -1,79 +0,0 @@
-Datatypes
-============
-
-Overview
-----------
-
-To manipulate instances of a datatype, one must first *declare* the datatype itself.
-Declaration happens in three phases. Let's consider declaring a cons-list of
-integers.
-
-First, we initialize the datatype with its *name*
-
-    >>> IntList = Datatype('IntList')
-
-Second, we declare constructors for the datatype, giving the *constructor name*
-and *field names and sorts*. Here is the empty list constructor:
-
-    >>> IntList.declare('nil', ())
-
-Here is the cons constructor:
-
-    >>> IntList.declare('cons', ('val', IntSort()), ('tail', IntList))
-
-Third, after all constructors are declared, we can *create* the datatype,
-finishing its declaration.
-
-    >>> IntList = IntList.create()
-
-Now, one has access to a number of tools for interacting with integer lists.
-
-* ``IntList.nil`` refers to the SMT term that is an empty list,
-  and ``IntList.cons`` refers to the cons constructor.
-* ``IntList.is_nil`` and ``IntList.is_cons`` are testors (a.k.a.,
-  recognizers) for those constructors.
-* ``IntList.val`` and ``IntList.tail`` are selectors (a.k.a. accessors)
-  for the cons constructor.
-
-If constructor, accessor, or selector names are ambiguous (e.g., if different
-constructors have selectors of the same name), then see the methods on
-:py:class:`cvc5_z3py_compat.DatatypeSortRef` to unambiguously access a specific
-function.
-
-To create mutually recursive datatypes, see
-:py:func:`cvc5_z3py_compat.CreateDatatypes`.
-
-To create a codataype (e.g., a possibly infinite stream of integers), pass the
-``isCoDatatype=True`` argument to the :py:class:`cvc5_z3py_compat.Datatype`
-constructor.
-
-    >>> IntStream = Datatype('IntStream', isCoDatatype=True)
-
-Declaration Utilities
----------------------
-
-.. autofunction:: cvc5_z3py_compat.CreateDatatypes
-.. autofunction:: cvc5_z3py_compat.TupleSort
-.. autofunction:: cvc5_z3py_compat.DisjointSum
-
-
-Classes
-------------------------
-.. autoclass:: cvc5_z3py_compat.Datatype
-  :members:
-  :special-members:
-.. autoclass:: cvc5_z3py_compat.DatatypeSortRef
-  :members:
-  :special-members:
-.. autoclass:: cvc5_z3py_compat.DatatypeConstructorRef
-  :members:
-  :special-members:
-.. autoclass:: cvc5_z3py_compat.DatatypeSelectorRef
-  :members:
-  :special-members:
-.. autoclass:: cvc5_z3py_compat.DatatypeRecognizerRef
-  :members:
-  :special-members:
-.. autoclass:: cvc5_z3py_compat.DatatypeRef
-  :members:
-  :special-members:

diff --git a/docs/api/python/z3compat/fp.rst b/docs/api/python/z3compat/fp.rst
deleted file mode 100644 (file)
index d8a72bf..0000000
--- a/docs/api/python/z3compat/fp.rst
+++ /dev/null
@@ -1,126 +0,0 @@
-Floating Point
-==============
-
-Basic FP Term Builders
--------------------------
-
-.. autofunction:: cvc5_z3py_compat.FP
-.. autofunction:: cvc5_z3py_compat.FPs
-.. autofunction:: cvc5_z3py_compat.FPVal
-.. autofunction:: cvc5_z3py_compat.fpNaN
-.. autofunction:: cvc5_z3py_compat.fpPlusInfinity
-.. autofunction:: cvc5_z3py_compat.fpMinusInfinity
-.. autofunction:: cvc5_z3py_compat.fpInfinity
-.. autofunction:: cvc5_z3py_compat.fpPlusZero
-.. autofunction:: cvc5_z3py_compat.fpMinusZero
-.. autofunction:: cvc5_z3py_compat.fpZero
-.. autofunction:: cvc5_z3py_compat.FPSort
-.. autofunction:: cvc5_z3py_compat.Float16
-.. autofunction:: cvc5_z3py_compat.FloatHalf
-.. autofunction:: cvc5_z3py_compat.Float32
-.. autofunction:: cvc5_z3py_compat.FloatSingle
-.. autofunction:: cvc5_z3py_compat.Float64
-.. autofunction:: cvc5_z3py_compat.FloatDouble
-.. autofunction:: cvc5_z3py_compat.Float128
-.. autofunction:: cvc5_z3py_compat.FloatQuadruple
-
-FP Operators
--------------------
-
-See the following operator overloads for building basic floating-point terms:
-
-* ``+``: :py:meth:`cvc5_z3py_compat.FPRef.__add__`
-* ``-``: :py:meth:`cvc5_z3py_compat.FPRef.__sub__`
-* ``*``: :py:meth:`cvc5_z3py_compat.FPRef.__mul__`
-* unary ``-``: :py:meth:`cvc5_z3py_compat.FPRef.__neg__`
-* ``/``: :py:meth:`cvc5_z3py_compat.FPRef.__div__`
-* ``%``: :py:meth:`cvc5_z3py_compat.FPRef.__mod__`
-* ``<=``: :py:meth:`cvc5_z3py_compat.FPRef.__le__`
-* ``<``: :py:meth:`cvc5_z3py_compat.FPRef.__lt__`
-* ``>=``: :py:meth:`cvc5_z3py_compat.FPRef.__ge__`
-* ``>``: :py:meth:`cvc5_z3py_compat.FPRef.__gt__`
-
-.. autofunction:: cvc5_z3py_compat.fpAbs
-.. autofunction:: cvc5_z3py_compat.fpNeg
-.. autofunction:: cvc5_z3py_compat.fpAdd
-.. autofunction:: cvc5_z3py_compat.fpSub
-.. autofunction:: cvc5_z3py_compat.fpMul
-.. autofunction:: cvc5_z3py_compat.fpDiv
-.. autofunction:: cvc5_z3py_compat.fpRem
-.. autofunction:: cvc5_z3py_compat.fpMin
-.. autofunction:: cvc5_z3py_compat.fpMax
-.. autofunction:: cvc5_z3py_compat.fpFMA
-.. autofunction:: cvc5_z3py_compat.fpSqrt
-.. autofunction:: cvc5_z3py_compat.fpRoundToIntegral
-.. autofunction:: cvc5_z3py_compat.fpIsNaN
-.. autofunction:: cvc5_z3py_compat.fpIsInf
-.. autofunction:: cvc5_z3py_compat.fpIsZero
-.. autofunction:: cvc5_z3py_compat.fpIsNormal
-.. autofunction:: cvc5_z3py_compat.fpIsSubnormal
-.. autofunction:: cvc5_z3py_compat.fpIsNegative
-.. autofunction:: cvc5_z3py_compat.fpIsPositive
-.. autofunction:: cvc5_z3py_compat.fpLT
-.. autofunction:: cvc5_z3py_compat.fpLEQ
-.. autofunction:: cvc5_z3py_compat.fpGT
-.. autofunction:: cvc5_z3py_compat.fpGEQ
-.. autofunction:: cvc5_z3py_compat.fpEQ
-.. autofunction:: cvc5_z3py_compat.fpNEQ
-.. autofunction:: cvc5_z3py_compat.fpFP
-.. autofunction:: cvc5_z3py_compat.fpToFP
-.. autofunction:: cvc5_z3py_compat.fpBVToFP
-.. autofunction:: cvc5_z3py_compat.fpFPToFP
-.. autofunction:: cvc5_z3py_compat.fpRealToFP
-.. autofunction:: cvc5_z3py_compat.fpSignedToFP
-.. autofunction:: cvc5_z3py_compat.fpUnsignedToFP
-.. autofunction:: cvc5_z3py_compat.fpToFPUnsigned
-.. autofunction:: cvc5_z3py_compat.fpToSBV
-.. autofunction:: cvc5_z3py_compat.fpToUBV
-.. autofunction:: cvc5_z3py_compat.fpToReal
-
-
-
-Testers
--------------------
-.. autofunction:: cvc5_z3py_compat.is_fp_sort
-.. autofunction:: cvc5_z3py_compat.is_fp
-.. autofunction:: cvc5_z3py_compat.is_fp_value
-.. autofunction:: cvc5_z3py_compat.is_fprm_sort
-.. autofunction:: cvc5_z3py_compat.is_fprm
-.. autofunction:: cvc5_z3py_compat.is_fprm_value
-
-
-FP Rounding Modes
--------------------------
-.. autofunction:: cvc5_z3py_compat.RoundNearestTiesToEven
-.. autofunction:: cvc5_z3py_compat.RNE
-.. autofunction:: cvc5_z3py_compat.RoundNearestTiesToAway
-.. autofunction:: cvc5_z3py_compat.RNA
-.. autofunction:: cvc5_z3py_compat.RoundTowardPositive
-.. autofunction:: cvc5_z3py_compat.RTP
-.. autofunction:: cvc5_z3py_compat.RoundTowardNegative
-.. autofunction:: cvc5_z3py_compat.RTN
-.. autofunction:: cvc5_z3py_compat.RoundTowardZero
-.. autofunction:: cvc5_z3py_compat.RTZ
-.. autofunction:: cvc5_z3py_compat.get_default_rounding_mode
-.. autofunction:: cvc5_z3py_compat.set_default_rounding_mode
-.. autofunction:: cvc5_z3py_compat.get_default_fp_sort
-.. autofunction:: cvc5_z3py_compat.set_default_fp_sort
-
-
-Classes (with overloads)
-------------------------
-
-.. autoclass:: cvc5_z3py_compat.FPSortRef
-  :members:
-  :special-members:
-.. autoclass:: cvc5_z3py_compat.FPRef
-  :members:
-  :special-members:
-.. autoclass:: cvc5_z3py_compat.FPNumRef
-  :members:
-  :special-members:
-.. autoclass:: cvc5_z3py_compat.FPRMRef
-  :members:
-  :special-members:
-
-

diff --git a/docs/api/python/z3compat/internals.rst b/docs/api/python/z3compat/internals.rst
deleted file mode 100644 (file)
index f555d3e..0000000
--- a/docs/api/python/z3compat/internals.rst
+++ /dev/null
@@ -1,17 +0,0 @@
-Internals
-============
-
-
-Testers
--------------------
-.. autofunction:: cvc5_z3py_compat.is_expr
-.. autofunction:: cvc5_z3py_compat.is_sort
-.. autofunction:: cvc5_z3py_compat.is_app
-.. autofunction:: cvc5_z3py_compat.is_app_of
-
-Exceptions
--------------------
-
-.. autoclass:: cvc5_z3py_compat.SMTException
-   :members:
-   :special-members:

diff --git a/docs/api/python/z3compat/quant.rst b/docs/api/python/z3compat/quant.rst
deleted file mode 100644 (file)
index ecf8544..0000000
--- a/docs/api/python/z3compat/quant.rst
+++ /dev/null
@@ -1,20 +0,0 @@
-Quantifiers
-============
-
-Builders
-------------------
-.. autofunction:: cvc5_z3py_compat.ForAll
-.. autofunction:: cvc5_z3py_compat.Exists
-.. autofunction:: cvc5_z3py_compat.Lambda
-
-Testers
--------------------
-.. autofunction:: cvc5_z3py_compat.is_var
-.. autofunction:: cvc5_z3py_compat.is_quantifier
-
-Classes
--------
-.. autoclass:: cvc5_z3py_compat.QuantifierRef
-   :members:
-   :special-members:
-

diff --git a/docs/api/python/z3compat/quickstart.rst b/docs/api/python/z3compat/quickstart.rst
deleted file mode 100644 (file)
index 764b157..0000000
--- a/docs/api/python/z3compat/quickstart.rst
+++ /dev/null
@@ -1,2 +0,0 @@
-Quickstart
-==========

diff --git a/docs/api/python/z3compat/set.rst b/docs/api/python/z3compat/set.rst
deleted file mode 100644 (file)
index 96c83c6..0000000
--- a/docs/api/python/z3compat/set.rst
+++ /dev/null
@@ -1,40 +0,0 @@
-Sets
-============
-
-
-Basic Set Term Builders
--------------------------
-
-.. autofunction:: cvc5_z3py_compat.SetSort
-.. autofunction:: cvc5_z3py_compat.Set
-.. autofunction:: cvc5_z3py_compat.EmptySet
-.. autofunction:: cvc5_z3py_compat.Singleton
-.. autofunction:: cvc5_z3py_compat.FullSet
-
-Set Operators
--------------------
-
-.. autofunction:: cvc5_z3py_compat.SetUnion
-.. autofunction:: cvc5_z3py_compat.SetIntersect
-.. autofunction:: cvc5_z3py_compat.SetAdd
-.. autofunction:: cvc5_z3py_compat.SetDel
-.. autofunction:: cvc5_z3py_compat.SetComplement
-.. autofunction:: cvc5_z3py_compat.SetDifference
-.. autofunction:: cvc5_z3py_compat.SetMinus
-.. autofunction:: cvc5_z3py_compat.IsMember
-.. autofunction:: cvc5_z3py_compat.IsSubset
-
-See the following operator overload for set terms:
-
-* is member: :py:meth:`cvc5_z3py_compat.SetRef.__getitem__`
-
-
-Classes (with overloads)
-------------------------
-
-.. autoclass:: cvc5_z3py_compat.SetSortRef
-  :members:
-  :special-members:
-.. autoclass:: cvc5_z3py_compat.SetRef
-  :members:
-  :special-members:

diff --git a/docs/api/python/z3compat/solver.rst b/docs/api/python/z3compat/solver.rst
deleted file mode 100644 (file)
index c268ec3..0000000
--- a/docs/api/python/z3compat/solver.rst
+++ /dev/null
@@ -1,52 +0,0 @@
-Solvers & Results
-===========================
-
-Simple Solving
-----------------
-
-.. autofunction:: cvc5_z3py_compat.solve
-.. autofunction:: cvc5_z3py_compat.solve_using
-.. autofunction:: cvc5_z3py_compat.prove
-
-
-The Solver Class
-----------------
-
-.. autofunction:: cvc5_z3py_compat.SolverFor
-
-.. autofunction:: cvc5_z3py_compat.SimpleSolver
-
-.. autoclass:: cvc5_z3py_compat.Solver
-  :members:
-  :special-members:
-
-Results & Models
-----------------
-.. data:: cvc5_z3py_compat.unsat
-
-  An *UNSAT* result.
-
-.. data:: cvc5_z3py_compat.sat
-
-  A *SAT* result.
-
-.. data:: cvc5_z3py_compat.unknown
-
-  The satisfiability could not be determined.
-
-.. autoclass:: cvc5_z3py_compat.CheckSatResult
-  :members:
-  :special-members:
-
-.. autoclass:: cvc5_z3py_compat.ModelRef
-  :members:
-  :special-members:
-
-Utilities
---------------
-
-.. autofunction:: cvc5_z3py_compat.evaluate
-.. autofunction:: cvc5_z3py_compat.simplify
-.. autofunction:: cvc5_z3py_compat.substitute
-.. autofunction:: cvc5_z3py_compat.Sum
-.. autofunction:: cvc5_z3py_compat.Product

diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/z3compat/z3compat.rst
deleted file mode 100644 (file)
index 8d13129..0000000
--- a/docs/api/python/z3compat/z3compat.rst
+++ /dev/null
@@ -1,43 +0,0 @@
-z3py compatibility 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.
-
-
-This API is missing some features from cvc5 and Z3Py.
-
-It does not (currently) support these cvc5 features:
-
-* The theories of strings and sequences
-* unsatisfiable cores
-* syntax-guided synthesis (SyGuS)
-
-It does not support the following features of Z3Py:
-
-* Patterns for quantifier instantiation
-* Pseudo-boolean counting constraints: AtMost, AtLeast, ...
-* Special relation classes: PartialOrder, LinearOrder, ...
-* HTML integration
-* Hooks for user-defined propagation and probing
-* Fixedpoint API
-* Finite domains
-* SMT2 file parsing
-
-.. toctree::
-    :maxdepth: 2
-
-    quickstart
-    boolean
-    arith
-    array
-    bitvec
-    dt
-    fp
-    set
-    quant
-    solver
-    internals

diff --git a/docs/conf.py.in b/docs/conf.py.in
index 23ef5da12ba4c9382da98c73be4706c70636b955..28c64d55521dd50682dee34c2b977ae3165032fa 100644 (file)
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -94,12 +94,12 @@ examples_types = {
                 'group': 'java'
         },
         '^<examples>.*\.py$': {
-                'title': 'Python',
+                'title': 'Python (base)',
                 'lang': 'python',
                 'group': 'py-regular'
         },
         '^<z3pycompat>.*\.py$': {
-                'title': 'Python z3py',
+                'title': 'Python (pythonic)',
                 'lang': 'python',
                 'group': 'py-z3pycompat'
         },