docs/statistics.rst

   1 Statistics
   2 ==========
   3
   4 cvc5 collects a wide variety of statistics that give some insight on how it solves a particular input.
   5 The statistics can be inspected via the :cpp:func:`Solver::getStatistics() <cvc5::api::Solver::getStatistics()>` API
   6 function, or printed using the following options:
   7
   8 - :ref:`stats <lbl-option-stats>` prints public statistics with non-default values
   9 - :ref:`stats-all <lbl-option-stats-all>` also prints statistics with default values
  10 - :ref:`stats-internal <lbl-option-stats-internal>` also prints internal statistics
  11 - :ref:`stats-every-query <lbl-option-stats-every-query>` prints statistics after every (incremental) check
  12
  13 Statistics collection is only available if the ``ENABLE_STATISTICS`` cmake option
  14 is set to true, which is the case for all but competition builds.
  15 Statistics, obtained via :cpp:func:`Solver::getStatistics() <cvc5::api::Solver::getStatistics()>`,
  16 are always a snapshot of the statistics values that is decoupled from the
  17 solver object and will not change when the solver is used again or deallocated.
  18 Individual statistics values can be obtained via the API either by iterating over the
  19 :cpp:class:`Statistics <cvc5::api::Statistics>` object or by querying it by name.
  20
  21 A statistic value (of type :cpp:class:`Stat <cvc5::api::Stat>`) has two general
  22 properties, :cpp:func:`isInternal() <cvc5::api::Stat::isInternal()>` and
  23 :cpp:func:`isDefault() <cvc5::api::Stat::isDefault()>`.
  24 :cpp:func:`isInternal() <cvc5::api::Stat::isInternal()>` indicates whether a
  25 statistic is considered public or internal. Public statistics are considered to
  26 be part of the public API and should therefore remain stable across different
  27 minor versions of cvc5. There is no such guarantee for internal statistics.
  28 :cpp:func:`isDefault() <cvc5::api::Stat::isDefault()>` checks whether the
  29 current value of a statistics is still the default value, or whether its value
  30 was changed.
  31
  32 A statistic value can be any of the following types:
  33
  34 - integer, more specifically a signed 64-bit integer (``int64_t`` in C++).
  35 - double, a 64-bit floating-point value (``double`` in C++).
  36 - string, a character sequence (``std::string`` in C++). Timer statistics are
  37   exported as string values as well, given as ``"<value>ms"``.
  38 - histogram, a mapping from some integral or enumeration type to their count.
  39   The integral or enumeration types are exported as string representations
  40   (``std::map<std::string, uint64_t>`` in C++).
  41
  42 Printing statistics on the command line looks like this:
  43
  44 .. run-command:: bin/cvc5 --stats ../test/regress/regress0/auflia/bug336.smt2
  45
  46 Public statistics include some general information about the input file
  47 (``driver::filename`` and ``api::*``), the overall runtime (``global::totalTime``)
  48 and the lemmas each theory sent to the core solver (``theory::*``).