Go to the source code of this file.
Functions | |
AST vectors | |
Z3_ast_vector Z3_API | Z3_mk_ast_vector (Z3_context c) |
Return an empty AST vector. More... | |
void Z3_API | Z3_ast_vector_inc_ref (Z3_context c, Z3_ast_vector v) |
Increment the reference counter of the given AST vector. More... | |
void Z3_API | Z3_ast_vector_dec_ref (Z3_context c, Z3_ast_vector v) |
Decrement the reference counter of the given AST vector. More... | |
unsigned Z3_API | Z3_ast_vector_size (Z3_context c, Z3_ast_vector v) |
Return the size of the given AST vector. More... | |
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 . More... | |
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 . More... | |
void Z3_API | Z3_ast_vector_resize (Z3_context c, Z3_ast_vector v, unsigned n) |
Resize the AST vector v . More... | |
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. More... | |
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 . More... | |
Z3_string Z3_API | Z3_ast_vector_to_string (Z3_context c, Z3_ast_vector v) |
Convert AST vector into a string. More... | |
AST maps | |
Z3_ast_map Z3_API | Z3_mk_ast_map (Z3_context c) |
Return an empty mapping from AST to AST. More... | |
void Z3_API | Z3_ast_map_inc_ref (Z3_context c, Z3_ast_map m) |
Increment the reference counter of the given AST map. More... | |
void Z3_API | Z3_ast_map_dec_ref (Z3_context c, Z3_ast_map m) |
Decrement the reference counter of the given AST map. More... | |
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 . More... | |
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 . More... | |
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. More... | |
void Z3_API | Z3_ast_map_erase (Z3_context c, Z3_ast_map m, Z3_ast k) |
Erase a key from the map. More... | |
void Z3_API | Z3_ast_map_reset (Z3_context c, Z3_ast_map m) |
Remove all keys from the given map. More... | |
unsigned Z3_API | Z3_ast_map_size (Z3_context c, Z3_ast_map m) |
Return the size of the given map. More... | |
Z3_ast_vector Z3_API | Z3_ast_map_keys (Z3_context c, Z3_ast_map m) |
Return the keys stored in the given map. More... | |
Z3_string Z3_API | Z3_ast_map_to_string (Z3_context c, Z3_ast_map m) |
Convert the given map into a string. More... | |
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
.
Referenced by AstMap::__contains__().
void Z3_API Z3_ast_map_dec_ref | ( | Z3_context | c, |
Z3_ast_map | m | ||
) |
Decrement the reference counter of the given AST map.
Referenced by AstMap::__del__().
void Z3_API Z3_ast_map_erase | ( | Z3_context | c, |
Z3_ast_map | m, | ||
Z3_ast | k | ||
) |
Erase a key from the map.
Referenced by AstMap::erase().
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
.
The procedure invokes the error handler if k
is not in the map.
Referenced by AstMap::__getitem__().
void Z3_API Z3_ast_map_inc_ref | ( | Z3_context | c, |
Z3_ast_map | m | ||
) |
Increment the reference counter of the given AST map.
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.
Referenced by AstMap::__setitem__().
Z3_ast_vector Z3_API Z3_ast_map_keys | ( | Z3_context | c, |
Z3_ast_map | m | ||
) |
Return the keys stored in the given map.
Referenced by AstMap::keys().
void Z3_API Z3_ast_map_reset | ( | Z3_context | c, |
Z3_ast_map | m | ||
) |
Remove all keys from the given map.
Referenced by AstMap::reset().
unsigned Z3_API Z3_ast_map_size | ( | Z3_context | c, |
Z3_ast_map | m | ||
) |
Return the size of the given map.
Referenced by AstMap::__len__().
Z3_string Z3_API Z3_ast_map_to_string | ( | Z3_context | c, |
Z3_ast_map | m | ||
) |
Convert the given map into a string.
Referenced by AstMap::__repr__().
void Z3_API Z3_ast_vector_dec_ref | ( | Z3_context | c, |
Z3_ast_vector | v | ||
) |
Decrement the reference counter of the given AST vector.
Referenced by AstVector::__del__(), ast_vector_tpl< T >::operator=(), and ast_vector_tpl< T >::~ast_vector_tpl().
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
.
Referenced by AstVector::__getitem__(), and ast_vector_tpl< T >::operator[]().
void Z3_API Z3_ast_vector_inc_ref | ( | Z3_context | c, |
Z3_ast_vector | v | ||
) |
Increment the reference counter of the given AST vector.
Referenced by ast_vector_tpl< T >::ast_vector_tpl(), and ast_vector_tpl< T >::operator=().
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.
Referenced by AstVector::push(), and ast_vector_tpl< T >::push_back().
void Z3_API Z3_ast_vector_resize | ( | Z3_context | c, |
Z3_ast_vector | v, | ||
unsigned | n | ||
) |
Resize the AST vector v
.
Referenced by AstVector::resize(), and ast_vector_tpl< T >::resize().
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
.
Referenced by AstVector::__setitem__(), ast_vector_tpl< T >::iterator::set(), and ast_vector_tpl< T >::set().
unsigned Z3_API Z3_ast_vector_size | ( | Z3_context | c, |
Z3_ast_vector | v | ||
) |
Return the size of the given AST vector.
Referenced by AstVector::__len__(), and ast_vector_tpl< T >::size().
Z3_string Z3_API Z3_ast_vector_to_string | ( | Z3_context | c, |
Z3_ast_vector | v | ||
) |
Convert AST vector into a string.
Referenced by AstVector::sexpr().
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
.
Referenced by AstVector::translate().
Z3_ast_map Z3_API Z3_mk_ast_map | ( | Z3_context | c | ) |
Return an empty mapping from AST to AST.
Z3_ast_vector Z3_API Z3_mk_ast_vector | ( | Z3_context | c | ) |
Return an empty AST vector.
Referenced by ast_vector_tpl< T >::ast_vector_tpl().