We decided to rename statistics from "public / expert" to "public / internal". Also, this adds some reasonable documentation about statistics to our online docs.
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
+Statistics are generally categorized into public and internal 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.
+<cvc5::api::Statistics::begin()>` method has Boolean flags ``internal`` and
+``def`` to also show internal statistics and defaulted statistics, respectively.
.. doxygenclass:: cvc5::api::Statistics
options
output-tags
resource-limits
+ statistics
--- /dev/null
+Statistics
+==========
+
+cvc5 collects a wide variety of statistics that can be inspected via the
+:cpp:func:`Solver::getStatistics() <cvc5::api::Solver::getStatistics()>` API
+function.
+Statistics collection is only availble if the ``ENABLE_STATISTICS`` cmake option
+is set to true, which is the case for all but competition builds.
+The :cpp:func:`Solver::getStatistics() <cvc5::api::Solver::getStatistics()>`
+method returns a snapshot of the statistics values that is decoupled from the
+solver object and will not change when the solver is used again or deallocated.
+Individual statistics values can be obtained either by iterating over the
+:cpp:class:`Statistics <cvc5::api::Statistics>` object or by querying it by name.
+
+A statistic value (of type :cpp:class:`Stat <cvc5::api::Stat>`) has two general
+properties, :cpp:func:`isInternal() <cvc5::api::Stat::isInternal()>` and
+:cpp:func:`isDefault() <cvc5::api::Stat::isDefault()>`.
+:cpp:func:`isInternal() <cvc5::api::Stat::isInternal()>` indicates whether a
+statistic is considered public or internal. Public statistics are considered to
+be part of the public API and should therefore remain stable across different
+minor versions of cvc5. There is no such guarantee for internal statistics.
+:cpp:func:`isDefault() <cvc5::api::Stat::isDefault()>` checks whether the
+current value of a statistics is still the default value, or whether its value
+was changed.
+
+In addition to the
+:cpp:func:`Solver::getStatistics() <cvc5::api::Solver::getStatistics()>` API
+function, statistics can be printed using the following options:
+
+- :ref:`stats <lbl-option-stats>` prints public statistics with non-default values
+- :ref:`stats-all <lbl-option-stats-all>` also prints statistics with default values
+- :ref:`stats-internal <lbl-option-stats-internal>` also prints internal statistics
+- :ref:`stats-every-query <lbl-option-stats-every-query>` prints statistics after every (incremental) check
+
+A statistic value can be any of the following types:
+
+- integer, more specifically a signed 64-bit integer (``int64_t`` in C++).
+- double, a 64-bit floating-point value (``double`` in C++).
+- string, a character sequence (``std::string`` in C++). Timer statistics are
+ exported as string values as well, given as ``"<value>ms"``.
+- histogram, a mapping from some integral or enumeration type to their count.
+ The integral or enumeration types are exported as string representations
+ (``std::map<std::string, uint64_t>`` in C++).
+
+Printing statistics on the command line looks like this:
+
+.. command-output:: bin/cvc5 --stats ../test/regress/regress0/auflia/bug336.smt2
+ :cwd: /../build_debug
+
+Public statistics include some general information about the input file
+(``driver::filename`` and ``api::*``), the overall runtime (``global::totalTime``)
+and the lemmas each theory sent to the core solver (``theory::*``).
\ No newline at end of file
Stat::~Stat() {}
Stat::Stat(const Stat& s)
- : d_expert(s.d_expert),
+ : d_internal(s.d_internal),
d_default(s.d_default),
d_data(std::make_unique<StatData>(s.d_data->data))
{
}
Stat& Stat::operator=(const Stat& s)
{
- d_expert = s.d_expert;
+ d_internal = s.d_internal;
+ d_default = s.d_default;
d_data = std::make_unique<StatData>(s.d_data->data);
return *this;
}
-bool Stat::isExpert() const { return d_expert; }
+bool Stat::isInternal() const { return d_internal; }
bool Stat::isDefault() const { return d_default; }
bool Stat::isInt() const
CVC5_API_TRY_CATCH_END;
}
-Stat::Stat(bool expert, bool defaulted, StatData&& sd)
- : d_expert(expert),
+Stat::Stat(bool internal, bool defaulted, StatData&& sd)
+ : d_internal(internal),
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 internal,
bool defaulted)
- : d_it(it), d_base(&base), d_showExpert(expert), d_showDefault(defaulted)
+ : d_it(it), d_base(&base), d_showInternal(internal), d_showDefault(defaulted)
{
while (!isVisible())
{
bool Statistics::iterator::isVisible() const
{
if (d_it == d_base->end()) return true;
- if (!d_showExpert && d_it->second.isExpert()) return false;
+ if (!d_showInternal && d_it->second.isInternal()) return false;
if (!d_showDefault && d_it->second.isDefault()) return false;
return true;
}
CVC5_API_TRY_CATCH_END;
}
-Statistics::iterator Statistics::begin(bool expert, bool defaulted) const
+Statistics::iterator Statistics::begin(bool internal, bool defaulted) const
{
- return iterator(d_stats.begin(), d_stats, expert, defaulted);
+ return iterator(d_stats.begin(), d_stats, internal, defaulted);
}
Statistics::iterator Statistics::end() const
{
for (const auto& svp : reg)
{
d_stats.emplace(svp.first,
- Stat(svp.second->d_expert,
+ Stat(svp.second->d_internal,
svp.second->isDefault(),
svp.second->getViewer()));
}
* (`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 expert statistic by
- * `isExpert()` and whether its value is the default value by `isDefault()`.
+ * It is possible to query whether this statistic is an internal statistic by
+ * `isInternal()` and whether its value is the default value by `isDefault()`.
*/
class CVC5_EXPORT Stat
{
Stat& operator=(const Stat& s);
/**
- * Is this value intended for experts only?
- * @return Whether this is an expert statistic.
+ * Is this value intended for internal use only?
+ * @return Whether this is an internal statistic.
*/
- bool isExpert() const;
+ bool isInternal() const;
/**
* Does this value hold the default value?
* @return Whether this is a defaulted statistic.
const HistogramData& getHistogram() const;
private:
- Stat(bool expert, bool def, StatData&& sd);
- /** Whether this statistic is only meant for experts */
- bool d_expert;
+ Stat(bool internal, bool def, StatData&& sd);
+ /** Whether this statistic is only meant for internal use */
+ bool d_internal;
/** Whether this statistic has the default value */
bool d_default;
std::unique_ptr<StatData> d_data;
* 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 expert, defaulted, or both, can be
+ * `begin()`, statistics that are internal, defaulted, or both, can be
* included as well. A single statistic value is represented as `Stat`.
*/
class CVC5_EXPORT Statistics
private:
iterator(BaseType::const_iterator it,
const BaseType& base,
- bool expert,
+ bool internal,
bool defaulted);
bool isVisible() const;
BaseType::const_iterator d_it;
const BaseType* d_base;
- bool d_showExpert = false;
+ bool d_showInternal = false;
bool d_showDefault = false;
};
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
+ * By default, only entries that are public and have been set
* are visible while the others are skipped.
- * @param expert If set to true, expert statistics are shown as well.
+ * @param internal If set to true, internal statistics are shown as well.
* @param defaulted If set to true, defaulted statistics are shown as well.
*/
- iterator begin(bool expert = false, bool defaulted = false) const;
+ iterator begin(bool internal = false, bool defaulted = false) const;
/** End iteration */
iterator end() const;
* ({@code Map<String, Long>}).
* The value type can be queried (using {@code isInt()}, {@code isDouble()}, etc.) and
* the stored value can be accessed (using {@code getInt()}, {@code getDouble()}, etc.).
- * It is possible to query whether this statistic is an expert statistic by
- * {@code isExpert()} and whether its value is the default value by {@code isDefault()}.
+ * It is possible to query whether this statistic is an internal statistic by
+ * {@code isInternal()} and whether its value is the default value by {@code isDefault()}.
*/
public class Stat extends AbstractPointer
{
protected native String toString(long pointer);
/**
- * Is this value intended for experts only?
- * @return Whether this is an expert statistic.
+ * Is this value intended for internal use only?
+ * @return Whether this is an internal statistic.
*/
- public boolean isExpert()
+ public boolean isInternal()
{
- return isExpert(pointer);
+ return isInternal(pointer);
}
- private native boolean isExpert(long pointer);
+ private native boolean isInternal(long pointer);
/**
* Does this value hold the default value?
/**
* Begin iteration over the statistics values.
- * By default, only entries that are public (non-expert) and have been set
+ * By default, only entries that are public (non-internal) and have been set
* are visible while the others are skipped.
- * @param expert If set to true, expert statistics are shown as well.
+ * @param internal If set to true, internal statistics are shown as well.
* @param defaulted If set to true, defaulted statistics are shown as well.
*/
/*
* Class: io_github_cvc5_api_Stat
- * Method: isExpert
+ * Method: isInternal
* Signature: (J)Z
*/
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Stat_isExpert(JNIEnv* env,
+JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Stat_isInternal(JNIEnv* env,
jobject,
jlong pointer)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Stat* current = reinterpret_cast<Stat*>(pointer);
- return static_cast<jboolean>(current->isExpert());
+ return static_cast<jboolean>(current->isInternal());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
}
JustifyStatistics::JustifyStatistics()
: d_numStatusNoDecision(smtStatisticsRegistry().registerInt(
- "JustifyStrategy::StatusNoDecision", 0)),
+ "JustifyStrategy::StatusNoDecision")),
d_numStatusDecision(smtStatisticsRegistry().registerInt(
- "JustifyStrategy::StatusDecision", 0)),
+ "JustifyStrategy::StatusDecision")),
d_numStatusBacktrack(smtStatisticsRegistry().registerInt(
- "JustifyStrategy::StatusBacktrack", 0)),
+ "JustifyStrategy::StatusBacktrack")),
d_maxStackSize(smtStatisticsRegistry().registerInt(
- "JustifyStrategy::MaxStackSize", 0)),
+ "JustifyStrategy::MaxStackSize")),
d_maxAssertionsSize(smtStatisticsRegistry().registerInt(
- "JustifyStrategy::MaxAssertionsSize", 0)),
+ "JustifyStrategy::MaxAssertionsSize")),
d_maxSkolemDefsSize(smtStatisticsRegistry().registerInt(
- "JustifyStrategy::MaxSkolemDefsSize", 0))
+ "JustifyStrategy::MaxSkolemDefsSize"))
{
}
if (d_solver->getOptionInfo("stats").boolValue())
{
const auto& stats = d_solver->getStatistics();
- auto it = stats.begin(d_solver->getOptionInfo("stats-expert").boolValue(),
+ auto it = stats.begin(d_solver->getOptionInfo("stats-internal").boolValue(),
d_solver->getOptionInfo("stats-all").boolValue());
for (; it != stats.end(); ++it)
{
help = "print unchanged (defaulted) statistics as well"
[[option]]
- name = "statisticsExpert"
- long = "stats-expert"
+ name = "statisticsInternal"
+ long = "stats-internal"
category = "expert"
type = "bool"
predicates = ["setStatsDetail"]
- help = "print expert (non-public) statistics as well"
+ help = "print internal (non-public) statistics as well"
[[option]]
name = "statisticsEveryQuery"
{
d_options->base.statisticsAll = false;
d_options->base.statisticsEveryQuery = false;
- d_options->base.statisticsExpert = false;
+ d_options->base.statisticsInternal = false;
}
}
CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry,
const std::string& prefix)
- : d_numSatCalls(registry.registerInt(prefix + "cadical::calls_to_solve", 0)),
- d_numVariables(registry.registerInt(prefix + "cadical::variables", 0)),
- d_numClauses(registry.registerInt(prefix + "cadical::clauses", 0)),
+ : d_numSatCalls(registry.registerInt(prefix + "cadical::calls_to_solve")),
+ d_numVariables(registry.registerInt(prefix + "cadical::variables")),
+ d_numClauses(registry.registerInt(prefix + "cadical::clauses")),
d_solveTime(registry.registerTimer(prefix + "cadical::solve_time"))
{
}
class StatisticsRegistry;
/**
- * Preregisters all public (non-expert) statistics.
+ * Preregisters all public statistics.
*/
void registerPublicStatistics(StatisticsRegistry& reg);
}
AverageStat StatisticsRegistry::registerAverage(const std::string& name,
- bool expert)
+ bool internal)
{
- return registerStat<AverageStat>(name, expert);
+ return registerStat<AverageStat>(name, internal);
}
-IntStat StatisticsRegistry::registerInt(const std::string& name, bool expert)
+IntStat StatisticsRegistry::registerInt(const std::string& name, bool internal)
{
- return registerStat<IntStat>(name, expert);
+ return registerStat<IntStat>(name, internal);
}
TimerStat StatisticsRegistry::registerTimer(const std::string& name,
- bool expert)
+ bool internal)
{
- return registerStat<TimerStat>(name, expert);
+ return registerStat<TimerStat>(name, internal);
}
void StatisticsRegistry::storeSnapshot()
d_lastSnapshot = std::make_unique<Snapshot>();
for (const auto& s : d_stats)
{
- if (!options().base.statisticsExpert && s.second->d_expert) continue;
+ if (!options().base.statisticsInternal && s.second->d_internal) continue;
if (!options().base.statisticsAll && s.second->isDefault()) continue;
d_lastSnapshot->emplace(
s.first,
{
for (const auto& s : d_stats)
{
- if (!options().base.statisticsExpert && s.second->d_expert) continue;
+ if (!options().base.statisticsInternal && s.second->d_internal) continue;
if (!options().base.statisticsAll && s.second->isDefault()) continue;
os << s.first << " = " << *s.second << std::endl;
}
{
for (const auto& s : d_stats)
{
- if (!options().base.statisticsExpert && s.second->d_expert) continue;
+ if (!options().base.statisticsInternal && s.second->d_internal) continue;
if (!options().base.statisticsAll && s.second->isDefault()) continue;
safe_print(fd, s.first);
}
for (const auto& s : d_stats)
{
- if (!options().base.statisticsExpert && s.second->d_expert) continue;
+ if (!options().base.statisticsInternal && s.second->d_internal) continue;
if (!options().base.statisticsAll && s.second->isDefault())
{
auto oldit = d_lastSnapshot->find(s.first);
*
* AverageStat is a BackedStat<double>.
*
- * HistogramStat counts instances of some type T. It is implemented as a
- * std::map<T, std::uint64_t>.
- *
- * IntegralHistogramStat is a (conceptual) specialization of HistogramStat
- * for types that are (convertible to) integral. This allows to use a
- * std::vector<std::uint64_t> instead of a std::map.
+ * HistogramStat counts instances of some type T. We assume that T is either an
+ * integral type, or an enum type (that is convertible to an interval type).
+ * This allows a more efficient implementation as std::vector<std::uint64_t>
+ * instead of a std::map<T, uint64_t>.
*
* TimerStat uses std::chrono to collect timing information. It is
* implemented as BackedStat<std::chrono::duration> and provides methods
* Note that the type of the re-registered statistic must always match
* the type of the previously registered statistic with the same name.
*
- * We generally distinguish between public (non-expert) and private (expert)
- * statistics. By default, `--stats` only shows public statistics. Private
- * ones are printed as well if `--all-statistics` is set.
- * All registration methods have a trailing argument `expert`, defaulting to
+ * We generally distinguish between public and internal statistics.
+ * By default, `--stats` only shows public statistics. Internal
+ * ones are printed as well if `--stats-internal` is set.
+ * All registration methods have a trailing argument `internal`, defaulting to
* true.
*
* If statistics are disabled entirely (i.e. the cmake option
/** Register a new running average statistic for `name` */
- AverageStat registerAverage(const std::string& name, bool expert = true);
+ AverageStat registerAverage(const std::string& name, bool internal = true);
/** Register a new histogram statistic for `name` */
template <typename T>
HistogramStat<T> registerHistogram(const std::string& name,
- bool expert = true)
+ bool internal = true)
{
- return registerStat<HistogramStat<T>>(name, expert);
+ return registerStat<HistogramStat<T>>(name, internal);
}
/** Register a new integer statistic for `name` */
- IntStat registerInt(const std::string& name, bool expert = true);
+ IntStat registerInt(const std::string& name, bool internal = true);
/** Register a new reference statistic for `name` */
template <typename T>
ReferenceStat<T> registerReference(const std::string& name,
- bool expert = true)
+ bool internal = true)
{
- return registerStat<ReferenceStat<T>>(name, expert);
+ return registerStat<ReferenceStat<T>>(name, internal);
}
/**
* Register a new reference statistic for `name` and initialize it to
template <typename T>
ReferenceStat<T> registerReference(const std::string& name,
const T& t,
- bool expert = true)
+ bool internal = true)
{
- ReferenceStat<T> res = registerStat<ReferenceStat<T>>(name, expert);
+ ReferenceStat<T> res = registerStat<ReferenceStat<T>>(name, internal);
res.set(t);
return res;
}
template <typename T>
SizeStat<T> registerSize(const std::string& name,
const T& t,
- bool expert = true)
+ bool internal = true)
{
- SizeStat<T> res = registerStat<SizeStat<T>>(name, expert);
+ SizeStat<T> res = registerStat<SizeStat<T>>(name, internal);
res.set(t);
return res;
}
/** Register a new timer statistic for `name` */
- TimerStat registerTimer(const std::string& name, bool expert = true);
+ TimerStat registerTimer(const std::string& name, bool internal = true);
/** Register a new value statistic for `name`. */
template <typename T>
- ValueStat<T> registerValue(const std::string& name, bool expert = true)
+ ValueStat<T> registerValue(const std::string& name, bool internal = true)
{
- return registerStat<ValueStat<T>>(name, expert);
+ return registerStat<ValueStat<T>>(name, internal);
}
/** Register a new value statistic for `name` and set it to `init`. */
template <typename T>
ValueStat<T> registerValue(const std::string& name,
const T& init,
- bool expert = true)
+ bool internal = true)
{
- ValueStat<T> res = registerStat<ValueStat<T>>(name, expert);
+ ValueStat<T> res = registerStat<ValueStat<T>>(name, internal);
res.set(init);
return res;
}
* statistic using `typeid`.
*/
template <typename Stat>
- Stat registerStat(const std::string& name, bool expert)
+ Stat registerStat(const std::string& name, bool internal)
{
if constexpr (configuration::isStatisticsBuild())
{
{
it = d_stats.emplace(name, std::make_unique<typename Stat::stat_type>())
.first;
- it->second->d_expert = expert;
+ it->second->d_internal = internal;
}
auto* ptr = it->second.get();
Assert(typeid(*ptr) == typeid(typename Stat::stat_type))
<< "Statistic value " << name
<< " was registered again with a different type.";
- it->second->d_expert = it->second->d_expert && expert;
+ it->second->d_internal = it->second->d_internal && internal;
return Stat(static_cast<typename Stat::stat_type*>(ptr));
}
return Stat(nullptr);
*/
virtual void printSafe(int fd) const = 0;
- bool d_expert = true;
+ bool d_internal = true;
};
/** Writes the data to an output stream */
std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv);
(get-option :stats)
(get-option :stats-all)
(get-option :stats-every-query)
-(get-option :stats-expert)
+(get-option :stats-internal)
(set-option :stats-all true)
(get-option :stats)
(get-option :stats-all)
(get-option :stats-every-query)
-(get-option :stats-expert)
+(get-option :stats-internal)
(set-option :stats false)
(get-option :stats)
(get-option :stats-all)
(get-option :stats-every-query)
-(get-option :stats-expert)
+(get-option :stats-internal)
-(set-option :stats-expert true)
+(set-option :stats-internal true)
(get-option :stats)
(get-option :stats-all)
(get-option :stats-every-query)
-(get-option :stats-expert)
+(get-option :stats-internal)
(set-option :stats false)
(get-option :stats)
(get-option :stats-all)
(get-option :stats-every-query)
-(get-option :stats-expert)
\ No newline at end of file
+(get-option :stats-internal)
\ No newline at end of file
projects / cvc5.git / commitdiff