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
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 2644 of file z3++.h.

Constructor & Destructor Documentation

stats() [1/3]

stats ( context &  c )

inline

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

:object(c), m_stats(0) {}

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 2652 of file z3++.h.

: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 2653 of file z3++.h.

: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 2654 of file z3++.h.

{ if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }

Member Function Documentation

double_value()

double double_value ( unsigned  i ) const

inline

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

{ double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }

is_double()

bool is_double ( unsigned  i ) const

inline

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

{ bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }

is_uint()

bool is_uint ( unsigned  i ) const

inline

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

{ bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }

key()

std::string key ( unsigned  i ) const

inline

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

{ Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }

operator Z3_stats()

operator Z3_stats ( ) const

inline

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

{ return m_stats; }

operator=()

stats& operator= ( stats const &  s )

inline

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

                                           {
            Z3_stats_inc_ref(s.ctx(), s.m_stats);
            if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
            object::operator=(s);
            m_stats = s.m_stats;
            return *this;
        }

size()

unsigned size ( ) const

inline

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

{ return Z3_stats_size(ctx(), m_stats); }

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 2667 of file z3++.h.

{ unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }

Friends And Related Function Documentation

operator<<

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

friend

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

{ out << Z3_stats_to_string(s.ctx(), s); return out; }