Z3
 
Loading...
Searching...
No Matches
ast Class Reference

#include <z3++.h>

+ Inheritance diagram for ast:

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
 
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)
 
virtual ~object ()=default
 
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.
 

Detailed Description

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

Constructor & Destructor Documentation

◆ ast() [1/3]

◆ ast() [2/3]

◆ ast() [3/3]

◆ ~ast()

~ast ( )
inlineoverride

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

558{ if (m_ast) { Z3_dec_ref(*m_ctx, m_ast); } }
context * m_ctx
Definition z3++.h:470
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_...

Member Function Documentation

◆ hash()

unsigned hash ( ) const
inline

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

570{ unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
Z3_error_code check_error() const
Definition z3++.h:475
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 but two different AST objects can m...

Referenced by AstRef::__hash__().

◆ kind()

Z3_ast_kind kind ( ) const
inline

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

569{ Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition z3_api.h:141
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.

Referenced by expr::is_app(), ArithSortRef::is_int(), expr::is_numeral(), expr::is_quantifier(), ArithSortRef::is_real(), and expr::is_var().

◆ operator bool()

operator bool ( ) const
inline

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

560{ return m_ast != 0; }

◆ operator Z3_ast()

operator Z3_ast ( ) const
inline

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

559{ return m_ast; }

◆ operator=()

ast & operator= ( ast const & s)
inline

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

561 {
562 Z3_inc_ref(s.ctx(), s.m_ast);
563 if (m_ast)
564 Z3_dec_ref(ctx(), m_ast);
565 object::operator=(s);
566 m_ast = s.m_ast;
567 return *this;
568 }

◆ to_string()

std::string to_string ( ) const
inline

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

572{ 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.

Friends And Related Symbol Documentation

◆ eq

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

Return true if the ASTs are structurally identical.

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

584{ return Z3_is_eq_ast(a.ctx(), a, b); }
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.

Referenced by AstRef::__eq__(), and SortRef::cast().

◆ operator<<

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

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

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

Field Documentation

◆ m_ast