CVCL::Debug Class Reference

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

#include <debug.h>

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 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]

Constructor. 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:

• debug.h
• debug.cpp

---