#include <z3++.h>
Definition at line 2686 of file z3++.h.
◆ stats() [1/3]
◆ stats() [2/3]
Definition at line 2694 of file z3++.h.
2694:object(c) { init(e); }
◆ stats() [3/3]
Definition at line 2695 of file z3++.h.
2695:object(s) { init(s.m_stats); }
◆ ~stats()
Definition at line 2696 of file z3++.h.
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
◆ double_value()
double double_value |
( |
unsigned | i | ) |
const |
|
inline |
Definition at line 2710 of file z3++.h.
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.
◆ is_double()
bool is_double |
( |
unsigned | i | ) |
const |
|
inline |
Definition at line 2708 of file z3++.h.
bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a double.
◆ is_uint()
bool is_uint |
( |
unsigned | i | ) |
const |
|
inline |
Definition at line 2707 of file z3++.h.
bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a unsigned integer.
◆ key()
std::string key |
( |
unsigned | i | ) |
const |
|
inline |
Definition at line 2706 of file z3++.h.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
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.
◆ operator Z3_stats()
operator Z3_stats |
( |
| ) |
const |
|
inline |
◆ operator=()
Definition at line 2698 of file z3++.h.
2698 {
2701 object::operator=(s);
2702 m_stats = s.m_stats;
2703 return *this;
2704 }
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
◆ size()
Definition at line 2705 of file z3++.h.
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 2709 of file z3++.h.
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.
◆ operator<<
std::ostream & operator<< |
( |
std::ostream & | out, |
|
|
stats const & | s ) |
|
friend |
Definition at line 2713 of file z3++.h.
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.