Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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.

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

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

:m_ctx(s.m_ctx) {}

Member Function Documentation

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

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

Referenced by FuncDeclRef::__call__(), ExprRef::__eq__(), ExprRef::__ne__(), solver::add(), goal::add(), tactic::apply(), probe::apply(), expr::arg(), ExprRef::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(), BoolSortRef::cast(), solver::check(), z3::cond(), z3::const_array(), apply_result::convert_model(), expr::decl(), ExprRef::decl(), func_decl::decl_kind(), goal::depth(), z3::distinct(), func_decl::domain(), FuncDeclRef::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(), SortRef::kind(), tactic::mk_solver(), func_decl::name(), SortRef::name(), FuncDeclRef::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(), FuncDeclRef::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(), ExprRef::sort(), BoolRef::sort(), 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().

{ return *m_ctx; }

Friends And Related Function Documentation

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

Field Documentation

context* m_ctx [protected]
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines