--- /dev/null
+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:
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;
}
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;
}
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;
}
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)))
{
}
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())
{
{
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
{
/**
* 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
{
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:
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;
/**
* 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++();
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;
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:
projects / cvc5.git / commitdiff