From aaab98c4491cd79cc27184a57c4b13f7650e5757 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 10 Mar 2022 00:40:43 +0100 Subject: [PATCH] Rename expert statistics to internal, add documentation (#8262) We decided to rename statistics from "public / expert" to "public / internal". Also, this adds some reasonable documentation about statistics to our online docs. --- docs/api/cpp/statistics.rst | 6 +-- docs/binary/binary.rst | 1 + docs/binary/statistics.rst | 52 ++++++++++++++++++ src/api/cpp/cvc5.cpp | 23 ++++---- src/api/cpp/cvc5.h | 28 +++++----- src/api/java/io/github/cvc5/api/Stat.java | 14 ++--- .../java/io/github/cvc5/api/Statistics.java | 4 +- src/api/java/jni/stat.cpp | 6 +-- src/decision/justify_stats.cpp | 12 ++--- src/main/command_executor.cpp | 2 +- src/options/base_options.toml | 6 +-- src/options/options_handler.cpp | 2 +- src/prop/cadical.cpp | 6 +-- src/util/statistics_public.h | 2 +- src/util/statistics_registry.cpp | 20 +++---- src/util/statistics_registry.h | 54 +++++++++---------- src/util/statistics_value.h | 2 +- test/regress/regress0/options/statistics.smt2 | 12 ++--- 18 files changed, 152 insertions(+), 100 deletions(-) create mode 100644 docs/binary/statistics.rst diff --git a/docs/api/cpp/statistics.rst b/docs/api/cpp/statistics.rst index ae1b525ab..77fab9545 100644 --- a/docs/api/cpp/statistics.rst +++ b/docs/api/cpp/statistics.rst @@ -22,12 +22,12 @@ 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 +Statistics are generally categorized into public and internal 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. +` method has Boolean flags ``internal`` and +``def`` to also show internal statistics and defaulted statistics, respectively. .. doxygenclass:: cvc5::api::Statistics diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst index 66c23ccd6..fe868c879 100644 --- a/docs/binary/binary.rst +++ b/docs/binary/binary.rst @@ -17,3 +17,4 @@ Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different prog options output-tags resource-limits + statistics diff --git a/docs/binary/statistics.rst b/docs/binary/statistics.rst new file mode 100644 index 000000000..e7fa9fcab --- /dev/null +++ b/docs/binary/statistics.rst @@ -0,0 +1,52 @@ +Statistics +========== + +cvc5 collects a wide variety of statistics that can be inspected via the +:cpp:func:`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() ` +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 ` object or by querying it by name. + +A statistic value (of type :cpp:class:`Stat `) has two general +properties, :cpp:func:`isInternal() ` and +:cpp:func:`isDefault() `. +:cpp:func:`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() ` 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() ` API +function, statistics can be printed using the following options: + +- :ref:`stats ` prints public statistics with non-default values +- :ref:`stats-all ` also prints statistics with default values +- :ref:`stats-internal ` also prints internal statistics +- :ref:`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 ``"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`` 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 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 2a9234a2f..562337fba 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -4814,19 +4814,20 @@ struct Stat::StatData 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(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(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 @@ -4876,8 +4877,8 @@ const Stat::HistogramData& Stat::getHistogram() 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(std::move(sd))) { @@ -4940,9 +4941,9 @@ bool Statistics::iterator::operator!=(const Statistics::iterator& rhs) const } 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()) { @@ -4952,7 +4953,7 @@ Statistics::iterator::iterator(Statistics::BaseType::const_iterator it, 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; } @@ -4967,9 +4968,9 @@ const Stat& Statistics::get(const std::string& name) 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 { @@ -4981,7 +4982,7 @@ Statistics::Statistics(const StatisticsRegistry& reg) 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())); } diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 316d26910..229fe6235 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2884,8 +2884,8 @@ std::ostream& operator<<(std::ostream& os, const OptionInfo& oi) CVC5_EXPORT; * (`std::map`). * 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 { @@ -2906,10 +2906,10 @@ 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. @@ -2958,9 +2958,9 @@ class CVC5_EXPORT Stat 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 d_data; @@ -2978,7 +2978,7 @@ std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC5_EXPORT; * 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 @@ -3005,12 +3005,12 @@ 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; }; @@ -3024,12 +3024,12 @@ class CVC5_EXPORT Statistics 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; diff --git a/src/api/java/io/github/cvc5/api/Stat.java b/src/api/java/io/github/cvc5/api/Stat.java index 6bcae5322..6218fade4 100644 --- a/src/api/java/io/github/cvc5/api/Stat.java +++ b/src/api/java/io/github/cvc5/api/Stat.java @@ -23,8 +23,8 @@ import java.util.Map; * ({@code Map}). * 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 { @@ -49,15 +49,15 @@ 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? diff --git a/src/api/java/io/github/cvc5/api/Statistics.java b/src/api/java/io/github/cvc5/api/Statistics.java index ad904aa1f..0c64370c0 100644 --- a/src/api/java/io/github/cvc5/api/Statistics.java +++ b/src/api/java/io/github/cvc5/api/Statistics.java @@ -57,9 +57,9 @@ public class Statistics extends AbstractPointer implements Iterable(pointer); - return static_cast(current->isExpert()); + return static_cast(current->isInternal()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } diff --git a/src/decision/justify_stats.cpp b/src/decision/justify_stats.cpp index 23bcfab11..0240852ce 100644 --- a/src/decision/justify_stats.cpp +++ b/src/decision/justify_stats.cpp @@ -22,17 +22,17 @@ namespace decision { 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")) { } diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 44629652d..34175f8f8 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -68,7 +68,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const 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) { diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 12c33601f..7c41e90b8 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -106,12 +106,12 @@ name = "Base" 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" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index a0d0edfa3..a41a2865a 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -205,7 +205,7 @@ void OptionsHandler::setStats(const std::string& flag, bool value) { d_options->base.statisticsAll = false; d_options->base.statisticsEveryQuery = false; - d_options->base.statisticsExpert = false; + d_options->base.statisticsInternal = false; } } diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index 570db1808..e878abcc2 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -202,9 +202,9 @@ bool CadicalSolver::ok() const { return d_inSatMode; } 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")) { } diff --git a/src/util/statistics_public.h b/src/util/statistics_public.h index 6b0a3c934..1e66a6111 100644 --- a/src/util/statistics_public.h +++ b/src/util/statistics_public.h @@ -23,7 +23,7 @@ namespace cvc5 { class StatisticsRegistry; /** - * Preregisters all public (non-expert) statistics. + * Preregisters all public statistics. */ void registerPublicStatistics(StatisticsRegistry& reg); diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 9a87b9f5b..5c43fb2d9 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -32,18 +32,18 @@ StatisticsRegistry::StatisticsRegistry(Env& env, bool registerPublic) } AverageStat StatisticsRegistry::registerAverage(const std::string& name, - bool expert) + bool internal) { - return registerStat(name, expert); + return registerStat(name, internal); } -IntStat StatisticsRegistry::registerInt(const std::string& name, bool expert) +IntStat StatisticsRegistry::registerInt(const std::string& name, bool internal) { - return registerStat(name, expert); + return registerStat(name, internal); } TimerStat StatisticsRegistry::registerTimer(const std::string& name, - bool expert) + bool internal) { - return registerStat(name, expert); + return registerStat(name, internal); } void StatisticsRegistry::storeSnapshot() @@ -53,7 +53,7 @@ void StatisticsRegistry::storeSnapshot() d_lastSnapshot = std::make_unique(); 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, @@ -79,7 +79,7 @@ void StatisticsRegistry::print(std::ostream& os) const { 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; } @@ -92,7 +92,7 @@ void StatisticsRegistry::printSafe(int fd) const { 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); @@ -114,7 +114,7 @@ void StatisticsRegistry::printDiff(std::ostream& os) const } 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); diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 1857ffbe2..671ff6258 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -37,12 +37,10 @@ * * AverageStat is a BackedStat. * - * HistogramStat counts instances of some type T. It is implemented as a - * std::map. - * - * IntegralHistogramStat is a (conceptual) specialization of HistogramStat - * for types that are (convertible to) integral. This allows to use a - * std::vector 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 + * instead of a std::map. * * TimerStat uses std::chrono to collect timing information. It is * implemented as BackedStat and provides methods @@ -100,10 +98,10 @@ struct StatisticBaseValue; * 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 @@ -129,24 +127,24 @@ class StatisticsRegistry : protected EnvObj /** 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 HistogramStat registerHistogram(const std::string& name, - bool expert = true) + bool internal = true) { - return registerStat>(name, expert); + return registerStat>(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 ReferenceStat registerReference(const std::string& name, - bool expert = true) + bool internal = true) { - return registerStat>(name, expert); + return registerStat>(name, internal); } /** * Register a new reference statistic for `name` and initialize it to @@ -155,9 +153,9 @@ class StatisticsRegistry : protected EnvObj template ReferenceStat registerReference(const std::string& name, const T& t, - bool expert = true) + bool internal = true) { - ReferenceStat res = registerStat>(name, expert); + ReferenceStat res = registerStat>(name, internal); res.set(t); return res; } @@ -169,30 +167,30 @@ class StatisticsRegistry : protected EnvObj template SizeStat registerSize(const std::string& name, const T& t, - bool expert = true) + bool internal = true) { - SizeStat res = registerStat>(name, expert); + SizeStat res = registerStat>(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 - ValueStat registerValue(const std::string& name, bool expert = true) + ValueStat registerValue(const std::string& name, bool internal = true) { - return registerStat>(name, expert); + return registerStat>(name, internal); } /** Register a new value statistic for `name` and set it to `init`. */ template ValueStat registerValue(const std::string& name, const T& init, - bool expert = true) + bool internal = true) { - ValueStat res = registerStat>(name, expert); + ValueStat res = registerStat>(name, internal); res.set(init); return res; } @@ -234,7 +232,7 @@ class StatisticsRegistry : protected EnvObj * statistic using `typeid`. */ template - Stat registerStat(const std::string& name, bool expert) + Stat registerStat(const std::string& name, bool internal) { if constexpr (configuration::isStatisticsBuild()) { @@ -243,13 +241,13 @@ class StatisticsRegistry : protected EnvObj { it = d_stats.emplace(name, std::make_unique()) .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(ptr)); } return Stat(nullptr); diff --git a/src/util/statistics_value.h b/src/util/statistics_value.h index 950bdd4ab..66f4c7864 100644 --- a/src/util/statistics_value.h +++ b/src/util/statistics_value.h @@ -67,7 +67,7 @@ struct StatisticBaseValue */ 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); diff --git a/test/regress/regress0/options/statistics.smt2 b/test/regress/regress0/options/statistics.smt2 index d6d5325b0..e27f1e0b6 100644 --- a/test/regress/regress0/options/statistics.smt2 +++ b/test/regress/regress0/options/statistics.smt2 @@ -23,32 +23,32 @@ (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 -- 2.30.2