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

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)

virtual	~object ()=default

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

Constructor & Destructor Documentation

stats ( context & c )

inline

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

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

z3::object::object

object(context &c)

Definition: z3++.h:538

stats	(	context &	c,
		Z3_stats	e
	)

inline

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

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

z3::object::object

object(context &c)

Definition: z3++.h:538

stats ( stats const & s )

inline

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

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

z3::object::object

object(context &c)

Definition: z3++.h:538

~stats ( )

inlineoverride

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

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

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.

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

Member Function Documentation

double double_value ( unsigned i ) const

inline

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

2841 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

bool is_double ( unsigned i ) const

inline

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

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

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

bool is_uint ( unsigned i ) const

inline

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

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

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

std::string key ( unsigned i ) const

inline

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

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

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

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.

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

Z3_string

const char * Z3_string

Z3 string type. It is just an alias for const char *.

Definition: z3_api.h:50

operator Z3_stats ( ) const

inline

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

2828 { return m_stats; }

stats& operator= ( stats const & s )

inline

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