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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
C API
=====
The C API of cvc5 is based on its :doc:`C++ API <../cpp/cpp>` and is
**feature complete**, within the limits of the C language.
The :doc:`quickstart guide <quickstart>` gives a short introduction of how
to use cvc5 via its C API.
For most applications, the :cpp:type:`Cvc5` solver struct is the main
entry point to cvc5.
One of the key differences is the way **how memory is managed**. While users of
the C++ API can rely on memory being efficiently managed automatically, on the
C level, management to maintain a low overhead needs **more manual
intervention**.
The C API offers **two modes** of memory management:
1. Let cvc5 handle memory management without manual intervention. All memory
allocated by the C API via a term manager (:cpp:type:`Cvc5TermManager`) or
solver (:cpp:type:`Cvc5`) instance will only be released when these
instances are deleted via :cpp:func:`cvc5_delete()` and
:cpp:func:`cvc5_term_manager_delete()`. For example:
.. code:: c
Cvc5TermManager* tm = cvc5_term_manager_new();
Cvc5* cvc5 = cvc5_new(tm);
Cvc5Term a = cvc5_mk_const(tm, cvc5_get_integer_sort(tm), "a");
Cvc5Term two = cvc5_mk_integer_int64(tm, 2);
Cvc5Term args1[2] = {a, two};
cvc5_assert_formula(cvc5, cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args1));
Cvc5Term b = cvc5_mk_const(tm, cvc5_get_integer_sort(tm), "b");
Cvc5Term args2[2] = {b, two};
cvc5_assert_formula(cvc5, cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2));
cvc5_check_sat(cvc5);
cvc5_delete(cvc5);
cvc5_term_manager_delete(tm);
2. Introduce a more fine-grained, user-level memory management for objects
created via a term manager or solver via the corresponding ``cvc5_*_copy()``
and ``cvc5_*_release()`` functions. The copy functions increment the
reference counter of an object, the release functions decrement the
reference counter and free its allocated memory when the counter reaches 0.
For example:
.. code:: c
Cvc5TermManager* tm = cvc5_term_manager_new();
Cvc5* cvc5 = cvc5_new(tm);
Cvc5Term a = cvc5_mk_const(tm, cvc5_get_integer_sort(tm), "a");
Cvc5Term two = cvc5_mk_integer_int64(tm, 2);
Cvc5Term args1[2] = {a, two};
cvc5_assert_formula(cvc5, cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args1));
// we can release 'a' here, not needed anymore
cvc5_term_release(a);
Cvc5Term b = cvc5_mk_const(tm, cvc5_get_integer_sort(tm), "b");
Cvc5Term args2[2] = {b, two};
cvc5_assert_formula(cvc5, cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2));
cvc5_check_sat(cvc5);
cvc5_delete(cvc5);
cvc5_term_manager_delete(tm);
.. container:: hide-toctree
.. toctree::
quickstart
types/cvc5
types/cvc5command
types/cvc5datatype
types/cvc5datatypedecl
types/cvc5datatypeconstructor
types/cvc5datatypeconstructordecl
types/cvc5datatypeselector
types/cvc5grammar
types/cvc5inputparser
types/cvc5op
types/cvc5proof
types/cvc5result
types/cvc5sort
types/cvc5statistics
types/cvc5symbolmanager
types/cvc5synthresult
types/cvc5term
types/cvc5termmanager
structs/cvc5optioninfo.rst
structs/cvc5plugin
enums/cvc5kind
enums/cvc5sortkind
enums/cvc5roundingmode
enums/cvc5unknownexplanation
enums/modes
---------
Types
-----
The following types are defined via typedefs but used as black boxes, their
internals are hidden.
- typedef struct :doc:`types/cvc5`
- typedef struct :doc:`types/cvc5command`
- typedef struct :doc:`types/cvc5datatype`
- typedef struct :doc:`types/cvc5datatypedecl`
- typedef struct :doc:`types/cvc5datatypeconstructor`
- typedef struct :doc:`types/cvc5datatypeconstructordecl`
- typedef struct :doc:`types/cvc5datatypeselector`
- typedef struct :doc:`types/cvc5grammar`
- typedef struct :doc:`types/cvc5inputparser`
- typedef struct :doc:`types/cvc5op`
- typedef struct :doc:`types/cvc5proof`
- typedef struct :doc:`types/cvc5result`
- typedef struct :doc:`types/cvc5sort`
- typedef struct :cpp:type:`Cvc5Stat`
- typedef struct :doc:`types/cvc5statistics`
- typedef struct :doc:`types/cvc5symbolmanager`
- typedef struct :doc:`types/cvc5synthresult`
- typedef struct :doc:`types/cvc5term`
- typedef struct :doc:`types/cvc5termmanager`
Structs
-------
The following structs are fully exposed via the API.
- struct :doc:`structs/cvc5optioninfo`
- struct :doc:`structs/cvc5plugin`
Enums
------
- enum :doc:`enums/cvc5kind`
- enum :doc:`enums/cvc5sortkind`
- enum :cpp:enum:`Cvc5OptionInfoKind`
- enum :doc:`enums/cvc5roundingmode`
- enum :doc:`enums/cvc5unknownexplanation`
- enums for :doc:`configuration modes <enums/modes>`
- enum :cpp:enum:`Cvc5BlockModelsMode`
- enum :cpp:enum:`Cvc5LearnedLitType`
- enum :cpp:enum:`Cvc5FindSynthTarget`
- enum :cpp:enum:`Cvc5OptionCategory`
- enum :cpp:enum:`Cvc5ProofComponent`
- enum :cpp:enum:`Cvc5ProofFormat`
- enums classes for :doc:`proof rules <enums/cvc5proofrule>`
- enum :cpp:enum:`Cvc5ProofRule`
- enum :cpp:enum:`Cvc5ProofRewriteRule`
|
