Z3 |

Public Member Functions | Friends
stats Class Reference

`#include <z3++.h>`

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
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
Public Member Functions inherited from object
| object (context &c)
context & | ctx () const
Z3_error_code | check_error () const

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

## Additional Inherited Members
Protected Attributes inherited from object
context * | m_ctx

## Detailed Description

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

## Constructor & Destructor Documentation

## ◆ stats() [1/3]

stats | ( | context & | c | ) |
| inline

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

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

Referenced by Statistics::__deepcopy__(), Statistics::__del__(), Statistics::__getitem__(), Statistics::__len__(), Statistics::__repr__(), Statistics::get_key_value(), and Statistics::keys().

## ◆ stats() [2/3]

stats | ( | context & | c,
|  | Z3_stats | e
| ) |  |
| inline

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

2522:object(c) { init(e); }

Referenced by Statistics::__deepcopy__(), Statistics::__del__(), Statistics::__getitem__(), Statistics::__len__(), Statistics::__repr__(), Statistics::get_key_value(), and Statistics::keys().

## ◆ stats() [3/3]

stats | ( | stats const & | s | ) |
| inline

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

2523:object(s) { init(s.m_stats); }

Referenced by Statistics::__deepcopy__(), Statistics::__del__(), Statistics::__getitem__(), Statistics::__len__(), Statistics::__repr__(), Statistics::get_key_value(), and Statistics::keys().

## ◆ ~stats()

~stats | ( |  | ) |
| inline

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

2524{ if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_stats_dec_ref
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 2538 of file z3++.h.

2538{ double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_stats_get_double_value
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 2536 of file z3++.h.

2536{ bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
Z3_stats_is_double
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 2535 of file z3++.h.

2535{ bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
Z3_stats_is_uint
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 2534 of file z3++.h.

2534{ Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
Z3_string
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:84
Z3_stats_get_key
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

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

2525{ return m_stats; }

## ◆ operator=()

stats & operator= | ( | stats const & | s | ) |
| inline

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

2526 {
2527 Z3_stats_inc_ref(s.ctx(), s.m_stats);
2528 if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
2529 object::operator=(s);
2530 m_stats = s.m_stats;
2531 return *this;
2532 }
Z3_stats_inc_ref
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 2533 of file z3++.h.

2533{ return Z3_stats_size(ctx(), m_stats); }
Z3_stats_size
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.

Referenced by ParamDescrsRef::__len__(), Goal::__len__(), BitVecNumRef::as_signed_long(), and BitVecSortRef::subsort().

## ◆ uint_value()

unsigned uint_value | ( | unsigned | i | ) | const
| inline

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

2537{ unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
Z3_stats_get_uint_value
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.

## Friends And Related Function Documentation

## ◆ operator<<

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

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

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