ast Class Reference

Inheritance diagram for ast:

Public Member Functions
	ast (context &c)
	ast (context &c, Z3_ast n)
	ast (ast const &s)
	~ast () override
	operator Z3_ast () const
	operator bool () const
ast &	operator= (ast const &s)
Z3_ast_kind	kind () const
unsigned	hash () const
std::string	to_string () const
Public Member Functions inherited from object
	object (context &c)
virtual	~object ()=default
context &	ctx () const
Z3_error_code	check_error () const

Protected Attributes
Z3_ast	m_ast
Protected Attributes inherited from object
context *	m_ctx

Friends
std::ostream &	operator<< (std::ostream &out, ast const &n)
bool	eq (ast const &a, ast const &b)
	Return true if the ASTs are structurally identical. More...

Detailed Description

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

Constructor & Destructor Documentation

ast() [1/3]

ast ( context &  c )

inline

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

:object(c), m_ast(0) {}

Referenced by FuncDeclRef::__call__(), AstRef::__deepcopy__(), AstRef::__del__(), SortRef::__eq__(), SortRef::__ne__(), DatatypeSortRef::accessor(), FuncDeclRef::arity(), AstRef::as_ast(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), PatternRef::as_ast(), QuantifierRef::as_ast(), FuncDeclRef::as_func_decl(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), DatatypeSortRef::constructor(), ArraySortRef::domain(), FuncDeclRef::domain(), ArraySortRef::domain_n(), FPSortRef::ebits(), QuantifierRef::is_exists(), QuantifierRef::is_forall(), QuantifierRef::is_lambda(), SeqSortRef::is_string(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), DatatypeSortRef::num_constructors(), QuantifierRef::num_no_patterns(), QuantifierRef::num_patterns(), QuantifierRef::num_vars(), FuncDeclRef::params(), QuantifierRef::pattern(), QuantifierRef::qid(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), FPSortRef::sbits(), BitVecSortRef::size(), FiniteDomainSortRef::size(), QuantifierRef::skolem_id(), QuantifierRef::var_name(), QuantifierRef::var_sort(), and QuantifierRef::weight().

ast() [2/3]

ast ( context &  c, Z3_ast  n  )

inline

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

:object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }

Referenced by FuncDeclRef::__call__(), AstRef::__deepcopy__(), AstRef::__del__(), SortRef::__eq__(), SortRef::__ne__(), DatatypeSortRef::accessor(), FuncDeclRef::arity(), AstRef::as_ast(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), PatternRef::as_ast(), QuantifierRef::as_ast(), FuncDeclRef::as_func_decl(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), DatatypeSortRef::constructor(), ArraySortRef::domain(), FuncDeclRef::domain(), ArraySortRef::domain_n(), FPSortRef::ebits(), QuantifierRef::is_exists(), QuantifierRef::is_forall(), QuantifierRef::is_lambda(), SeqSortRef::is_string(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), DatatypeSortRef::num_constructors(), QuantifierRef::num_no_patterns(), QuantifierRef::num_patterns(), QuantifierRef::num_vars(), FuncDeclRef::params(), QuantifierRef::pattern(), QuantifierRef::qid(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), FPSortRef::sbits(), BitVecSortRef::size(), FiniteDomainSortRef::size(), QuantifierRef::skolem_id(), QuantifierRef::var_name(), QuantifierRef::var_sort(), and QuantifierRef::weight().

ast() [3/3]

ast ( ast const &  s )

inline

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

:object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }

Referenced by FuncDeclRef::__call__(), AstRef::__deepcopy__(), AstRef::__del__(), SortRef::__eq__(), SortRef::__ne__(), DatatypeSortRef::accessor(), FuncDeclRef::arity(), AstRef::as_ast(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), PatternRef::as_ast(), QuantifierRef::as_ast(), FuncDeclRef::as_func_decl(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), DatatypeSortRef::constructor(), ArraySortRef::domain(), FuncDeclRef::domain(), ArraySortRef::domain_n(), FPSortRef::ebits(), QuantifierRef::is_exists(), QuantifierRef::is_forall(), QuantifierRef::is_lambda(), SeqSortRef::is_string(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), DatatypeSortRef::num_constructors(), QuantifierRef::num_no_patterns(), QuantifierRef::num_patterns(), QuantifierRef::num_vars(), FuncDeclRef::params(), QuantifierRef::pattern(), QuantifierRef::qid(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), FPSortRef::sbits(), BitVecSortRef::size(), FiniteDomainSortRef::size(), QuantifierRef::skolem_id(), QuantifierRef::var_name(), QuantifierRef::var_sort(), and QuantifierRef::weight().

~ast()

~ast ( )

inlineoverride

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

{ if (m_ast) { Z3_dec_ref(*m_ctx, m_ast); } }

Member Function Documentation

hash()

unsigned hash ( ) const

inline

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

{ unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }

Referenced by AstRef::__hash__().

kind()

Z3_ast_kind kind ( ) const

inline

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

{ Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }

Referenced by expr::is_app(), ArithSortRef::is_int(), expr::is_numeral(), expr::is_quantifier(), ArithSortRef::is_real(), and expr::is_var().

operator bool()

operator bool ( ) const

inline

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

{ return m_ast != 0; }

operator Z3_ast()

operator Z3_ast ( ) const

inline

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

{ return m_ast; }

operator=()

ast& operator= ( ast const &  s )

inline

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

                                       {
            Z3_inc_ref(s.ctx(), s.m_ast);
            if (m_ast)
                Z3_dec_ref(ctx(), m_ast);
            object::operator=(s);
            m_ast = s.m_ast;
            return *this;
        }

to_string()

std::string to_string ( ) const

inline

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

{ return std::string(Z3_ast_to_string(ctx(), m_ast)); }

Friends And Related Function Documentation

eq

bool eq ( ast const &  a, ast const &  b  )

friend

Return true if the ASTs are structurally identical.

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

{ return Z3_is_eq_ast(a.ctx(), a, b); }

Referenced by AstRef::__eq__(), UserPropagateBase::add_eq(), SortRef::cast(), and BoolSortRef::cast().

operator<<

std::ostream& operator<< ( std::ostream &  out, ast const &  n  )

friend

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

                                                                    {
        out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
    }

Field Documentation

m_ast

Z3_ast m_ast

protected

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

Referenced by expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), expr::as_binary(), ast::ast(), expr::bool_value(), expr::denominator(), expr::get_decimal_string(), expr::get_sort(), expr::get_string(), expr::get_u32string(), ast::hash(), expr::id(), expr::is_algebraic(), expr::is_exists(), expr::is_forall(), expr::is_lambda(), expr::is_numeral(), expr::is_numeral_i(), expr::is_numeral_i64(), expr::is_numeral_u(), expr::is_numeral_u64(), expr::is_string_value(), expr::is_well_sorted(), ast::kind(), expr::loop(), expr::mk_from_ieee_bv(), expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), expr::mk_to_ieee_bv(), expr::numerator(), ast::operator bool(), expr::operator Z3_app(), ast::operator Z3_ast(), func_decl::operator Z3_func_decl(), sort::operator Z3_sort(), ast::operator=(), expr::simplify(), expr::substitute(), ast::to_string(), and ast::~ast().