Z3
z3_ast_containers.h File Reference

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...
 

Function Documentation

◆ 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.

Referenced by AstMap::__contains__().

◆ 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.

Referenced by AstMap::__del__().

◆ 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.

Referenced by AstMap::erase().

◆ 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.

The procedure invokes the error handler if k is not in the map.

Referenced by AstMap::__getitem__().

◆ 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_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.

Referenced by AstMap::__setitem__().

◆ 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.

Referenced by AstMap::keys().

◆ 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.

Referenced by AstMap::reset().

◆ 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.

Referenced by AstMap::__len__().

◆ 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.

Referenced by AstMap::__repr__().

◆ 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.

Referenced by AstVector::__del__(), ast_vector_tpl< T >::operator=(), and ast_vector_tpl< T >::~ast_vector_tpl().

◆ 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.

Precondition
i < Z3_ast_vector_size(c, v)

Referenced by AstVector::__getitem__(), and ast_vector_tpl< T >::operator[]().

◆ 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.

Referenced by ast_vector_tpl< T >::ast_vector_tpl(), and ast_vector_tpl< T >::operator=().

◆ 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.

Referenced by AstVector::push(), and ast_vector_tpl< T >::push_back().

◆ 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.

Referenced by AstVector::resize(), and ast_vector_tpl< T >::resize().

◆ 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.

Precondition
i < Z3_ast_vector_size(c, v)

Referenced by AstVector::__setitem__(), ast_vector_tpl< T >::iterator::set(), and ast_vector_tpl< T >::set().

◆ 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.

Referenced by AstVector::__len__(), and ast_vector_tpl< T >::size().

◆ 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.

Referenced by AstVector::sexpr().

◆ 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.

Referenced by AstVector::translate().

◆ Z3_mk_ast_map()

Z3_ast_map Z3_API Z3_mk_ast_map ( Z3_context  c)

Return an empty mapping from AST to AST.

Remarks
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.

◆ Z3_mk_ast_vector()

Z3_ast_vector Z3_API Z3_mk_ast_vector ( Z3_context  c)

Return an empty AST vector.

Remarks
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.

Referenced by ast_vector_tpl< T >::ast_vector_tpl().