Statistics
See
Statistics
for general information on statistics in cvc5..
The
Statistics
object is essentially a
mapping from names (as
std::string
) to statistic values, represented by the
Stat
class. A
Stat
can 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

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 theSolver
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 (viabegin()
andend()
) shows only public statistics that have been changed. By passing appropriate flags tobegin()
, statistics that are internal, defaulted, or both, can be included as well. A single statistic value is represented asStat
.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

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

class
cvc5
::
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 (usingisInt()
,isDouble()
, etc.) and the stored value can be accessed (usinggetInt()
,getDouble()
, etc.). It is possible to query whether this statistic is an internal statistic byisInternal()
and whether its value is the default value byisDefault()
.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 allgetX()
throw an API exception. It solely exists because it makes implementing bindings for other languages much easier.

~Stat
(
)

Destructor

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.

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