Public Member Functions | |
ast (context &c) | |
ast (context &c, Z3_ast n) | |
ast (ast const &s) | |
~ast () | |
operator Z3_ast () const | |
operator bool () const | |
ast & | operator= (ast const &s) |
Z3_ast_kind | kind () const |
unsigned | hash () const |
Protected Attributes | |
Z3_ast | m_ast |
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. |
Definition at line 325 of file z3++.h.
Referenced by FuncDeclRef::__call__(), SortRef::__eq__(), SortRef::__ne__(), FuncDeclRef::arity(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), FuncDeclRef::as_func_decl(), FuncDeclRef::domain(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), and FuncDeclRef::range().
Definition at line 326 of file z3++.h.
Referenced by FuncDeclRef::__call__(), SortRef::__eq__(), SortRef::__ne__(), FuncDeclRef::arity(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), FuncDeclRef::as_func_decl(), FuncDeclRef::domain(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), and FuncDeclRef::range().
:object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
Definition at line 327 of file z3++.h.
Referenced by FuncDeclRef::__call__(), SortRef::__eq__(), SortRef::__ne__(), FuncDeclRef::arity(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), FuncDeclRef::as_func_decl(), FuncDeclRef::domain(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), and FuncDeclRef::range().
:object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
unsigned hash | ( | ) | const [inline] |
Definition at line 333 of file z3++.h.
{ unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
Z3_ast_kind kind | ( | ) | const [inline] |
Definition at line 332 of file z3++.h.
Referenced by expr::is_app(), expr::is_numeral(), expr::is_quantifier(), and expr::is_var().
{ Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
Definition at line 331 of file z3++.h.
{ Z3_inc_ref(s.ctx(), s.m_ast); if (m_ast) Z3_dec_ref(ctx(), m_ast); m_ctx = s.m_ctx; m_ast = s.m_ast; return *this; }
Return true if the ASTs are structurally identical.
Definition at line 344 of file z3++.h.
Referenced by SortRef::cast(), and BoolSortRef::cast().
{ return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
std::ostream& operator<< | ( | std::ostream & | out, |
ast const & | n | ||
) | [friend] |
Definition at line 334 of file z3++.h.
{ out << Z3_ast_to_string(n.ctx(), n.m_ast); return out; }
Z3_ast m_ast [protected] |
Definition at line 323 of file z3++.h.
Referenced by ast::ast(), expr::get_sort(), ast::hash(), expr::is_well_sorted(), ast::kind(), 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(), and ast::~ast().