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

ast &	operator= (ast const &s)

Z3_ast_kind	kind () const

unsigned	hash () const

Public Member Functions inherited from object
	object (context &c)

	object (object const &s)

context &	ctx () const

void	check_error () const

Protected Attributes
Z3_ast	m_ast

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

Detailed Description

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

Constructor & Destructor Documentation

ast ( context & c )

inline

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

325 :object(c), m_ast(0) {}

z3::object::object

object(context &c)

Definition: z3++.h:270

z3::ast::m_ast

Z3_ast m_ast

Definition: z3++.h:323

ast	(	context &	c,
		Z3_ast	n
	)

inline

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

326 :object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }

Z3_inc_ref

void Z3_API Z3_inc_ref(__in Z3_context c, __in Z3_ast a)

Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...

z3::object::ctx

context & ctx() const

Definition: z3++.h:272

z3::object::object

object(context &c)

Definition: z3++.h:270

z3::ast::m_ast

Z3_ast m_ast

Definition: z3++.h:323

ast ( ast const & s )

inline

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

327 :object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }

Z3_inc_ref

void Z3_API Z3_inc_ref(__in Z3_context c, __in Z3_ast a)

Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...

z3::object::ctx

context & ctx() const

Definition: z3++.h:272

z3::object::object

object(context &c)

Definition: z3++.h:270

z3::ast::m_ast

Z3_ast m_ast

Definition: z3++.h:323

~ast ( )

inline

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

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

Z3_dec_ref

void Z3_API Z3_dec_ref(__in Z3_context c, __in 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

Z3_ast m_ast

Definition: z3++.h:323

z3::object::m_ctx

context * m_ctx

Definition: z3++.h:268

Member Function Documentation

unsigned hash ( ) const

inline

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

333 { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }

z3::object::ctx

context & ctx() const

Definition: z3++.h:272

z3::object::check_error

void check_error() const

Definition: z3++.h:273

Z3_get_ast_hash

unsigned Z3_API Z3_get_ast_hash(__in Z3_context c, __in Z3_ast a)

Return a hash code for the given AST.

z3::ast::m_ast

Z3_ast m_ast

Definition: z3++.h:323

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().

332 { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }

Z3_get_ast_kind

Z3_ast_kind Z3_API Z3_get_ast_kind(__in Z3_context c, __in Z3_ast a)

Return the kind of the given AST.

Z3_ast_kind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...

Definition: z3_api.h:212

z3::object::ctx

context & ctx() const

Definition: z3++.h:272

z3::object::check_error

void check_error() const

Definition: z3++.h:273

z3::ast::m_ast

Z3_ast m_ast

Definition: z3++.h:323

operator bool ( ) const

inline

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

330 { return m_ast != 0; }

z3::ast::m_ast

Z3_ast m_ast

Definition: z3++.h:323

operator Z3_ast ( ) const

inline

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

329 { return m_ast; }

z3::ast::m_ast

Z3_ast m_ast

Definition: z3++.h:323

ast& operator= ( ast const & s )

inline

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

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

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

Z3_inc_ref

void Z3_API Z3_inc_ref(__in Z3_context c, __in Z3_ast a)

Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...

Z3_dec_ref

void Z3_API Z3_dec_ref(__in Z3_context c, __in Z3_ast a)

Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...

z3::object::ctx

context & ctx() const

Definition: z3++.h:272

z3::ast::m_ast

Z3_ast m_ast

Definition: z3++.h:323

z3::object::m_ctx

context * m_ctx

Definition: z3++.h:268

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().

344 { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }

Z3_is_eq_ast

Z3_bool Z3_API Z3_is_eq_ast(__in Z3_context c, __in Z3_ast t1, Z3_ast t2)

compare terms.

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

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

Referenced by expr::get_sort(), expr::is_well_sorted(), expr::operator Z3_app(), ast::operator Z3_ast(), func_decl::operator Z3_func_decl(), sort::operator Z3_sort(), ast::operator=(), expr::simplify(), and expr::substitute().

Public Member Functions

Protected Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Field Documentation