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 () | |
operator Z3_ast_vector () const | |
unsigned | size () const |
T | operator[] (int 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) |
Friends | |
std::ostream & | operator<< (std::ostream &out, ast_vector_tpl const &v) |
ast_vector_tpl | ( | context & | c | ) | [inline] |
Definition at line 1016 of file z3++.h.
:object(c) { init(Z3_mk_ast_vector(c)); }
ast_vector_tpl | ( | context & | c, |
Z3_ast_vector | v | ||
) | [inline] |
ast_vector_tpl | ( | ast_vector_tpl< T > const & | s | ) | [inline] |
Definition at line 1018 of file z3++.h.
:object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
~ast_vector_tpl | ( | ) | [inline] |
Definition at line 1019 of file z3++.h.
{ Z3_ast_vector_dec_ref(ctx(), m_vector); }
T back | ( | ) | const [inline] |
Definition at line 1025 of file z3++.h.
{ return operator[](size() - 1); }
operator Z3_ast_vector | ( | ) | const [inline] |
ast_vector_tpl& operator= | ( | ast_vector_tpl< T > const & | s | ) | [inline] |
Definition at line 1028 of file z3++.h.
{ Z3_ast_vector_inc_ref(s.ctx(), s.m_vector); Z3_ast_vector_dec_ref(ctx(), m_vector); m_ctx = s.m_ctx; m_vector = s.m_vector; return *this; }
T operator[] | ( | int | i | ) | const [inline] |
Definition at line 1022 of file z3++.h.
Referenced by ast_vector_tpl< T >::back().
{ assert(0 <= i); Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
void pop_back | ( | ) | [inline] |
void push_back | ( | T const & | e | ) | [inline] |
Definition at line 1023 of file z3++.h.
Referenced by context::enumeration_sort().
{ Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
void resize | ( | unsigned | sz | ) | [inline] |
Definition at line 1024 of file z3++.h.
Referenced by ast_vector_tpl< T >::pop_back().
{ Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
unsigned size | ( | ) | const [inline] |
Definition at line 1021 of file z3++.h.
Referenced by array< T >::array(), ast_vector_tpl< T >::back(), solver::check(), z3::distinct(), ast_vector_tpl< T >::empty(), context::function(), func_decl::operator()(), ast_vector_tpl< T >::pop_back(), and expr::substitute().
{ return Z3_ast_vector_size(ctx(), m_vector); }
std::ostream& operator<< | ( | std::ostream & | out, |
ast_vector_tpl< T > const & | v | ||
) | [friend] |
Definition at line 1035 of file z3++.h.
{ out << Z3_ast_vector_to_string(v.ctx(), v); return out; }