Public Member Functions | |
stats (context &c) | |
stats (context &c, Z3_stats e) | |
stats (stats const &s) | |
~stats () | |
operator Z3_stats () const | |
stats & | operator= (stats const &s) |
unsigned | size () const |
std::string | key (unsigned i) const |
bool | is_uint (unsigned i) const |
bool | is_double (unsigned i) const |
unsigned | uint_value (unsigned i) const |
double | double_value (unsigned i) const |
Friends | |
std::ostream & | operator<< (std::ostream &out, stats const &s) |
~stats | ( | ) | [inline] |
Definition at line 1220 of file z3++.h.
{ if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
double double_value | ( | unsigned | i | ) | const [inline] |
Definition at line 1234 of file z3++.h.
{ double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
bool is_double | ( | unsigned | i | ) | const [inline] |
Definition at line 1232 of file z3++.h.
{ Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
bool is_uint | ( | unsigned | i | ) | const [inline] |
Definition at line 1231 of file z3++.h.
{ Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
std::string key | ( | unsigned | i | ) | const [inline] |
Definition at line 1230 of file z3++.h.
{ Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
Definition at line 1222 of file z3++.h.
{ Z3_stats_inc_ref(s.ctx(), s.m_stats); if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); m_ctx = s.m_ctx; m_stats = s.m_stats; return *this; }
unsigned size | ( | ) | const [inline] |
Definition at line 1229 of file z3++.h.
{ return Z3_stats_size(ctx(), m_stats); }
unsigned uint_value | ( | unsigned | i | ) | const [inline] |
Definition at line 1233 of file z3++.h.
{ unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
std::ostream& operator<< | ( | std::ostream & | out, |
stats const & | s | ||
) | [friend] |
Definition at line 1235 of file z3++.h.
{ out << Z3_stats_to_string(s.ctx(), s); return out; }