CVC4::Statistics Class Reference

#include <statistics.h>

Inheritance diagram for CVC4::Statistics:

Public Types
typedef iterator	const_iterator
	An iterator type over a set of statistics. More...

Public Member Functions
	Statistics (const StatisticsBase &stats)
	Override the copy constructor to do a "deep" copy of statistics values. More...
	Statistics (const Statistics &stats)
	~Statistics ()
Statistics &	operator= (const StatisticsBase &stats)
	Override the assignment operator to do a "deep" copy of statistics values. More...
Statistics &	operator= (const Statistics &stats)
virtual void	setPrefix (const std::string &prefix)
	Set the output prefix for this set of statistics. More...
void	flushInformation (std::ostream &out) const
	Flush all statistics to the given output stream. More...
SExpr	getStatistic (std::string name) const
	Get the value of a named statistic. More...
const_iterator	begin () const
	Get an iterator to the beginning of the range of the set of statistics. More...
const_iterator	end () const
	Get an iterator to the end of the range of the set of statistics. More...

Protected Types
typedef std::set< Stat *, StatCmp >	StatSet
	A type for a set of statistics. More...

Protected Attributes
std::string	d_prefix
StatSet	d_stats
	The set of statistics in this object. More...

Static Protected Attributes
static std::string	s_regDelim

Detailed Description

Definition at line 103 of file statistics.h.

Member Typedef Documentation

typedef iterator CVC4::StatisticsBase::const_iterator

inherited

An iterator type over a set of statistics.

Definition at line 79 of file statistics.h.

typedef std::set< Stat*, StatCmp > CVC4::StatisticsBase::StatSet

protectedinherited

A type for a set of statistics.

Definition at line 46 of file statistics.h.

Constructor & Destructor Documentation

CVC4::Statistics::Statistics

(

const StatisticsBase &

stats

)

Override the copy constructor to do a "deep" copy of statistics values.

CVC4::Statistics::Statistics

(

const Statistics &

stats

)

CVC4::Statistics::~Statistics

(

)

Member Function Documentation

const_iterator CVC4::StatisticsBase::begin ( ) const

inherited

Get an iterator to the beginning of the range of the set of statistics.

const_iterator CVC4::StatisticsBase::end ( ) const

inherited

Get an iterator to the end of the range of the set of statistics.

void CVC4::StatisticsBase::flushInformation ( std::ostream &  out ) const

inherited

Flush all statistics to the given output stream.

SExpr CVC4::StatisticsBase::getStatistic ( std::string  name ) const

inherited

Get the value of a named statistic.

Statistics& CVC4::Statistics::operator=

(

const StatisticsBase &

stats

)

Override the assignment operator to do a "deep" copy of statistics values.

Statistics& CVC4::Statistics::operator=

(

const Statistics &

stats

)

virtual void CVC4::StatisticsBase::setPrefix ( const std::string &  prefix )

virtualinherited

Set the output prefix for this set of statistics.

Field Documentation

std::string CVC4::StatisticsBase::d_prefix

protectedinherited

Definition at line 48 of file statistics.h.

StatSet CVC4::StatisticsBase::d_stats

protectedinherited

The set of statistics in this object.

Definition at line 51 of file statistics.h.

std::string CVC4::StatisticsBase::s_regDelim

staticprotectedinherited

Definition at line 38 of file statistics.h.

---

The documentation for this class was generated from the following file:

• src/util/statistics.h