cvc4-1.4
|
#include <statistics.h>
Data Structures | |
class | iterator |
struct | StatCmp |
A helper class for comparing two statistics. More... | |
Public Types | |
typedef iterator | const_iterator |
An iterator type over a set of statistics. More... | |
Public Member Functions | |
virtual | ~StatisticsBase () |
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 Member Functions | |
StatisticsBase () | |
StatisticsBase (const StatisticsBase &stats) | |
StatisticsBase & | operator= (const StatisticsBase &stats) |
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 |
Definition at line 35 of file statistics.h.
An iterator type over a set of statistics.
Definition at line 79 of file statistics.h.
|
protected |
A type for a set of statistics.
Definition at line 46 of file statistics.h.
|
protected |
|
protected |
|
inlinevirtual |
Definition at line 59 of file statistics.h.
const_iterator CVC4::StatisticsBase::begin | ( | ) | const |
Get an iterator to the beginning of the range of the set of statistics.
const_iterator CVC4::StatisticsBase::end | ( | ) | const |
Get an iterator to the end of the range of the set of statistics.
void CVC4::StatisticsBase::flushInformation | ( | std::ostream & | out | ) | const |
Flush all statistics to the given output stream.
SExpr CVC4::StatisticsBase::getStatistic | ( | std::string | name | ) | const |
Get the value of a named statistic.
|
protected |
|
virtual |
Set the output prefix for this set of statistics.
|
protected |
Definition at line 48 of file statistics.h.
|
protected |
The set of statistics in this object.
Definition at line 51 of file statistics.h.
|
staticprotected |
Definition at line 38 of file statistics.h.