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 |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
void | 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 337 of file z3++.h.
Definition at line 336 of file z3++.h.
Referenced by sort::operator=(), func_decl::operator=(), and expr::operator=().
Return true if the ASTs are structurally identical.
Definition at line 349 of file z3++.h.
Referenced by SortRef::cast(), and BoolSortRef::cast().
|
friend |
|
protected |
Definition at line 328 of file z3++.h.
Referenced by ast::operator=().