Z3
Public Member Functions | Friends
ast_vector_tpl< T > Class Template Reference
+ Inheritance diagram for ast_vector_tpl< T >:

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
 
operator[] (int i) const
 
void push_back (T const &e)
 
void resize (unsigned sz)
 
back () const
 
void pop_back ()
 
bool empty () const
 
ast_vector_tploperator= (ast_vector_tpl const &s)
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Friends

std::ostream & operator<< (std::ostream &out, ast_vector_tpl const &v)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

template<typename T>
class z3::ast_vector_tpl< T >

Definition at line 66 of file z3++.h.

Constructor & Destructor Documentation

ast_vector_tpl ( context c)
inline

Definition at line 1019 of file z3++.h.

1019 :object(c) { init(Z3_mk_ast_vector(c)); }
object(context &c)
Definition: z3++.h:270
Z3_ast_vector Z3_API Z3_mk_ast_vector(__in Z3_context c)
Return an empty AST vector.
ast_vector_tpl ( context c,
Z3_ast_vector  v 
)
inline

Definition at line 1020 of file z3++.h.

1020 :object(c) { init(v); }
object(context &c)
Definition: z3++.h:270
ast_vector_tpl ( ast_vector_tpl< T > const &  s)
inline

Definition at line 1021 of file z3++.h.

1021 :object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
context & ctx() const
Definition: z3++.h:272
object(context &c)
Definition: z3++.h:270
void Z3_API Z3_ast_vector_inc_ref(__in Z3_context c, __in Z3_ast_vector v)
Increment the reference counter of the given AST vector.
~ast_vector_tpl ( )
inline

Definition at line 1022 of file z3++.h.

1022 { Z3_ast_vector_dec_ref(ctx(), m_vector); }
context & ctx() const
Definition: z3++.h:272
void Z3_API Z3_ast_vector_dec_ref(__in Z3_context c, __in Z3_ast_vector v)
Decrement the reference counter of the given AST vector.

Member Function Documentation

T back ( ) const
inline

Definition at line 1028 of file z3++.h.

1028 { return operator[](size() - 1); }
unsigned size() const
Definition: z3++.h:1024
T operator[](int i) const
Definition: z3++.h:1025
bool empty ( ) const
inline

Definition at line 1030 of file z3++.h.

1030 { return size() == 0; }
unsigned size() const
Definition: z3++.h:1024
operator Z3_ast_vector ( ) const
inline

Definition at line 1023 of file z3++.h.

1023 { return m_vector; }
ast_vector_tpl& operator= ( ast_vector_tpl< T > const &  s)
inline

Definition at line 1031 of file z3++.h.

1031  {
1032  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
1033  Z3_ast_vector_dec_ref(ctx(), m_vector);
1034  m_ctx = s.m_ctx;
1035  m_vector = s.m_vector;
1036  return *this;
1037  }
context & ctx() const
Definition: z3++.h:272
void Z3_API Z3_ast_vector_inc_ref(__in Z3_context c, __in Z3_ast_vector v)
Increment the reference counter of the given AST vector.
void Z3_API Z3_ast_vector_dec_ref(__in Z3_context c, __in Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
context * m_ctx
Definition: z3++.h:268
T operator[] ( int  i) const
inline

Definition at line 1025 of file z3++.h.

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

1025 { assert(0 <= i); Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_ast Z3_API Z3_ast_vector_get(__in Z3_context c, __in Z3_ast_vector v, __in unsigned i)
Return the AST at position i in the AST vector v.
void pop_back ( )
inline

Definition at line 1029 of file z3++.h.

1029 { assert(size() > 0); resize(size() - 1); }
void resize(unsigned sz)
Definition: z3++.h:1027
unsigned size() const
Definition: z3++.h:1024
void push_back ( T const &  e)
inline

Definition at line 1026 of file z3++.h.

Referenced by context::enumeration_sort().

1026 { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
context & ctx() const
Definition: z3++.h:272
void Z3_API Z3_ast_vector_push(__in Z3_context c, __in Z3_ast_vector v, __in Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.
void check_error() const
Definition: z3++.h:273
void resize ( unsigned  sz)
inline

Definition at line 1027 of file z3++.h.

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

1027 { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
void Z3_API Z3_ast_vector_resize(__in Z3_context c, __in Z3_ast_vector v, __in unsigned n)
Resize the AST vector v.
unsigned size ( ) const
inline

Definition at line 1024 of file z3++.h.

Referenced by 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().

1024 { return Z3_ast_vector_size(ctx(), m_vector); }
context & ctx() const
Definition: z3++.h:272
unsigned Z3_API Z3_ast_vector_size(__in Z3_context c, __in Z3_ast_vector v)
Return the size of the given AST vector.

Friends And Related Function Documentation

std::ostream& operator<< ( std::ostream &  out,
ast_vector_tpl< T > const &  v 
)
friend

Definition at line 1038 of file z3++.h.

1038 { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
Z3_string Z3_API Z3_ast_vector_to_string(__in Z3_context c, __in Z3_ast_vector v)
Convert AST vector into a string.