Add API documentation for statistics (#6364)

This PR adds documentation for api::Statistics and api::Stat, as well as further explanations in sphinx.
It also adds a custom css to our sphinx theme that slightly changes how inline code blocks look.

7 files changed, 143 insertions, 47 deletions

diff --git a/docs/_static/custom.css b/docs/_static/custom.css
new file mode 100644
index 000000000..b2db580ef
--- /dev/null
+++ b/docs/_static/custom.css
@@ -0,0 +1,11 @@
+code {
+    border: 0px !important;
+}
+
+code.xref {
+    color: unset !important;
+}
+
+.rst-content code {
+    padding: 1px !important;
+}
diff --git a/docs/conf.py b/docs/conf.py
index 3ec162d34..91a3b3a9a 100644
--- a/docs/conf.py
+++ b/docs/conf.py
@@ -52,13 +52,9 @@ exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
 # a list of builtin themes.
 #
 html_theme = 'sphinx_rtd_theme'
-html_theme_options = {
-}
-
-# Add any paths that contain custom static files (such as style sheets) here,
-# relative to this directory. They are copied after the builtin static files,
-# so a file named "default.css" will overwrite the builtin "default.css".
-html_static_path = []
+html_theme_options = {}
+html_static_path = ['_static']
+html_css_files = ['custom.css']
 
 # -- Breathe configuration ---------------------------------------------------
 breathe_default_project = "cvc5"
diff --git a/docs/cpp/cpp.rst b/docs/cpp/cpp.rst
index 86b310d6e..ad4f177de 100644
--- a/docs/cpp/cpp.rst
+++ b/docs/cpp/cpp.rst
@@ -48,6 +48,9 @@ Class Hierarchy
 
     * struct :ref:`SortHashFunction<sort>`
 
+    * class :cpp:class:`cvc5::api::Statistics`
+    * class :cpp:class:`cvc5::api::Stat`
+
 
 
 Full API Documentation
@@ -69,4 +72,5 @@ Full API Documentation
   roundingmode
   solver
   sort
+  statistics
   term
diff --git a/docs/cpp/statistics.rst b/docs/cpp/statistics.rst
new file mode 100644
index 000000000..ae1b525ab
--- /dev/null
+++ b/docs/cpp/statistics.rst
@@ -0,0 +1,41 @@
+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::api::Statistics>` object that can
+be obtained from :cpp:func:`Solver::getStatistics()
+<cvc5::api::Solver::getStatistics>`. It is a copy of the internal solver
+statistics at this point in time.
+
+The :cpp:class:`Statistics <cvc5::api::Statistics>` object is essentially a
+mapping from names (as ``std::string``) to statistic values, represented by the
+:cpp:class:`Stat <cvc5::api::Stat>` class. A :cpp:class:`Stat <cvc5::api::Stat>`
+can hold values of different types (``int64_t``, ``double``, ``std::string`` and
+histograms) and can be inspected by identifying the type
+(:cpp:func:`Stat::isInt() <cvc5::api::Stat::isInt()>`,
+:cpp:func:`Stat::isDouble() <cvc5::api::Stat::isDouble()>`, etc) and obtaining
+the actual value (:cpp:func:`Stat::getInt() <cvc5::api::Stat::getInt()>`,
+:cpp:func:`Stat::getDouble() <cvc5::api::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
+and the value is the frequency of this particular value.
+
+Statistics are generally categorized into public and expert statistics, and
+furthermore into changed and defaulted statistics. By default, iterating a
+:cpp:class:`Statistics <cvc5::api::Statistics>` object only shows statistics
+that are both public and changed. The :cpp:func:`Statistics::begin()
+<cvc5::api::Statistics::begin()>` method has Boolean flags ``expert`` and
+``def`` to also show expert statistics and defaulted statistics, respectively.
+
+
+.. doxygenclass:: cvc5::api::Statistics
+    :project: cvc5
+    :members: get, begin, end
+    :undoc-members:
+
+.. doxygenclass:: cvc5::api::Stat
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/ext/.gitignore b/docs/ext/.gitignore
new file mode 100644
index 000000000..ba0430d26
--- /dev/null
+++ b/docs/ext/.gitignore
@@ -0,0 +1 @@
+__pycache__/
\ No newline at end of file
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 4dbd06ce8..c5472cdfe 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4147,7 +4147,7 @@ bool Stat::isInt() const
 int64_t Stat::getInt() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(isInt()) << "Expected Stat of type int64_t.";
+  CVC5_API_RECOVERABLE_CHECK(isInt()) << "Expected Stat of type int64_t.";
   return std::get<int64_t>(d_data->data);
   CVC5_API_TRY_CATCH_END;
 }
@@ -4158,7 +4158,7 @@ bool Stat::isDouble() const
 double Stat::getDouble() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(isDouble()) << "Expected Stat of type double.";
+  CVC5_API_RECOVERABLE_CHECK(isDouble()) << "Expected Stat of type double.";
   return std::get<double>(d_data->data);
   CVC5_API_TRY_CATCH_END;
 }
@@ -4169,7 +4169,7 @@ bool Stat::isString() const
 const std::string& Stat::getString() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(isString()) << "Expected Stat of type std::string.";
+  CVC5_API_RECOVERABLE_CHECK(isString()) << "Expected Stat of type std::string.";
   return std::get<std::string>(d_data->data);
   CVC5_API_TRY_CATCH_END;
 }
@@ -4180,14 +4180,14 @@ bool Stat::isHistogram() const
 const Stat::HistogramData& Stat::getHistogram() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(isHistogram()) << "Expected Stat of type histogram.";
+  CVC5_API_RECOVERABLE_CHECK(isHistogram()) << "Expected Stat of type histogram.";
   return std::get<HistogramData>(d_data->data);
   CVC5_API_TRY_CATCH_END;
 }
 
-Stat::Stat(bool expert, bool def, StatData&& sd)
+Stat::Stat(bool expert, bool defaulted, StatData&& sd)
     : d_expert(expert),
-      d_default(def),
+      d_default(defaulted),
       d_data(std::make_unique<StatData>(std::move(sd)))
 {
 }
@@ -4250,8 +4250,8 @@ bool Statistics::iterator::operator!=(const Statistics::iterator& rhs) const
 Statistics::iterator::iterator(Statistics::BaseType::const_iterator it,
                                const Statistics::BaseType& base,
                                bool expert,
-                               bool def)
-    : d_it(it), d_base(&base), d_showExpert(expert), d_showDefault(def)
+                               bool defaulted)
+    : d_it(it), d_base(&base), d_showExpert(expert), d_showDefault(defaulted)
 {
   while (!isVisible())
   {
@@ -4270,15 +4270,15 @@ const Stat& Statistics::get(const std::string& name)
 {
   CVC5_API_TRY_CATCH_BEGIN;
   auto it = d_stats.find(name);
-  CVC5_API_CHECK(it != d_stats.end())
+  CVC5_API_RECOVERABLE_CHECK(it != d_stats.end())
       << "No stat with name \"" << name << "\" exists.";
   return it->second;
   CVC5_API_TRY_CATCH_END;
 }
 
-Statistics::iterator Statistics::begin(bool expert, bool def) const
+Statistics::iterator Statistics::begin(bool expert, bool defaulted) const
 {
-  return iterator(d_stats.begin(), d_stats, expert, def);
+  return iterator(d_stats.begin(), d_stats, expert, defaulted);
 }
 Statistics::iterator Statistics::end() const
 {
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 96e287f84..b3785c10e 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2342,10 +2342,12 @@ struct CVC5_EXPORT RoundingModeHashFunction
 
 /**
  * Represents a snapshot of a single statistic value.
- * A value can be of type int64_t, double, std::string or a histogram
+ * 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`, `isString`, etc.) and
- * the stored value can be accessed (using `getInt`, `getString`, etc.).
+ * 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 expert statistic by
+ * `isExpert()` and whether its value is the default value by `isDefault()`.
  */
 class CVC5_EXPORT Stat
 {
@@ -2354,33 +2356,67 @@ class CVC5_EXPORT Stat
  public:
   friend class Statistics;
   friend std::ostream& operator<<(std::ostream& os, const Stat& sv);
+  /** Representation of a histogram: maps names to frequencies. */
   using HistogramData = std::map<std::string, uint64_t>;
-  /** Create from the given value. */
+  /** Can only be obtained from a `Statistics` object. */
   Stat() = delete;
+  /** Copy constructor */
   Stat(const Stat& s);
+  /** Destructor */
   ~Stat();
+  /** Copy assignment */
   Stat& operator=(const Stat& s);
 
-  /** Is this value intended for experts only? */
+  /**
+   * Is this value intended for experts only?
+   * @return Whether this is an expert statistic.
+   */
   bool isExpert() const;
-  /** Does this value hold the default value? */
+  /**
+   * Does this value hold the default value?
+   * @return Whether this is a defaulted statistic.
+   */
   bool isDefault() const;
 
-  /** Is this value an integer? */
+  /**
+   * Is this value an integer?
+   * @return Whether the value is an integer.
+   */
   bool isInt() const;
-  /** Return the integer value */
+  /**
+   * Return the integer value.
+   * @return The integer value.
+   */
   int64_t getInt() const;
-  /** Is this value a double? */
+  /**
+   * Is this value a double?
+   * @return Whether the value is a double.
+   */
   bool isDouble() const;
-  /** Return the double value */
+  /**
+   * Return the double value.
+   * @return The double value.
+   */
   double getDouble() const;
-  /** Is this value an string? */
+  /**
+   * Is this value a string?
+   * @return Whether the value is a string.
+   */
   bool isString() const;
-  /** Return the string value */
+  /**
+   * Return the string value.
+   * @return The string value.
+   */
   const std::string& getString() const;
-  /** Is this value an histogram? */
+  /**
+   * Is this value a histogram?
+   * @return Whether the value is a histogram.
+   */
   bool isHistogram() const;
-  /** Return the histogram value */
+  /**
+   * Return the histogram value.
+   * @return The histogram value.
+   */
   const HistogramData& getHistogram() const;
 
  private:
@@ -2392,6 +2428,9 @@ class CVC5_EXPORT Stat
   std::unique_ptr<StatData> d_data;
 };
 
+/**
+ * Print a `Stat` object to an ``std::ostream``.
+ */
 std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC5_EXPORT;
 
 /**
@@ -2399,25 +2438,23 @@ std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC5_EXPORT;
  * 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.
- * Statistics are generally categorized as public and expert statistics.
- * Furthermore, statistics may hold the default values and thus be not of
- * interest.
  * Iterating on this class (via `begin()` and `end()`) shows only public
- * statistics that have been set. By passing appropriate flags to `begin()`,
- * statistics that are expert, unchanged, or both, can be included as well.
- * A single statistic value is represented as `Stat`.
+ * statistics that have been changed. By passing appropriate flags to
+ * `begin()`, statistics that are expert, defaulted, or both, can be
+ * included as well. A single statistic value is represented as `Stat`.
  */
 class CVC5_EXPORT Statistics
 {
  public:
-  friend Solver;
+  friend class Solver;
+  /** How the statistics are stored internally. */
   using BaseType = std::map<std::string, Stat>;
 
-  /** Custom iterator to hide expert statistics from regular iteration */
+  /** Custom iterator to hide certain statistics from regular iteration */
   class iterator
   {
    public:
-    friend Statistics;
+    friend class Statistics;
     BaseType::const_reference operator*() const;
     BaseType::const_pointer operator->() const;
     iterator& operator++();
@@ -2431,7 +2468,7 @@ class CVC5_EXPORT Statistics
     iterator(BaseType::const_iterator it,
              const BaseType& base,
              bool expert,
-             bool def);
+             bool defaulted);
     bool isVisible() const;
     BaseType::const_iterator d_it;
     const BaseType* d_base;
@@ -2439,17 +2476,23 @@ class CVC5_EXPORT Statistics
     bool d_showDefault = false;
   };
 
-  /** Retrieve the statistic with the given name. */
+  /**
+   * Retrieve the statistic with the given name.
+   * Asserts that a statistic with the given name actually exists and throws
+   * a `CVC4ApiRecoverableException` if it does not.
+   * @param name Name of the statistic.
+   * @return The statistic with the given name.
+   */
   const Stat& get(const std::string& name);
   /**
    * Begin iteration over the statistics values.
    * By default, only entries that are public (non-expert) and have been set
    * are visible while the others are skipped.
-   * With `expert` set to true, expert statistics are shown as well.
-   * With `def` set to true, defaulted statistics are shown as well.
+   * @param expert If set to true, expert statistics are shown as well.
+   * @param defaulted If set to true, defaulted statistics are shown as well.
    */
-  iterator begin(bool expert = false, bool def = false) const;
-  /** end iteration */
+  iterator begin(bool expert = false, bool defaulted = false) const;
+  /** End iteration */
   iterator end() const;
 
  private: