Definition at line 2324 of file z3++.h.
◆ stats() [1/3]
◆ stats() [2/3]
◆ stats() [3/3]
◆ ~stats()
◆ double_value()
double double_value |
( |
unsigned |
i | ) |
const |
|
inline |
◆ is_double()
bool is_double |
( |
unsigned |
i | ) |
const |
|
inline |
◆ is_uint()
bool is_uint |
( |
unsigned |
i | ) |
const |
|
inline |
◆ key()
std::string key |
( |
unsigned |
i | ) |
const |
|
inline |
◆ operator Z3_stats()
operator Z3_stats |
( |
| ) |
const |
|
inline |
◆ operator=()
Definition at line 2336 of file z3++.h.
2340 m_stats = s.m_stats;
◆ size()
◆ uint_value()
unsigned uint_value |
( |
unsigned |
i | ) |
const |
|
inline |
◆ operator<<
std::ostream& operator<< |
( |
std::ostream & |
out, |
|
|
stats const & |
s |
|
) |
| |
|
friend |
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.
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.
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.
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
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.
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
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.
Z3_error_code check_error() const
const typedef char * Z3_string
Z3 string type. It is just an alias for const char *.