Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Protected Attributes | Friends
ast Class Reference
+ Inheritance diagram for ast:

Public Member Functions

 ast (context &c)
 
 ast (context &c, Z3_ast n)
 
 ast (ast const &s)
 
 ~ast ()
 
 operator Z3_ast () const
 
 operator bool () const
 
astoperator= (ast const &s)
 
Z3_ast_kind kind () const
 
unsigned hash () const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Protected Attributes

Z3_ast m_ast
 
- Protected Attributes inherited from object
contextm_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.
 

Detailed Description

Definition at line 295 of file z3++.h.

Constructor & Destructor Documentation

ast ( context c)
inline

Definition at line 299 of file z3++.h.

:object(c), m_ast(0) {}
ast ( context c,
Z3_ast  n 
)
inline

Definition at line 300 of file z3++.h.

:object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
ast ( ast const &  s)
inline

Definition at line 301 of file z3++.h.

:object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
~ast ( )
inline

Definition at line 302 of file z3++.h.

Member Function Documentation

unsigned hash ( ) const
inline

Definition at line 307 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 306 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; }
operator bool ( ) const
inline

Definition at line 304 of file z3++.h.

{ return m_ast != 0; }
operator Z3_ast ( ) const
inline

Definition at line 303 of file z3++.h.

{ return m_ast; }
ast& operator= ( ast const &  s)
inline

Definition at line 305 of file z3++.h.

Referenced by sort::operator=(), func_decl::operator=(), and expr::operator=().

{ 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; }

Friends And Related Function Documentation

bool eq ( ast const &  a,
ast const &  b 
)
friend

Return true if the ASTs are structurally identical.

Definition at line 313 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 308 of file z3++.h.

{ out << Z3_ast_to_string(n.ctx(), n.m_ast); return out; }

Field Documentation

Z3_ast m_ast
protected