Z3 |

Public Member Functions | Protected Attributes | Friends
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 (ast &&s) noexcept
| ~ast ()
| operator Z3_ast () const
| operator bool () const
ast & | operator= (ast const &s)
ast & | operator= (ast &&s) noexcept
Z3_ast_kind | kind () const
unsigned | hash () const
std::string | to_string () const
Public Member Functions inherited from object
| object (context &c)
context & | ctx () const
Z3_error_code | 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 498 of file z3++.h.

## Constructor & Destructor Documentation

## ◆ ast() [1/4]

ast | ( | context & | c | ) |
| inline

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

502:object(c), m_ast(0) {}
z3::ast::m_ast
Z3_ast m_ast
Definition: z3++.h:500
z3::object::object
object(context &c)
Definition: z3++.h:421

Referenced by FuncDeclRef::__call__(), AstRef::__deepcopy__(), AstRef::__del__(), SortRef::__eq__(), SortRef::__ne__(), DatatypeSortRef::accessor(), FuncDeclRef::arity(), AstRef::as_ast(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), PatternRef::as_ast(), QuantifierRef::as_ast(), FuncDeclRef::as_func_decl(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), DatatypeSortRef::constructor(), ArraySortRef::domain(), FuncDeclRef::domain(), FPSortRef::ebits(), QuantifierRef::is_exists(), QuantifierRef::is_forall(), QuantifierRef::is_lambda(), SeqSortRef::is_string(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), DatatypeSortRef::num_constructors(), QuantifierRef::num_no_patterns(), QuantifierRef::num_patterns(), QuantifierRef::num_vars(), FuncDeclRef::params(), QuantifierRef::pattern(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), FPSortRef::sbits(), BitVecSortRef::size(), FiniteDomainSortRef::size(), QuantifierRef::var_name(), QuantifierRef::var_sort(), and QuantifierRef::weight().

## ◆ ast() [2/4]

ast | ( | context & | c,
|  | Z3_ast | n
| ) |  |
| inline

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

503:object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_inc_ref
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_...

Referenced by FuncDeclRef::__call__(), AstRef::__deepcopy__(), AstRef::__del__(), SortRef::__eq__(), SortRef::__ne__(), DatatypeSortRef::accessor(), FuncDeclRef::arity(), AstRef::as_ast(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), PatternRef::as_ast(), QuantifierRef::as_ast(), FuncDeclRef::as_func_decl(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), DatatypeSortRef::constructor(), ArraySortRef::domain(), FuncDeclRef::domain(), FPSortRef::ebits(), QuantifierRef::is_exists(), QuantifierRef::is_forall(), QuantifierRef::is_lambda(), SeqSortRef::is_string(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), DatatypeSortRef::num_constructors(), QuantifierRef::num_no_patterns(), QuantifierRef::num_patterns(), QuantifierRef::num_vars(), FuncDeclRef::params(), QuantifierRef::pattern(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), FPSortRef::sbits(), BitVecSortRef::size(), FiniteDomainSortRef::size(), QuantifierRef::var_name(), QuantifierRef::var_sort(), and QuantifierRef::weight().

## ◆ ast() [3/4]

ast | ( | ast const & | s | ) |
| inline

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

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

Referenced by FuncDeclRef::__call__(), AstRef::__deepcopy__(), AstRef::__del__(), SortRef::__eq__(), SortRef::__ne__(), DatatypeSortRef::accessor(), FuncDeclRef::arity(), AstRef::as_ast(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), PatternRef::as_ast(), QuantifierRef::as_ast(), FuncDeclRef::as_func_decl(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), DatatypeSortRef::constructor(), ArraySortRef::domain(), FuncDeclRef::domain(), FPSortRef::ebits(), QuantifierRef::is_exists(), QuantifierRef::is_forall(), QuantifierRef::is_lambda(), SeqSortRef::is_string(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), DatatypeSortRef::num_constructors(), QuantifierRef::num_no_patterns(), QuantifierRef::num_patterns(), QuantifierRef::num_vars(), FuncDeclRef::params(), QuantifierRef::pattern(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), FPSortRef::sbits(), BitVecSortRef::size(), FiniteDomainSortRef::size(), QuantifierRef::var_name(), QuantifierRef::var_sort(), and QuantifierRef::weight().

## ◆ ast() [4/4]

ast | ( | ast && | s | ) |
| inline noexcept

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

505: object(std::forward<object>(s)), m_ast(s.m_ast) { s.m_ast = nullptr; }

Referenced by FuncDeclRef::__call__(), AstRef::__deepcopy__(), AstRef::__del__(), SortRef::__eq__(), SortRef::__ne__(), DatatypeSortRef::accessor(), FuncDeclRef::arity(), AstRef::as_ast(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), PatternRef::as_ast(), QuantifierRef::as_ast(), FuncDeclRef::as_func_decl(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), DatatypeSortRef::constructor(), ArraySortRef::domain(), FuncDeclRef::domain(), FPSortRef::ebits(), QuantifierRef::is_exists(), QuantifierRef::is_forall(), QuantifierRef::is_lambda(), SeqSortRef::is_string(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), DatatypeSortRef::num_constructors(), QuantifierRef::num_no_patterns(), QuantifierRef::num_patterns(), QuantifierRef::num_vars(), FuncDeclRef::params(), QuantifierRef::pattern(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), FPSortRef::sbits(), BitVecSortRef::size(), FiniteDomainSortRef::size(), QuantifierRef::var_name(), QuantifierRef::var_sort(), and QuantifierRef::weight().

## ◆ ~ast()

~ast | ( |  | ) |
| inline

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

506{ if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
z3::object::m_ctx
context * m_ctx
Definition: z3++.h:419
Z3_dec_ref
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 526 of file z3++.h.

526{ unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_get_ast_hash
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 525 of file z3++.h.

525{ Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
Z3_ast_kind
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180
Z3_get_ast_kind
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 508 of file z3++.h.

508{ return m_ast != 0; }

## ◆ operator Z3_ast()

operator Z3_ast | ( |  | ) | const
| inline

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

507{ return m_ast; }

## ◆ operator=() [1/2]

ast & operator= | ( | ast && | s | ) |
| inline noexcept

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

517 {
518 if (this != &s) {
519 object::operator=(std::forward<object>(s));
520 m_ast = s.m_ast;
521 s.m_ast = nullptr;
522 }
523 return *this;
524 }

## ◆ operator=() [2/2]

ast & operator= | ( | ast const & | s | ) |
| inline

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

509 {
510 Z3_inc_ref(s.ctx(), s.m_ast);
511 if (m_ast)
512 Z3_dec_ref(ctx(), m_ast);
513 object::operator=(s);
514 m_ast = s.m_ast;
515 return *this;
516 }

## ◆ to_string()

std::string to_string | ( |  | ) | const
| inline

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

528{ return std::string(Z3_ast_to_string(ctx(), m_ast)); }
Z3_ast_to_string
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 Function Documentation

## ◆ eq

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

Return true if the ASTs are structurally identical.

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

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

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

## ◆ operator<<

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

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

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

## Field Documentation

## ◆ m_ast

Z3_ast m_ast
| protected

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

Referenced by expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), expr::as_binary(), ast::ast(), expr::bool_value(), expr::denominator(), expr::get_decimal_string(), expr::get_escaped_string(), expr::get_sort(), expr::get_string(), ast::hash(), expr::id(), expr::is_algebraic(), expr::is_exists(), expr::is_forall(), expr::is_lambda(), expr::is_numeral(), expr::is_numeral_i(), expr::is_numeral_i64(), expr::is_numeral_u(), expr::is_numeral_u64(), expr::is_string_value(), expr::is_well_sorted(), ast::kind(), expr::loop(), expr::mk_from_ieee_bv(), expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), expr::mk_to_ieee_bv(), expr::numerator(), ast::operator bool(), expr::operator Z3_app(), ast::operator Z3_ast(), func_decl::operator Z3_func_decl(), sort::operator Z3_sort(), ast::operator=(), expr::simplify(), expr::substitute(), ast::to_string(), and ast::~ast().