A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://z3prover.github.io/api/html/classz3_1_1ast__vector__tpl.html below:

Z3: ast_vector_tpl< T > Class Template Reference

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

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

◆ ast_vector_tpl() [1/4]

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

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() [3/4]

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

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]

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

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()

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

void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)

Decrement the reference counter of the given AST vector.

◆ back()

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

T operator[](unsigned i) const

◆ begin() ◆ empty()

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

604

{

return size

() == 0; }

◆ end() ◆ operator Z3_ast_vector() operator Z3_ast_vector ( ) const inline ◆ operator=()

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

608

object::operator=(s);

609

m_vector = s.m_vector;

◆ operator[]() T operator[] ( unsigned  i ) const inline

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

Z3_error_code check_error() const

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() ◆ push_back() void push_back ( T const &  e ) inline ◆ resize() void resize ( unsigned  sz ) inline ◆ set()

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

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()

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

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(), user_propagator_base::conflict(), 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(), user_propagator_base::propagate(), z3::re_intersect(), BitVecSortRef::subsort(), expr::substitute(), and solver::trail().

◆ to_string() std::string to_string ( ) const inline

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

Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)

Convert AST vector into a string.

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

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4