Z3
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 254 of file z3++.h.

Constructor & Destructor Documentation

array ( unsigned  sz)
inline

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

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

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

1049  {
1050  m_array = new T[v.size()];
1051  m_size = v.size();
1052  for (unsigned i = 0; i < m_size; i++) {
1053  m_array[i] = v[i];
1054  }
1055  }
~array ( )
inline

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

263 { delete[] m_array; }

Member Function Documentation

T& operator[] ( int  i)
inline

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

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

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

266 { 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 268 of file z3++.h.

268 { return m_array; }
unsigned size ( ) const
inline

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

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

264 { return m_size; }