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)
	object (object const &s)
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 2324 of file z3++.h.

Constructor & Destructor Documentation

stats() [1/3]

stats ( context &  c )

inline

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

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

stats() [2/3]

stats ( context &  c, Z3_stats  e  )

inline

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

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

stats() [3/3]

stats ( stats const &  s )

inline

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

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

~stats()

~stats ( )

inline

Definition at line 2334 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 2348 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 2346 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 2345 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 2344 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 2335 of file z3++.h.

{ return m_stats; }

operator=()

stats& operator= ( stats const &  s )

inline

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

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

size()

unsigned size ( ) const

inline

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

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

uint_value()

unsigned uint_value ( unsigned  i ) const

inline

Definition at line 2347 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 2351 of file z3++.h.

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