ast_vector_tpl< T > Class Template Reference

#include <z3++.h>

Inheritance diagram for ast_vector_tpl< T >:

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

Detailed Description

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

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

Constructor & Destructor Documentation

ast_vector_tpl() [1/4]

template<typename T>

ast_vector_tpl ( context & c )

inline

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

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

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

ast_vector_tpl() [2/4]

template<typename T>

ast_vector_tpl ( context & c, Z3_ast_vector v )

inline

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

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

ast_vector_tpl() [3/4]

template<typename T>

ast_vector_tpl ( ast_vector_tpl< T > const & s )

inline

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

:object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }

ast_vector_tpl() [4/4]

template<typename T>

ast_vector_tpl ( context & c, ast_vector_tpl< T > const & src )

inline

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

: object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }

~ast_vector_tpl()

template<typename T>

~ast_vector_tpl ( )

inlineoverride

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

{ Z3_ast_vector_dec_ref(ctx(), m_vector); }

Member Function Documentation

back()

template<typename T>

T back ( ) const

inline

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

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

begin()

template<typename T>

iterator begin ( ) const

inlinenoexcept

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

{ return iterator(this, 0); }

Referenced by optimize::add(), and optimize::optimize().

empty()

template<typename T>

bool empty ( ) const

inline

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

{ return size() == 0; }

end()

template<typename T>

iterator end ( ) const

inline

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

{ return iterator(this, size()); }

Referenced by optimize::add(), and optimize::optimize().

operator Z3_ast_vector()

template<typename T>

operator Z3_ast_vector ( ) const

inline

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

{ return m_vector; }

operator=()

template<typename T>

ast_vector_tpl & operator= ( ast_vector_tpl< T > const & s )

inline

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

                                                           {
            Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
            Z3_ast_vector_dec_ref(ctx(), m_vector);
            object::operator=(s);
            m_vector = s.m_vector;
            return *this;
        }

operator[]()

template<typename T>

T operator[] ( unsigned i ) const

inline

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

{ Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }

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

pop_back()

template<typename T>

void pop_back ( )

inline

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

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

push_back()

template<typename T>

void push_back ( T const & e )

inline

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

{ Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }

Referenced by func_decl::accessors(), expr::args(), sort::constructors(), context::datatypes(), context::enumeration_sort(), constructors::query(), sort::recognizers(), solver::solve_for(), and context::tuple_sort().

resize()

template<typename T>

void resize ( unsigned sz )

inline

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

{ Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }

Referenced by ast_vector_tpl< ast >::pop_back(), and constructors::query().

set()

template<typename T>

ast_vector_tpl & set ( unsigned idx, ast & a )

inline

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

                                                  {
            Z3_ast_vector_set(ctx(), m_vector, idx, a);
            return *this;
        }

size()

template<typename T>

unsigned size ( ) const

inline

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

{ return Z3_ast_vector_size(ctx(), m_vector); }

Referenced by goal::add(), solver::add(), expr::atleast, expr::atmost, ast_vector_tpl< ast >::back(), optimize::check(), solver::check(), user_propagator_base::conflict(), ast_vector_tpl< ast >::empty(), ast_vector_tpl< ast >::end(), context::function(), func_decl::operator()(), context::parse_file(), context::parse_string(), expr::pbeq, expr::pbge, expr::pble, ast_vector_tpl< ast >::pop_back(), user_propagator_base::propagate(), z3::re_intersect(), solver::solve_for(), expr::substitute(), expr::substitute(), expr::substitute(), and solver::trail().

to_string()

template<typename T>

std::string to_string ( ) const

inline

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

{ return std::string(Z3_ast_vector_to_string(ctx(), m_vector)); }

Friends And Related Symbol Documentation

operator<<

template<typename T>

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

friend

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

{ out << Z3_ast_vector_to_string(v.ctx(), v); return out; }