1 /********************* */
4 ** Original author: taking
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief [[ Add one-line brief description here ]]
16 ** [[ Add lengthier description here ]]
17 ** \todo document this file
20 #include "cvc4_public.h"
22 #ifndef __CVC4__STATS_H
23 #define __CVC4__STATS_H
31 #include "util/Assert.h"
32 #include "lib/clock_gettime.h"
37 #ifdef CVC4_STATISTICS_ON
38 # define __CVC4_USE_STATISTICS true
40 # define __CVC4_USE_STATISTICS false
43 class CVC4_PUBLIC Stat
;
45 class CVC4_PUBLIC StatisticsRegistry
{
49 typedef std::set
< Stat
*, StatCmp
> StatSet
;
50 static StatSet d_registeredStats
;
53 static void flushStatistics(std::ostream
& out
);
55 static inline void registerStat(Stat
* s
) throw(AssertionException
);
56 static inline void unregisterStat(Stat
* s
) throw(AssertionException
);
57 };/* class StatisticsRegistry */
60 class CVC4_PUBLIC Stat
{
64 static std::string s_delim
;
68 Stat(const std::string
& s
) throw(CVC4::AssertionException
) : d_name(s
)
70 if(__CVC4_USE_STATISTICS
) {
71 AlwaysAssert(d_name
.find(s_delim
) == std::string::npos
);
76 virtual void flushInformation(std::ostream
& out
) const = 0;
78 void flushStat(std::ostream
& out
) const {
79 if(__CVC4_USE_STATISTICS
) {
80 out
<< d_name
<< s_delim
;
81 flushInformation(out
);
85 const std::string
& getName() const {
91 struct StatisticsRegistry::StatCmp
{
92 bool operator()(const Stat
* s1
, const Stat
* s2
) const
94 return (s1
->getName()) < (s2
->getName());
99 inline void StatisticsRegistry::registerStat(Stat
* s
) throw(AssertionException
) {
100 if(__CVC4_USE_STATISTICS
) {
101 AlwaysAssert(d_registeredStats
.find(s
) == d_registeredStats
.end());
102 d_registeredStats
.insert(s
);
104 }/* StatisticsRegistry::registerStat */
107 inline void StatisticsRegistry::unregisterStat(Stat
* s
) throw(AssertionException
) {
108 if(__CVC4_USE_STATISTICS
) {
109 AlwaysAssert(d_registeredStats
.find(s
) != d_registeredStats
.end());
110 d_registeredStats
.erase(s
);
112 }/* StatisticsRegistry::unregisterStat */
117 * class T must have stream insertion operation defined.
118 * std::ostream& operator<<(std::ostream&, const T&);
121 class DataStat
: public Stat
{
123 DataStat(const std::string
& s
) : Stat(s
) {}
125 virtual const T
& getData() const = 0;
126 virtual void setData(const T
&) = 0;
128 void flushInformation(std::ostream
& out
) const {
129 if(__CVC4_USE_STATISTICS
) {
133 };/* class DataStat */
136 /** T must have an assignment operator=(). */
138 class ReferenceStat
: public DataStat
<T
> {
143 ReferenceStat(const std::string
& s
):
144 DataStat
<T
>(s
), d_data(NULL
)
147 ReferenceStat(const std::string
& s
, const T
& data
):
148 DataStat
<T
>(s
), d_data(NULL
)
153 void setData(const T
& t
) {
154 if(__CVC4_USE_STATISTICS
) {
158 const T
& getData() const {
159 if(__CVC4_USE_STATISTICS
) {
165 };/* class ReferenceStat */
168 /** T must have an operator=() and a copy constructor. */
170 class BackedStat
: public DataStat
<T
> {
176 BackedStat(const std::string
& s
, const T
& init
): DataStat
<T
>(s
), d_data(init
)
179 void setData(const T
& t
) {
180 if(__CVC4_USE_STATISTICS
) {
185 BackedStat
<T
>& operator=(const T
& t
) {
186 if(__CVC4_USE_STATISTICS
) {
192 const T
& getData() const {
193 if(__CVC4_USE_STATISTICS
) {
199 };/* class BackedStat */
202 class IntStat
: public BackedStat
<int64_t> {
205 IntStat(const std::string
& s
, int64_t init
): BackedStat
<int64_t>(s
, init
)
208 IntStat
& operator++() {
209 if(__CVC4_USE_STATISTICS
) {
215 IntStat
& operator+=(int64_t val
) {
216 if(__CVC4_USE_STATISTICS
) {
222 void maxAssign(int64_t val
) {
223 if(__CVC4_USE_STATISTICS
) {
230 void minAssign(int64_t val
) {
231 if(__CVC4_USE_STATISTICS
) {
237 };/* class IntStat */
240 // some utility functions for ::timespec
241 inline ::timespec
& operator+=(::timespec
& a
, const ::timespec
& b
) {
242 // assumes a.tv_nsec and b.tv_nsec are in range
243 const long nsec_per_sec
= 1000000000L; // one thousand million
244 a
.tv_sec
+= b
.tv_sec
;
245 long nsec
= a
.tv_nsec
+ b
.tv_nsec
;
247 nsec
+= nsec_per_sec
;
250 while(nsec
>= nsec_per_sec
) {
251 nsec
-= nsec_per_sec
;
257 inline ::timespec
& operator-=(::timespec
& a
, const ::timespec
& b
) {
258 // assumes a.tv_nsec and b.tv_nsec are in range
259 const long nsec_per_sec
= 1000000000L; // one thousand million
260 a
.tv_sec
-= b
.tv_sec
;
261 long nsec
= a
.tv_nsec
- b
.tv_nsec
;
263 nsec
+= nsec_per_sec
;
266 while(nsec
>= nsec_per_sec
) {
267 nsec
-= nsec_per_sec
;
273 inline ::timespec
operator+(const ::timespec
& a
, const ::timespec
& b
) {
274 ::timespec result
= a
;
277 inline ::timespec
operator-(const ::timespec
& a
, const ::timespec
& b
) {
278 ::timespec result
= a
;
281 inline bool operator==(const ::timespec
& a
, const ::timespec
& b
) {
282 // assumes a.tv_nsec and b.tv_nsec are in range
283 return a
.tv_sec
== b
.tv_sec
&& a
.tv_nsec
== b
.tv_nsec
;
285 inline bool operator!=(const ::timespec
& a
, const ::timespec
& b
) {
286 // assumes a.tv_nsec and b.tv_nsec are in range
289 inline bool operator<(const ::timespec
& a
, const ::timespec
& b
) {
290 // assumes a.tv_nsec and b.tv_nsec are in range
291 return a
.tv_sec
< b
.tv_sec
||
292 (a
.tv_sec
== b
.tv_sec
&& a
.tv_nsec
< b
.tv_nsec
);
294 inline bool operator>(const ::timespec
& a
, const ::timespec
& b
) {
295 // assumes a.tv_nsec and b.tv_nsec are in range
296 return a
.tv_sec
> b
.tv_sec
||
297 (a
.tv_sec
== b
.tv_sec
&& a
.tv_nsec
> b
.tv_nsec
);
299 inline bool operator<=(const ::timespec
& a
, const ::timespec
& b
) {
300 // assumes a.tv_nsec and b.tv_nsec are in range
303 inline bool operator>=(const ::timespec
& a
, const ::timespec
& b
) {
304 // assumes a.tv_nsec and b.tv_nsec are in range
307 inline std::ostream
& operator<<(std::ostream
& os
, const ::timespec
& t
) {
308 // assumes t.tv_nsec is in range
309 return os
<< t
.tv_sec
<< "."
310 << std::setfill('0') << std::setw(8) << std::right
<< t
.tv_nsec
;
314 class TimerStat
: public BackedStat
< ::timespec
> {
315 // strange: timespec isn't placed in 'std' namespace ?!
321 TimerStat(const std::string
& s
) :
322 BackedStat
< ::timespec
>(s
, ::timespec()),
327 if(__CVC4_USE_STATISTICS
) {
328 AlwaysAssert(!d_running
);
329 clock_gettime(CLOCK_MONOTONIC
, &d_start
);
335 if(__CVC4_USE_STATISTICS
) {
336 AlwaysAssert(d_running
);
338 clock_gettime(CLOCK_MONOTONIC
, &end
);
339 d_data
+= end
- d_start
;
343 };/* class TimerStat */
346 #undef __CVC4_USE_STATISTICS
348 }/* CVC4 namespace */
350 #endif /* __CVC4__STATS_H */