Z3
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
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Friends

std::ostream & operator<< (std::ostream &out, stats const &s)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

§ stats() [1/3]

stats ( context c)
inline

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

1655 :object(c), m_stats(0) {}
object(context &c)
Definition: z3++.h:330

§ stats() [2/3]

stats ( context c,
Z3_stats  e 
)
inline

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

1656 :object(c) { init(e); }
object(context &c)
Definition: z3++.h:330

§ stats() [3/3]

stats ( stats const &  s)
inline

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

1657 :object(s) { init(s.m_stats); }
object(context &c)
Definition: z3++.h:330

§ ~stats()

~stats ( )
inline

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

1658 { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.

Member Function Documentation

§ double_value()

double double_value ( unsigned  i) const
inline

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

1672 { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ is_double()

bool is_double ( unsigned  i) const
inline

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

1670 { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
Z3_bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a double.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Definition: z3_api.h:84
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ is_uint()

bool is_uint ( unsigned  i) const
inline

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

1669 { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Definition: z3_api.h:84
context & ctx() const
Definition: z3++.h:332
Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
void check_error() const
Definition: z3++.h:333

§ key()

std::string key ( unsigned  i) const
inline

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

1668 { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
context & ctx() const
Definition: z3++.h:332
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
void check_error() const
Definition: z3++.h:333
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:89

§ operator Z3_stats()

operator Z3_stats ( ) const
inline

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

1659 { return m_stats; }

§ operator=()

stats& operator= ( stats const &  s)
inline

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

1660  {
1661  Z3_stats_inc_ref(s.ctx(), s.m_stats);
1662  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
1663  m_ctx = s.m_ctx;
1664  m_stats = s.m_stats;
1665  return *this;
1666  }
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
context * m_ctx
Definition: z3++.h:328
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.

§ size()

unsigned size ( ) const
inline

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

1667 { return Z3_stats_size(ctx(), m_stats); }
context & ctx() const
Definition: z3++.h:332
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.

§ uint_value()

unsigned uint_value ( unsigned  i) const
inline

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

1671 { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

Friends And Related Function Documentation

§ operator<<

std::ostream& operator<< ( std::ostream &  out,
stats const &  s 
)
friend

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

1675 { out << Z3_stats_to_string(s.ctx(), s); return out; }
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.