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 ast_vector_tpl< T >::ast_vector_tpl(), and 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().