From 48e880074f563926a8d681f802116c2d14d01f62 Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Fri, 17 Dec 2021 10:42:48 -0800
Subject: [PATCH] More documentation for idiomatic python API (#7798)

Arithmetic, bit-vectors, arrays.
---
 docs/api/python/z3compat/arith.rst    | 120 ++++++++++++++++++++++++
 docs/api/python/z3compat/array.rst    |  43 +++++++++
 docs/api/python/z3compat/bitvec.rst   | 128 ++++++++++++++++++++++++++
 docs/api/python/z3compat/boolean.rst  |   7 +-
 docs/api/python/z3compat/z3compat.rst |  13 +--
 5 files changed, 299 insertions(+), 12 deletions(-)

diff --git a/docs/api/python/z3compat/arith.rst b/docs/api/python/z3compat/arith.rst
index 783518e32..38ecf4ea5 100644
--- 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 27a6608b6..599189470 100644
--- 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 df4eb16ec..d8eea4889 100644
--- 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 8ccc649c5..085ed157f 100644
--- 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 d5a06195d..33f2f98f1 100644
--- 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:
-- 
2.30.2