docs/api/python/pythonic/pythonic.rst

Pythonic API
=========================================

.. only:: not bindings_python

    .. warning::

        This documentation was built while python bindings were disabled. This part of the documentation is likely either empty or outdated. Please enable :code:`BUILD_BINDINGS_PYTHON` in :code:`cmake` and build the documentation again.


This API is missing some features from cvc5 and Z3Py.

It does not (currently) support these cvc5 features:

* The theory of bags
* unsatisfiable cores
* syntax-guided synthesis (SyGuS)

It does not (currently) support the following features of Z3Py:

* Patterns for quantifier instantiation
* Pseudo-boolean counting constraints: AtMost, AtLeast, ...
* Special relation classes: PartialOrder, LinearOrder, ...
* HTML integration
* Hooks for user-defined propagation and probing
* Fixedpoint API
* Finite domains
* SMT2 file parsing

.. toctree::
    :maxdepth: 2

    quickstart
    boolean
    arith
    array
    bitvec
    dt
    finite_field
    fp
    set
    string
    sequence
    quant
    solver
    internals
Rename python APIs (#7950) Rename python APIs to "base" and "pythonic" 2022-01-14 13:45:19 -08:00			`Pythonic API`
Add documentation for z3py compatibility API (#7652) This PR includes documentation for the z3py compatibility API into our general API. It does so by adding the z3py compatibility API as an external project to download it and then have sphinx document it via the autodoc extension that we already use for our regular python API. Right now we simply show everything on one page, which should be refactored in the future. 2021-11-17 11:40:49 -08:00			`=========================================`

			`.. only:: not bindings_python`

			`.. warning::`

			This documentation was built while python bindings were disabled. This part of the documentation is likely either empty or outdated. Please enable :code:`BUILD_BINDINGS_PYTHON` in :code:`cmake` and build the documentation again.

Add new idiomatic examples (#7912) 2022-01-10 16:49:02 -08:00
			`This API is missing some features from cvc5 and Z3Py.`

			`It does not (currently) support these cvc5 features:`

Updating missing features in pythonic API (#9929) Following cvc5/cvc5_pythonic_api#86 . 2023-08-07 12:25:31 -07:00			`* The theory of bags`
Add new idiomatic examples (#7912) 2022-01-10 16:49:02 -08:00			`* unsatisfiable cores`
			`* syntax-guided synthesis (SyGuS)`

Rename python APIs (#7950) Rename python APIs to "base" and "pythonic" 2022-01-14 13:45:19 -08:00			`It does not (currently) support the following features of Z3Py:`
Add new idiomatic examples (#7912) 2022-01-10 16:49:02 -08:00
			`* Patterns for quantifier instantiation`
			`* Pseudo-boolean counting constraints: AtMost, AtLeast, ...`
			`* Special relation classes: PartialOrder, LinearOrder, ...`
			`* HTML integration`
			`* Hooks for user-defined propagation and probing`
			`* Fixedpoint API`
			`* Finite domains`
			`* SMT2 file parsing`

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			`.. toctree::`
			`:maxdepth: 2`

			`quickstart`
			`boolean`
			`arith`
			`array`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays. 2021-12-17 10:42:48 -08:00			`bitvec`
			`dt`
More external FF documentation (#10049) - document the (extension) theory itself - add a pythonic API example 2023-11-10 12:10:27 -08:00			`finite_field`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays. 2021-12-17 10:42:48 -08:00			`fp`
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			`set`
Add strings and sequences to the pythonic API documentation (#10654) This PR adds the documentation for strings and sequences in the pythonic API. 2024-04-19 15:34:00 +03:00			`string`
			`sequence`
More documentation for idiomatic python API (#7798) Arithmetic, bit-vectors, arrays. 2021-12-17 10:42:48 -08:00			`quant`
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			`solver`
			`internals`