Z3 |

Public Member Functions
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 400 of file z3++.h.

## Constructor & Destructor Documentation

## ◆ array() [1/2]

array | ( | unsigned | sz | ) |
| inline

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

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

## ◆ array() [2/2]

array | ( | ast_vector_tpl< T2 > const & | v | ) |

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

2181 :m_array(new T[v.size()]), m_size(v.size()) {
2182 for (unsigned i = 0; i < m_size; i++) {
2183 m_array[i] = v[i];
2184 }
2185 }

## Member Function Documentation

## ◆ operator[]() [1/2]

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

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

411{ 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 412 of file z3++.h.

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

## ◆ ptr() [1/2]

T * ptr | ( |  | ) |
| inline

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

414{ return m_array.get(); }

## ◆ ptr() [2/2]

T const * ptr | ( |  | ) | const
| inline

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

413{ return m_array.get(); }

Referenced by context::array_sort(), goal::as_expr(), context::bv_val(), optimize::check(), solver::check(), context::enumeration_sort(), z3::exists(), z3::forall(), context::function(), z3::lambda(), func_decl::operator()(), context::parse_file(), context::parse_string(), fixedpoint::query(), z3::re_intersect(), context::recdef(), context::recfun(), z3::select(), z3::store(), expr::substitute(), solver::to_smt2(), fixedpoint::to_string(), solver::trail(), and context::tuple_sort().

## ◆ resize()

void resize | ( | unsigned | sz | ) |
| inline

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

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

Referenced by solver::trail().

## ◆ size()

unsigned size | ( |  | ) | const
| inline

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

410{ return m_size; }

Referenced by ParamDescrsRef::__len__(), Goal::__len__(), context::array_sort(), BitVecNumRef::as_signed_long(), z3::exists(), z3::forall(), z3::lambda(), fixedpoint::query(), z3::re_intersect(), context::recdef(), z3::select(), z3::store(), BitVecSortRef::subsort(), solver::to_smt2(), and fixedpoint::to_string().