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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
C++ API
=====================
The C++ API is the primary interface for cvc5 and exposes the full
functionality of cvc5.
The :doc:`quickstart guide <quickstart>` gives a short introduction, while the
following class hierarchy of the ``cvc5`` namespace provides more details on
the individual classes.
For most applications, the :cpp:class:`Solver <cvc5::Solver>` class is the main
entry point to cvc5.
.. container:: hide-toctree
.. toctree::
quickstart
exceptions/exceptions
classes/command
classes/datatype
classes/datatypeconstructor
classes/datatypeconstructordecl
classes/datatypedecl
classes/datatypeselector
classes/driveroptions
classes/grammar
classes/inputparser
enums/kind
enums/modes
classes/op
classes/optioninfo
classes/plugin
classes/proof
classes/result
enums/roundingmode
classes/solver
classes/sort
enums/sortkind
classes/statistics
classes/symbolmanager
classes/synthresult
classes/term
classes/termmanager
enums/unknownexplanation
Class hierarchy
^^^^^^^^^^^^^^^
``namespace cvc5 {``
* class :cpp:class:`CVC5ApiException <cvc5::CVC5ApiException>`
* class :cpp:class:`CVC5ApiRecoverableException <cvc5::CVC5ApiRecoverableException>`
* class :doc:`classes/datatype`
* class :cpp:class:`const_iterator <cvc5::Datatype::const_iterator>`
* class :doc:`classes/datatypeconstructor`
* class :cpp:class:`const_iterator <cvc5::DatatypeConstructor::const_iterator>`
* class :doc:`classes/datatypeconstructordecl`
* class :doc:`classes/datatypedecl`
* class :doc:`classes/datatypeselector`
* class :doc:`classes/driveroptions`
* class :doc:`classes/grammar`
* class :doc:`classes/op`
* class :doc:`classes/optioninfo`
* class :doc:`classes/proof`
* class :doc:`classes/result`
* class :doc:`classes/plugin`
* class :doc:`classes/termmanager`
* class :doc:`classes/solver`
* class :doc:`classes/sort`
* class :cpp:class:`Stat <cvc5::Stat>`
* class :doc:`classes/statistics`
* class :doc:`classes/synthresult`
* class :doc:`classes/term`
* class :cpp:class:`const_iterator <cvc5::Term::const_iterator>`
* enum class :doc:`enums/kind`
* enum class :doc:`enums/sortkind`
* enum class :doc:`enums/roundingmode`
* enum class :doc:`enums/unknownexplanation`
* enum classes for :doc:`proof rules <enums/proofrule>`
* enum class :cpp:enum:`ProofRule <cvc5::ProofRule>`
* enum class :cpp:enum:`ProofRewriteRule <cvc5::ProofRewriteRule>`
``namespace modes {``
* enum classes for :doc:`configuration modes <enums/modes>`
* enum class for :cpp:enum:`cvc5::modes::BlockModelsMode`
* enum class for :cpp:enum:`cvc5::modes::LearnedLitType`
* enum class for :cpp:enum:`cvc5::modes::FindSynthTarget`
* enum class for :cpp:enum:`cvc5::modes::OptionCategory`
* enum class for :cpp:enum:`cvc5::modes::ProofComponent`
* enum class for :cpp:enum:`cvc5::modes::ProofFormat`
``}``
``namespace parser {``
* class :cpp:class:`ParserException <cvc5::parser::ParserException>`
* class :cpp:class:`Command <cvc5::parser::Command>`
* class :doc:`classes/inputparser`
* class :cpp:class:`SymbolManager <cvc5::parser::SymbolManager>`
``}``
``}``
|
