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 278 of file z3++.h.
Referenced by z3::const_array(), z3::exists(), z3::fail_if(), z3::forall(), z3::ite(), z3::pw(), z3::repeat(), z3::select(), z3::store(), z3::to_real(), z3::try_for(), z3::when(), and z3::with().
|
inline |
Definition at line 277 of file z3++.h.
Referenced by z3::concat(), z3::cond(), z3::const_array(), z3::distinct(), z3::eq(), z3::exists(), z3::fail_if(), z3::forall(), context::function(), z3::function(), z3::implies(), z3::ite(), 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=(), z3::pw(), z3::repeat(), z3::select(), z3::store(), z3::to_real(), z3::try_for(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), z3::when(), and z3::with().
|
protected |
Definition at line 273 of file z3++.h.
Referenced by z3::check_context(), 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=(), and probe::operator=().