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.

• keys – The resulting arrays with the keys of the statistic, map to the values given in the resulting values array..

• values – The resulting arrays with the values of the statistic.

• size – The size of the resulting keys/values arrays.

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.