Z3
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
 
std::string to_string () const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
Z3_error_code 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. More...
 

Detailed Description

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

Constructor & Destructor Documentation

§ ast() [1/3]

ast ( context c)
inline

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

454 :object(c), m_ast(0) {}
object(context &c)
Definition: z3++.h:371
Z3_ast m_ast
Definition: z3++.h:452

§ ast() [2/3]

ast ( context c,
Z3_ast  n 
)
inline

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

455 :object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:373
object(context &c)
Definition: z3++.h:371
Z3_ast m_ast
Definition: z3++.h:452
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...

§ ast() [3/3]

ast ( ast const &  s)
inline

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

456 :object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:373
object(context &c)
Definition: z3++.h:371
Z3_ast m_ast
Definition: z3++.h:452
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...

§ ~ast()

~ast ( )
inline

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

457 { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast m_ast
Definition: z3++.h:452
context * m_ctx
Definition: z3++.h:369

Member Function Documentation

§ hash()

unsigned hash ( ) const
inline

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

462 { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:374
context & ctx() const
Definition: z3++.h:373
unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a)
Return a hash code for the given AST. The hash code is structural. You can use Z3_get_ast_id intercha...
Z3_ast m_ast
Definition: z3++.h:452

§ kind()

Z3_ast_kind kind ( ) const
inline

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

461 { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:374
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
context & ctx() const
Definition: z3++.h:373
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:176
Z3_ast m_ast
Definition: z3++.h:452

§ operator bool()

operator bool ( ) const
inline

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

459 { return m_ast != 0; }
Z3_ast m_ast
Definition: z3++.h:452

§ operator Z3_ast()

operator Z3_ast ( ) const
inline

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

458 { return m_ast; }
Z3_ast m_ast
Definition: z3++.h:452

§ operator=()

ast& operator= ( ast const &  s)
inline

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

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

460 { 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; }
context & ctx() const
Definition: z3++.h:373
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast m_ast
Definition: z3++.h:452
context * m_ctx
Definition: z3++.h:369
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...

§ to_string()

std::string to_string ( ) const
inline

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

464 { return std::string(Z3_ast_to_string(ctx(), m_ast)); }
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
context & ctx() const
Definition: z3++.h:373
Z3_ast m_ast
Definition: z3++.h:452

Friends And Related Function Documentation

§ eq

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

Return true if the ASTs are structurally identical.

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

476 { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.

§ operator<<

std::ostream& operator<< ( std::ostream &  out,
ast const &  n 
)
friend

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

472  {
473  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
474  }
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.

Field Documentation

§ m_ast

Z3_ast m_ast
protected

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

Referenced by z3::operator<<(), and ast::operator=().