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

18 files changed, 41 insertions, 47 deletions

diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp
index 7c3ce6aaf..49247ee38 100644
--- a/src/util/abstract_value.cpp
+++ b/src/util/abstract_value.cpp
@@ -20,7 +20,7 @@
 #include <sstream>
 #include <string>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 
 using namespace std;
 
diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h
index d6a7c95d7..7ada9a655 100644
--- a/src/util/bin_heap.h
+++ b/src/util/bin_heap.h
@@ -26,7 +26,7 @@
 #include <limits>
 #include <functional>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/exception.h"
 
 namespace CVC4 {
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index ce1763ba1..6615f8378 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -16,7 +16,7 @@
 
 #include "util/cardinality.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 
 namespace CVC4 {
 
@@ -174,9 +174,10 @@ Cardinality& Cardinality::operator^=(const Cardinality& c) {
     // inf ^ finite == inf
     return *this;
   } else {
-    Assert(compare(2) != LESS && !c.isFinite(),
-           "fall-through case not as expected:\n%s\n%s",
-           this->toString().c_str(), c.toString().c_str());
+    Assert(compare(2) != LESS && !c.isFinite())
+        << "fall-through case not as expected:\n"
+        << this << "\n"
+        << c;
     // (>= 2) ^ beth_k == beth_(k+1)
     // unless the base is already > the exponent
     if (compare(c) == GREATER) {
diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index cc1a094eb..08da8faaa 100644
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -29,7 +29,7 @@
 #include <limits>
 #include <vector>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "util/index.h"
 
 
@@ -101,7 +101,7 @@ public:
     if( x >= allocated()){
       return false;
     }else{
-      Assert(x <  allocated());
+      Assert(x < allocated());
       return d_posVector[x] != +POSITION_SENTINEL;
     }
   }
diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp
index f336a318c..c89886fa8 100644
--- a/src/util/divisible.cpp
+++ b/src/util/divisible.cpp
@@ -17,7 +17,7 @@
 
 #include "util/divisible.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/exception.h"
 
 using namespace std;
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index f7e73ca4b..1b1bfddc2 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -15,7 +15,7 @@
  **/
 
 #include "util/floatingpoint.h"
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "util/integer.h"
 
 #include <math.h>
@@ -459,7 +459,7 @@ void traits::invariant(const prop &p)
 #ifndef CVC4_USE_SYMFPU
 void FloatingPointLiteral::unfinished(void) const
 {
-  Unimplemented("Floating-point literals not yet implemented.");
+  Unimplemented() << "Floating-point literals not yet implemented.";
 }
 #endif
 
@@ -500,7 +500,7 @@ static FloatingPointLiteral constructorHelperBitVector(
 #else
   return FloatingPointLiteral(2, 2, 0.0);
 #endif
-  Unreachable("Constructor helper broken");
+  Unreachable() << "Constructor helper broken";
   }
   
   FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) :
@@ -592,7 +592,7 @@ static FloatingPointLiteral constructorHelperBitVector(
 
       // Compute the sticky bit
       Rational remainder(r - workingSig);
-      Assert(Rational(0,1) <= remainder);
+      Assert(Rational(0, 1) <= remainder);
 
       if (!remainder.isZero()) {
 	sig = sig | one;
@@ -616,10 +616,10 @@ static FloatingPointLiteral constructorHelperBitVector(
           symfpu::convertFloatToFloat(exactFormat, ct, rm, exactFloat));
       return rounded;
 #else
-      Unreachable("no concrete implementation of FloatingPointLiteral");
+      Unreachable() << "no concrete implementation of FloatingPointLiteral";
 #endif
     }
-    Unreachable("Constructor helper broken");
+    Unreachable() << "Constructor helper broken";
   }
   
   FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const Rational &r) :
@@ -923,7 +923,7 @@ static FloatingPointLiteral constructorHelperBitVector(
       
       // Only have pow(uint32_t) so we should check this.
       Assert(this->t.significand() <= 32);
-      
+
       if (!(exp.strictlyNegative())) {
 	Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt()));
 	return PartialRational(Rational(r), true);
@@ -935,7 +935,7 @@ static FloatingPointLiteral constructorHelperBitVector(
       }
     }
 
-    Unreachable("Convert float literal to real broken.");
+    Unreachable() << "Convert float literal to real broken.";
   }
 
   BitVector FloatingPoint::pack (void) const {
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 6439708b9..5cca2fcba 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -26,7 +26,7 @@
 #  error "This source should only ever be built if CVC4_CLN_IMP is on !"
 #endif /* CVC4_CLN_IMP */
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 
 using namespace std;
 
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index ed206bb45..2bc11f0a7 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -22,7 +22,7 @@
 
 #include "cvc4autoconfig.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "util/rational.h"
 
 #ifndef CVC4_GMP_IMP
diff --git a/src/util/random.cpp b/src/util/random.cpp
index 72a8fbc24..325fac325 100644
--- a/src/util/random.cpp
+++ b/src/util/random.cpp
@@ -19,7 +19,7 @@
 #include "util/random.h"
 
 #include <cfloat>
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 
 namespace CVC4 {
 
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index ca67dd6cb..d19f99d31 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -24,7 +24,7 @@
 #  error "This source should only ever be built if CVC4_CLN_IMP is on !"
 #endif /* CVC4_CLN_IMP */
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 
 using namespace std;
 
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index 229b51db7..0127381b6 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -25,7 +25,7 @@
 #  error "This source should only ever be built if CVC4_GMP_IMP is on !"
 #endif /* CVC4_GMP_IMP */
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 
 namespace CVC4 {
 
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index a76e9084b..d91280926 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -23,7 +23,7 @@
 #include <iostream>
 #include <sstream>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/exception.h"
 
 using namespace std;
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 6d7e08736..8f00a23ea 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -16,7 +16,7 @@
 **/
 #include "util/resource_manager.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/output.h"
 #include "options/smt_options.h"
 
@@ -49,7 +49,7 @@ void Timer::set(uint64_t millis, bool wallTime) {
 
 /** Return the milliseconds elapsed since last set(). */
 uint64_t Timer::elapsedWall() const {
-  Assert (d_wall_time);
+  Assert(d_wall_time);
   timeval tv;
   gettimeofday(&tv, NULL);
   Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl;
@@ -60,7 +60,7 @@ uint64_t Timer::elapsedWall() const {
 }
 
 uint64_t Timer::elapsedCPU() const {
-  Assert (!d_wall_time);
+  Assert(!d_wall_time);
   clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time;
   Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <<std::endl;
   return elapsed;
@@ -212,7 +212,6 @@ void ResourceManager::beginCall() {
     }
 
     if (d_timeBudgetCumulative) {
-
       AlwaysAssert(d_cumulativeTimer.on());
       // timer was on since the option was set
       d_cumulativeTimeUsed = d_cumulativeTimer.elapsed();
diff --git a/src/util/result.cpp b/src/util/result.cpp
index e6390cd41..433dcbf29 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -20,7 +20,7 @@
 #include <iostream>
 #include <string>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "options/set_language.h"
 
 using namespace std;
@@ -172,8 +172,7 @@ Result Result::asSatisfiabilityResult() const {
       case VALIDITY_UNKNOWN:
         return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
 
-      default:
-        Unhandled(d_validity);
+      default: Unhandled() << d_validity;
     }
   }
 
@@ -197,8 +196,7 @@ Result Result::asValidityResult() const {
       case SAT_UNKNOWN:
         return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
 
-      default:
-        Unhandled(d_sat);
+      default: Unhandled() << d_sat;
     }
   }
 
@@ -223,8 +221,7 @@ ostream& operator<<(ostream& out, enum Result::Sat s) {
     case Result::SAT_UNKNOWN:
       out << "SAT_UNKNOWN";
       break;
-    default:
-      Unhandled(s);
+    default: Unhandled() << s;
   }
   return out;
 }
@@ -240,8 +237,7 @@ ostream& operator<<(ostream& out, enum Result::Validity v) {
     case Result::VALIDITY_UNKNOWN:
       out << "VALIDITY_UNKNOWN";
       break;
-    default:
-      Unhandled(v);
+    default: Unhandled() << v;
   }
   return out;
 }
@@ -278,8 +274,7 @@ ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) {
     case Result::UNKNOWN_REASON:
       out << "UNKNOWN_REASON";
       break;
-    default:
-      Unhandled(e);
+    default: Unhandled() << e;
   }
   return out;
 }
diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp
index 948b4dfd3..eeb38f988 100644
--- a/src/util/sampler.cpp
+++ b/src/util/sampler.cpp
@@ -17,7 +17,7 @@
 
 #include "util/sampler.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "util/bitvector.h"
 
 namespace CVC4 {
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 88aeb3e2f..b2dcbbc8e 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -28,7 +28,7 @@
 #include <sstream>
 #include <vector>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "options/set_language.h"
 #include "util/ostream_util.h"
 #include "util/smt2_quote_string.h"
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 2ccbc2971..7f93a690e 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -20,8 +20,7 @@
 #include <cstdlib>
 #include <iostream>
 
-#include "base/cvc4_assert.h"
-#include "base/cvc4_check.h"
+#include "base/check.h"
 #include "lib/clock_gettime.h"
 #include "util/ostream_util.h"
 
@@ -77,7 +76,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) {
     nsec -= nsec_per_sec;
     ++a.tv_sec;
   }
-  CVC4_DCHECK(nsec >= 0 && nsec < nsec_per_sec);
+  Assert(nsec >= 0 && nsec < nsec_per_sec);
   a.tv_nsec = nsec;
   return a;
 }
@@ -168,8 +167,8 @@ void StatisticsRegistry::registerStat(Stat* s)
 void StatisticsRegistry::unregisterStat(Stat* s)
 {
 #ifdef CVC4_STATISTICS_ON
-  CVC4_CHECK(s != nullptr);
-  CVC4_CHECK(d_stats.erase(s) > 0)
+  AlwaysAssert(s != nullptr);
+  AlwaysAssert(d_stats.erase(s) > 0)
       << "Statistic `" << s->getName()
       << "' was not registered with this registry.";
 #endif /* CVC4_STATISTICS_ON */
@@ -203,7 +202,7 @@ void TimerStat::start() {
 
 void TimerStat::stop() {
   if(CVC4_USE_STATISTICS) {
-    CVC4_CHECK(d_running) << "timer not running";
+    AlwaysAssert(d_running) << "timer not running";
     ::timespec end;
     clock_gettime(CLOCK_MONOTONIC, &end);
     d_data += end - d_start;
diff --git a/src/util/utility.cpp b/src/util/utility.cpp
index 97d5ef36b..acabd8739 100644
--- a/src/util/utility.cpp
+++ b/src/util/utility.cpp
@@ -21,7 +21,7 @@
 #include <cstdlib>
 #include <iostream>
 
-#include "base/cvc4_check.h"
+#include "base/check.h"
 
 namespace CVC4 {