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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
z3_ast_containers.h
Abstract:
AST Containers
Author:
Christoph M. Wintersteiger (cwinter) 2015-12-03
Notes:
--*/
#ifndef Z3_AST_CONTAINERS_H_
#define Z3_AST_CONTAINERS_H_
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
/** \defgroup capi C API */
/*@{*/
/** @name AST vectors */
/*@{*/
/**
\brief Return an empty AST vector.
\remark Reference counting must be used to manage AST vectors, even when the Z3_context was
created using #Z3_mk_context instead of #Z3_mk_context_rc.
def_API('Z3_mk_ast_vector', AST_VECTOR, (_in(CONTEXT),))
*/
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c);
/**
\brief Increment the reference counter of the given AST vector.
def_API('Z3_ast_vector_inc_ref', VOID, (_in(CONTEXT), _in(AST_VECTOR)))
*/
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v);
/**
\brief Decrement the reference counter of the given AST vector.
def_API('Z3_ast_vector_dec_ref', VOID, (_in(CONTEXT), _in(AST_VECTOR)))
*/
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v);
/**
\brief Return the size of the given AST vector.
def_API('Z3_ast_vector_size', UINT, (_in(CONTEXT), _in(AST_VECTOR)))
*/
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v);
/**
\brief Return the AST at position \c i in the AST vector \c v.
\pre i < Z3_ast_vector_size(c, v)
def_API('Z3_ast_vector_get', AST, (_in(CONTEXT), _in(AST_VECTOR), _in(UINT)))
*/
Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i);
/**
\brief Update position \c i of the AST vector \c v with the AST \c a.
\pre i < Z3_ast_vector_size(c, v)
def_API('Z3_ast_vector_set', VOID, (_in(CONTEXT), _in(AST_VECTOR), _in(UINT), _in(AST)))
*/
void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a);
/**
\brief Resize the AST vector \c v.
def_API('Z3_ast_vector_resize', VOID, (_in(CONTEXT), _in(AST_VECTOR), _in(UINT)))
*/
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n);
/**
\brief Add the AST \c a in the end of the AST vector \c v. The size of \c v is increased by one.
def_API('Z3_ast_vector_push', VOID, (_in(CONTEXT), _in(AST_VECTOR), _in(AST)))
*/
void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a);
/**
\brief Translate the AST vector \c v from context \c s into an AST vector in context \c t.
def_API('Z3_ast_vector_translate', AST_VECTOR, (_in(CONTEXT), _in(AST_VECTOR), _in(CONTEXT)))
*/
Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t);
/**
\brief Convert AST vector into a string.
def_API('Z3_ast_vector_to_string', STRING, (_in(CONTEXT), _in(AST_VECTOR)))
*/
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v);
/*@}*/
/** @name AST maps */
/*@{*/
/**
\brief Return an empty mapping from AST to AST
\remark Reference counting must be used to manage AST maps, even when the Z3_context was
created using #Z3_mk_context instead of #Z3_mk_context_rc.
def_API('Z3_mk_ast_map', AST_MAP, (_in(CONTEXT),) )
*/
Z3_ast_map Z3_API Z3_mk_ast_map(Z3_context c);
/**
\brief Increment the reference counter of the given AST map.
def_API('Z3_ast_map_inc_ref', VOID, (_in(CONTEXT), _in(AST_MAP)))
*/
void Z3_API Z3_ast_map_inc_ref(Z3_context c, Z3_ast_map m);
/**
\brief Decrement the reference counter of the given AST map.
def_API('Z3_ast_map_dec_ref', VOID, (_in(CONTEXT), _in(AST_MAP)))
*/
void Z3_API Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m);
/**
\brief Return true if the map \c m contains the AST key \c k.
def_API('Z3_ast_map_contains', BOOL, (_in(CONTEXT), _in(AST_MAP), _in(AST)))
*/
bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k);
/**
\brief Return the value associated with the key \c k.
The procedure invokes the error handler if \c k is not in the map.
def_API('Z3_ast_map_find', AST, (_in(CONTEXT), _in(AST_MAP), _in(AST)))
*/
Z3_ast Z3_API Z3_ast_map_find(Z3_context c, Z3_ast_map m, Z3_ast k);
/**
\brief Store/Replace a new key, value pair in the given map.
def_API('Z3_ast_map_insert', VOID, (_in(CONTEXT), _in(AST_MAP), _in(AST), _in(AST)))
*/
void Z3_API Z3_ast_map_insert(Z3_context c, Z3_ast_map m, Z3_ast k, Z3_ast v);
/**
\brief Erase a key from the map.
def_API('Z3_ast_map_erase', VOID, (_in(CONTEXT), _in(AST_MAP), _in(AST)))
*/
void Z3_API Z3_ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k);
/**
\brief Remove all keys from the given map.
def_API('Z3_ast_map_reset', VOID, (_in(CONTEXT), _in(AST_MAP)))
*/
void Z3_API Z3_ast_map_reset(Z3_context c, Z3_ast_map m);
/**
\brief Return the size of the given map.
def_API('Z3_ast_map_size', UINT, (_in(CONTEXT), _in(AST_MAP)))
*/
unsigned Z3_API Z3_ast_map_size(Z3_context c, Z3_ast_map m);
/**
\brief Return the keys stored in the given map.
def_API('Z3_ast_map_keys', AST_VECTOR, (_in(CONTEXT), _in(AST_MAP)))
*/
Z3_ast_vector Z3_API Z3_ast_map_keys(Z3_context c, Z3_ast_map m);
/**
\brief Convert the given map into a string.
def_API('Z3_ast_map_to_string', STRING, (_in(CONTEXT), _in(AST_MAP)))
*/
Z3_string Z3_API Z3_ast_map_to_string(Z3_context c, Z3_ast_map m);
/*@}*/
/*@}*/
#ifdef __cplusplus
}
#endif // __cplusplus
#endif
|
