Z3 |

z3_ast_containers.h
Go to the documentation of this file.
1/*++
2 Copyright (c) 2015 Microsoft Corporation
3
4 Module Name:
5
6 z3_ast_containers.h
7
8 Abstract:
9
10 AST Containers
11
12 Author:
13
14 Christoph M. Wintersteiger (cwinter) 2015-12-03
15
16 Notes:
17
18--*/
19#pragma once
20
21#ifdef __cplusplus
22 extern "C" {
23#endif // __cplusplus
24
27
37 Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c);
38
43 void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v);
44
49 void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v);
50
55 unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v);
56
63 Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i);
64
71 void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a);
72
77 void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n);
78
83 void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a);
84
89 Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t);
90
95 Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v);
96
108 Z3_ast_map Z3_API Z3_mk_ast_map(Z3_context c);
109
114 void Z3_API Z3_ast_map_inc_ref(Z3_context c, Z3_ast_map m);
115
120 void Z3_API Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m);
121
126 bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k);
127
134 Z3_ast Z3_API Z3_ast_map_find(Z3_context c, Z3_ast_map m, Z3_ast k);
135
140 void Z3_API Z3_ast_map_insert(Z3_context c, Z3_ast_map m, Z3_ast k, Z3_ast v);
141
146 void Z3_API Z3_ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k);
147
152 void Z3_API Z3_ast_map_reset(Z3_context c, Z3_ast_map m);
153
158 unsigned Z3_API Z3_ast_map_size(Z3_context c, Z3_ast_map m);
159
164 Z3_ast_vector Z3_API Z3_ast_map_keys(Z3_context c, Z3_ast_map m);
165
170 Z3_string Z3_API Z3_ast_map_to_string(Z3_context c, Z3_ast_map m);
173
174#ifdef __cplusplus
175}
176#endif // __cplusplus
177
Z3_string
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:84
Z3_ast_map_inc_ref
void Z3_API Z3_ast_map_inc_ref(Z3_context c, Z3_ast_map m)
Increment the reference counter of the given AST map.
Z3_ast_map_find
Z3_ast Z3_API Z3_ast_map_find(Z3_context c, Z3_ast_map m, Z3_ast k)
Return the value associated with the key k.
Z3_ast_map_to_string
Z3_string Z3_API Z3_ast_map_to_string(Z3_context c, Z3_ast_map m)
Convert the given map into a string.
Z3_ast_vector_set
void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a)
Update position i of the AST vector v with the AST a.
Z3_ast_map_contains
bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k)
Return true if the map m contains the AST key k.
Z3_ast_map_keys
Z3_ast_vector Z3_API Z3_ast_map_keys(Z3_context c, Z3_ast_map m)
Return the keys stored in the given map.
Z3_ast_vector_translate
Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t)
Translate the AST vector v from context s into an AST vector in context t.
Z3_ast_vector_to_string
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)
Convert AST vector into a string.
Z3_ast_vector_resize
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.
Z3_ast_map_size
unsigned Z3_API Z3_ast_map_size(Z3_context c, Z3_ast_map m)
Return the size of the given map.
Z3_ast_vector_dec_ref
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
Z3_ast_map_dec_ref
void Z3_API Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m)
Decrement the reference counter of the given AST map.
Z3_ast_vector_size
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.
Z3_ast_vector_inc_ref
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v)
Increment the reference counter of the given AST vector.
Z3_mk_ast_vector
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.
Z3_ast_map_erase
void Z3_API Z3_ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k)
Erase a key from the map.
Z3_ast_vector_push
void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.
Z3_mk_ast_map
Z3_ast_map Z3_API Z3_mk_ast_map(Z3_context c)
Return an empty mapping from AST to AST.
Z3_ast_vector_get
Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i)
Return the AST at position i in the AST vector v.
Z3_ast_map_insert
void Z3_API Z3_ast_map_insert(Z3_context c, Z3_ast_map m, Z3_ast k, Z3_ast v)
Store/Replace a new key, value pair in the given map.
Z3_ast_map_reset
void Z3_API Z3_ast_map_reset(Z3_context c, Z3_ast_map m)
Remove all keys from the given map.