From: Gereon Kremer Date: Thu, 22 Apr 2021 19:38:57 +0000 (+0200) Subject: Add API documentation for statistics (#6364) X-Git-Tag: cvc5-1.0.0~1852 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=69992245e3d2326ca8ecf2295a7e03d395046fc1;p=cvc5.git 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. --- 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` + * 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 ` object that can +be obtained from :cpp:func:`Solver::getStatistics() +`. It is a copy of the internal solver +statistics at this point in time. + +The :cpp:class:`Statistics ` object is essentially a +mapping from names (as ``std::string``) to statistic values, represented by the +:cpp:class:`Stat ` class. A :cpp:class:`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() `, +:cpp:func:`Stat::isDouble() `, etc) and obtaining +the actual value (:cpp:func:`Stat::getInt() `, +:cpp:func:`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`` 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 ` object only shows statistics +that are both public and changed. The :cpp:func:`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(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(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(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(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(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`). - * 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; - /** 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 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; - /** 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: