Improve documentation for Statistics in C++ API (#8476)

This PR improves the documentation of the Statistics and the Stat class in the C++ API.

diff --git a/docs/api/cpp/statistics.rst b/docs/api/cpp/statistics.rst
index 069f2b851c66e0a908876b6254d8c0284ffd18fd..6bb3ebbae636df25c03d2d913872d8b6c8b628d0 100644 (file)
--- a/docs/api/cpp/statistics.rst
+++ b/docs/api/cpp/statistics.rst
@@ -1,13 +1,7 @@
 Statistics
 ==========
 
-The solver collects a variety of statistics that can be helpful in understanding
-what the solver is doing internally. The entirety of collected statistics are
-represented by a :cpp:class:`Statistics <cvc5::Statistics>` object that can
-be obtained from :cpp:func:`Solver::getStatistics()
-<cvc5::Solver::getStatistics>`. It is a copy of the internal solver
-statistics at this point in time.
-
+See :doc:`/statistics` for general information on statistics in cvc5..
 The :cpp:class:`Statistics <cvc5::Statistics>` object is essentially a
 mapping from names (as ``std::string``) to statistic values, represented by the
 :cpp:class:`Stat <cvc5::Stat>` class. A :cpp:class:`Stat <cvc5::Stat>`
@@ -17,13 +11,10 @@ histograms) and can be inspected by identifying the type
 :cpp:func:`Stat::isDouble() <cvc5::Stat::isDouble()>`, etc) and obtaining
 the actual value (:cpp:func:`Stat::getInt() <cvc5::Stat::getInt()>`,
 :cpp:func:`Stat::getDouble() <cvc5::Stat::getDouble()>`, etc). Histograms
-conceptually count the frequency of different values of an arbitrary type,
-usually an enumeration type. They are represented as ``std::map<std::string,
-uint64_t>`` where the key is the strings representation of one enumeration value
+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.
 
-Statistics are generally categorized into public and internal statistics, and
-furthermore into changed and defaulted statistics. By default, iterating a
+By default, iterating over a
 :cpp:class:`Statistics <cvc5::Statistics>` object only shows statistics
 that are both public and changed. The :cpp:func:`Statistics::begin()
 <cvc5::Statistics::begin()>` method has Boolean flags ``internal`` and

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 0416f1a2d518c960d5ed58e6f7108fd41a6cb4c9..30d0000d0466eb9bae006fb88d0d3e5a750ddc5f 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2879,13 +2879,18 @@ std::ostream& operator<<(std::ostream& os, const OptionInfo& oi) CVC5_EXPORT;
 /* -------------------------------------------------------------------------- */
 
 /**
- * Represents a snapshot of a single statistic value.
- * 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 (using `isInt()`, `isDouble()`, etc.) and
- * the stored value can be accessed (using `getInt()`, `getDouble()`, etc.).
+ * \verbatim embed:rst:leading-asterisk
+ * Represents a snapshot of a single statistic value. See :doc:`/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 (using ``isInt()``, ``isDouble()``, etc.) and
+ * the stored value can be accessed (using ``getInt()``, ``getDouble()``, etc.).
  * It is possible to query whether this statistic is an internal statistic by
- * `isInternal()` and whether its value is the default value by `isDefault()`.
+ * :cpp:func:`isInternal() <cvc5::Stat::isInternal()>` and whether its value is
+ * the default value by :cpp:func:`isDefault() <cvc5::Stat::isDefault()>`.
+ * \endverbatim
  */
 class CVC5_EXPORT Stat
 {
@@ -2976,14 +2981,19 @@ class CVC5_EXPORT Stat
 std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC5_EXPORT;
 
 /**
- * Represents a snapshot of the solver statistics.
- * Once obtained, an instance of this class is independent of the `Solver`
- * object: it will not change when the solvers internal statistics do, it
- * will not be invalidated if the solver is destroyed.
- * Iterating on this class (via `begin()` and `end()`) shows only public
- * statistics that have been changed. By passing appropriate flags to
- * `begin()`, statistics that are internal, defaulted, or both, can be
- * included as well. A single statistic value is represented as `Stat`.
+ * \verbatim embed:rst:leading-asterisk
+ * Represents a snapshot of the solver statistics. See :doc:`/statistics` for
+ * how statistics can be used.
+ * Once obtained via :cpp:func:`Solver::getStatistics()
+ * <cvc5::Solver::getStatistics()>`, an instance of this class is independent of
+ * the :cpp:class:`Solver <cvc5::Solver>` 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 (via :cpp:func:`begin()
+ * <cvc5::Statistics::begin()>` and :cpp:func:`end() <cvc5::Statistics::end()>`)
+ * shows only public statistics that have been changed. By passing appropriate
+ * flags to :cpp:func:`begin() <cvc5::Statistics::begin()>`, statistics that are
+ * internal, defaulted, or both, can be included as well. A single statistic
+ * value is represented as :cpp:class:`Stat <cvc5::Stat>`. \endverbatim
  */
 class CVC5_EXPORT Statistics
 {