22 #ifndef _cvc3__debug_h
23 #define _cvc3__debug_h
37 #define FatalAssert(cond, msg) if(!(cond)) \
38 CVC3::fatalError(__FILE__, __LINE__, #cond, msg)
45 const std::string& cond,
const std::string& msg);
48 #ifdef _CVC3_DEBUG_MODE
54 #define IF_DEBUG(code) code
59 #define DBG_PRINT(cond, pre, v, post) if(cond) CVC3::debugger.getOS() \
60 << (pre) << (v) << (post) << std::endl
63 #define DBG_PRINT_MSG(cond, msg) \
64 if(cond) CVC3::debugger.getOS() << (msg) << std::endl
68 #define TRACE(flag, pre, v, post) \
69 DBG_PRINT(CVC3::debugger.trace(flag), pre, v, post)
72 #define TRACE_MSG(flag, msg) \
73 DBG_PRINT_MSG(CVC3::debugger.trace(flag), msg)
76 #define DebugAssert(cond, str) if(!(cond)) \
77 CVC3::debugError(__FILE__, __LINE__, #cond, str)
84 class DebugException:
public Exception {
87 DebugException(
const std::string& msg):
Exception(msg) { }
89 virtual std::string
toString()
const {
90 return "Assertion violation " +
d_msg;
96 extern CVC_DLL void debugError(
const std::string& file,
int line,
97 const std::string& cond,
const std::string& msg);
109 DebugFlag(
bool& flag) : d_flag(&flag) { }
113 operator bool() {
return *d_flag; }
117 bool operator--() { *d_flag =
false;
return false; }
118 bool operator++() { *d_flag =
true;
return true; }
120 bool operator--(
int) {
bool x=*d_flag; *d_flag=
false;
return x; }
121 bool operator++(
int) {
bool x=*d_flag; *d_flag=
true;
return x; }
123 DebugFlag& operator=(
bool x) { *d_flag=(x!=
false);
return *
this; }
125 friend bool operator==(
const DebugFlag& f1,
const DebugFlag& f2);
126 friend bool operator!=(
const DebugFlag& f1,
const DebugFlag& f2);
128 friend std::ostream&
operator<<(std::ostream& os,
const DebugFlag& f);
132 inline bool operator==(
const DebugFlag& f1,
const DebugFlag& f2) {
133 return (*f1.d_flag) == (*f2.d_flag);
136 inline bool operator!=(
const DebugFlag& f1,
const DebugFlag& f2) {
137 return (*f1.d_flag) != (*f2.d_flag);
140 inline std::ostream&
operator<<(std::ostream& os,
const DebugFlag& f) {
141 if(*f.d_flag)
return(os <<
"true");
142 else return(os <<
"false");
156 DebugCounter(
int& c) : d_counter(&c) { }
162 operator int() {
return *d_counter; }
167 int operator--() {
return --(*d_counter); }
169 int operator++() {
return ++(*d_counter); }
171 int operator--(
int) {
return (*d_counter)--; }
173 int operator++(
int) {
return (*d_counter)++; }
175 DebugCounter& operator=(
int x) { *d_counter=x;
return *
this; }
176 DebugCounter& operator+=(
int x) { *d_counter+=x;
return *
this; }
177 DebugCounter& operator-=(
int x) { *d_counter-=x;
return *
this; }
180 DebugCounter& operator=(
const DebugCounter& x)
181 { *d_counter=*x.d_counter;
return *
this; }
183 DebugCounter& operator-=(
const DebugCounter& x)
184 { *d_counter-=*x.d_counter;
return *
this; }
186 DebugCounter& operator+=(
const DebugCounter& x)
187 { *d_counter+=*x.d_counter;
return *
this; }
189 friend bool operator==(
const DebugCounter& c1,
const DebugCounter& c2);
190 friend bool operator!=(
const DebugCounter& c1,
const DebugCounter& c2);
191 friend bool operator==(
int c1,
const DebugCounter& c2);
192 friend bool operator!=(
int c1,
const DebugCounter& c2);
193 friend bool operator==(
const DebugCounter& c1,
int c2);
194 friend bool operator!=(
const DebugCounter& c1,
int c2);
196 friend std::ostream&
operator<<(std::ostream& os,
const DebugCounter& f);
199 inline bool operator==(
const DebugCounter& c1,
const DebugCounter& c2) {
200 return (*c1.d_counter) == (*c2.d_counter);
202 inline bool operator!=(
const DebugCounter& c1,
const DebugCounter& c2) {
203 return (*c1.d_counter) != (*c2.d_counter);
205 inline bool operator==(
int c1,
const DebugCounter& c2) {
206 return c1 == (*c2.d_counter);
208 inline bool operator!=(
int c1,
const DebugCounter& c2) {
209 return c1 != (*c2.d_counter);
211 inline bool operator==(
const DebugCounter& c1,
int c2) {
212 return (*c1.d_counter) == c2;
214 inline bool operator!=(
const DebugCounter& c1,
int c2) {
215 return (*c1.d_counter) != c2;
217 inline std::ostream&
operator<<(std::ostream& os,
const DebugCounter& c) {
218 return (os << *c.d_counter);
239 DebugTimer(DebugTime* time,
bool take_time =
false)
240 : d_time(time), d_clean_time(take_time) { }
248 DebugTimer(
const DebugTimer& timer);
250 DebugTimer& operator=(
const DebugTimer& timer);
258 DebugTimer& operator+=(
const DebugTimer& timer);
259 DebugTimer& operator-=(
const DebugTimer& timer);
261 DebugTimer
operator+(
const DebugTimer& timer);
263 DebugTimer
operator-(
const DebugTimer& timer);
268 friend bool operator==(
const DebugTimer& t1,
const DebugTimer& t2);
269 friend bool operator!=(
const DebugTimer& t1,
const DebugTimer& t2);
270 friend bool operator<(
const DebugTimer& t1,
const DebugTimer& t2);
271 friend bool operator>(
const DebugTimer& t1,
const DebugTimer& t2);
272 friend bool operator<=(
const DebugTimer& t1,
const DebugTimer& t2);
273 friend bool operator>=(
const DebugTimer& t1,
const DebugTimer& t2);
276 friend std::ostream&
operator<<(std::ostream& os,
const DebugTimer& timer);
288 const std::vector<std::pair<std::string,bool> >* d_traceOptions;
290 const std::string* d_dumpName;
294 std::ostream* d_osDumpTrace;
298 size_t operator()(
const std::string& s)
const {
308 FlagMap d_traceFlags;
309 CounterMap d_counters;
317 Debug(): d_traceOptions(NULL), d_os(&std::cerr), d_osDumpTrace(NULL) { }
321 void init(
const std::vector<std::pair<std::string,bool> >* traceOptions,
322 const std::string* dumpName);
328 DebugFlag flag(
const std::string& name)
329 {
return DebugFlag(d_flags[name]); }
333 DebugFlag traceFlag(
const std::string& name)
334 {
return DebugFlag(d_traceFlags[name]); }
336 DebugFlag traceFlag(
const char* name);
338 void traceAll(
bool enable =
true);
341 DebugCounter counter(
const std::string& name)
342 {
return DebugCounter(d_counters[name]); }
345 DebugTimer timer(
const std::string& name);
350 bool trace(
const std::string& name);
359 static DebugTimer newTimer();
362 void setCurrentTime(DebugTimer& timer);
363 void setCurrentTime(
const std::string& name) {
364 DebugTimer t(timer(name));
372 void setElapsed(DebugTimer& timer);
375 std::ostream& getOS() {
return *d_os; }
377 std::ostream& getOSDumpTrace();
380 void dumpTrace(
const std::string& title,
381 const std::vector<std::pair<std::string,std::string> >&
384 void setOS(std::ostream& os) { d_os = &os; }
387 void printAll(std::ostream& os);
390 void printAll() { printAll(*d_os); }
402 #else // if _CVC3_DEBUG_MODE is not defined
406 #define IF_DEBUG(code)
408 #define DebugAssert(cond, str)
410 #define DBG_PRINT(cond, pre, v, post)
411 #define TRACE(cond, pre, v, post)
413 #define DBG_PRINT_MSG(cond, msg)
414 #define TRACE_MSG(flag, msg)
421 #endif // _CVC3_DEBUG_MODE
425 #endif // _cvc3__debug_h
CVC_DLL void fatalError(const std::string &file, int line, const std::string &cond, const std::string &msg)
Function for fatal exit.
ExprStream & reset(ExprStream &os)
Reset the indentation to the default at this level.
bool operator<=(const Expr &e1, const Expr &e2)
ostream & operator<<(ostream &os, const Expr &e)
Expr operator+(const Expr &left, const Expr &right)
bool operator==(const Expr &e1, const Expr &e2)
bool operator>(const Expr &e1, const Expr &e2)
Expr operator-(const Expr &child)
virtual std::string toString() const
Abstraction over different operating systems.
bool operator<(const Expr &e1, const Expr &e2)
bool operator>=(const Expr &e1, const Expr &e2)
bool operator!=(const Expr &e1, const Expr &e2)