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
Friends
std::ostream &	operator<< (std::ostream &out, stats const &s)

---

Detailed Description

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

---

Constructor & Destructor Documentation

stats

(

context &

c

)

[inline]

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

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

stats	(	context &	c,
		Z3_stats	e
	)		[inline]

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

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

stats

(

stats const &

s

)

[inline]

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

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

~stats

(

)

[inline]

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

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

---

Member Function Documentation

double double_value

(

unsigned

i

)

const [inline]

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

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

bool is_double

(

unsigned

i

)

const [inline]

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

{ Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }

bool is_uint

(

unsigned

i

)

const [inline]

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

{ Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }

std::string key

(

unsigned

i

)

const [inline]

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

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

operator Z3_stats

(

)

const [inline]

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

{ return m_stats; }

stats& operator=

(

stats const &

s

)

[inline]

Definition at line 1222 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; 
        }

unsigned size

(

)

const [inline]

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

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

unsigned uint_value

(

unsigned

i

)

const [inline]

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

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

---

Friends And Related Function Documentation

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

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

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