diff options
Diffstat (limited to 'src/util/statistics_registry.cpp')
-rw-r--r-- | src/util/statistics_registry.cpp | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index cad0e63fa..2ccbc2971 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -26,9 +26,9 @@ #include "util/ostream_util.h" #ifdef CVC4_STATISTICS_ON -# define __CVC4_USE_STATISTICS true +# define CVC4_USE_STATISTICS true #else -# define __CVC4_USE_STATISTICS false +# define CVC4_USE_STATISTICS false #endif @@ -148,7 +148,7 @@ std::ostream& operator<<(std::ostream& os, const timespec& t) { StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name) { d_prefix = name; - if(__CVC4_USE_STATISTICS) { + if(CVC4_USE_STATISTICS) { PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name, "StatisticsRegistry names cannot contain the string \"%s\"", s_regDelim.c_str()); @@ -194,7 +194,7 @@ void StatisticsRegistry::safeFlushInformation(int fd) const { } void TimerStat::start() { - if(__CVC4_USE_STATISTICS) { + if(CVC4_USE_STATISTICS) { PrettyCheckArgument(!d_running, *this, "timer already running"); clock_gettime(CLOCK_MONOTONIC, &d_start); d_running = true; @@ -202,7 +202,7 @@ void TimerStat::start() { }/* TimerStat::start() */ void TimerStat::stop() { - if(__CVC4_USE_STATISTICS) { + if(CVC4_USE_STATISTICS) { CVC4_CHECK(d_running) << "timer not running"; ::timespec end; clock_gettime(CLOCK_MONOTONIC, &end); @@ -217,7 +217,7 @@ bool TimerStat::running() const { timespec TimerStat::getData() const { ::timespec data = d_data; - if(__CVC4_USE_STATISTICS && d_running) { + if(CVC4_USE_STATISTICS && d_running) { ::timespec end; clock_gettime(CLOCK_MONOTONIC, &end); data += end - d_start; @@ -227,7 +227,7 @@ timespec TimerStat::getData() const { SExpr TimerStat::getValue() const { ::timespec data = d_data; - if(__CVC4_USE_STATISTICS && d_running) { + if(CVC4_USE_STATISTICS && d_running) { ::timespec end; clock_gettime(CLOCK_MONOTONIC, &end); data += end - d_start; @@ -253,4 +253,4 @@ RegisterStatistic::~RegisterStatistic() { }/* CVC4 namespace */ -#undef __CVC4_USE_STATISTICS +#undef CVC4_USE_STATISTICS |