Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
array< T > Class Template Reference

Public Member Functions

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


Constructor & Destructor Documentation

array ( unsigned  sz) [inline]

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

:m_size(sz) { m_array = new T[sz]; }
array ( ast_vector_tpl< T2 > const &  v)

Definition at line 1040 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 ( ) [inline]

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

{ delete[] m_array; }

Member Function Documentation

T& operator[] ( int  i) [inline]

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

{ assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
T const& operator[] ( int  i) const [inline]

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

{ assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
T const* ptr ( ) const [inline]
T* ptr ( ) [inline]

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

{ return m_array; }
unsigned size ( ) const [inline]

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

Referenced by z3::distinct(), z3::exists(), and z3::forall().

{ return m_size; }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines