Z3
 
Loading...
Searching...
No Matches
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 () override
 
 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)
 
virtual ~object ()=default
 
contextctx () 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
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

◆ stats() [1/3]

◆ stats() [2/3]

◆ stats() [3/3]

◆ ~stats()

~stats ( )
inlineoverride

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

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

2710{ double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
Z3_error_code check_error() const
Definition z3++.h:475
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.

2708{ bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
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.

2707{ bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
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.

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

2697{ return m_stats; }

◆ operator=()

stats & operator= ( stats const & s)
inline

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

2698 {
2699 Z3_stats_inc_ref(s.ctx(), s.m_stats);
2700 if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
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()

unsigned size ( ) const
inline

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

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

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

◆ uint_value()

unsigned uint_value ( unsigned i) const
inline

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

2709{ 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.

Friends And Related Symbol Documentation

◆ operator<<

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

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

2713{ 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.