object Class Reference

Inheritance diagram for object:

Public Member Functions
	object (context &c)
	object (object const &s)
context &	ctx () const
Z3_error_code	check_error () const

Protected Attributes
context *	m_ctx

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

Detailed Description

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

Constructor & Destructor Documentation

object() [1/2]

object ( context &  c )

inline

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

:m_ctx(&c) {}

object() [2/2]

object ( object const &  s )

inline

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

:m_ctx(s.m_ctx) {}

Member Function Documentation

check_error()

Z3_error_code check_error ( ) const

inline

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

Referenced by z3::abs(), z3::as_array(), z3::bv2int(), z3::bvadd_no_overflow(), z3::bvadd_no_underflow(), z3::bvmul_no_overflow(), z3::bvmul_no_underflow(), z3::bvneg_no_overflow(), z3::bvsdiv_no_overflow(), z3::bvsub_no_overflow(), z3::bvsub_no_underflow(), z3::empty(), z3::exists(), z3::fail_if(), z3::forall(), z3::indexof(), z3::int2bv(), z3::ite(), z3::lambda(), z3::last_indexof(), 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::par_and_then(), z3::prefixof(), z3::range(), z3::re_empty(), z3::re_full(), z3::repeat(), z3::select(), z3::set_intersect(), z3::set_union(), z3::sqrt(), z3::store(), z3::suffixof(), z3::to_real(), z3::try_for(), z3::when(), and z3::with().

{ return m_ctx->check_error(); }

ctx()

context& ctx ( ) const

inline

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

Referenced by z3::abs(), z3::as_array(), z3::ashr(), ast_vector_tpl< expr >::ast_vector_tpl(), z3::atleast(), z3::atmost(), z3::bv2int(), z3::bvadd_no_overflow(), z3::bvadd_no_underflow(), z3::bvmul_no_overflow(), z3::bvmul_no_underflow(), z3::bvneg_no_overflow(), z3::bvsdiv_no_overflow(), z3::bvsub_no_overflow(), z3::bvsub_no_underflow(), z3::concat(), z3::cond(), z3::distinct(), z3::empty(), z3::eq(), z3::exists(), z3::fail_if(), z3::fma(), z3::forall(), context::function(), z3::function(), z3::implies(), z3::indexof(), z3::int2bv(), z3::ite(), z3::lambda(), z3::last_indexof(), z3::linear_order(), z3::lshr(), z3::max(), z3::min(), z3::mk_and(), z3::mk_or(), z3::mod(), model::model(), z3::nand(), z3::nor(), 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< expr >::operator=(), func_entry::operator=(), func_interp::operator=(), model::operator=(), stats::operator=(), solver::operator=(), goal::operator=(), apply_result::operator=(), tactic::operator=(), probe::operator=(), optimize::operator=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::operator^(), z3::operator|(), z3::operator||(), z3::operator~(), optimize::optimize(), z3::par_and_then(), z3::partial_order(), z3::pbeq(), z3::pbge(), z3::pble(), z3::piecewise_linear_order(), z3::prefixof(), user_propagator_base::propagate(), z3::pw(), z3::range(), z3::re_empty(), z3::re_full(), z3::re_intersect(), context::recdef(), z3::recfun(), z3::rem(), z3::repeat(), z3::select(), ast_vector_tpl< T >::iterator::set(), z3::set_intersect(), z3::set_union(), z3::sext(), z3::shl(), z3::sle(), z3::slt(), z3::smod(), solver::solver(), z3::sqrt(), z3::srem(), z3::store(), z3::suffixof(), z3::sum(), z3::to_real(), z3::tree_order(), z3::try_for(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), z3::urem(), z3::when(), z3::with(), z3::xnor(), and z3::zext().

{ return *m_ctx; }

Friends And Related Function Documentation

check_context

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

friend

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

{ (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }

Field Documentation

m_ctx

context* m_ctx

protected

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

Referenced by z3::check_context(), symbol::operator=(), param_descrs::operator=(), params::operator=(), ast::operator=(), ast_vector_tpl< expr >::operator=(), func_entry::operator=(), func_interp::operator=(), model::operator=(), stats::operator=(), solver::operator=(), goal::operator=(), apply_result::operator=(), tactic::operator=(), probe::operator=(), and optimize::operator=().