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 theories of strings, sequences and 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
    fp
    set
    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:`

Add a few miscellaneous pieces of documentation (#8533) 2022-04-01 20:02:47 -05:00			`* The theories of strings, sequences and 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`
			`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`
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`