diff options
Diffstat (limited to 'src/util/statistics_registry.h')
| -rw-r--r-- | src/util/statistics_registry.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 474abfea3..af9088663 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -613,6 +613,8 @@ public: };/* class StatisticsRegistry */ +}/* CVC4 namespace */ + /****************************************************************************/ /* Some utility functions for timespec */ /****************************************************************************/ @@ -621,6 +623,7 @@ inline std::ostream& operator<<(std::ostream& os, const timespec& t); /** Compute the sum of two timespecs. */ inline timespec& operator+=(timespec& a, const timespec& b) { + using namespace CVC4; // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); @@ -643,6 +646,7 @@ inline timespec& operator+=(timespec& a, const timespec& b) { /** Compute the difference of two timespecs. */ inline timespec& operator-=(timespec& a, const timespec& b) { + using namespace CVC4; // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); @@ -719,6 +723,8 @@ inline std::ostream& operator<<(std::ostream& os, const timespec& t) { << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec; } +namespace CVC4 { + class CodeTimer; /** |