Statistics 

See Statistics for general information on statistics in cvc5.

Class cvc5::Statistics represents a mapping from statistic names (as std::string ) to statistic values, which are represented by class cvc5::Stat . A cvc5::Stat may hold values of different types ( int64_t , double , std::string and histograms) and can be inspected by identifying the type ( Stat::isInt() , Stat::isDouble() , etc) and obtaining the actual value ( Stat::getInt() , Stat::getDouble() , etc). Histograms are represented as std::map<std::string, uint64_t> where the key is the string representation of one enumeration value and the value is the frequency of this particular value.

By default, iterating over a Statistics object shows all statistics, including internal and unchanged ones. The inclusion of internal and defaulted statistics can be configured via Boolean parameters internal and defaulted of function Statistics::begin() .

• class cvc5::Statistics

• std::ostream& cvc5::operator<< (std::ostream& out, const Statistics& s)

• class cvc5::Stat

• std::ostream& cvc5::operator<< (std::ostream& out, const Stat& s)

class Statistics 

Represents a snapshot of the solver statistics. See Statistics for how statistics can be used.

Statistics can be queried from the Solver via Solver::getStatistics() , and from the TermManager via TermManager::getStatistics() . An statistics instance obtained from either call is independent of the Solver (and its associated :cpp:class: ` TermManager <cvc5::TermManager>`object: it will not change when new terms are created or the solver’s internal statistics do. It will also not be invalidated if the solver/term manageris destroyed.

Iterating over this class (via begin() and end() ) shows only public statistics that have been changed. By passing appropriate flags to begin() , statistics that are internal, defaulted, or both, can be included as well. A single statistic value is represented as Stat .

Public Functions

const Stat & get ( const std :: string & name ) 

Retrieve the statistic with the given name.

Note

Asserts that a statistic with the given name actually exists and throws a CVC5ApiRecoverableException if it does not.

Parameters :

name – The name of the statistic.

Returns :

The statistic with the given name.

iterator begin ( bool internal = true , bool defaulted = true ) const 

Begin iteration over the statistics values. By default, only entries that are public and have been set are visible while the others are skipped.

Parameters :

• internal – If set to true, internal statistics are shown as well.

• defaulted – If set to true, defaulted statistics are shown as well.

iterator end ( ) const 

End iteration

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const Statistics & stats ) 

class Stat 

Represents a snapshot of a single statistic value. See Statistics for how statistics can be used. A value can be of type int64_t , double , std::string or a histogram ( std::map<std::string, uint64_t> ). The value type can be queried (using isInt() , isDouble() , etc.) and the stored value can be accessed (using getInt() , getDouble() , etc.). It is possible to query whether this statistic is an internal statistic by isInternal() and whether its value is the default value by isDefault() .

Public Types

using HistogramData = std :: map < std :: string , uint64_t > 

Representation of a histogram: maps names to frequencies.

Public Functions

Stat ( ) 

Create an empty statistics object. On such an object all isX() return false and all getX() throw an API exception. It solely exists because it makes implementing bindings for other languages much easier.

Stat ( const Stat & s ) 

Copy constructor

~Stat ( ) 

Destructor

Stat & operator = ( const Stat & s ) 

Copy assignment

bool isInternal ( ) const 

Determine if this statistic is intended for internal use only.

Returns :

True if this is an internal statistic.

bool isDefault ( ) const 

Determine if this statistic holds the default value.

Returns :

True if this is a defaulted statistic.

bool isInt ( ) const 

Determine if this statistic holds an integer value.

Returns :

True if this value is an integer.

int64_t getInt ( ) const 

Get the value of an integer statistic.

Returns :

The integer value.

bool isDouble ( ) const 

Determine if this statistic holds a double value.

Returns :

True if this value is a double.

double getDouble ( ) const 

Get the value of a double statistic.

Returns :

The double value.

bool isString ( ) const 

Determine if this statistic holds a string value.

Returns :

True if this value is a string.

const std :: string & getString ( ) const 

Get the value of a string statistic.

Returns :

The string value.

bool isHistogram ( ) const 

Determine if this statistics holds a histogram.

Returns :

True if this value is a histogram.

const HistogramData & getHistogram ( ) const 

Get the value of a histogram statistic.

Returns :

The histogram value.

std :: string toString ( ) const 

Get a string represenation of this statistic.

Returns :

The string represenation.

Friends

friend class Statistics

friend std :: ostream & operator << ( std :: ostream & os , const Stat & sv ) 

Print a Stat object to an std::ostream .

std :: ostream & cvc5 :: operator << ( std :: ostream & os , const Stat & stat ) 

Print a Stat object to an std::ostream .