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:

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 = { Kind::AND: 1, Kind::APPLY_UF: 4, Kind::EQUAL: 4, Kind::NOT: 2, Kind::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::* ).