Cvc5Statistics 

See Statistics for general information on statistics in cvc5.

Struct cvc5::Statistics represents a mapping from statistic names to statistic values, which are represented by struct Cvc5Stat . A Cvc5Stat may hold values of different types ( bool , int64_t , uint64_t , double , const char* and histograms) and can be inspected by identifying the type via functions cvc5_stat_is_<type> and obtaining the actual value via functions cvc5_stat_get_<type> . Histograms are represented as a paar of arrays ( const char** keys[] and uint64_t* values[] ) where the key is the string representation of one enumeration value and the value is the frequency of this particular value.

A statistics iterator can be initialized via cvc5_stats_iter_init() , which allows to configure the visbility of internal and unchanged statistic entries. Iteration over statistics entries is then provided via functions cvc5_stats_iter_has_next() and cvc5_stats_iter_next() .

typedef struct cvc5_stat_t * Cvc5Stat 

A cvc5 statistic.

bool cvc5_stat_is_internal ( Cvc5Stat stat ) 

Determine if a given statistic is intended for internal use only.

Parameters :

stat – The statistic.

Returns :

True if this is an internal statistic.

bool cvc5_stat_is_default ( Cvc5Stat stat ) 

Determine if a given statistics statistic holds the default value.

Parameters :

stat – The statistic.

Returns :

True if this is a defaulted statistic.

bool cvc5_stat_is_int ( Cvc5Stat stat ) 

Determine if a given statistic holds an integer value.

Parameters :

stat – The statistic.

Returns :

True if this value is an integer.

int64_t cvc5_stat_get_int ( Cvc5Stat stat ) 

Get the value of an integer statistic.

Parameters :

stat – The statistic.

Returns :

The integer value.

bool cvc5_stat_is_double ( Cvc5Stat stat ) 

Determine if a given statistic holds a double value.

Parameters :

stat – The statistic.

Returns :

True if this value is a double.

double cvc5_stat_get_double ( Cvc5Stat stat ) 

Get the value of a double statistic.

Parameters :

stat – The statistic.

Returns :

The double value.

bool cvc5_stat_is_string ( Cvc5Stat stat ) 

Determine if a given statistic holds a string value.

Parameters :

stat – The statistic.

Returns :

True if this value is a string.

const char * cvc5_stat_get_string ( Cvc5Stat stat ) 

Get value of a string statistic.

Note

The returned char pointer is only valid until the next call to this function.

Parameters :

stat – The statistic.

Returns :

The string value.

bool cvc5_stat_is_histogram ( Cvc5Stat stat ) 

Determine if a given statistic holds a histogram.

Parameters :

stat – The statistic.

Returns :

True if this value is a histogram.

void cvc5_stat_get_histogram ( Cvc5Stat stat , const char * * keys [ ] , uint64_t * values [ ] , size_t * size ) 

Get the value of a histogram statistic.

Parameters :

stat – The statistic.

Returns :

The histogram value.

const char * cvc5_stat_to_string ( Cvc5Stat stat ) 

Get a string representation of a given statistic.

Note

The returned char* pointer is only valid until the next call to this function.

Parameters :

stat – The statistic.

Returns :

The string representation.

typedef struct cvc5_stats_t * Cvc5Statistics 

A cvc5 statistics instance.

void cvc5_stats_iter_init ( Cvc5Statistics stat , bool internal , bool dflt ) 

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

Parameters :

• stat – The statistics.

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

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

bool cvc5_stats_iter_has_next ( Cvc5Statistics stat ) 

Determine if statistics iterator has more statitics to query.

Note

Requires that iterator was initialized with cvc5_stats_iter_init() .

Parameters :

stat – The statistics.

Returns :

True if the iterator has more statistics to query.

Cvc5Stat cvc5_stats_iter_next ( Cvc5Statistics stat , const char * * name ) 

Get next statistic and increment iterator.

Note

Requires that iterator was initialized with cvc5_stats_iter_init() and that cvc5_stats_iter_has_next() .

Note

The returned char* pointer are only valid until the next call to this function.

Parameters :

• stat – The statistics.

• name – The output parameter for the name of the returned statistic. May be NULL to ignore.

Returns :

The next statistic.

Cvc5Stat cvc5_stats_get ( Cvc5Statistics stat , const char * name ) 

Retrieve the statistic with the given name.

Note

Requires that a statistic with the given name actually exists.

Parameters :

• stat – The statistics.

• name – The name of the statistic.

Returns :

The statistic with the given name.

const char * cvc5_stats_to_string ( Cvc5Statistics stat ) 

Get a string representation of a given statistics object.

Note

The returned char* pointer is only valid until the next call to this function.

Parameters :

stat – The statistics.

Returns :

The string representation.