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 |
std::string | to_string () const |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
Z3_error_code | check_error () const |
Protected Attributes | |
Z3_ast | m_ast |
![]() | |
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... | |
|
inline |
|
inline |
|
inline |
Definition at line 495 of file z3++.h.
Referenced by expr::is_app(), expr::is_numeral(), expr::is_quantifier(), and expr::is_var().
Definition at line 494 of file z3++.h.
Referenced by sort::operator=(), func_decl::operator=(), and expr::operator=().
|
inline |
|
friend |
|
protected |
Definition at line 486 of file z3++.h.
Referenced by ast::ast(), expr::bool_value(), expr::denominator(), expr::get_decimal_string(), expr::get_escaped_string(), expr::get_sort(), expr::get_string(), 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_well_sorted(), ast::kind(), expr::loop(), expr::numerator(), ast::operator bool(), expr::operator Z3_app(), ast::operator Z3_ast(), func_decl::operator Z3_func_decl(), sort::operator Z3_sort(), z3::operator<<(), ast::operator=(), expr::simplify(), expr::substitute(), ast::to_string(), and ast::~ast().