array< T > Class Template Reference

#include <z3++.h>

Public Member Functions
	array (unsigned sz)
template<typename T2>
	array (ast_vector_tpl< T2 > const &v)
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 517 of file z3++.h.

Constructor & Destructor Documentation

array() [1/2]

template<typename T>

array ( unsigned sz )

inline

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

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

array() [2/2]

template<typename T>

template<typename T2>

array

(

ast_vector_tpl< T2 > const &

v

)

Definition at line 2425 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];
        }
    }

Member Function Documentation

operator[]() [1/2]

template<typename T>

T & operator[] ( int i )

inline

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

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

operator[]() [2/2]

template<typename T>

T const & operator[] ( int i ) const

inline

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

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

ptr() [1/2]

template<typename T>

T * ptr ( )

inline

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

{ return m_array.get(); }

ptr() [2/2]

template<typename T>

T const * ptr ( ) const

inline

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

{ return m_array.get(); }

Referenced by constructors::add(), context::array_sort(), goal::as_expr(), expr::atleast, expr::atmost, context::bv_val(), optimize::check(), solver::check(), solver::check(), expr::concat, user_propagator_base::conflict(), user_propagator_base::conflict(), constructor_list::constructor_list(), context::datatype(), context::datatype(), context::datatype_sort(), context::datatypes(), expr::distinct, context::enumeration_sort(), z3::exists(), z3::forall(), context::function(), context::function(), z3::lambda(), expr::mk_and, expr::mk_or, func_decl::operator()(), func_decl::operator()(), tactic::par_or, context::parse_file(), context::parse_string(), expr::pbeq, expr::pbge, expr::pble, user_propagator_base::propagate(), user_propagator_base::propagate(), constructors::query(), fixedpoint::query(), z3::re_intersect(), context::recdef(), context::recfun(), context::recfun(), z3::select(), z3::store(), expr::substitute(), expr::substitute(), expr::substitute(), expr::sum, solver::to_smt2(), fixedpoint::to_string(), solver::trail(), context::tuple_sort(), expr::update(), and context::user_propagate_function().

resize()

template<typename T>

void resize ( unsigned sz )

inline

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

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

Referenced by solver::trail().

size()

template<typename T>

unsigned size ( ) const

inline

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

{ return m_size; }

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