#include <z3++.h>
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. |
Definition at line 555 of file z3++.h.
Referenced by ast(), eq, expr::expr(), expr::expr(), func_decl::func_decl(), func_decl::func_decl(), operator<<, operator=(), sort::sort(), sort::sort(), and sort::sort().
Definition at line 556 of file z3++.h.
Definition at line 557 of file z3++.h.
|
inlineoverride |
|
inline |
|
inline |
Definition at line 569 of file z3++.h.
Referenced by expr::is_app(), expr::is_numeral(), expr::is_quantifier(), and expr::is_var().
Definition at line 561 of file z3++.h.
|
inline |
|
friend |
|
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(), ast(), expr::bool_value(), expr::denominator(), expr::get_decimal_string(), expr::get_sort(), expr::get_string(), expr::get_u32string(), hash(), expr::id(), expr::is_algebraic(), expr::is_exists(), expr::is_forall(), expr::is_lambda(), expr::is_numeral(), expr::is_numeral(), 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(), kind(), expr::loop(), 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(), operator bool(), expr::operator Z3_app(), operator Z3_ast(), func_decl::operator Z3_func_decl(), sort::operator Z3_sort(), operator<<, sort::operator<<, operator=(), expr::simplify(), expr::simplify(), expr::substitute(), expr::substitute(), expr::substitute(), to_string(), and ~ast().