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) | |
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 568 of file z3++.h.
Referenced by expr::is_app(), expr::is_numeral(), expr::is_quantifier(), and expr::is_var().
Definition at line 560 of file z3++.h.
|
inline |
|
friend |
|
protected |
Definition at line 552 of file z3++.h.
Referenced by expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), expr::as_binary(), expr::bool_value(), expr::denominator(), expr::get_decimal_string(), expr::get_sort(), expr::get_string(), expr::get_u32string(), 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(), 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(), expr::operator Z3_app(), ast::operator Z3_ast(), func_decl::operator Z3_func_decl(), sort::operator Z3_sort(), z3::operator<<(), ast::operator=(), expr::simplify(), and expr::substitute().