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) |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
void | check_error () const |
Friends | |
std::ostream & | operator<< (std::ostream &out, ast_vector_tpl const &v) |
Additional Inherited Members | |
![]() | |
context * | m_ctx |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 1031 of file z3++.h.
|
inline |
Definition at line 1032 of file z3++.h.
Referenced by context::enumeration_sort().
|
inline |
|
inline |
Definition at line 1030 of file z3++.h.
Referenced by array< T >::array(), solver::check(), z3::distinct(), context::function(), func_decl::operator()(), and expr::substitute().
|
friend |