blob: 96177e7d8c71c7e9e8c53e0f4ce38c94a2186bbb (
plain)
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
|
C++ API Documentation
=====================
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::api`` namespace provides more details on the individual classes.
For most applications, the :cpp:class:`Solver <cvc5::api::Solver>` class is the main entry point to cvc5.
.. container:: hide-toctree
.. toctree::
:maxdepth: 0
quickstart
exceptions
datatype
datatypeconstructor
datatypeconstructordecl
datatypedecl
datatypeselector
grammar
kind
op
optioninfo
result
roundingmode
solver
sort
statistics
term
Class hierarchy
^^^^^^^^^^^^^^^
``namespace cvc5::api {``
* class :cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>`
* class :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>`
* class :ref:`api/cpp/datatype:datatype`
* class :cpp:class:`const_iterator <cvc5::api::Datatype::const_iterator>`
* class :ref:`api/cpp/datatypeconstructor:datatypeconstructor`
* class :cpp:class:`const_iterator <cvc5::api::DatatypeConstructor::const_iterator>`
* class :ref:`api/cpp/datatypeconstructordecl:datatypeconstructordecl`
* class :ref:`api/cpp/datatypedecl:datatypedecl`
* class :ref:`api/cpp/datatypeselector:datatypeselector`
* class :ref:`api/cpp/grammar:grammar`
* class :ref:`api/cpp/kind:kind`
* class :ref:`api/cpp/op:op`
* class :ref:`api/cpp/optioninfo:optioninfo`
* class :ref:`api/cpp/result:result`
* enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>`
* class :ref:`api/cpp/roundingmode:roundingmode`
* class :ref:`api/cpp/solver:solver`
* class :ref:`api/cpp/sort:sort`
* class :cpp:class:`Stat <cvc5::api::Stat>`
* class :cpp:class:`Statistics <cvc5::api::Statistics>`
* class :ref:`api/cpp/term:term`
* class :cpp:class:`const_iterator <cvc5::api::Term::const_iterator>`
``}``
|
