Renaming CHECK to CVC4_CHECK. This avoids name collisions with other popular assertion macros. This name is likely temporary while Assert() is deprecated. (#1590)

3 files changed, 35 insertions, 32 deletions

diff --git a/src/base/cvc4_check.h b/src/base/cvc4_check.h
index fb4ec0bba..5cb3315f4 100644
--- a/src/base/cvc4_check.h
+++ b/src/base/cvc4_check.h
@@ -11,24 +11,25 @@
  **
  ** \brief Assertion utility classes, functions and macros.
  **
- ** The CHECK utility classes, functions and macros are related to the Assert()
- ** macros defined in base/cvc4_assert.h. The major distinguishing attribute
- ** is the CHECK's abort() the process on failures while Assert() statements
- ** throw C++ exceptions.
+ ** The CVC4_CHECK utility classes, functions and macros are related to the
+ ** Assert() macros defined in base/cvc4_assert.h. The major distinguishing
+ ** attribute is the CVC4_CHECK's abort() the process on failures while
+ ** Assert() statements throw C++ exceptions.
  **
- ** The main usage in the file is the CHECK macros. The CHECK macros assert a
- ** condition and aborts()'s the process if the condition is not satisfied. The
- ** macro leaves a hanging ostream for the user to specify additional
- ** information about the failure. Example usage:
- **   CHECK(x >= 0) << "x must be positive.";
+ ** The main usage in the file is the CVC4_CHECK macros. The CVC4_CHECK macros
+ ** assert a condition and aborts()'s the process if the condition is not
+ ** satisfied. The macro leaves a hanging ostream for the user to specify
+ ** additional information about the failure. Example usage:
+ **   CVC4_CHECK(x >= 0) << "x must be positive.";
  **
- ** DCHECK is a CHECK that is only enabled in debug builds.
- **   DCHECK(pointer != nullptr);
+ ** CVC4_DCHECK is a CVC4_CHECK that is only enabled in debug builds.
+ **   CVC4_DCHECK(pointer != nullptr);
  **
  ** CVC4_FATAL() can be used to indicate unreachable code.
  **
- ** The CHECK and DCHECK macros are not safe for use in signal-handling code.
- ** TODO(taking): Add a signal-handling safe version of CHECK.
+ ** The CVC4_CHECK and CVC4_DCHECK macros are not safe for use in
+ ** signal-handling code. In future, a a signal-handling safe version of
+ ** CVC4_CHECK may be added.
  **/
 
 #include "cvc4_private.h"
@@ -65,10 +66,11 @@ namespace CVC4 {
 
 // Implementation notes:
 // To understand FatalStream and OStreamVoider, it is useful to understand
-// how a CHECK is structured. CHECK(cond) is roughly the following pattern:
+// how a CVC4_CHECK is structured. CVC4_CHECK(cond) is roughly the following
+// pattern:
 //  cond ? (void)0 : OstreamVoider() & FatalStream().stream()
 // This is a carefully crafted message to achieve a hanging ostream using
-// operator precedence. The line `CHECK(cond) << foo << bar;` will bind as
+// operator precedence. The line `CVC4_CHECK(cond) << foo << bar;` will bind as
 // follows:
 //  `cond ? ((void)0) : (OSV() & ((FS().stream() << foo) << bar));`
 // Once the expression is evaluated, the destructor ~FatalStream() of the
@@ -123,19 +125,19 @@ class OstreamVoider
 // If `cond` is false, log an error message and abort()'s the process.
 // Otherwise, does nothing. This leaves a hanging std::ostream& that can be
 // inserted into using operator<<. Example usages:
-//   CHECK(x >= 0);
-//   CHECK(x >= 0) << "x must be positive";
-//   CHECK(x >= 0) << "expected a positive value. Got " << x << " instead";
-#define CHECK(cond)                                               \
+//   CVC4_CHECK(x >= 0);
+//   CVC4_CHECK(x >= 0) << "x must be positive";
+//   CVC4_CHECK(x >= 0) << "expected a positive value. Got " << x << " instead";
+#define CVC4_CHECK(cond)                                          \
   CVC4_FATAL_IF(!(cond), __PRETTY_FUNCTION__, __FILE__, __LINE__) \
       << "Check failure\n\n " << #cond << "\n"
 
-// DCHECK is a variant of CHECK() that is only checked when CVC4_ASSERTIONS is
-// defined. We rely on the optimizer to remove the deadcode.
+// CVC4_DCHECK is a variant of CVC4_CHECK() that is only checked when
+// CVC4_ASSERTIONS is defined. We rely on the optimizer to remove the deadcode.
 #ifdef CVC4_ASSERTIONS
-#define DCHECK(cond) CHECK(cond)
+#define CVC4_DCHECK(cond) CVC4_CHECK(cond)
 #else
-#define DCHECK(cond) \
+#define CVC4_DCHECK(cond) \
   CVC4_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__)
 #endif /* CVC4_DEBUG */
 
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 2dd1eddd7..b9f6998d4 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -77,7 +77,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) {
     nsec -= nsec_per_sec;
     ++a.tv_sec;
   }
-  DCHECK(nsec >= 0 && nsec < nsec_per_sec);
+  CVC4_DCHECK(nsec >= 0 && nsec < nsec_per_sec);
   a.tv_nsec = nsec;
   return a;
 }
@@ -168,9 +168,10 @@ void StatisticsRegistry::registerStat(Stat* s)
 void StatisticsRegistry::unregisterStat(Stat* s)
 {
 #ifdef CVC4_STATISTICS_ON
-  CHECK(s != nullptr);
-  CHECK(d_stats.erase(s) > 0) << "Statistic `" << s->getName()
-                              << "' was not registered with this registry.";
+  CVC4_CHECK(s != nullptr);
+  CVC4_CHECK(d_stats.erase(s) > 0)
+      << "Statistic `" << s->getName()
+      << "' was not registered with this registry.";
 #endif /* CVC4_STATISTICS_ON */
 } /* StatisticsRegistry::unregisterStat() */
 
@@ -202,7 +203,7 @@ void TimerStat::start() {
 
 void TimerStat::stop() {
   if(__CVC4_USE_STATISTICS) {
-    CHECK(d_running) << "timer not running";
+    CVC4_CHECK(d_running) << "timer not running";
     ::timespec end;
     clock_gettime(CLOCK_MONOTONIC, &end);
     d_data += end - d_start;
diff --git a/test/unit/util/check_white.h b/test/unit/util/check_white.h
index e57afa6c7..b0c540265 100644
--- a/test/unit/util/check_white.h
+++ b/test/unit/util/check_white.h
@@ -39,19 +39,19 @@ class CheckWhite : public CxxTest::TestSuite
                     "return type.";
   }
 
-  void testCheck() { CHECK(kOne >= 0) << kOne << " must be positive"; }
+  void testCheck() { CVC4_CHECK(kOne >= 0) << kOne << " must be positive"; }
   void testDCheck()
   {
-    DCHECK(kOne == 1) << "always passes";
+    CVC4_DCHECK(kOne == 1) << "always passes";
 #ifndef CVC4_ASSERTIONS
-    DCHECK(false) << "Will not be compiled in when CVC4_ASSERTIONS off.";
+    CVC4_DCHECK(false) << "Will not be compiled in when CVC4_ASSERTIONS off.";
 #endif /* CVC4_ASSERTIONS */
   }
 
   void testPointerTypeCanBeTheCondition()
   {
     const int* one_pointer = &kOne;
-    CHECK(one_pointer);
+    CVC4_CHECK(one_pointer);
   }
 };