diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/util | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/abstract_value.cpp | 2 | ||||
-rw-r--r-- | src/util/bin_heap.h | 2 | ||||
-rw-r--r-- | src/util/cardinality.cpp | 9 | ||||
-rw-r--r-- | src/util/dense_map.h | 4 | ||||
-rw-r--r-- | src/util/divisible.cpp | 2 | ||||
-rw-r--r-- | src/util/floatingpoint.cpp | 16 | ||||
-rw-r--r-- | src/util/integer_cln_imp.cpp | 2 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.cpp | 2 | ||||
-rw-r--r-- | src/util/random.cpp | 2 | ||||
-rw-r--r-- | src/util/rational_cln_imp.cpp | 2 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.cpp | 2 | ||||
-rw-r--r-- | src/util/regexp.cpp | 2 | ||||
-rw-r--r-- | src/util/resource_manager.cpp | 7 | ||||
-rw-r--r-- | src/util/result.cpp | 17 | ||||
-rw-r--r-- | src/util/sampler.cpp | 2 | ||||
-rw-r--r-- | src/util/sexpr.cpp | 2 | ||||
-rw-r--r-- | src/util/statistics_registry.cpp | 11 | ||||
-rw-r--r-- | src/util/utility.cpp | 2 |
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 { |