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

#include <z3++.h>

Inheritance diagram for object:

Public Member Functions

 object (context &c)
virtual ~object ()=default
contextctx () const
Z3_error_code check_error () const

Protected Attributes

contextm_ctx

Friends

void check_context (object const &a, object const &b)

Detailed Description

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

Constructor & Destructor Documentation

◆ object()

◆ ~object()

virtual ~object ( )
virtualdefault

Member Function Documentation

◆ check_error()

Z3_error_code check_error ( ) const
inline

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

475{ return m_ctx->check_error(); }

Referenced by expr::abs, goal::add(), solver::add(), solver::add(), model::add_const_interp(), fixedpoint::add_cover(), func_interp::add_entry(), fixedpoint::add_fact(), model::add_func_interp(), fixedpoint::add_rule(), expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), probe::apply(), tactic::apply(), expr::arg(), func_entry::arg(), sort::array_domain(), sort::array_range(), z3::as_array(), expr::as_binary(), fixedpoint::assertions(), optimize::assertions(), solver::assertions(), expr::at(), expr::body(), expr::bv2int, sort::bv_size(), expr::bvadd_no_overflow, expr::bvadd_no_underflow, expr::bvmul_no_overflow, expr::bvmul_no_underflow, expr::bvneg_no_overflow, expr::bvredand, expr::bvredor, expr::bvsdiv_no_overflow, expr::bvsub_no_overflow, expr::bvsub_no_underflow, expr::char_from_bv(), expr::char_to_bv(), expr::char_to_int(), optimize::check(), optimize::check(), solver::check(), solver::check(), solver::check(), z3::cond(), solver::consequences(), expr::contains(), goal::convert_model(), solver::cube(), expr::decl(), expr::denominator(), param_descrs::documentation(), func_decl::domain(), stats::double_value(), func_interp::else_value(), z3::empty(), func_interp::entry(), model::eval(), z3::exists(), z3::exists(), z3::exists(), z3::exists(), z3::exists(), expr::extract(), z3::fail_if(), expr::fma, z3::forall(), z3::forall(), z3::forall(), z3::forall(), z3::forall(), expr::fp_eq, sort::fpa_ebits(), expr::fpa_fp, sort::fpa_sbits(), expr::fpa_to_fpa, expr::fpa_to_sbv, expr::fpa_to_ubv, fixedpoint::from_file(), optimize::from_file(), fixedpoint::from_string(), optimize::from_string(), fixedpoint::get_answer(), model::get_const_decl(), model::get_const_interp(), fixedpoint::get_cover_delta(), model::get_func_decl(), model::get_func_interp(), goal::get_model(), optimize::get_model(), solver::get_model(), fixedpoint::get_num_levels(), expr::get_sort(), expr::get_string(), ast::hash(), optimize::help(), simplifier::help(), tactic::help(), expr::id(), func_decl::id(), sort::id(), z3::indexof(), expr::int2bv, expr::is_digit(), stats::is_double(), expr::is_numeral(), expr::is_numeral(), expr::is_numeral(), expr::is_numeral_i(), expr::is_numeral_i64(), expr::is_numeral_u(), expr::is_numeral_u64(), stats::is_uint(), expr::is_well_sorted(), expr::ite, expr::itos(), stats::key(), ast::kind(), z3::lambda(), z3::lambda(), z3::lambda(), z3::lambda(), z3::lambda(), z3::last_indexof(), expr::length(), expr::loop(), expr::loop(), optimize::lower(), expr::max, expr::min, 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(), tactic::mk_solver(), expr::mk_to_ieee_bv(), func_decl::name(), sort::name(), expr::nand, solver::non_units(), expr::nor, expr::nth(), expr::num_args(), func_entry::num_args(), func_interp::num_entries(), expr::numerator(), optimize::objectives(), probe::operator!, expr::operator!=, expr::operator&, simplifier::operator&, tactic::operator&, expr::operator&&, probe::operator&&, func_decl::operator()(), func_decl::operator()(), expr::operator*, expr::operator+, expr::operator-, expr::operator-, expr::operator/, expr::operator<, probe::operator<, expr::operator<=, probe::operator<=, expr::operator==, probe::operator==, expr::operator>, probe::operator>, expr::operator>=, probe::operator>=, apply_result::operator[](), ast_vector_tpl< ast >::operator[](), goal::operator[](), expr::operator^, expr::operator|, tactic::operator|, expr::operator||, probe::operator||, tactic::par_and_then, solver::pop(), z3::prefixof(), probe::probe(), probe::probe(), solver::proof(), solver::push(), ast_vector_tpl< ast >::push_back(), fixedpoint::query(), fixedpoint::query(), func_decl::range(), z3::re_empty(), z3::re_full(), solver::reason_unknown(), tactic::repeat, expr::replace(), solver::reset(), ast_vector_tpl< ast >::resize(), expr::round_fpa_to_closest_integer, fixedpoint::rules(), expr::sbv_to_fpa, expr::sbvtos(), z3::select(), z3::select(), fixedpoint::set(), optimize::set(), solver::set(), func_interp::set_else(), optimize::set_initial_value(), solver::set_initial_value(), z3::set_intersect(), z3::set_union(), simplifier::simplifier(), expr::simplify(), expr::simplify(), solver::solver(), solver::solver(), solver::solver(), solver::solver(), expr::sqrt, fixedpoint::statistics(), optimize::statistics(), solver::statistics(), expr::stoi(), z3::store(), z3::store(), expr::substitute(), expr::substitute(), expr::substitute(), z3::suffixof(), tactic::tactic(), z3::to_real(), solver::trail(), solver::trail(), func_decl::transitive_closure(), tactic::try_for, expr::ubv_to_fpa, expr::ubvtos(), stats::uint_value(), expr::unit(), solver::units(), optimize::unsat_core(), solver::unsat_core(), fixedpoint::update_rule(), optimize::upper(), func_entry::value(), z3::when(), simplifier::with, tactic::with, and expr::xnor.

◆ ctx()

context & ctx ( ) const
inline

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

474{ return *m_ctx; }

Referenced by expr::abs, func_decl::accessors(), goal::add(), optimize::add(), optimize::add(), optimize::add(), solver::add(), solver::add(), solver::add(), model::add_const_interp(), fixedpoint::add_cover(), func_interp::add_entry(), fixedpoint::add_fact(), model::add_func_interp(), fixedpoint::add_rule(), optimize::add_soft(), optimize::add_soft(), expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), probe::apply(), tactic::apply(), expr::arg(), func_entry::arg(), expr::args(), func_decl::arity(), sort::array_domain(), sort::array_range(), z3::as_array(), expr::as_binary(), goal::as_expr(), z3::ashr(), z3::ashr(), z3::ashr(), fixedpoint::assertions(), optimize::assertions(), solver::assertions(), ast::ast(), ast::ast(), ast_vector_tpl< ast >::ast_vector_tpl(), ast_vector_tpl< ast >::ast_vector_tpl(), expr::at(), expr::atleast, expr::atmost, expr::bit2bool(), expr::body(), expr::bool_value(), expr::bv2int, sort::bv_size(), expr::bvadd_no_overflow, expr::bvadd_no_underflow, expr::bvmul_no_overflow, expr::bvmul_no_underflow, expr::bvneg_no_overflow, expr::bvredand, expr::bvredor, expr::bvsdiv_no_overflow, expr::bvsub_no_overflow, expr::bvsub_no_underflow, expr::char_from_bv(), expr::char_to_bv(), expr::char_to_int(), optimize::check(), optimize::check(), solver::check(), solver::check(), solver::check(), expr::concat, expr::concat, z3::cond(), solver::consequences(), sort::constructors(), expr::contains(), goal::convert_model(), solver::cube(), solver::cube_generator::cube_generator(), solver::cube_generator::cube_generator(), solver::cube_iterator::cube_iterator(), expr::decl(), func_decl::decl_kind(), expr::denominator(), goal::depth(), goal::dimacs(), solver::dimacs(), expr::distinct, param_descrs::documentation(), func_decl::domain(), stats::double_value(), func_interp::else_value(), z3::empty(), func_interp::entry(), ast::eq, model::eval(), z3::exists(), z3::exists(), z3::exists(), z3::exists(), z3::exists(), expr::extract(), expr::extract(), z3::fail_if(), fixedpoint::fixedpoint(), expr::fma, z3::foldl(), z3::foldli(), z3::forall(), z3::forall(), z3::forall(), z3::forall(), z3::forall(), expr::fp_eq, sort::fpa_ebits(), expr::fpa_fp, sort::fpa_sbits(), expr::fpa_to_fpa, expr::fpa_to_sbv, expr::fpa_to_ubv, fixedpoint::from_file(), optimize::from_file(), solver::from_file(), fixedpoint::from_string(), optimize::from_string(), solver::from_string(), fixedpoint::get_answer(), model::get_const_decl(), model::get_const_interp(), fixedpoint::get_cover_delta(), expr::get_decimal_string(), model::get_func_decl(), model::get_func_interp(), goal::get_model(), optimize::get_model(), solver::get_model(), fixedpoint::get_num_levels(), expr::get_numeral_int(), expr::get_numeral_int64(), expr::get_numeral_uint(), expr::get_numeral_uint64(), fixedpoint::get_param_descrs(), simplifier::get_param_descrs(), solver::get_param_descrs(), tactic::get_param_descrs(), expr::get_string(), expr::get_u32string(), model::has_interp(), ast::hash(), fixedpoint::help(), optimize::help(), simplifier::help(), tactic::help(), expr::hi(), expr::id(), func_decl::id(), sort::id(), expr::implies, expr::implies, goal::inconsistent(), z3::indexof(), expr::int2bv, expr::is_algebraic(), goal::is_decided_sat(), goal::is_decided_unsat(), expr::is_digit(), stats::is_double(), expr::is_exists(), expr::is_forall(), expr::is_lambda(), expr::is_numeral(), expr::is_numeral(), expr::is_numeral(), expr::is_numeral_i(), expr::is_numeral_i64(), expr::is_numeral_u(), expr::is_numeral_u64(), expr::is_string_value(), stats::is_uint(), expr::is_well_sorted(), expr::ite, expr::itos(), stats::key(), ast::kind(), param_descrs::kind(), symbol::kind(), z3::lambda(), z3::lambda(), z3::lambda(), z3::lambda(), z3::lambda(), z3::last_indexof(), expr::length(), z3::linear_order(), expr::lo(), expr::loop(), expr::loop(), optimize::lower(), z3::lshr(), z3::lshr(), z3::lshr(), z3::map(), z3::mapi(), expr::max, optimize::maximize(), expr::min, optimize::minimize(), 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(), tactic::mk_solver(), expr::mk_to_ieee_bv(), expr::mod, expr::mod, model::model(), func_decl::name(), param_descrs::name(), sort::name(), expr::nand, solver::non_units(), expr::nor, expr::nth(), expr::num_args(), func_entry::num_args(), model::num_consts(), func_interp::num_entries(), goal::num_exprs(), model::num_funcs(), func_decl::num_parameters(), expr::numerator(), optimize::objectives(), probe::operator!, expr::operator!=, expr::operator!=, expr::operator!=, z3::operator!=(), z3::operator!=(), expr::operator&, expr::operator&, expr::operator&, simplifier::operator&, tactic::operator&, expr::operator&&, expr::operator&&, expr::operator&&, probe::operator&&, func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), expr::operator*, expr::operator*, expr::operator*, expr::operator+, expr::operator+, expr::operator+, expr::operator-, expr::operator-, expr::operator-, expr::operator-, expr::operator/, expr::operator/, expr::operator/, expr::operator<, expr::operator<, expr::operator<, probe::operator<, probe::operator<, probe::operator<, apply_result::operator<<, ast::operator<<, ast_vector_tpl< ast >::operator<<, goal::operator<<, z3::operator<<(), optimize::operator<<, params::operator<<, solver::operator<<, sort::operator<<, stats::operator<<, expr::operator<=, expr::operator<=, expr::operator<=, probe::operator<=, probe::operator<=, probe::operator<=, apply_result::operator=(), ast::operator=(), ast_vector_tpl< ast >::operator=(), fixedpoint::operator=(), func_entry::operator=(), func_interp::operator=(), goal::operator=(), model::operator=(), optimize::operator=(), param_descrs::operator=(), params::operator=(), probe::operator=(), simplifier::operator=(), solver::operator=(), stats::operator=(), tactic::operator=(), expr::operator==, expr::operator==, expr::operator==, z3::operator==(), z3::operator==(), probe::operator==, probe::operator==, probe::operator==, expr::operator>, expr::operator>, expr::operator>, probe::operator>, probe::operator>, probe::operator>, expr::operator>=, expr::operator>=, expr::operator>=, probe::operator>=, probe::operator>=, probe::operator>=, apply_result::operator[](), ast_vector_tpl< ast >::operator[](), goal::operator[](), expr::operator^, expr::operator^, expr::operator^, expr::operator|, expr::operator|, expr::operator|, tactic::operator|, expr::operator||, expr::operator||, expr::operator||, probe::operator||, expr::operator~, optimize::optimize(), tactic::par_and_then, tactic::par_or, param_descrs::param_descrs(), params::params(), params::params(), z3::partial_order(), expr::pbeq, expr::pbge, expr::pble, z3::piecewise_linear_order(), optimize::pop(), solver::pop(), goal::precision(), z3::prefixof(), solver::proof(), user_propagator_base::propagate(), user_propagator_base::propagate(), optimize::push(), solver::push(), ast_vector_tpl< ast >::push_back(), expr::pw, expr::pw, fixedpoint::query(), fixedpoint::query(), func_decl::range(), z3::re_diff(), z3::re_empty(), z3::re_full(), z3::re_intersect(), fixedpoint::reason_unknown(), solver::reason_unknown(), context::recdef(), sort::recognizers(), fixedpoint::register_relation(), expr::rem, expr::rem, expr::repeat(), tactic::repeat, expr::replace(), goal::reset(), solver::reset(), ast_vector_tpl< ast >::resize(), expr::rotate_left(), expr::rotate_right(), expr::round_fpa_to_closest_integer, fixedpoint::rules(), expr::sbv_to_fpa, expr::sbvtos(), z3::select(), z3::select(), z3::select(), ast_vector_tpl< ast >::set(), fixedpoint::set(), optimize::set(), params::set(), params::set(), params::set(), params::set(), params::set(), solver::set(), solver::set(), solver::set(), solver::set(), solver::set(), solver::set(), func_interp::set_else(), optimize::set_initial_value(), optimize::set_initial_value(), optimize::set_initial_value(), solver::set_initial_value(), solver::set_initial_value(), solver::set_initial_value(), z3::set_intersect(), z3::set_union(), z3::sext(), z3::sge(), z3::sge(), z3::sge(), z3::sgt(), z3::sgt(), z3::sgt(), z3::shl(), z3::shl(), z3::shl(), expr::simplify(), expr::simplify(), apply_result::size(), ast_vector_tpl< ast >::size(), goal::size(), param_descrs::size(), stats::size(), z3::sle(), z3::sle(), z3::sle(), z3::slt(), z3::slt(), z3::slt(), z3::smod(), z3::smod(), z3::smod(), solver::solver(), solver::solver(), expr::sqrt, z3::srem(), z3::srem(), z3::srem(), fixedpoint::statistics(), optimize::statistics(), solver::statistics(), expr::stoi(), z3::store(), z3::store(), z3::store(), z3::store(), z3::store(), symbol::str(), expr::substitute(), expr::substitute(), expr::substitute(), z3::suffixof(), expr::sum, symbol::to_int(), z3::to_real(), solver::to_smt2(), ast::to_string(), ast_vector_tpl< ast >::to_string(), fixedpoint::to_string(), fixedpoint::to_string(), model::to_string(), param_descrs::to_string(), solver::trail(), solver::trail(), func_decl::transitive_closure(), z3::tree_order(), tactic::try_for, expr::ubv_to_fpa, expr::ubvtos(), z3::udiv(), z3::udiv(), z3::udiv(), z3::uge(), z3::uge(), z3::uge(), z3::ugt(), z3::ugt(), z3::ugt(), stats::uint_value(), z3::ule(), z3::ule(), z3::ule(), z3::ult(), z3::ult(), z3::ult(), expr::unit(), solver::units(), optimize::unsat_core(), solver::unsat_core(), fixedpoint::update_rule(), optimize::upper(), z3::urem(), z3::urem(), z3::urem(), func_entry::value(), z3::when(), simplifier::with, tactic::with, expr::xnor, z3::zext(), apply_result::~apply_result(), ast_vector_tpl< ast >::~ast_vector_tpl(), fixedpoint::~fixedpoint(), func_entry::~func_entry(), func_interp::~func_interp(), goal::~goal(), model::~model(), optimize::~optimize(), param_descrs::~param_descrs(), params::~params(), probe::~probe(), simplifier::~simplifier(), solver::~solver(), stats::~stats(), and tactic::~tactic().

◆ check_context

Field Documentation

◆ m_ctx

context* m_ctx
protected

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

Referenced by check_context, check_error(), ctx(), expr::get_sort(), object(), sort::sort_kind(), and ast::~ast().