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 333 of file z3++.h.
Referenced by z3::empty(), z3::exists(), z3::fail_if(), z3::forall(), z3::implies(), z3::in_re(), z3::indexof(), z3::ite(), z3::mk_and(), z3::mk_or(), z3::operator &(), z3::operator &&(), z3::operator!(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::operator|(), z3::operator||(), z3::option(), z3::plus(), z3::prefixof(), z3::pw(), z3::repeat(), z3::select(), z3::set_intersect(), z3::set_union(), z3::star(), z3::store(), z3::suffixof(), z3::to_re(), z3::to_real(), z3::try_for(), z3::when(), and z3::with().
|
inline |
Definition at line 332 of file z3++.h.
Referenced by z3::ashr(), z3::concat(), z3::cond(), z3::distinct(), z3::empty(), z3::eq(), z3::exists(), z3::fail_if(), z3::forall(), context::function(), z3::function(), z3::implies(), z3::in_re(), z3::indexof(), z3::interpolant(), z3::ite(), z3::lshr(), z3::mk_and(), z3::mk_or(), z3::operator &(), z3::operator &&(), z3::operator!(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<<(), z3::operator<=(), param_descrs::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=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::operator^(), z3::operator|(), z3::operator||(), z3::operator~(), z3::option(), z3::plus(), z3::prefixof(), z3::pw(), z3::repeat(), z3::select(), z3::set_intersect(), z3::set_union(), z3::sext(), z3::shl(), solver::solver(), z3::srem(), z3::star(), z3::store(), z3::suffixof(), z3::to_re(), z3::to_real(), z3::try_for(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), z3::urem(), z3::when(), z3::with(), and z3::zext().
|
protected |
Definition at line 328 of file z3++.h.
Referenced by z3::check_context(), symbol::operator=(), param_descrs::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=().