Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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

Protected Attributes

Z3_ast m_ast

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 321 of file z3++.h.


Constructor & Destructor Documentation

ast ( context c) [inline]
ast ( context c,
Z3_ast  n 
) [inline]
ast ( ast const &  s) [inline]
~ast ( ) [inline]

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

{ if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }

Member Function Documentation

unsigned hash ( ) const [inline]

Definition at line 333 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 332 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 330 of file z3++.h.

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

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

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

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

{ 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 344 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 334 of file z3++.h.

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

Field Documentation

Z3_ast m_ast [protected]
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines