mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
ea5e75d04a
We decided we want to ship the pythonic API together with our base python API. This PR adds a new target cvc5_python_api that first builds the base python API and then copies the pythonic API over. Furthermore we now use the cvc5.pythonic module to generate the corresponding documentation.
127 lines
4.2 KiB
ReStructuredText
127 lines
4.2 KiB
ReStructuredText
Floating Point
|
|
==============
|
|
|
|
Basic FP Term Builders
|
|
-------------------------
|
|
|
|
.. autofunction:: cvc5.pythonic.FP
|
|
.. autofunction:: cvc5.pythonic.FPs
|
|
.. autofunction:: cvc5.pythonic.FPVal
|
|
.. autofunction:: cvc5.pythonic.fpNaN
|
|
.. autofunction:: cvc5.pythonic.fpPlusInfinity
|
|
.. autofunction:: cvc5.pythonic.fpMinusInfinity
|
|
.. autofunction:: cvc5.pythonic.fpInfinity
|
|
.. autofunction:: cvc5.pythonic.fpPlusZero
|
|
.. autofunction:: cvc5.pythonic.fpMinusZero
|
|
.. autofunction:: cvc5.pythonic.fpZero
|
|
.. autofunction:: cvc5.pythonic.FPSort
|
|
.. autofunction:: cvc5.pythonic.Float16
|
|
.. autofunction:: cvc5.pythonic.FloatHalf
|
|
.. autofunction:: cvc5.pythonic.Float32
|
|
.. autofunction:: cvc5.pythonic.FloatSingle
|
|
.. autofunction:: cvc5.pythonic.Float64
|
|
.. autofunction:: cvc5.pythonic.FloatDouble
|
|
.. autofunction:: cvc5.pythonic.Float128
|
|
.. autofunction:: cvc5.pythonic.FloatQuadruple
|
|
|
|
FP Operators
|
|
-------------------
|
|
|
|
See the following operator overloads for building basic floating-point terms:
|
|
|
|
* ``+``: :py:meth:`cvc5.pythonic.FPRef.__add__`
|
|
* ``-``: :py:meth:`cvc5.pythonic.FPRef.__sub__`
|
|
* ``*``: :py:meth:`cvc5.pythonic.FPRef.__mul__`
|
|
* unary ``-``: :py:meth:`cvc5.pythonic.FPRef.__neg__`
|
|
* ``/``: :py:meth:`cvc5.pythonic.FPRef.__div__`
|
|
* ``%``: :py:meth:`cvc5.pythonic.FPRef.__mod__`
|
|
* ``<=``: :py:meth:`cvc5.pythonic.FPRef.__le__`
|
|
* ``<``: :py:meth:`cvc5.pythonic.FPRef.__lt__`
|
|
* ``>=``: :py:meth:`cvc5.pythonic.FPRef.__ge__`
|
|
* ``>``: :py:meth:`cvc5.pythonic.FPRef.__gt__`
|
|
|
|
.. autofunction:: cvc5.pythonic.fpAbs
|
|
.. autofunction:: cvc5.pythonic.fpNeg
|
|
.. autofunction:: cvc5.pythonic.fpAdd
|
|
.. autofunction:: cvc5.pythonic.fpSub
|
|
.. autofunction:: cvc5.pythonic.fpMul
|
|
.. autofunction:: cvc5.pythonic.fpDiv
|
|
.. autofunction:: cvc5.pythonic.fpRem
|
|
.. autofunction:: cvc5.pythonic.fpMin
|
|
.. autofunction:: cvc5.pythonic.fpMax
|
|
.. autofunction:: cvc5.pythonic.fpFMA
|
|
.. autofunction:: cvc5.pythonic.fpSqrt
|
|
.. autofunction:: cvc5.pythonic.fpRoundToIntegral
|
|
.. autofunction:: cvc5.pythonic.fpIsNaN
|
|
.. autofunction:: cvc5.pythonic.fpIsInf
|
|
.. autofunction:: cvc5.pythonic.fpIsZero
|
|
.. autofunction:: cvc5.pythonic.fpIsNormal
|
|
.. autofunction:: cvc5.pythonic.fpIsSubnormal
|
|
.. autofunction:: cvc5.pythonic.fpIsNegative
|
|
.. autofunction:: cvc5.pythonic.fpIsPositive
|
|
.. autofunction:: cvc5.pythonic.fpLT
|
|
.. autofunction:: cvc5.pythonic.fpLEQ
|
|
.. autofunction:: cvc5.pythonic.fpGT
|
|
.. autofunction:: cvc5.pythonic.fpGEQ
|
|
.. autofunction:: cvc5.pythonic.fpEQ
|
|
.. autofunction:: cvc5.pythonic.fpNEQ
|
|
.. autofunction:: cvc5.pythonic.fpFP
|
|
.. autofunction:: cvc5.pythonic.fpToFP
|
|
.. autofunction:: cvc5.pythonic.fpBVToFP
|
|
.. autofunction:: cvc5.pythonic.fpFPToFP
|
|
.. autofunction:: cvc5.pythonic.fpRealToFP
|
|
.. autofunction:: cvc5.pythonic.fpSignedToFP
|
|
.. autofunction:: cvc5.pythonic.fpUnsignedToFP
|
|
.. autofunction:: cvc5.pythonic.fpToFPUnsigned
|
|
.. autofunction:: cvc5.pythonic.fpToSBV
|
|
.. autofunction:: cvc5.pythonic.fpToUBV
|
|
.. autofunction:: cvc5.pythonic.fpToReal
|
|
|
|
|
|
|
|
Testers
|
|
-------------------
|
|
.. autofunction:: cvc5.pythonic.is_fp_sort
|
|
.. autofunction:: cvc5.pythonic.is_fp
|
|
.. autofunction:: cvc5.pythonic.is_fp_value
|
|
.. autofunction:: cvc5.pythonic.is_fprm_sort
|
|
.. autofunction:: cvc5.pythonic.is_fprm
|
|
.. autofunction:: cvc5.pythonic.is_fprm_value
|
|
|
|
|
|
FP Rounding Modes
|
|
-------------------------
|
|
.. autofunction:: cvc5.pythonic.RoundNearestTiesToEven
|
|
.. autofunction:: cvc5.pythonic.RNE
|
|
.. autofunction:: cvc5.pythonic.RoundNearestTiesToAway
|
|
.. autofunction:: cvc5.pythonic.RNA
|
|
.. autofunction:: cvc5.pythonic.RoundTowardPositive
|
|
.. autofunction:: cvc5.pythonic.RTP
|
|
.. autofunction:: cvc5.pythonic.RoundTowardNegative
|
|
.. autofunction:: cvc5.pythonic.RTN
|
|
.. autofunction:: cvc5.pythonic.RoundTowardZero
|
|
.. autofunction:: cvc5.pythonic.RTZ
|
|
.. autofunction:: cvc5.pythonic.get_default_rounding_mode
|
|
.. autofunction:: cvc5.pythonic.set_default_rounding_mode
|
|
.. autofunction:: cvc5.pythonic.get_default_fp_sort
|
|
.. autofunction:: cvc5.pythonic.set_default_fp_sort
|
|
|
|
|
|
Classes (with overloads)
|
|
------------------------
|
|
|
|
.. autoclass:: cvc5.pythonic.FPSortRef
|
|
:members:
|
|
:special-members:
|
|
.. autoclass:: cvc5.pythonic.FPRef
|
|
:members:
|
|
:special-members:
|
|
.. autoclass:: cvc5.pythonic.FPNumRef
|
|
:members:
|
|
:special-members:
|
|
.. autoclass:: cvc5.pythonic.FPRMRef
|
|
:members:
|
|
:special-members:
|
|
|
|
|