CVC3::DebugTimer Class Reference

Time counter. More...

#include <debug.h>

Collaboration diagram for CVC3::DebugTimer:

[legend]List of all members.

Public Member Functions

DebugTimer (DebugTime *time, bool take_time=false)
Constructor: takes the pointer to the actual time value.
DebugTimer (const DebugTimer &timer)
Copy constructor: copy the *pointer* from public timers, and *value* from private.
DebugTimer & operator= (const DebugTimer &timer)
Assignment: same logistics as for the copy constructor.
~DebugTimer ()
Destructor.
void reset ()
Set time to zero.
DebugTimer & operator+= (const DebugTimer &timer)
DebugTimer & operator-= (const DebugTimer &timer)
DebugTimer operator+ (const DebugTimer &timer)
Produces new "private" timer.
DebugTimer operator- (const DebugTimer &timer)
Produces new "private" timer.

Private Attributes

DebugTime * d_time
The time value.
bool d_clean_time
Set if we own *d_time.

Friends

class Debug
bool operator== (const DebugTimer &t1, const DebugTimer &t2)
bool operator!= (const DebugTimer &t1, const DebugTimer &t2)
bool operator< (const DebugTimer &t1, const DebugTimer &t2)
bool operator> (const DebugTimer &t1, const DebugTimer &t2)
bool operator<= (const DebugTimer &t1, const DebugTimer &t2)
bool operator>= (const DebugTimer &t1, const DebugTimer &t2)
std::ostream & operator<< (std::ostream &os, const DebugTimer &timer)
Print the timer's value.

Detailed Description

Time counter.

Intended use is to store time intervals or accumulated time for multiple events (e.g. time spent to execute certain lines of code, or accumulated time spent in a particular function).

Definition at line 248 of file debug.h.

Constructor & Destructor Documentation

CVC3::DebugTimer::DebugTimer	(	DebugTime *	time,
		bool	take_time = `false`
	)			`[inline]`

Constructor: takes the pointer to the actual time value.

It is either stored in class Debug below (then the timer is "public"), or we own it, making the timer "private".

Definition at line 256 of file debug.h.

Referenced by operator+(), and operator-().

CVC3::DebugTimer::DebugTimer ( const DebugTimer & timer )

Copy constructor: copy the *pointer* from public timers, and *value* from private.

The reason for different behavior for public and private time is the following. When you modify a public timer, you want the changes to show in the central database and everywhere else, whereas private timers are used as independent temporary variables holding intermediate time values.

Definition at line 158 of file debug.cpp.

References d_clean_time, and d_time.

CVC3::DebugTimer::~DebugTimer ( )

Destructor.

Definition at line 134 of file debug.cpp.

References d_clean_time, and d_time.