From 966407c1490695bdac2a4d95397625adbcce433a Mon Sep 17 00:00:00 2001 From: Matthew Sotoudeh Date: Mon, 10 Jan 2022 10:29:10 -0800 Subject: [PATCH] Avoid gcc/10.1.0 bug by moving some configuration into a namespace Eventually there is intention to move all of cvc5::Configuration into cvc5::configuration, this is a first step that also has the nice side-effect of letting it build under an otherwise-buggy version of gcc/10.1.0 that was causing issues. Signed-off-by: Matthew Sotoudeh --- src/api/cpp/cvc5.cpp | 6 +++--- src/base/configuration.h | 24 +++++++++++++++--------- src/options/options_handler.cpp | 2 +- src/util/statistics_registry.cpp | 10 +++++----- src/util/statistics_registry.h | 2 +- src/util/statistics_stats.cpp | 24 ++++++++++++------------ src/util/statistics_stats.h | 18 +++++++++--------- 7 files changed, 46 insertions(+), 40 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 868fdd028..aa1f2eb6e 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5038,7 +5038,7 @@ NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr; } void Solver::increment_term_stats(Kind kind) const { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_stats->d_terms << kind; } @@ -5046,7 +5046,7 @@ void Solver::increment_term_stats(Kind kind) const void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { const TypeNode tn = sort.getTypeNode(); TypeConstant tc = tn.getKind() == cvc5::kind::TYPE_CONSTANT @@ -5465,7 +5465,7 @@ bool Solver::isValidInteger(const std::string& s) const void Solver::resetStatistics() { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_stats.reset(new APIStatistics{ d_slv->getStatisticsRegistry().registerHistogram( diff --git a/src/base/configuration.h b/src/base/configuration.h index 816a70741..ece91c4ae 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -12,6 +12,10 @@ * * Interface to a public class that provides compile-time information * about the cvc5 library. + * + * Eventually, the configuration methods will all be migrated to the + * cvc5::configuration namespace below. This is cleaner and avoids a gcc/10.1.0 + * bug. See https://github.com/cvc5/cvc5/pull/7898 for details. */ #include "cvc5_public.h" @@ -26,6 +30,17 @@ namespace cvc5 { +namespace configuration { + static constexpr bool isStatisticsBuild() + { +#ifdef CVC5_STATISTICS_ON + return true; +#else + return false; +#endif + } +} // namespace configuration + /** * Represents the (static) configuration of cvc5. */ @@ -48,15 +63,6 @@ public: static bool isDebugBuild(); - static constexpr bool isStatisticsBuild() - { -#ifdef CVC5_STATISTICS_ON - return true; -#else - return false; -#endif - } - static bool isTracingBuild(); static bool isMuzzledBuild(); diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 132525e6d..cdb9bdeab 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -428,7 +428,7 @@ void OptionsHandler::showConfiguration(const std::string& flag, bool value) std::cout << std::endl; print_config_cond("debug code", Configuration::isDebugBuild()); - print_config_cond("statistics", Configuration::isStatisticsBuild()); + print_config_cond("statistics", configuration::isStatisticsBuild()); print_config_cond("tracing", Configuration::isTracingBuild()); print_config_cond("muzzled", Configuration::isMuzzledBuild()); print_config_cond("assertions", Configuration::isAssertionBuild()); diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 815c61059..9a87b9f5b 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -48,7 +48,7 @@ TimerStat StatisticsRegistry::registerTimer(const std::string& name, void StatisticsRegistry::storeSnapshot() { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_lastSnapshot = std::make_unique(); for (const auto& s : d_stats) @@ -64,7 +64,7 @@ void StatisticsRegistry::storeSnapshot() StatisticBaseValue* StatisticsRegistry::get(const std::string& name) const { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { auto it = d_stats.find(name); if (it == d_stats.end()) return nullptr; @@ -75,7 +75,7 @@ StatisticBaseValue* StatisticsRegistry::get(const std::string& name) const void StatisticsRegistry::print(std::ostream& os) const { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { for (const auto& s : d_stats) { @@ -88,7 +88,7 @@ void StatisticsRegistry::print(std::ostream& os) const void StatisticsRegistry::printSafe(int fd) const { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { for (const auto& s : d_stats) { @@ -104,7 +104,7 @@ void StatisticsRegistry::printSafe(int fd) const } void StatisticsRegistry::printDiff(std::ostream& os) const { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { if (!d_lastSnapshot) { diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 923880dbf..1857ffbe2 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -236,7 +236,7 @@ class StatisticsRegistry : protected EnvObj template Stat registerStat(const std::string& name, bool expert) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { auto it = d_stats.find(name); if (it == d_stats.end()) diff --git a/src/util/statistics_stats.cpp b/src/util/statistics_stats.cpp index 1ecbf61ce..9adbe3bb1 100644 --- a/src/util/statistics_stats.cpp +++ b/src/util/statistics_stats.cpp @@ -22,7 +22,7 @@ namespace cvc5 { AverageStat& AverageStat::operator<<(double v) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->d_sum += v; d_data->d_count++; @@ -32,7 +32,7 @@ AverageStat& AverageStat::operator<<(double v) IntStat& IntStat::operator=(int64_t val) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->d_value = val; } @@ -41,7 +41,7 @@ IntStat& IntStat::operator=(int64_t val) IntStat& IntStat::operator++() { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->d_value++; } @@ -50,7 +50,7 @@ IntStat& IntStat::operator++() IntStat& IntStat::operator++(int) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->d_value++; } @@ -59,7 +59,7 @@ IntStat& IntStat::operator++(int) IntStat& IntStat::operator+=(int64_t val) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->d_value += val; } @@ -68,7 +68,7 @@ IntStat& IntStat::operator+=(int64_t val) void IntStat::maxAssign(int64_t val) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { if (d_data->d_value < val) { @@ -79,7 +79,7 @@ void IntStat::maxAssign(int64_t val) void IntStat::minAssign(int64_t val) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { if (d_data->d_value > val) { @@ -90,7 +90,7 @@ void IntStat::minAssign(int64_t val) void TimerStat::start() { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { Assert(!d_data->d_running) << "timer is already running"; d_data->d_start = StatisticTimerValue::clock::now(); @@ -99,7 +99,7 @@ void TimerStat::start() } void TimerStat::stop() { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { Assert(d_data->d_running) << "timer is not running"; d_data->d_duration += StatisticTimerValue::clock::now() - d_data->d_start; @@ -108,7 +108,7 @@ void TimerStat::stop() } bool TimerStat::running() const { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { return d_data->d_running; } @@ -118,7 +118,7 @@ bool TimerStat::running() const CodeTimer::CodeTimer(TimerStat& timer, bool allow_reentrant) : d_timer(timer), d_reentrant(false) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { if (!allow_reentrant || !(d_reentrant = d_timer.running())) { @@ -128,7 +128,7 @@ CodeTimer::CodeTimer(TimerStat& timer, bool allow_reentrant) } CodeTimer::~CodeTimer() { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { if (!d_reentrant) { diff --git a/src/util/statistics_stats.h b/src/util/statistics_stats.h index 982190b79..0cbe0a99b 100644 --- a/src/util/statistics_stats.h +++ b/src/util/statistics_stats.h @@ -86,7 +86,7 @@ class HistogramStat /** Add the value `val` to the histogram */ HistogramStat& operator<<(Integral val) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->add(val); } @@ -126,7 +126,7 @@ class ReferenceStat void set(const TT& t) { static_assert(std::is_same_v, "Incorrect type for ReferenceStat"); - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->d_value = &t; } @@ -134,7 +134,7 @@ class ReferenceStat /** Commit the value currently pointed to and release it. */ void reset() { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->commit(); d_data->d_value = nullptr; @@ -143,7 +143,7 @@ class ReferenceStat /** Copy the current value of the referenced object. */ ~ReferenceStat() { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->commit(); } @@ -174,7 +174,7 @@ class SizeStat /** Reset the reference to point to `t`. */ void set(const T& t) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->d_value = &t; } @@ -182,7 +182,7 @@ class SizeStat /** Copy the current size of the referenced container. */ ~SizeStat() { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->commit(); } @@ -286,7 +286,7 @@ class ValueStat /** Set to `t` */ void set(const T& t) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_data->d_value = t; } @@ -294,7 +294,7 @@ class ValueStat /** Set to `t` */ ValueStat& operator=(const T& t) { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { set(t); } @@ -302,7 +302,7 @@ class ValueStat } T get() const { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { return d_data->d_value; } -- 2.30.2