Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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 244 of file z3++.h.

Constructor & Destructor Documentation

object ( context c)
inline

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

:m_ctx(&c) {}
object ( object const &  s)
inline

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

:m_ctx(s.m_ctx) {}

Member Function Documentation

void check_error ( ) const
inline
context& ctx ( ) const
inline

Definition at line 250 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(), 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(), func_decl::domain(), stats::double_value(), func_interp::else_value(), func_interp::entry(), 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(), goal::inconsistent(), goal::is_decided_sat(), goal::is_decided_unsat(), stats::is_double(), stats::is_uint(), expr::is_well_sorted(), 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(), func_decl::range(), solver::reason_unknown(), 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(), symbol::to_int(), z3::to_real(), z3::udiv(), z3::uge(), z3::ugt(), stats::uint_value(), z3::ule(), z3::ult(), solver::unsat_core(), func_entry::value(), z3::when(), 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().

{ return *m_ctx; }

Friends And Related Function Documentation

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

Field Documentation

context* m_ctx
protected