From e1c81278ece836ac58ba4a84c0b65defcaf5c92f Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 5 Jan 2022 12:47:09 -0800 Subject: [PATCH] Py idiomatic API: Doc sets, datatypes, FP (#7877) --- docs/api/python/z3compat/dt.rst | 77 +++++++++++++++++++ docs/api/python/z3compat/fp.rst | 126 ++++++++++++++++++++++++++++++- docs/api/python/z3compat/set.rst | 38 ++++++++++ 3 files changed, 240 insertions(+), 1 deletion(-) 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: -- 2.30.2