Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Friends
stats Class Reference
+ Inheritance diagram for stats:

Public Member Functions

 stats (context &c)
 stats (context &c, Z3_stats e)
 stats (stats const &s)
 ~stats ()
 operator Z3_stats () const
statsoperator= (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)

Detailed Description

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


Constructor & Destructor Documentation

stats ( context c) [inline]

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

:object(c), m_stats(0) {}
stats ( context c,
Z3_stats  e 
) [inline]

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

:object(c) { init(e); }
stats ( stats const &  s) [inline]

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

:object(s) { init(s.m_stats); }
~stats ( ) [inline]

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

{ if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }

Member Function Documentation

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; }
operator Z3_stats ( ) const [inline]

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

{ return m_stats; }
stats& operator= ( stats const &  s) [inline]

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; }

Friends And Related Function Documentation

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; }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines