array< T > Class Template Reference

Public Member Functions
	array (unsigned sz)
template<typename T2 >
	array (ast_vector_tpl< T2 > const &v)
	~array ()
void	resize (unsigned sz)
unsigned	size () const
T &	operator[] (int i)
T const &	operator[] (int i) const
T const *	ptr () const
T *	ptr ()

Detailed Description

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

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

Constructor & Destructor Documentation

array() [1/2]

array ( unsigned  sz )

inline

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

:m_size(sz) { m_array = new T[sz]; }

array() [2/2]

array

(

ast_vector_tpl< T2 > const &

v

)

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

                                                {
        m_array = new T[v.size()];
        m_size  = v.size();
        for (unsigned i = 0; i < m_size; i++) {
            m_array[i] = v[i];
        }
    }

~array()

~array ( )

inline

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

{ delete[] m_array; }

Member Function Documentation

operator[]() [1/2]

T& operator[] ( int  i )

inline

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

{ assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }

operator[]() [2/2]

T const& operator[] ( int  i ) const

inline

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

{ assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }

ptr() [1/2]

T const* ptr ( ) const

inline

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

Referenced by context::array_sort(), goal::as_expr(), z3::atleast(), z3::atmost(), context::bv_val(), solver::check(), optimize::check(), z3::concat(), z3::distinct(), context::enumeration_sort(), z3::exists(), z3::forall(), context::function(), z3::lambda(), z3::mk_and(), z3::mk_or(), func_decl::operator()(), z3::par_or(), context::parse_file(), context::parse_string(), z3::pbeq(), z3::pbge(), z3::pble(), fixedpoint::query(), z3::re_intersect(), context::recdef(), context::recfun(), z3::select(), z3::store(), z3::sum(), solver::to_smt2(), fixedpoint::to_string(), solver::trail(), and context::tuple_sort().

{ return m_array; }

ptr() [2/2]

T* ptr ( )

inline

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

{ return m_array; }

resize()

void resize ( unsigned  sz )

inline

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

Referenced by solver::trail().

{ delete[] m_array; m_size = sz; m_array = new T[sz]; }

size()

unsigned size ( ) const

inline

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

Referenced by context::array_sort(), z3::atleast(), z3::atmost(), z3::concat(), z3::distinct(), z3::exists(), z3::forall(), z3::lambda(), z3::mk_and(), z3::mk_or(), z3::pbeq(), z3::pbge(), z3::pble(), fixedpoint::query(), z3::re_intersect(), context::recdef(), z3::select(), z3::store(), z3::sum(), solver::to_smt2(), and fixedpoint::to_string().

{ return m_size; }