CVCL::Debug Class Reference

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

#include <debug.h>

List of all members.

Public Member Functions

Static Public Member Functions

Private Types

Private Attributes


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 311 of file debug.h.

Member Typedef Documentation

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

Definition at line 330 of file debug.h.

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

Definition at line 331 of file debug.h.

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

Definition at line 332 of file debug.h.

Constructor & Destructor Documentation

CVCL::Debug::Debug  )  [inline]


Definition at line 343 of file debug.h.

CVCL::Debug::~Debug  ) 

Destructor (must destroy objects it d_timers).

Definition at line 267 of file debug.cpp.

References d_osDumpTrace, and d_timers.

Member Function Documentation

void CVCL::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.

DebugFlag CVCL::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 352 of file debug.h.

References d_flags.

Referenced by CVCL::AVHash::AVHash(), and CVCL::Scope::~Scope().

DebugFlag CVCL::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 357 of file debug.h.

References d_traceFlags.

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

DebugFlag CVCL::Debug::traceFlag char *  name  ) 

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

Definition at line 155 of file debug.cpp.

References traceFlag().

void CVCL::Debug::traceAll bool  enable = true  ) 

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

Definition at line 158 of file debug.cpp.

References traceFlag().

DebugCounter CVCL::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 365 of file debug.h.

References d_counters.

Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::TheoryBitvector::addSharedTerm(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::TheoryBitvector::assertFact(), CVCL::TheoryArith::assertFact(), TheoryCore::assertFactCore(), TheoryCore::assertFormula(), CVCL::SearchEngineFast::bcp(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::TheoryBitvector::bitBlastEqn(), CVCL::TheoryUF::checkSat(), TheoryCore::checkSat(), CVCL::TheoryBitvector::checkSat(), TheoryCore::checkSATCore(), CVCL::TheoryBitvector::collectSharedSubterms(), CVCL::TheoryArith::doSolve(), TheoryCore::enqueueFact(), CVCL::VCCmd::evaluateNext(), CVCL::SearchEngineFast::findSplitter(), CVCL::DecisionEngineMBTF::findSplitter(), CVCL::DecisionEngineDFS::findSplitter(), CVCL::DecisionEngineCaching::findSplitter(), CVCL::TheoremProducer::newTheorem(), CVCL::TheoremProducer::newTheorem3(), CVCL::TheoryArith::normalizeProjectIneqs(), TheoryCore::processEquality(), TheoryCore::processFactQueue(), CVCL::TheoryArith::projectInequalities(), CVCL::Context::push(), CVCL::SearchEngineFast::recordFact(), CVCL::Expr::recursiveSubst(), CVCL::TheoryUF::rewrite(), CVCL::TheoryBitvector::rewriteAux(), CVCL::TheoryBitvector::rewriteBV(), CVCL::Theory::setInconsistent(), CVCL::SearchEngineFast::setInconsistent(), CVCL::TheoryBitvector::setupExpr(), TheoryCore::setupTerm(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyOp(), CVCL::SearchEngineFast::split(), CVCL::TheoryBitvector::update(), and CVCL::TheoryArith::update().

DebugTimer CVCL::Debug::timer const std::string &  name  ) 

Accessing timers by name.

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

Referenced by setCurrentTime().

bool CVCL::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

Referenced by CVCL::SearchEngineFast::analyzeUIPs(), CVCL::SearchEngineFast::fixConflict(), CVCL::CNF_TheoremProducer::learnedClause(), CVCL::SearchImplBase::newUserAssumption(), and CVCL::Scope::~Scope().

DebugTimer CVCL::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 299 of file debug.cpp.

void CVCL::Debug::setCurrentTime DebugTimer timer  ) 

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

Definition at line 303 of file debug.cpp.

References CVCL::DebugTimer::d_time.

Referenced by setCurrentTime().

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

Definition at line 387 of file debug.h.

References setCurrentTime(), and timer().

void CVCL::Debug::setElapsed DebugTimer timer  ) 

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

Intended to obtain the time interval since the last call to setCurrentTime() with that timer.

Definition at line 312 of file debug.cpp.

References CVCL::DebugTimer::d_time.

std::ostream& CVCL::Debug::getOS  )  [inline]

Return the ostream used for debugging output.

Definition at line 399 of file debug.h.

References d_os.

Referenced by CVCL::SearchEngineFast::analyzeUIPs(), CVCL::TheoryArith::kidsCanonical(), CVCL::CNF_TheoremProducer::learnedClause(), CVCL::SearchImplBase::newUserAssumption(), and CVCL::Scope::~Scope().

ostream & CVCL::Debug::getOSDumpTrace  ) 

Return the ostream for dumping trace.

If the stream is not initialized, open the file If the filename is empty or "-", then return cout (but do not initialize the stream in this case).

Definition at line 325 of file debug.cpp.

References d_dumpName, and d_osDumpTrace.

void CVCL::Debug::dumpTrace const std::string &  title,
const std::vector< std::pair< std::string, std::string > > &  fields

Print an entry to the dump file.

void CVCL::Debug::setOS std::ostream &  os  )  [inline]

Set the debugging ostream.

Definition at line 408 of file debug.h.

References d_os.

void CVCL::Debug::printAll std::ostream &  os  ) 

Print all the collected data if "DEBUG" flag is set to 'os'.

Referenced by main(), and sighandler().

void CVCL::Debug::printAll  )  [inline]

Print all the collected data if "DEBUG" flag is set to the default debug stream.

Definition at line 414 of file debug.h.

References d_os.

int CVCL::Debug::scopeLevel  ) 

Get the current scope level.

Member Data Documentation

const std::vector<std::pair<std::string,bool> >* CVCL::Debug::d_traceOptions [private]

Command line options for tracing; these override the TRACE command.

Definition at line 314 of file debug.h.

const std::string* CVCL::Debug::d_dumpName [private]

name of dump file

Definition at line 316 of file debug.h.

Referenced by getOSDumpTrace().

std::ostream* CVCL::Debug::d_os [private]

Definition at line 318 of file debug.h.

Referenced by getOS(), printAll(), and setOS().

std::ostream* CVCL::Debug::d_osDumpTrace [private]

Definition at line 320 of file debug.h.

Referenced by getOSDumpTrace(), and ~Debug().

FlagMap CVCL::Debug::d_flags [private]

Set of flags.

Definition at line 333 of file debug.h.

Referenced by flag().

FlagMap CVCL::Debug::d_traceFlags [private]

Set of trace flags.

Definition at line 334 of file debug.h.

Referenced by traceFlag().

CounterMap CVCL::Debug::d_counters [private]

Set of counters.

Definition at line 335 of file debug.h.

Referenced by counter().

TimerMap CVCL::Debug::d_timers [private]

Set of timers.

Note, that the d_timers map does *not* own the pointers; so the objects in d_timers must be destroyed explicitly in our destructor.

Definition at line 339 of file debug.h.

Referenced by ~Debug().

The documentation for this class was generated from the following files:
Generated on Thu Apr 13 16:57:43 2006 for CVC Lite by  doxygen 1.4.4