ada/cvc5
0
0
Fork 0
mirror of https://github.com/AdaCore/cvc5.git synced 2026-02-12 12:32:16 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
24-sustained
cvc5/docs/api/python/pythonic/bitvec.rst

131 lines
3.4 KiB
ReStructuredText
Raw Permalink Normal View History

Scaffold the idiomatic API's documentation (#7715) Scaffolding the documentation, and fleshing it out for the Boolean functions and terms.
2021-11-30 13:06:30 -08:00
Bit-Vectors
============
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
Basic Bit-Vector Term Builders
----------------------------------
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
.. autofunction:: cvc5.pythonic.BitVec
.. autofunction:: cvc5.pythonic.BitVecVal
.. autofunction:: cvc5.pythonic.BitVecSort
.. autofunction:: cvc5.pythonic.BitVecs
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
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 (``+``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__add__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
subtraction (``-``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__sub__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
multiplication (``*``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__mul__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
division (``/``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__div__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
* bit-wise
or (``|``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__or__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
and (``&``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__and__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
xor (``^``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__xor__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
bit complement (``~``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__invert__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
negation (``-``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__neg__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
left shift (``<<``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__lshift__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
right shift (``>>``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__rshift__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
* comparisons
signed greater than (``>``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__gt__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
signed less than (``<``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__lt__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
signed greater than or equal to (``>=``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__ge__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
signed less than or equal to (``<=``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.BitVecRef.__le__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
equal (``==``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.ExprRef.__eq__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
not equal (``!=``)
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
:py:meth:`cvc5.pythonic.ExprRef.__ne__`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
Bit-Vector Term Builders
------------------------
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
.. autofunction:: cvc5.pythonic.BV2Int
.. autofunction:: cvc5.pythonic.Int2BV
.. autofunction:: cvc5.pythonic.Concat
.. autofunction:: cvc5.pythonic.Extract
.. autofunction:: cvc5.pythonic.ULE
.. autofunction:: cvc5.pythonic.ULT
.. autofunction:: cvc5.pythonic.UGE
.. autofunction:: cvc5.pythonic.UGT
.. autofunction:: cvc5.pythonic.SLE
.. autofunction:: cvc5.pythonic.SLT
.. autofunction:: cvc5.pythonic.SGE
.. autofunction:: cvc5.pythonic.SGT
.. autofunction:: cvc5.pythonic.UDiv
.. autofunction:: cvc5.pythonic.URem
.. autofunction:: cvc5.pythonic.SDiv
.. autofunction:: cvc5.pythonic.SMod
.. autofunction:: cvc5.pythonic.SRem
.. autofunction:: cvc5.pythonic.LShR
.. autofunction:: cvc5.pythonic.RotateLeft
.. autofunction:: cvc5.pythonic.RotateRight
.. autofunction:: cvc5.pythonic.SignExt
.. autofunction:: cvc5.pythonic.ZeroExt
.. autofunction:: cvc5.pythonic.RepeatBitVec
.. autofunction:: cvc5.pythonic.BVRedAnd
.. autofunction:: cvc5.pythonic.BVRedOr
.. autofunction:: cvc5.pythonic.BVAdd
.. autofunction:: cvc5.pythonic.BVMult
.. autofunction:: cvc5.pythonic.BVSub
.. autofunction:: cvc5.pythonic.BVOr
.. autofunction:: cvc5.pythonic.BVAnd
.. autofunction:: cvc5.pythonic.BVXor
.. autofunction:: cvc5.pythonic.BVNeg
.. autofunction:: cvc5.pythonic.BVNot
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
Testers
-------------------
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
.. autofunction:: cvc5.pythonic.is_bv_sort
.. autofunction:: cvc5.pythonic.is_bv
.. autofunction:: cvc5.pythonic.is_bv_value
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
Classes (with overloads)
-----------------------------
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
.. autoclass:: cvc5.pythonic.BitVecSortRef
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
:members:
:special-members:
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
.. autoclass:: cvc5.pythonic.BitVecRef
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
:members:
:special-members:
Integrate pythonic api (#8131) 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.
2022-03-03 03:16:09 +01:00
.. autoclass:: cvc5.pythonic.BitVecNumRef
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays.
2021-12-17 10:42:48 -08:00
:members:
:special-members:
Reference in New Issue Copy Permalink