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
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() [1/3]

stats ( context & c )

inline

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

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

Referenced by operator<<, operator=(), and stats().

stats() [2/3]

stats ( context & c, Z3_stats e )

inline

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

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

stats() [3/3]

stats ( stats const & s )

inline

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

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

~stats()

~stats ( )

inlineoverride

Definition at line 2827 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 2841 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 2839 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 2838 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 2837 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 2828 of file z3++.h.

{ return m_stats; }

operator=()

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;
        }

size()

unsigned size ( ) const

inline

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

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

uint_value()

unsigned uint_value ( unsigned i ) const

inline

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

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

Friends And Related Symbol Documentation

operator<<

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

friend

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

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