1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
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
|
