mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
49 lines
2.7 KiB
ReStructuredText
49 lines
2.7 KiB
ReStructuredText
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 :cpp:func:`Solver::getStatistics() <cvc5::Solver::getStatistics()>` API
|
|
function, or printed using the following options:
|
|
|
|
- :ref:`stats <lbl-option-stats>` prints public statistics with non-default values
|
|
- :ref:`stats-all <lbl-option-stats-all>` also prints statistics with default values
|
|
- :ref:`stats-internal <lbl-option-stats-internal>` also prints internal statistics
|
|
- :ref:`stats-every-query <lbl-option-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 :cpp:func:`Solver::getStatistics() <cvc5::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
|
|
:cpp:class:`Statistics <cvc5::Statistics>` object or by querying it by name.
|
|
|
|
A statistic value (of type :cpp:class:`Stat <cvc5::Stat>`) has two general
|
|
properties, :cpp:func:`isInternal() <cvc5::Stat::isInternal()>` and
|
|
:cpp:func:`isDefault() <cvc5::Stat::isDefault()>`.
|
|
:cpp:func:`isInternal() <cvc5::Stat::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.
|
|
:cpp:func:`isDefault() <cvc5::Stat::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:
|
|
|
|
.. run-command:: bin/cvc5 --stats ../test/regress/cli/regress0/auflia/bug336.smt2
|
|
|
|
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::*``).
|