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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
Base Python 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 is the base Python API.
It is implemented on top of the C++ API and mirrors the :doc:`C++ API
<../../cpp/cpp>`.
For a higher-level, more pythonic programming experience, cvc5 provides the
:doc:`pythonic API <../pythonic/pythonic>`.
.. toctree::
:maxdepth: 1
:hidden:
quickstart
command
datatype
datatypeconstructor
datatypeconstructordecl
datatypedecl
datatypeselector
grammar
inputparser
kind
modes
op
plugin
proof
result
roundingmode
solver
sort
sortkind
statistics
symbolmanager
synthresult
term
termmanager
unknownexplanation
----
Classes
-------
- :doc:`command`
- :doc:`datatype`
- :doc:`datatypeconstructor`
- :doc:`datatypeconstructordecl`
- :doc:`datatypedecl`
- :doc:`datatypeselector`
- :doc:`grammar`
- :doc:`inputparser`
- :doc:`op`
- :doc:`plugin`
- :doc:`proof`
- :doc:`result`
- :doc:`solver`
- :doc:`sort`
- :doc:`statistics`
- :doc:`symbolmanager`
- :doc:`synthresult`
- :doc:`term`
Enums
-----
- :doc:`kind`
- :doc:`proofrule`
- :doc:`roundingmode`
- :doc:`unknownexplanation`
- enums for :doc:`configuration modes <modes>`
- :py:obj:`BlockModelsMode <cvc5.BlockModelsMode>`
- :py:obj:`LearnedLitType <cvc5.LearnedLitType>`
- :py:obj:`OptionCategory <cvc5.OptionCategory>`
- :py:obj:`ProofComponent <cvc5.ProofComponent>`
- :py:obj:`ProofFormat <cvc5.ProofFormat>`
|
