From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Wed, 5 Jan 2022 20:47:09 +0000 (-0800)
Subject: Py idiomatic API: Doc sets, datatypes, FP (#7877)
X-Git-Tag: cvc5-1.0.0~595
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e1c81278ece836ac58ba4a84c0b65defcaf5c92f;p=cvc5.git

Py idiomatic API: Doc sets, datatypes, FP (#7877)
---

diff --git a/docs/api/python/z3compat/dt.rst b/docs/api/python/z3compat/dt.rst
index 82fb2c7fe..6a293479e 100644
--- a/docs/api/python/z3compat/dt.rst
+++ b/docs/api/python/z3compat/dt.rst
@@ -1,2 +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/z3compat/fp.rst b/docs/api/python/z3compat/fp.rst
index 2306028c1..d8a72bfb0 100644
--- a/docs/api/python/z3compat/fp.rst
+++ b/docs/api/python/z3compat/fp.rst
@@ -1,2 +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/z3compat/set.rst b/docs/api/python/z3compat/set.rst
index 52a853ce8..96c83c6ad 100644
--- a/docs/api/python/z3compat/set.rst
+++ b/docs/api/python/z3compat/set.rst
@@ -1,2 +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: