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.

5 files changed, 60 insertions, 7 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