Data Structures | |
class | iterator |
Public Member Functions | |
ast_vector_tpl (context &c) | |
ast_vector_tpl (context &c, Z3_ast_vector v) | |
ast_vector_tpl (ast_vector_tpl const &s) | |
ast_vector_tpl (context &c, ast_vector_tpl const &src) | |
~ast_vector_tpl () override | |
operator Z3_ast_vector () const | |
unsigned | size () const |
T | operator[] (unsigned i) const |
void | push_back (T const &e) |
void | resize (unsigned sz) |
T | back () const |
void | pop_back () |
bool | empty () const |
ast_vector_tpl & | operator= (ast_vector_tpl const &s) |
ast_vector_tpl & | set (unsigned idx, ast &a) |
iterator | begin () const noexcept |
iterator | end () const |
std::string | to_string () const |
Public Member Functions inherited from object | |
object (context &c) | |
virtual | ~object ()=default |
context & | ctx () const |
Z3_error_code | check_error () const |
Friends | |
std::ostream & | operator<< (std::ostream &out, ast_vector_tpl const &v) |
Additional Inherited Members | |
Protected Attributes inherited from object | |
context * | m_ctx |
|
inline |
|
inline |
|
inline |
|
inline |
|
inlineoverride |
|
inlinenoexcept |
Definition at line 647 of file z3++.h.
Referenced by optimize::add(), and optimize::optimize().
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 599 of file z3++.h.
Referenced by ast_vector_tpl< T >::back().
|
inline |
Definition at line 600 of file z3++.h.
Referenced by func_decl::accessors(), expr::args(), sort::constructors(), context::datatypes(), context::enumeration_sort(), constructors::query(), sort::recognizers(), and context::tuple_sort().
|
inline |
Definition at line 601 of file z3++.h.
Referenced by ast_vector_tpl< T >::pop_back(), and constructors::query().
|
inline |
|
inline |
Definition at line 598 of file z3++.h.
Referenced by ParamDescrsRef::__len__(), Goal::__len__(), solver::add(), goal::add(), BitVecNumRef::as_signed_long(), ast_vector_tpl< T >::back(), optimize::check(), solver::check(), user_propagator_base::conflict(), ast_vector_tpl< T >::empty(), ast_vector_tpl< T >::end(), context::function(), func_decl::operator()(), context::parse_file(), context::parse_string(), ast_vector_tpl< T >::pop_back(), user_propagator_base::propagate(), z3::re_intersect(), BitVecSortRef::subsort(), expr::substitute(), and solver::trail().
|
inline |
|
friend |