CVC3::Debug

CVC3::Debug Class Reference

The heart of the Bug Extermination Kingdom. More...

#include <debug.h>

Collaboration diagram for CVC3::Debug:

[legend]List of all members.

Public Member Functions

Debug ()
Constructor.
~Debug ()
Destructor (must destroy objects it d_timers).
void init (const std::vector< std::pair< std::string, bool > > *traceOptions, const std::string *dumpName)
Must be called before Debug class can be safely used.
DebugFlag flag (const std::string &name)
Accessing flags by name.
DebugFlag traceFlag (const std::string &name)
Accessing tracing flags by name.
DebugFlag traceFlag (char *name)
Accessing tracing flag by char* name (mostly for GDB).
void traceAll (bool enable=true)
Set tracing of everything on (1) and off (0) [for use in GDB].
DebugCounter counter (const std::string &name)
Accessing counters by name.
DebugTimer timer (const std::string &name)
Accessing timers by name.
bool trace (const std::string &name)
Check whether to print trace info for a particular flag.
void setCurrentTime (DebugTimer &timer)
Set the timer to the current time (whatever that means).
void setCurrentTime (const std::string &name)
void setElapsed (DebugTimer &timer)
Set the timer to the difference between current time and the time stored in the timer: timer = currentTime - timer.
std::ostream & getOS ()
Return the ostream used for debugging output.
std::ostream & getOSDumpTrace ()
Return the ostream for dumping trace.
void dumpTrace (const std::string &title, const std::vector< std::pair< std::string, std::string > > &fields)
Print an entry to the dump file.
void setOS (std::ostream &os)
Set the debugging ostream.
void printAll (std::ostream &os)
Print all the collected data if "DEBUG" flag is set to 'os'.
void printAll ()
Print all the collected data if "DEBUG" flag is set to the default debug stream.
int scopeLevel ()
Get the current scope level.

Static Public Member Functions

static DebugTimer newTimer ()
Create a new "private" timer, initially set to 0.

Private Types

typedef std::hash_map< std::string,
bool, stringHash > FlagMap
typedef std::hash_map< std::string,
int, stringHash > CounterMap
typedef std::hash_map< std::string,
DebugTime *, stringHash > TimerMap

Private Attributes

const std::vector< std::pair<
std::string, bool > > * d_traceOptions
Command line options for tracing; these override the TRACE command.
const std::string * d_dumpName
name of dump file
std::ostream * d_os
std::ostream * d_osDumpTrace
FlagMap d_flags
Set of flags.
FlagMap d_traceFlags
Set of trace flags.
CounterMap d_counters
Set of counters.
TimerMap d_timers
Set of timers.

Classes

class stringHash
Private hasher class for strings. More...

Detailed Description

The heart of the Bug Extermination Kingdom.

This class exposes many important components of the entire CVC-lite system for use in debugging, keeps all the flags, counters, and timers in the central database, and provides timing and printing functions.

Definition at line 302 of file debug.h.

Member Typedef Documentation

typedef std::hash_map<std::string, bool, stringHash> CVC3::Debug::FlagMap [private]

Definition at line 321 of file debug.h.

typedef std::hash_map<std::string, int, stringHash> CVC3::Debug::CounterMap [private]

Definition at line 322 of file debug.h.

typedef std::hash_map<std::string, DebugTime*, stringHash> CVC3::Debug::TimerMap [private]

Definition at line 323 of file debug.h.

Constructor & Destructor Documentation

CVC3::Debug::Debug ( ) [inline]

Constructor.

Definition at line 334 of file debug.h.

CVC3::Debug::~Debug ( )

Destructor (must destroy objects it d_timers).

Definition at line 254 of file debug.cpp.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::begin(), d_osDumpTrace, d_timers, and Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end().

Member Function Documentation

void CVC3::Debug::init	(	const std::vector< std::pair< std::string, bool > > *	traceOptions,
		const std::string *	dumpName
	)

Must be called before Debug class can be safely used.

Definition at line 139 of file debug.cpp.

References d_dumpName, and d_traceOptions.

DebugFlag CVC3::Debug::flag ( const std::string & name ) [inline]

Accessing flags by name.

If a flag doesn't exist, it is created and initialized to false.

Definition at line 343 of file debug.h.

References d_flags.

Referenced by CVC3::Scope::check().

DebugFlag CVC3::Debug::traceFlag ( const std::string & name ) [inline]

Accessing tracing flags by name.

If a flag doesn't exist, it is created and initialized to false.

Definition at line 348 of file debug.h.

References d_traceFlags.

Referenced by CVC3::VCCmd::evaluateCommand(), trace(), traceAll(), and traceFlag().

DebugFlag CVC3::Debug::traceFlag ( char * name )

Accessing tracing flag by char* name (mostly for GDB).

Definition at line 148 of file debug.cpp.

References traceFlag().

void CVC3::Debug::traceAll ( bool enable = true )

Set tracing of everything on (1) and off (0) [for use in GDB].

Definition at line 151 of file debug.cpp.

References traceFlag().

DebugCounter CVC3::Debug::counter ( const std::string & name ) [inline]

Accessing counters by name.

If a counter doesn't exist, it is created and initialized to 0.

Definition at line 356 of file debug.h.

References d_counters.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryBitvector::addSharedTerm(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryUF::checkSat(), CVC3::TheoryCore::checkSATCore(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::VCCmd::evaluateNext(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::SearchEngineFast::findSplitter(), CVC3::DecisionEngineMBTF::findSplitter(), CVC3::DecisionEngineDFS::findSplitter(), CVC3::DecisionEngineCaching::findSplitter(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::newTheorem3(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryCore::processEquality(), CVC3::TheoryArithOld::projectInequalities(), CVC3::Context::push(), CVC3::SearchEngineFast::recordFact(), CVC3::Expr::recursiveSubst(), CVC3::TheoryUF::rewrite(), CVC3::TheoryBitvector::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::Theory::setInconsistent(), CVC3::SearchEngineFast::setInconsistent(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryCore::simplifyOp(), CVC3::SearchEngineFast::split(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithNew::update().

DebugTimer CVC3::Debug::timer ( const std::string & name )

Accessing timers by name.

If a timer doesn't exist, it is created and initialized to 0.

Definition at line 275 of file debug.cpp.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count(), and d_timers.

Referenced by setCurrentTime(), setElapsed(), and CVC3::CommonTheoremProducer::substitutivityRule().

bool CVC3::Debug::trace ( const std::string & name )

Check whether to print trace info for a particular flag.

Trace flags are the same DebugFlag objects, but live in a different namespace from the normal debug flags

Definition at line 263 of file debug.cpp.

References d_traceOptions, and traceFlag().

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), CVC3::Scope::check(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineFast::fixConflict(), CVC3::CNF_TheoremProducer::learnedClause(), CVC3::SearchImplBase::newUserAssumption(), printAll(), CVC3::TheoryArithOld::solvedForm(), and CVC3::TheoryArithNew::solvedForm().

DebugTimer CVC3::Debug::newTimer ( ) [static]

Create a new "private" timer, initially set to 0.

The new timer will not be added to the set of timers, will not have a name, and will not be printed by 'printAll()'. It is intended to be used to measure time intervals which are later added or assigned to the named timers.

Definition at line 286 of file debug.cpp.

Referenced by CVC3::CommonTheoremProducer::substitutivityRule().

void CVC3::Debug::setCurrentTime ( DebugTimer & timer )

Set the timer to the current time (whatever that means).

Definition at line 290 of file debug.cpp.

References CVC3::DebugTimer::d_time, and timer().

Referenced by setCurrentTime(), and CVC3::CommonTheoremProducer::substitutivityRule().

void CVC3::Debug::setCurrentTime ( const std::string & name ) [inline]

Definition at line 378 of file debug.h.

References setCurrentTime(), and timer().

void CVC3::Debug::setElapsed ( DebugTimer & timer )

Set the timer to the difference between current time and the time stored in the timer: timer = currentTime - timer.