Z3 |

Data Structures | Public Member Functions | Friends
ast_vector_tpl< T > Class Template Reference

`#include <z3++.h>`

Inheritance diagram for ast_vector_tpl< T >:

## Data Structures
class | iterator

## Public Member Functions
| ast_vector_tpl (context &c)
| ast_vector_tpl (context &c, Z3_ast_vector v)
| ast_vector_tpl (ast_vector_tpl const &s)
| ast_vector_tpl (context &c, ast_vector_tpl const &src)
| ~ast_vector_tpl ()
| operator Z3_ast_vector () const
unsigned | size () const
T | operator[] (int i) const
void | push_back (T const &e)
void | resize (unsigned sz)
T | back () const
void | pop_back ()
bool | empty () const
ast_vector_tpl & | operator= (ast_vector_tpl const &s)
ast_vector_tpl & | set (unsigned idx, ast &a)
iterator | begin () const noexcept
iterator | end () const
Public Member Functions inherited from object
| object (context &c)
context & | ctx () const
Z3_error_code | check_error () const

## Friends
std::ostream & | operator<< (std::ostream &out, ast_vector_tpl const &v)

## Additional Inherited Members
Protected Attributes inherited from object
context * | m_ctx

## Detailed Description

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

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

## Constructor & Destructor Documentation

## ◆ ast_vector_tpl() [1/4]

ast_vector_tpl | ( | context & | c | ) |
| inline

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

547:object(c) { init(Z3_mk_ast_vector(c)); }
z3::object::object
object(context &c)
Definition: z3++.h:421
Z3_mk_ast_vector
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.

## ◆ ast_vector_tpl() [2/4]

ast_vector_tpl | ( | context & | c,
|  | Z3_ast_vector | v
| ) |  |
| inline

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

548:object(c) { init(v); }

## ◆ ast_vector_tpl() [3/4]

ast_vector_tpl | ( | ast_vector_tpl< T > const & | s | ) |
| inline

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

549:object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_ast_vector_inc_ref
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v)
Increment the reference counter of the given AST vector.

## ◆ ast_vector_tpl() [4/4]

ast_vector_tpl | ( | context & | c,
|  | ast_vector_tpl< T > const & | src
| ) |  |
| inline

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

550: object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
Z3_ast_vector_translate
Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t)
Translate the AST vector v from context s into an AST vector in context t.

## ◆ ~ast_vector_tpl()

~ast_vector_tpl | ( |  | ) |
| inline

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

552{ Z3_ast_vector_dec_ref(ctx(), m_vector); }
Z3_ast_vector_dec_ref
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)
Decrement the reference counter of the given AST vector.

## Member Function Documentation

## ◆ back()

T back | ( |  | ) | const
| inline

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

558{ return operator[](size() - 1); }
z3::ast_vector_tpl::size
unsigned size() const
Definition: z3++.h:554
z3::ast_vector_tpl::operator[]
T operator[](int i) const
Definition: z3++.h:555

## ◆ begin()

iterator begin | ( |  | ) | const
| inline noexcept

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

603{ return iterator(this, 0); }

Referenced by optimize::add(), and optimize::optimize().

## ◆ empty()

bool empty | ( |  | ) | const
| inline

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

560{ return size() == 0; }

## ◆ end()

iterator end | ( |  | ) | const
| inline

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

604{ return iterator(this, size()); }

Referenced by optimize::add(), and optimize::optimize().

## ◆ operator Z3_ast_vector()

operator Z3_ast_vector | ( |  | ) | const
| inline

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

553{ return m_vector; }

## ◆ operator=()

ast_vector_tpl & operator= | ( | ast_vector_tpl< T > const & | s | ) |
| inline

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

561 {
562 Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
563 Z3_ast_vector_dec_ref(ctx(), m_vector);
564 object::operator=(s);
565 m_vector = s.m_vector;
566 return *this;
567 }

## ◆ operator[]()

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

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

555{ assert(0 <= i); Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_ast_vector_get
Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i)
Return the AST at position i in the AST vector v.

Referenced by ast_vector_tpl< T >::back().

## ◆ pop_back()

void pop_back | ( |  | ) |
| inline

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

559{ assert(size() > 0); resize(size() - 1); }
z3::ast_vector_tpl::resize
void resize(unsigned sz)
Definition: z3++.h:557

## ◆ push_back()

void push_back | ( | T const & | e | ) |
| inline

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

556{ Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
Z3_ast_vector_push
void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.

Referenced by context::enumeration_sort(), and context::tuple_sort().

## ◆ resize()

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

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

557{ Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
Z3_ast_vector_resize
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.

Referenced by ast_vector_tpl< T >::pop_back().

## ◆ set()

ast_vector_tpl & set | ( | unsigned | idx,
|  | ast & | a
| ) |  |
| inline

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

568 {
569 Z3_ast_vector_set(ctx(), m_vector, idx, a);
570 return *this;
571 }
Z3_ast_vector_set
void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a)
Update position i of the AST vector v with the AST a.

## ◆ size()

unsigned size | ( |  | ) | const
| inline

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

554{ return Z3_ast_vector_size(ctx(), m_vector); }
Z3_ast_vector_size
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.

Referenced by ParamDescrsRef::__len__(), Goal::__len__(), solver::add(), goal::add(), BitVecNumRef::as_signed_long(), ast_vector_tpl< T >::back(), optimize::check(), solver::check(), ast_vector_tpl< T >::empty(), ast_vector_tpl< T >::end(), context::function(), func_decl::operator()(), context::parse_file(), context::parse_string(), ast_vector_tpl< T >::pop_back(), z3::re_intersect(), BitVecSortRef::subsort(), expr::substitute(), and solver::trail().

## Friends And Related Function Documentation

## ◆ operator<<

std::ostream & operator<< | ( | std::ostream & | out,
|  | ast_vector_tpl< T > const & | v
| ) |  |
| friend

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

605{ out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
Z3_ast_vector_to_string
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)
Convert AST vector into a string.