diff options
author | Tim King <taking@cs.nyu.edu> | 2018-02-07 10:19:04 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-07 10:19:04 -0800 |
commit | a5c952d63bca9f94d3886db4d9c09d08d7a23033 (patch) | |
tree | 9b3748cf9d7ec36e12df9a5b361862ae6ec0fabb /src/util/statistics_registry.cpp | |
parent | 0533b9009d23a39bcc78ef85d6e98b62ef304351 (diff) |
Adds a new CHECK macro that abort()s on failure. (#1532)
Diffstat (limited to 'src/util/statistics_registry.cpp')
-rw-r--r-- | src/util/statistics_registry.cpp | 33 |
1 files changed, 7 insertions, 26 deletions
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 38113c512..2dd1eddd7 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -21,6 +21,7 @@ #include <iostream> #include "base/cvc4_assert.h" +#include "base/cvc4_check.h" #include "lib/clock_gettime.h" #include "util/ostream_util.h" @@ -76,7 +77,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) { nsec -= nsec_per_sec; ++a.tv_sec; } - Assert(nsec >= 0 && nsec < nsec_per_sec); + DCHECK(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } @@ -167,22 +168,11 @@ void StatisticsRegistry::registerStat(Stat* s) void StatisticsRegistry::unregisterStat(Stat* s) { #ifdef CVC4_STATISTICS_ON - try - { - PrettyCheckArgument(d_stats.find(s) != d_stats.end(), - s, - "Statistic `%s' was not registered with this registry.", - s->getName().c_str()); - } - catch (Exception& e) - { - std::cerr << "Failure in StatisticsRegistry::unregisterStat():" << e.what() - << std::endl; - abort(); - } - d_stats.erase(s); + CHECK(s != nullptr); + CHECK(d_stats.erase(s) > 0) << "Statistic `" << s->getName() + << "' was not registered with this registry."; #endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::unregisterStat_() */ +} /* StatisticsRegistry::unregisterStat() */ void StatisticsRegistry::flushStat(std::ostream &out) const { #ifdef CVC4_STATISTICS_ON @@ -212,16 +202,7 @@ void TimerStat::start() { void TimerStat::stop() { if(__CVC4_USE_STATISTICS) { - try - { - PrettyCheckArgument(d_running, *this, "timer not running"); - } - catch (Exception& e) - { - std::cerr << "Fatal failure in TimerStat::stop(): " << e.what() - << std::endl; - abort(); - } + CHECK(d_running) << "timer not running"; ::timespec end; clock_gettime(CLOCK_MONOTONIC, &end); d_data += end - d_start; |