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

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
 
operator[] (unsigned i) const
 
void push_back (T const &e)
 
void resize (unsigned sz)
 
back () const
 
void pop_back ()
 
bool empty () const
 
ast_vector_tploperator= (ast_vector_tpl const &s)
 
ast_vector_tplset (unsigned idx, ast &a)
 
iterator begin () const noexcept
 
iterator end () const
 
std::string to_string () const
 

Friends

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

Detailed Description

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

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

Constructor & Destructor Documentation

◆ ast_vector_tpl() [1/4]

ast_vector_tpl ( context c)
inline

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

568 :object(c) { init(Z3_mk_ast_vector(c)); }

◆ ast_vector_tpl() [2/4]

ast_vector_tpl ( context c,
Z3_ast_vector  v 
)
inline

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

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

◆ ast_vector_tpl() [3/4]

ast_vector_tpl ( ast_vector_tpl< T > const &  s)
inline

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

570 :object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }

◆ ast_vector_tpl() [4/4]

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

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

571 : object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }

◆ ~ast_vector_tpl()

~ast_vector_tpl ( )
inline

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

573 { Z3_ast_vector_dec_ref(ctx(), m_vector); }

Member Function Documentation

◆ back()

T back ( ) const
inline

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

579 { return operator[](size() - 1); }

◆ begin()

iterator begin ( ) const
inlinenoexcept

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

624 { return iterator(this, 0); }

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

◆ empty()

bool empty ( ) const
inline

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

581 { return size() == 0; }

Referenced by z3::mk_xor().

◆ end()

iterator end ( ) const
inline

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

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

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

◆ operator Z3_ast_vector()

operator Z3_ast_vector ( ) const
inline

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

574 { return m_vector; }

◆ operator=()

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

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

582  {
583  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
584  Z3_ast_vector_dec_ref(ctx(), m_vector);
585  object::operator=(s);
586  m_vector = s.m_vector;
587  return *this;
588  }

◆ operator[]()

T operator[] ( unsigned  i) const
inline

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

576 { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }

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

◆ pop_back()

void pop_back ( )
inline

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

580 { assert(size() > 0); resize(size() - 1); }

◆ push_back()

void push_back ( T const &  e)
inline

◆ resize()

void resize ( unsigned  sz)
inline

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

578 { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }

Referenced by ast_vector_tpl< expr >::pop_back(), and constructors::query().

◆ set()

ast_vector_tpl& set ( unsigned  idx,
ast a 
)
inline

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

589  {
590  Z3_ast_vector_set(ctx(), m_vector, idx, a);
591  return *this;
592  }

◆ size()

unsigned size ( ) const
inline

◆ to_string()

std::string to_string ( ) const
inline

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

627 { return std::string(Z3_ast_vector_to_string(ctx(), m_vector)); }

Friends And Related Function Documentation

◆ operator<<

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

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

626 { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
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.
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.
z3::ast_vector_tpl::resize
void resize(unsigned sz)
Definition: z3++.h:578
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.
Z3_mk_ast_vector
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.
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.
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.
z3::ast_vector_tpl::size
unsigned size() const
Definition: z3++.h:575
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.
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.
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.
z3::ast_vector_tpl::operator[]
T operator[](unsigned i) const
Definition: z3++.h:576
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.
Microsoft.Z3.Z3_ast
System.IntPtr Z3_ast
Definition: NativeContext.cs:28