From: Morgan Deters Date: Thu, 31 Jan 2013 21:54:22 +0000 (-0500) Subject: Fix a small problem in clang builds due to namespaces and symbol lookup X-Git-Tag: cvc5-1.0.0~7437 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b70f290bb39bdddb840e9f6d2e15edf0c6b98f6;p=cvc5.git Fix a small problem in clang builds due to namespaces and symbol lookup --- 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; /**