Statistics
cvc5 collects a wide variety of statistics that give some insight on how it solves a particular input.
The statistics can be inspected via the
Solver::getStatistics()
API
function, or printed using the following options:
-
stats prints public statistics with non-default values
-
stats-all also prints statistics with default values
-
stats-internal also prints internal statistics
-
stats-every-query prints statistics after every (incremental) check
Statistics collection is only available if the
ENABLE_STATISTICS
cmake option
is set to true, which is the case for all but competition builds.
Statistics, obtained via
Solver::getStatistics()
,
are always a snapshot of the statistics values that is decoupled from the
solver object and will not change when the solver is used again or deallocated.
Individual statistics values can be obtained via the API either by iterating over the
Statistics
object or by querying it by name.
A statistic value (of type
Stat
) has two general
properties,
isInternal()
and
isDefault()
.
isInternal()
indicates whether a
statistic is considered public or internal. Public statistics are considered to
be part of the public API and should therefore remain stable across different
minor versions of cvc5. There is no such guarantee for internal statistics.
isDefault()
checks whether the
current value of a statistics is still the default value, or whether its value
was changed.
A statistic value can be any of the following types:
-
integer, more specifically a signed 64-bit integer (
int64_t
in C++). -
double, a 64-bit floating-point value (
double
in C++). -
string, a character sequence (
std::string
in C++). Timer statistics are exported as string values as well, given as"<value>ms"
. -
histogram, a mapping from some integral or enumeration type to their count. The integral or enumeration types are exported as string representations (
std::map<std::string, uint64_t>
in C++).
Printing statistics on the command line looks like this:
$ bin/cvc5 --stats ../test/regress/cli/regress0/auflia/bug336.smt2
unsat
cvc5::TERM = { AND: 1, APPLY_UF: 4, EQUAL: 4, NOT: 2, STORE: 2 }
cvc5::VARIABLE = { Boolean type: 5 }
driver::filename = ../test/regress/cli/regress0/auflia/bug336.smt2
global::totalTime = 2ms
theory::arith::inferencesLemma = { ARITH_SPLIT_DEQ: 1 }
theory::arrays::inferencesFact = { ARRAYS_READ_OVER_WRITE_1: 2 }
theory::arrays::inferencesLemma = { ARRAYS_EXT: 1, ARRAYS_READ_OVER_WRITE: 3 }
theory::builtin::inferencesLemma = { COMBINATION_SPLIT: 1 }
Public statistics include some general information about the input file
(
driver::filename
and
*
), the overall runtime (
global::totalTime
)
and the lemmas each theory sent to the core solver (
theory::*
).