Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

11 files changed, 50 insertions, 51 deletions

diff --git a/src/context/backtrackable.h b/src/context/backtrackable.h
index 5d358941f..85281e7fa 100644
--- a/src/context/backtrackable.h
+++ b/src/context/backtrackable.h
@@ -160,7 +160,7 @@ template <class T>
 void List<T>::concat (List<T>* other) {
   bck->checkConsistency();
   bck->notifyConcat(this, other);
-  Assert(tail->next==NULL);
+  Assert(tail->next == NULL);
   tail->next = other->head;
   Assert(other->ptr_to_head == NULL);
   other->ptr_to_head = tail;
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 05d68ead5..fc42c0e85 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -88,9 +88,9 @@
 #include <unordered_map>
 #include <vector>
 
-#include "base/cvc4_assert.h"
-#include "context/context.h"
+#include "base/check.h"
 #include "context/cdhashmap_forward.h"
+#include "context/context.h"
 
 namespace CVC4 {
 namespace context {
@@ -278,7 +278,11 @@ class CDHashMap : public ContextObj {
   Context* d_context;
 
   // Nothing to save; the elements take care of themselves
-  ContextObj* save(ContextMemoryManager* pCMM) override { Unreachable(); }
+  ContextObj* save(ContextMemoryManager* pCMM) override
+  {
+    Unreachable();
+    SuppressWrongNoReturnWarning;
+  }
 
   // Similarly, nothing to restore
   void restore(ContextObj* data) override { Unreachable(); }
diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h
index a35ecae88..57cd101a9 100644
--- a/src/context/cdhashset.h
+++ b/src/context/cdhashset.h
@@ -19,10 +19,9 @@
 #ifndef CVC4__CONTEXT__CDHASHSET_H
 #define CVC4__CONTEXT__CDHASHSET_H
 
-#include "base/cvc4_assert.h"
-#include "context/context.h"
+#include "base/check.h"
 #include "context/cdinsert_hashmap.h"
-
+#include "context/context.h"
 
 namespace CVC4 {
 namespace context {
@@ -51,7 +50,7 @@ public:
   }
 
   static void operator delete(void* pMem) {
-    AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!");
+    AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!";
   }
 
   CDHashSet(Context* context) :
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index f15c418eb..0b3c713d2 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -38,13 +38,12 @@
 #include <unordered_map>
 #include <utility>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/output.h"
-#include "context/context.h"
 #include "context/cdinsert_hashmap_forward.h"
+#include "context/context.h"
 #include "expr/node.h"
 
-
 #pragma once
 
 namespace CVC4 {
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index dda88a0fd..95501df8e 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -25,10 +25,10 @@
 #include <string>
 #include <sstream>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
+#include "context/cdlist_forward.h"
 #include "context/context.h"
 #include "context/context_mm.h"
-#include "context/cdlist_forward.h"
 
 namespace CVC4 {
 namespace context {
@@ -139,8 +139,8 @@ private:
       size_t newSize = GROWTH_FACTOR * d_sizeAlloc;
       if(newSize > d_allocator.max_size()) {
         newSize = d_allocator.max_size();
-        Assert(newSize > d_sizeAlloc,
-               "cannot request larger list due to allocator limits");
+        Assert(newSize > d_sizeAlloc)
+            << "cannot request larger list due to allocator limits";
       }
       T* newList = d_allocator.allocate(newSize);
       Debug("cdlist") << "2x grow of cdlist " << this
@@ -306,7 +306,7 @@ public:
    * Access to the ith item in the list.
    */
   const T& operator[](size_t i) const {
-    Assert(i < d_size, "index out of bounds in CDList::operator[]");
+    Assert(i < d_size) << "index out of bounds in CDList::operator[]";
     return d_list[i];
   }
 
@@ -314,7 +314,7 @@ public:
    * Returns the most recent item added to the list.
    */
   const T& back() const {
-    Assert(d_size > 0, "CDList::back() called on empty list");
+    Assert(d_size > 0) << "CDList::back() called on empty list";
     return d_list[d_size - 1];
   }
 
diff --git a/src/context/cdo.h b/src/context/cdo.h
index fe588afb0..b7d32d856 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -19,7 +19,6 @@
 #ifndef CVC4__CONTEXT__CDO_H
 #define CVC4__CONTEXT__CDO_H
 
-#include "base/cvc4_assert.h"
 #include "context/context.h"
 
 
diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h
index 6ad0e9339..079d2265c 100644
--- a/src/context/cdqueue.h
+++ b/src/context/cdqueue.h
@@ -125,21 +125,21 @@ public:
    * function.
    */
   void pop(){
-    Assert(!empty(), "Attempting to pop from an empty queue.");
+    Assert(!empty()) << "Attempting to pop from an empty queue.";
     ParentType::makeCurrent();
     d_iter = d_iter + 1;
     if (empty() && d_lastsave != ParentType::d_size) {
       // Some elements have been enqueued and dequeued in the same
       // context and now the queue is empty we can destruct them.
       ParentType::truncateList(d_lastsave);
-      Assert(ParentType::d_size ==  d_lastsave);
+      Assert(ParentType::d_size == d_lastsave);
       d_iter = d_lastsave;
     }
   }
 
   /** Returns a reference to the next element on the queue. */
   const T& front() const{
-    Assert(!empty(), "No front in an empty queue.");
+    Assert(!empty()) << "No front in an empty queue.";
     return ParentType::d_list[d_iter];
   }
 
@@ -147,7 +147,7 @@ public:
    * Returns the most recent item added to the queue.
    */
   const T& back() const {
-    Assert(!empty(), "CDQueue::back() called on empty list");
+    Assert(!empty()) << "CDQueue::back() called on empty list";
     return ParentType::d_list[ParentType::d_size - 1];
   }
 
diff --git a/src/context/cdtrail_queue.h b/src/context/cdtrail_queue.h
index ad2bef54c..4042c4223 100644
--- a/src/context/cdtrail_queue.h
+++ b/src/context/cdtrail_queue.h
@@ -74,7 +74,7 @@ public:
 
   /** Moves the iterator for the queue forward. */
   void dequeue(){
-    Assert(!empty(), "Attempting to queue from an empty queue.");
+    Assert(!empty()) << "Attempting to queue from an empty queue.";
     d_iter = d_iter + 1;
   }
 
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 310f88b04..e1de944fe 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -18,7 +18,7 @@
 #include <iostream>
 #include <vector>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "context/context.h"
 
 
@@ -72,7 +72,7 @@ void Context::push() {
 
 
 void Context::pop() {
-  Assert(getLevel() > 0, "Cannot pop below level 0");
+  Assert(getLevel() > 0) << "Cannot pop below level 0";
 
   // Notify the (pre-pop) ContextNotifyObj objects
   ContextNotifyObj* pCNO = d_pCNOpre;
@@ -149,11 +149,11 @@ void ContextObj::update()
                    << *getContext() << std::endl;
 
   // Check that base class data was saved
-  Assert( ( pContextObjSaved->d_pContextObjNext == d_pContextObjNext &&
-            pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev &&
-            pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore &&
-            pContextObjSaved->d_pScope == d_pScope ),
-          "save() did not properly copy information in base class" );
+  Assert((pContextObjSaved->d_pContextObjNext == d_pContextObjNext
+          && pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev
+          && pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore
+          && pContextObjSaved->d_pScope == d_pScope))
+      << "save() did not properly copy information in base class";
 
   // Link the "saved" object in place of this ContextObj in the scope
   // we're moving it FROM.
@@ -204,8 +204,8 @@ ContextObj* ContextObj::restoreAndContinue()
     // might not be bottom scope, since objects allocated in context
     // memory don't get linked to scope 0
     //
-    // Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
-    //        "Expected bottom scope");
+    // Assert(d_pScope == d_pScope->getContext()->getBottomScope()) <<
+    //        "Expected bottom scope";
 
     Debug("context") << "NULL restore object! " << this << std::endl;
     pContextObjNext = d_pContextObjNext;
@@ -270,8 +270,7 @@ ContextObj::ContextObj(Context* pContext) :
   d_pContextObjRestore(NULL),
   d_pContextObjNext(NULL),
   d_ppContextObjPrev(NULL) {
-
-  Assert(pContext != NULL, "NULL context pointer");
+  Assert(pContext != NULL) << "NULL context pointer";
 
   Debug("context") << "create new ContextObj(" << this << " inCMM=false)" << std::endl;
   d_pScope = pContext->getBottomScope();
@@ -284,8 +283,7 @@ ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
   d_pContextObjRestore(NULL),
   d_pContextObjNext(NULL),
   d_ppContextObjPrev(NULL) {
-
-  Assert(pContext != NULL, "NULL context pointer");
+  Assert(pContext != NULL) << "NULL context pointer";
 
   Debug("context") << "create new ContextObj(" << this << " inCMM=" << allocatedInCMM << ")" << std::endl;
   if(allocatedInCMM) {
@@ -341,16 +339,16 @@ std::ostream& operator<<(std::ostream& out, const Scope& scope)
 {
   out << "Scope " << scope.d_level << " [" << &scope << "]:";
   ContextObj* pContextObj = scope.d_pContextObjList;
-  Assert(pContextObj == NULL ||
-         pContextObj->prev() == &scope.d_pContextObjList);
+  Assert(pContextObj == NULL
+         || pContextObj->prev() == &scope.d_pContextObjList);
   while(pContextObj != NULL) {
     out << " <--> " << pContextObj;
     if(pContextObj->d_pScope != &scope) {
       out << " XXX bad scope" << std::endl;
     }
     Assert(pContextObj->d_pScope == &scope);
-    Assert(pContextObj->next() == NULL ||
-           pContextObj->next()->prev() == &pContextObj->next());
+    Assert(pContextObj->next() == NULL
+           || pContextObj->next()->prev() == &pContextObj->next());
     pContextObj = pContextObj->next();
   }
   return out << " --> NULL";
diff --git a/src/context/context.h b/src/context/context.h
index d9d73f770..2bfc83a43 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -27,7 +27,7 @@
 #include <typeinfo>
 #include <vector>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/output.h"
 #include "context/context_mm.h"
 
@@ -135,10 +135,10 @@ public:
     }
     ~ScopedPush() noexcept(false) {
       d_context->pop();
-      AlwaysAssert(d_context->getTopScope() == d_scope,
-                   "Context::ScopedPush observed an uneven Context (at pop, "
-                   "top scope doesn't match what it was at the time the "
-                   "ScopedPush was applied)");
+      AlwaysAssert(d_context->getTopScope() == d_scope)
+          << "Context::ScopedPush observed an uneven Context (at pop, "
+             "top scope doesn't match what it was at the time the "
+             "ScopedPush was applied)";
     }
   };/* Context::ScopedPush */
 
@@ -569,7 +569,7 @@ class ContextObj {
    * calling deleteSelf().
    */
   static void operator delete(void* pMem) {
-    AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!");
+    AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!";
   }
 
   /**
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index 76a2168d1..a9186f5f9 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -24,7 +24,7 @@
 #include <valgrind/memcheck.h>
 #endif /* CVC4_VALGRIND */
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/output.h"
 #include "context/context_mm.h"
 
@@ -37,8 +37,8 @@ void ContextMemoryManager::newChunk() {
 
   // Increment index to chunk list
   ++d_indexChunkList;
-  Assert(d_chunkList.size() == d_indexChunkList,
-         "Index should be at the end of the list");
+  Assert(d_chunkList.size() == d_indexChunkList)
+      << "Index should be at the end of the list";
 
   // Create new chunk if no free chunk available
   if(d_freeChunks.empty()) {
@@ -105,8 +105,8 @@ void* ContextMemoryManager::newData(size_t size) {
     newChunk();
     res = (void*)d_nextFree;
     d_nextFree += size;
-    AlwaysAssert(d_nextFree <= d_endChunk,
-                 "Request is bigger than memory chunk size");
+    AlwaysAssert(d_nextFree <= d_endChunk)
+        << "Request is bigger than memory chunk size";
   }
   Debug("context") << "ContextMemoryManager::newData(" << size
                    << ") returning " << res << " at level "