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
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)

---

Detailed Description

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

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

---

Constructor & Destructor Documentation

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]

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

:object(c) { init(v); }

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); }

---

Member Function Documentation

T back

(

)

const [inline]

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

{ return operator[](size() - 1); }

bool empty

(

)

const [inline]

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

{ return size() == 0; }

operator Z3_ast_vector

(

)

const [inline]

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

{ return m_vector; }

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]

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

{ assert(size() > 0); resize(size() - 1); }

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); }

---

Friends And Related Function Documentation

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; }