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 <sotoudeh@stanford.edu>

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 868fdd028c6c3604df0abe4b2da46378533e5d30..aa1f2eb6e6da599b4fd388387350d657bb7fb1fb 100644 (file)
--- 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<TypeConstant>(

diff --git a/src/base/configuration.h b/src/base/configuration.h
index 816a70741a1785561291096c8de56f0a8cf01d83..ece91c4ae71486b4d7cb60ca0e838be143f9edce 100644 (file)
--- 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 132525e6d3248a8fca4c3b55e2af0f64f982192e..cdb9bdeabbf090b882e275d95563832a431b47fb 100644 (file)
--- 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 815c61059beee8fcd37f34bd08ee1ee17ad21565..9a87b9f5b4f3bf285ee7a65df749588c3c92c987 100644 (file)
--- 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<Snapshot>();
     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 923880dbf181a0f4e2cb50daf63ffb7b59e4e1ea..1857ffbe20f492c61d171b59cc11354370db5765 100644 (file)
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -236,7 +236,7 @@ class StatisticsRegistry : protected EnvObj
   template <typename Stat>
   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 1ecbf61ce147643705b09a57a1b3ecbe94b99e31..9adbe3bb13b8d7544325aba8a77b7475c7ed1f6c 100644 (file)
--- 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 982190b7970c5d963793a843a6eaf77e520552f3..0cbe0a99b630bbe84acdc6ce582fca082c54480e 100644 (file)
--- 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<T, TT>, "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<T>& 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;
     }