Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
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
 
void check_error () const
 

Protected Attributes

contextm_ctx
 

Friends

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

Detailed Description

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

Constructor & Destructor Documentation

object ( context c)
inline

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

270 :m_ctx(&c) {}
context * m_ctx
Definition: z3++.h:268
object ( object const &  s)
inline

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

271 :m_ctx(s.m_ctx) {}
context * m_ctx
Definition: z3++.h:268

Member Function Documentation

void check_error ( ) const
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().

273 { m_ctx->check_error(); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
context * m_ctx
Definition: z3++.h:268
context& ctx ( ) const
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().

272 { return *m_ctx; }
context * m_ctx
Definition: z3++.h:268

Friends And Related Function Documentation

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

Field Documentation

context* m_ctx
protected