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

6 files changed, 38 insertions, 33 deletions

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index 7ba689d0a..4b5873e80 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -23,6 +23,7 @@
 
 #include "preprocessing/passes/ackermann.h"
 
+#include "base/check.h"
 #include "options/options.h"
 
 using namespace CVC4;
@@ -169,9 +170,8 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
       }
       else
       {
-        AlwaysAssert(
-            term.getKind() != kind::STORE,
-            "Cannot use Ackermannization on formula with stores to arrays");
+        AlwaysAssert(term.getKind() != kind::STORE)
+            << "Cannot use Ackermannization on formula with stores to arrays";
         /* add children to the vector, so that they are processed later */
         for (TNode n : term)
         {
diff --git a/src/preprocessing/passes/apply_to_const.cpp b/src/preprocessing/passes/apply_to_const.cpp
index 12591db0b..e8681e40c 100644
--- a/src/preprocessing/passes/apply_to_const.cpp
+++ b/src/preprocessing/passes/apply_to_const.cpp
@@ -67,12 +67,11 @@ Node ApplyToConst::rewriteApplyToConst(TNode n, NodeMap& cache)
       Trace("rewriteApplyToConst") << "made :: " << newvar << std::endl;
       return newvar;
     }
-    stringstream ss;
-    ss << "The rewrite-apply-to-const preprocessor is currently limited;\n"
-       << "it only works if all function symbols are unary and with Integer\n"
-       << "domain, and all applications are to integer values.\n"
-       << "Found application: " << n;
-    Unhandled(ss.str());
+    Unhandled()
+        << "The rewrite-apply-to-const preprocessor is currently limited;\n"
+        << "it only works if all function symbols are unary and with Integer\n"
+        << "domain, and all applications are to integer values.\n"
+        << "Found application: " << n;
   }
 
   NodeBuilder<> builder(n.getKind());
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index 09d963ba3..0f2674680 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -264,7 +264,7 @@ BVGauss::Result BVGauss::gaussElim(Integer prime,
 
   #ifdef CVC4_ASSERTIONS
   for (size_t i = 1; i < nrows; ++i) Assert(lhs[i].size() == ncols);
-  #endif
+#endif
   /* (1) if element in pivot column is non-zero and != 1, divide row elements
    *     by element in pivot column modulo prime, i.e., multiply row with
    *     multiplicative inverse of element in pivot column modulo prime
@@ -284,7 +284,10 @@ BVGauss::Result BVGauss::gaussElim(Integer prime,
     for (size_t j = prow; j < nrows; ++j)
     {
 #ifdef CVC4_ASSERTIONS
-      for (size_t k = 0; k < pcol; ++k) { Assert(lhs[j][k] == 0); }
+      for (size_t k = 0; k < pcol; ++k)
+      {
+        Assert(lhs[j][k] == 0);
+      }
 #endif
       /* normalize element in pivot column to modulo prime */
       lhs[j][pcol] = lhs[j][pcol].euclidianDivideRemainder(prime);
@@ -571,7 +574,10 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
   Assert(nvars);
   size_t nrows = vars.begin()->second.size();
 #ifdef CVC4_ASSERTIONS
-  for (const auto& p : vars) { Assert(p.second.size() == nrows); }
+  for (const auto& p : vars)
+  {
+    Assert(p.second.size() == nrows);
+  }
 #endif
 
   if (nrows < 1)
@@ -588,7 +594,10 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
   }
 
 #ifdef CVC4_ASSERTIONS
-  for (const auto& row : lhs) { Assert(row.size() == nvars); }
+  for (const auto& row : lhs)
+  {
+    Assert(row.size() == nvars);
+  }
   Assert(lhs.size() == rhs.size());
 #endif
 
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 37bc363f8..d6259294a 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -447,7 +447,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
           {  // exclude single-var case; nothing to check there
             uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1;
             sz = (sz == 0) ? -1 : sz;  // fix for overflow
-            Assert(sz == mark, "expected size %u == mark %u", sz, mark);
+            Assert(sz == mark) << "expected size " << sz << " == mark " << mark;
             for (size_t k = 0; k < checks[pos_var].size(); ++k)
             {
               if ((k & (k - 1)) != 0)
@@ -476,14 +476,11 @@ PreprocessingPassResult MipLibTrick::applyInternal(
               }
               else
               {
-                Assert(checks[pos_var][k] == 0,
-                       "checks[(%s,%s)][%u] should be 0, but it's %s",
-                       pos.toString().c_str(),
-                       var.toString().c_str(),
-                       k,
-                       checks[pos_var][k]
-                           .toString()
-                           .c_str());  // we never set for single-positive-var
+                Assert(checks[pos_var][k] == 0)
+                    << "checks[(" << pos << "," << var << ")][" << k
+                    << "] should be 0, but it's "
+                    << checks[pos_var]
+                             [k];  // we never set for single-positive-var
               }
             }
           }
@@ -529,15 +526,15 @@ PreprocessingPassResult MipLibTrick::applyInternal(
               SubstitutionMap nullMap(&fakeContext);
               Theory::PPAssertStatus status CVC4_UNUSED;  // just for assertions
               status = te->solve(geq, nullMap);
-              Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED,
-                     "unexpected solution from arith's ppAssert()");
-              Assert(nullMap.empty(),
-                     "unexpected substitution from arith's ppAssert()");
+              Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED)
+                  << "unexpected solution from arith's ppAssert()";
+              Assert(nullMap.empty())
+                  << "unexpected substitution from arith's ppAssert()";
               status = te->solve(leq, nullMap);
-              Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED,
-                     "unexpected solution from arith's ppAssert()");
-              Assert(nullMap.empty(),
-                     "unexpected substitution from arith's ppAssert()");
+              Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED)
+                  << "unexpected solution from arith's ppAssert()";
+              Assert(nullMap.empty())
+                  << "unexpected substitution from arith's ppAssert()";
               te->getModel()->addSubstitution(*ii, newVar.eqNode(one));
               newVars.push_back(newVar);
               varRef = newVar;
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 0f71943c9..1d834ce60 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -199,7 +199,7 @@ bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
 }
 
 bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
-  Assert( n.getKind()==APPLY_UF );
+  Assert(n.getKind() == APPLY_UF);
   TypeNode tno = n.getOperator().getType();
   std::map< Node, bool > vars;
   // allow if a vector of unique variables of the same type as UF arguments
@@ -437,7 +437,7 @@ Node QuantifierMacros::simplify( Node n ){
             }else if( !etc.isConst() ){
               cond.push_back( etc );
             }
-            Assert( children[i].getType().isSubtypeOf( tno[i] ) );
+            Assert(children[i].getType().isSubtypeOf(tno[i]));
           }
           if( success ){
             //do substitution if necessary
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index 82132774b..5df449237 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -20,7 +20,7 @@
 #include <algorithm>
 #include <utility>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/map_util.h"
 #include "base/output.h"
 #include "preprocessing/passes/ackermann.h"