Z3
 
Loading...
Searching...
No Matches
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 () override
 
 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
 
- Public Member Functions inherited from object
 object (context &c)
 
virtual ~object ()=default
 
contextctx () 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
contextm_ctx
 

Detailed Description

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

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

Constructor & Destructor Documentation

◆ ast_vector_tpl() [1/4]

template<typename T >
ast_vector_tpl ( context & c)
inline

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

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

◆ ast_vector_tpl() [2/4]

template<typename T >
ast_vector_tpl ( context & c,
Z3_ast_vector v )
inline

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

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

◆ ast_vector_tpl() [3/4]

template<typename T >
ast_vector_tpl ( ast_vector_tpl< T > const & s)
inline

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

593:object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
context & ctx() const
Definition z3++.h:474
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]

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

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

594: object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
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()

template<typename T >
~ast_vector_tpl ( )
inlineoverride

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

596{ Z3_ast_vector_dec_ref(ctx(), m_vector); }
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()

template<typename T >
T back ( ) const
inline

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

602{ return operator[](size() - 1); }
unsigned size() const
Definition z3++.h:598
T operator[](unsigned i) const
Definition z3++.h:599

◆ begin()

template<typename T >
iterator begin ( ) const
inlinenoexcept

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

647{ return iterator(this, 0); }

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

◆ empty()

template<typename T >
bool empty ( ) const
inline

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

604{ return size() == 0; }

◆ end()

template<typename T >
iterator end ( ) const
inline

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

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

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

◆ operator Z3_ast_vector()

template<typename T >
operator Z3_ast_vector ( ) const
inline

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

597{ return m_vector; }

◆ operator=()

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

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

605 {
606 Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
607 Z3_ast_vector_dec_ref(ctx(), m_vector);
608 object::operator=(s);
609 m_vector = s.m_vector;
610 return *this;
611 }

◆ operator[]()

template<typename T >
T operator[] ( unsigned i) const
inline

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

599{ Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
Z3_error_code check_error() const
Definition z3++.h:475
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()

template<typename T >
void pop_back ( )
inline

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

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

◆ push_back()

template<typename T >
void push_back ( T const & e)
inline

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

600{ Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
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 func_decl::accessors(), expr::args(), sort::constructors(), context::datatypes(), context::enumeration_sort(), constructors::query(), sort::recognizers(), and context::tuple_sort().

◆ resize()

template<typename T >
void resize ( unsigned sz)
inline

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

601{ Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
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(), and constructors::query().

◆ set()

template<typename T >
ast_vector_tpl & set ( unsigned idx,
ast & a )
inline

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

612 {
613 Z3_ast_vector_set(ctx(), m_vector, idx, a);
614 return *this;
615 }
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()

◆ to_string()

template<typename T >
std::string to_string ( ) const
inline

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

650{ return std::string(Z3_ast_vector_to_string(ctx(), m_vector)); }
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)
Convert AST vector into a string.

Friends And Related Symbol Documentation

◆ operator<<

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

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

649{ out << Z3_ast_vector_to_string(v.ctx(), v); return out; }