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 only shows statistics that are both public and changed. The Statistics::begin() method has Boolean flags internal and def to also show internal statistics and defaulted statistics, respectively.

• 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. Once obtained via Solver::getStatistics() , an instance of this class is independent of the Solver object: it will not change when the solvers internal statistics do, and it will not be invalidated if the solver is 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 = false , bool defaulted = false ) 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 value is intended for internal use only.

Returns :

True if this is an internal statistic.

bool isDefault ( ) const 

Determine if this value holds the default value.

Returns :

True if this is a defaulted statistic.

bool isInt ( ) const 

Determine if this value is an integer.

Returns :

True if this value is an integer.

int64_t getInt ( ) const 

Return the integer value.

Returns :

The integer value.

bool isDouble ( ) const 

Determine if this value is a double.

Returns :

True if this value is a double.

double getDouble ( ) const 

Return the double value.

Returns :

The double value.

bool isString ( ) const 

Determine if this value is a string.

Returns :

True if this value is a string.

const std :: string & getString ( ) const 

Return the string value.

Returns :

The string value.

bool isHistogram ( ) const 

Determine if this value is a histogram.

Returns :

True if this value is a histogram.

const HistogramData & getHistogram ( ) const 

Return the histogram value.

Returns :

The histogram value.

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 & sv ) 

Print a Stat object to an std::ostream .