Z3
Public Member Functions | Protected Attributes | Friends
object Class Reference
+ Inheritance diagram for object:

Public Member Functions

 object (context &c)
 
 object (object const &s)
 
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 412 of file z3++.h.

Constructor & Destructor Documentation

◆ object() [1/2]

object ( context c)
inline

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

416 :m_ctx(&c) {}

◆ object() [2/2]

object ( object const &  s)
inline

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

417 :m_ctx(s.m_ctx) {}

Member Function Documentation

◆ check_error()

Z3_error_code check_error ( ) const
inline

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

419 { return m_ctx->check_error(); }

Referenced by z3::abs(), solver::add(), goal::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(), tactic::apply(), probe::apply(), expr::arg(), func_entry::arg(), sort::array_domain(), sort::array_range(), z3::as_array(), expr::as_binary(), solver::assertions(), optimize::assertions(), fixedpoint::assertions(), expr::at(), expr::body(), z3::bv2int(), sort::bv_size(), z3::bvadd_no_overflow(), z3::bvadd_no_underflow(), z3::bvmul_no_overflow(), z3::bvmul_no_underflow(), z3::bvneg_no_overflow(), z3::bvsdiv_no_overflow(), z3::bvsub_no_overflow(), z3::bvsub_no_underflow(), solver::check(), optimize::check(), 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(), expr::extract(), z3::fail_if(), z3::forall(), sort::fpa_ebits(), expr::fpa_rounding_mode(), sort::fpa_sbits(), optimize::from_file(), fixedpoint::from_file(), optimize::from_string(), fixedpoint::from_string(), fixedpoint::get_answer(), model::get_const_decl(), model::get_const_interp(), fixedpoint::get_cover_delta(), expr::get_escaped_string(), model::get_func_decl(), model::get_func_interp(), solver::get_model(), goal::get_model(), optimize::get_model(), fixedpoint::get_num_levels(), expr::get_sort(), expr::get_string(), ast::hash(), tactic::help(), optimize::help(), sort::id(), func_decl::id(), expr::id(), z3::indexof(), z3::int2bv(), stats::is_double(), 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(), z3::ite(), expr::itos(), stats::key(), ast::kind(), z3::lambda(), z3::last_indexof(), expr::length(), expr::loop(), optimize::lower(), z3::mk_and(), z3::mk_or(), tactic::mk_solver(), sort::name(), func_decl::name(), solver::non_units(), expr::nth(), expr::num_args(), func_entry::num_args(), func_interp::num_entries(), expr::numerator(), optimize::objectives(), z3::operator!(), z3::operator!=(), z3::operator&(), z3::operator&&(), func_decl::operator()(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), ast_vector_tpl< expr >::operator[](), goal::operator[](), apply_result::operator[](), z3::operator|(), z3::operator||(), z3::par_and_then(), solver::pop(), z3::prefixof(), probe::probe(), solver::proof(), solver::push(), ast_vector_tpl< expr >::push_back(), fixedpoint::query(), func_decl::range(), z3::range(), z3::re_empty(), z3::re_full(), solver::reason_unknown(), z3::repeat(), expr::replace(), solver::reset(), ast_vector_tpl< expr >::resize(), fixedpoint::rules(), z3::select(), solver::set(), optimize::set(), fixedpoint::set(), func_interp::set_else(), z3::set_intersect(), z3::set_union(), expr::simplify(), z3::sqrt(), solver::statistics(), optimize::statistics(), fixedpoint::statistics(), expr::stoi(), z3::store(), expr::substitute(), z3::suffixof(), tactic::tactic(), z3::to_real(), solver::trail(), func_decl::transitive_closure(), z3::try_for(), stats::uint_value(), expr::unit(), solver::units(), solver::unsat_core(), optimize::unsat_core(), fixedpoint::update_rule(), optimize::upper(), func_entry::value(), z3::when(), and z3::with().

◆ ctx()

context& ctx ( ) const
inline

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

418 { return *m_ctx; }

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

Friends And Related Function Documentation

◆ check_context

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

Field Documentation

◆ m_ctx

context* m_ctx
protected
z3::object::m_ctx
context * m_ctx
Definition: z3++.h:414
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:187