Z3
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 271 of file z3++.h.

Constructor & Destructor Documentation

object ( context c)
inline

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

275 :m_ctx(&c) {}
context * m_ctx
Definition: z3++.h:273
object ( object const &  s)
inline

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

276 :m_ctx(s.m_ctx) {}
context * m_ctx
Definition: z3++.h:273

Member Function Documentation

void check_error ( ) const
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().

278 { m_ctx->check_error(); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
context * m_ctx
Definition: z3++.h:273
context& ctx ( ) const
inline

Friends And Related Function Documentation

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

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

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

Field Documentation

context* m_ctx
protected