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
>