diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-31 16:54:22 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-31 18:30:42 -0500 |
| commit | 9b70f290bb39bdddb840e9f6d2e15edf0c6b98f6 (patch) | |
| tree | 1c51c9f6d52cae3b4b87a16177a2ad2091f59400 /src/util/statistics_registry.h | |
| parent | 9d7f0244034f1807e28b8ded23f4d6104ecf5263 (diff) | |
Fix a small problem in clang builds due to namespaces and symbol lookup
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; /** |