Public Member Functions | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
void | check_error () const |
Protected Attributes | |
context * | m_ctx |
Friends | |
void | check_context (object const &a, object const &b) |
|
inline |
Definition at line 273 of file z3++.h.
Referenced by solver::add(), goal::add(), tactic::apply(), probe::apply(), expr::arg(), func_entry::arg(), sort::array_domain(), sort::array_range(), solver::assertions(), expr::body(), sort::bv_size(), solver::check(), z3::const_array(), apply_result::convert_model(), expr::decl(), func_decl::domain(), stats::double_value(), func_interp::else_value(), func_interp::entry(), model::eval(), z3::exists(), z3::fail_if(), z3::forall(), model::get_const_decl(), model::get_const_interp(), model::get_func_decl(), model::get_func_interp(), solver::get_model(), expr::get_sort(), ast::hash(), tactic::help(), stats::is_double(), stats::is_uint(), expr::is_well_sorted(), z3::ite(), stats::key(), ast::kind(), tactic::mk_solver(), func_decl::name(), expr::num_args(), func_entry::num_args(), func_interp::num_entries(), func_decl::operator()(), ast_vector_tpl< T >::operator[](), goal::operator[](), apply_result::operator[](), solver::pop(), probe::probe(), solver::proof(), solver::push(), ast_vector_tpl< T >::push_back(), z3::pw(), func_decl::range(), solver::reason_unknown(), z3::repeat(), solver::reset(), ast_vector_tpl< T >::resize(), z3::select(), solver::set(), expr::simplify(), solver::statistics(), z3::store(), expr::substitute(), tactic::tactic(), z3::to_real(), z3::try_for(), stats::uint_value(), solver::unsat_core(), func_entry::value(), z3::when(), and z3::with().
|
inline |
Definition at line 272 of file z3++.h.
Referenced by solver::add(), goal::add(), tactic::apply(), probe::apply(), expr::arg(), func_entry::arg(), func_decl::arity(), sort::array_domain(), sort::array_range(), goal::as_expr(), solver::assertions(), ast::ast(), ast_vector_tpl< T >::ast_vector_tpl(), expr::body(), sort::bv_size(), solver::check(), z3::cond(), z3::const_array(), apply_result::convert_model(), expr::decl(), func_decl::decl_kind(), goal::depth(), z3::distinct(), func_decl::domain(), stats::double_value(), func_interp::else_value(), func_interp::entry(), z3::eq(), model::eval(), z3::exists(), z3::fail_if(), z3::forall(), context::function(), z3::function(), model::get_const_decl(), model::get_const_interp(), model::get_func_decl(), model::get_func_interp(), solver::get_model(), ast::hash(), tactic::help(), z3::implies(), goal::inconsistent(), goal::is_decided_sat(), goal::is_decided_unsat(), stats::is_double(), stats::is_uint(), expr::is_well_sorted(), z3::ite(), stats::key(), symbol::kind(), ast::kind(), tactic::mk_solver(), func_decl::name(), expr::num_args(), func_entry::num_args(), model::num_consts(), func_interp::num_entries(), goal::num_exprs(), model::num_funcs(), func_decl::operator()(), params::operator=(), ast::operator=(), ast_vector_tpl< T >::operator=(), func_entry::operator=(), func_interp::operator=(), model::operator=(), stats::operator=(), solver::operator=(), goal::operator=(), apply_result::operator=(), tactic::operator=(), probe::operator=(), ast_vector_tpl< T >::operator[](), goal::operator[](), apply_result::operator[](), params::params(), solver::pop(), goal::precision(), solver::proof(), solver::push(), ast_vector_tpl< T >::push_back(), z3::pw(), func_decl::range(), solver::reason_unknown(), z3::repeat(), solver::reset(), goal::reset(), ast_vector_tpl< T >::resize(), z3::select(), params::set(), solver::set(), expr::simplify(), ast_vector_tpl< T >::size(), stats::size(), goal::size(), apply_result::size(), solver::statistics(), z3::store(), symbol::str(), expr::substitute(), symbol::to_int(), z3::to_real(), z3::try_for(), z3::udiv(), z3::uge(), z3::ugt(), stats::uint_value(), z3::ule(), z3::ult(), solver::unsat_core(), func_entry::value(), z3::when(), z3::with(), apply_result::~apply_result(), ast_vector_tpl< T >::~ast_vector_tpl(), func_entry::~func_entry(), func_interp::~func_interp(), goal::~goal(), model::~model(), params::~params(), probe::~probe(), solver::~solver(), stats::~stats(), and tactic::~tactic().
Definition at line 276 of file z3++.h.
Referenced by goal::add(), tactic::apply(), solver::check(), apply_result::convert_model(), model::eval(), model::get_const_interp(), model::get_func_interp(), and func_decl::operator()().
|
protected |
Definition at line 268 of file z3++.h.
Referenced by z3::check_context(), object::ctx(), expr::get_sort(), symbol::operator=(), params::operator=(), ast::operator=(), ast_vector_tpl< T >::operator=(), func_entry::operator=(), func_interp::operator=(), model::operator=(), stats::operator=(), solver::operator=(), goal::operator=(), apply_result::operator=(), tactic::operator=(), probe::operator=(), sort::sort_kind(), and ast::~ast().