More documentation for idiomatic python API (#7798)

Arithmetic, bit-vectors, arrays.

diff --git a/docs/api/python/z3compat/arith.rst b/docs/api/python/z3compat/arith.rst
index 783518e32b10acef35ec8198c6cd6d01cca2e39f..38ecf4ea53b99bb0223a0a05284f167271d728a4 100644 (file)
--- a/docs/api/python/z3compat/arith.rst
+++ b/docs/api/python/z3compat/arith.rst
@@ -1,2 +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/z3compat/array.rst b/docs/api/python/z3compat/array.rst
index 27a6608b69c14b35e058c798032871356ad629e5..599189470842a371e286dd7213b0fe910b096896 100644 (file)
--- a/docs/api/python/z3compat/array.rst
+++ b/docs/api/python/z3compat/array.rst
@@ -1,2 +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/z3compat/bitvec.rst b/docs/api/python/z3compat/bitvec.rst
index df4eb16ec46a53c5d8c855385974c364e57b972e..d8eea48895a95a7d98317d8d98e08aaacfc895e1 100644 (file)
--- a/docs/api/python/z3compat/bitvec.rst
+++ b/docs/api/python/z3compat/bitvec.rst
@@ -1,2 +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/z3compat/boolean.rst b/docs/api/python/z3compat/boolean.rst
index 8ccc649c554f7f72efe395a4926cceacc63196b7..085ed157ff87468f4a51fc8b8c25dd3b08a1b67b 100644 (file)
--- a/docs/api/python/z3compat/boolean.rst
+++ b/docs/api/python/z3compat/boolean.rst
@@ -4,10 +4,10 @@ Core & Booleans
 Basic Boolean Term Builders
 ---------------------------
 .. autofunction:: cvc5_z3py_compat.Bool
-.. autofunction:: cvc5_z3py_compat.Bools
 .. 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
@@ -43,6 +43,7 @@ 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
@@ -54,8 +55,8 @@ Testers
 .. autofunction:: cvc5_z3py_compat.is_const
 
 
-Classes
--------
+Classes (with overloads)
+----------------------------
 .. autoclass:: cvc5_z3py_compat.ExprRef
    :members:
    :special-members:

diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/z3compat/z3compat.rst
index d5a06195d887f65272bcf4f6f232478a2a596d71..33f2f98f14a2055820bf2bfbd8c7ee055b6ebdfe 100644 (file)
--- a/docs/api/python/z3compat/z3compat.rst
+++ b/docs/api/python/z3compat/z3compat.rst
@@ -12,18 +12,13 @@ z3py compatibility Python API
 
     quickstart
     boolean
-    bitvec
     arith
     array
+    bitvec
+    dt
+    fp
     set
+    quant
     solver
     commands
-    fp
-    dt
-    quant
     internals
-
-.. automodule:: cvc5_z3py_compat
-   :members:
-   :private-members:
-   :imported-members: