From 5fbb341a673ec5fa42f260bb137f423ac2aea324 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 8 Mar 2011 21:43:45 +0000 Subject: Clean up Theory base class as per code review bug #60; also fixes to CodeTimer statistic, and adding a CodeTimer to TheoryEngine::EngineOutputChannel::newFact() for investigation into (possible) slow or redundant theory registration. --- src/util/stats.h | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) (limited to 'src/util') diff --git a/src/util/stats.h b/src/util/stats.h index 978893a51..4dbf31120 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -509,16 +509,20 @@ public: inline ::timespec& operator+=(::timespec& a, const ::timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million + Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); + Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); a.tv_sec += b.tv_sec; long nsec = a.tv_nsec + b.tv_nsec; - while(nsec < 0) { + Assert(nsec >= 0); + if(nsec < 0) { nsec += nsec_per_sec; - ++a.tv_sec; + --a.tv_sec; } - while(nsec >= nsec_per_sec) { + if(nsec >= nsec_per_sec) { nsec -= nsec_per_sec; - --a.tv_sec; + ++a.tv_sec; } + Assert(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } @@ -527,16 +531,19 @@ inline ::timespec& operator+=(::timespec& a, const ::timespec& b) { inline ::timespec& operator-=(::timespec& a, const ::timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million + Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); + Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); a.tv_sec -= b.tv_sec; long nsec = a.tv_nsec - b.tv_nsec; - while(nsec < 0) { + if(nsec < 0) { nsec += nsec_per_sec; - ++a.tv_sec; + --a.tv_sec; } - while(nsec >= nsec_per_sec) { + if(nsec >= nsec_per_sec) { nsec -= nsec_per_sec; - --a.tv_sec; + ++a.tv_sec; } + Assert(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } -- cgit v1.2.3