00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #ifndef _cvc3__debug_h
00023 #define _cvc3__debug_h
00024
00025 #include <string>
00026 #include <iostream>
00027 #include <sstream>
00028 #include <vector>
00029 #include "os.h"
00030 #include "exception.h"
00031
00032
00033
00034
00035
00036
00037 #define FatalAssert(cond, msg) if(!(cond)) \
00038 CVC3::fatalError(__FILE__, __LINE__, #cond, msg)
00039
00040 namespace CVC3 {
00041
00042
00043
00044 extern void fatalError(const std::string& file, int line,
00045 const std::string& cond, const std::string& msg);
00046 }
00047
00048 #ifdef DEBUG
00049
00050 #include "compat_hash_map.h"
00051 #include "compat_hash_set.h"
00052
00053
00054 #define IF_DEBUG(code) code
00055
00056
00057
00058
00059 #define DBG_PRINT(cond, pre, v, post) if(cond) CVC3::debugger.getOS() \
00060 << (pre) << (v) << (post) << std::endl
00061
00062
00063 #define DBG_PRINT_MSG(cond, msg) \
00064 if(cond) CVC3::debugger.getOS() << (msg) << std::endl
00065
00066
00067
00068 #define TRACE(flag, pre, v, post) \
00069 DBG_PRINT(CVC3::debugger.trace(flag), pre, v, post)
00070
00071
00072 #define TRACE_MSG(flag, msg) \
00073 DBG_PRINT_MSG(CVC3::debugger.trace(flag), msg)
00074
00075
00076 #define DebugAssert(cond, str) if(!(cond)) \
00077 CVC3::debugError(__FILE__, __LINE__, #cond, str)
00078
00079
00080 namespace CVC3 {
00081
00082
00083
00084
00085
00086
00087
00088
00089
00090
00091 class ScopeWatcher {
00092 private:
00093 bool *d_flag;
00094 public:
00095 ScopeWatcher(bool *flag): d_flag(flag) { *d_flag = true; }
00096 ~ScopeWatcher() { *d_flag = false; }
00097 };
00098
00099 class Expr;
00100
00101 class DebugException: public Exception {
00102 public:
00103
00104 DebugException(const std::string& msg): Exception(msg) { }
00105
00106 virtual std::string toString() const {
00107 return "Assertion violation " + d_msg;
00108 }
00109 };
00110
00111
00112
00113 extern void debugError(const std::string& file, int line,
00114 const std::string& cond, const std::string& msg);
00115
00116
00117
00118
00119
00120 class DebugFlag {
00121 private:
00122 bool* d_flag;
00123 public:
00124
00125
00126 DebugFlag(bool& flag) : d_flag(&flag) { }
00127
00128 ~DebugFlag() { }
00129
00130 operator bool() { return *d_flag; }
00131
00132
00133
00134 bool operator--() { *d_flag = false; return false; }
00135 bool operator++() { *d_flag = true; return true; }
00136
00137 bool operator--(int) { bool x=*d_flag; *d_flag=false; return x; }
00138 bool operator++(int) { bool x=*d_flag; *d_flag=true; return x; }
00139
00140 DebugFlag& operator=(bool x) { *d_flag=(x!=false); return *this; }
00141
00142 friend bool operator==(const DebugFlag& f1, const DebugFlag& f2);
00143 friend bool operator!=(const DebugFlag& f1, const DebugFlag& f2);
00144
00145 friend std::ostream& operator<<(std::ostream& os, const DebugFlag& f);
00146 };
00147
00148
00149 inline bool operator==(const DebugFlag& f1, const DebugFlag& f2) {
00150 return (*f1.d_flag) == (*f2.d_flag);
00151 }
00152
00153 inline bool operator!=(const DebugFlag& f1, const DebugFlag& f2) {
00154 return (*f1.d_flag) != (*f2.d_flag);
00155 }
00156
00157 inline std::ostream& operator<<(std::ostream& os, const DebugFlag& f) {
00158 if(*f.d_flag) return(os << "true");
00159 else return(os << "false");
00160 }
00161
00162
00163
00164
00165
00166 class DebugCounter {
00167 private:
00168 int* d_counter;
00169 public:
00170
00171
00172
00173 DebugCounter(int& c) : d_counter(&c) { }
00174
00175 ~DebugCounter() { }
00176
00177
00178
00179 operator int() { return *d_counter; }
00180
00181
00182
00183
00184 int operator--() { return --(*d_counter); }
00185
00186 int operator++() { return ++(*d_counter); }
00187
00188 int operator--(int) { return (*d_counter)--; }
00189
00190 int operator++(int) { return (*d_counter)++; }
00191
00192 DebugCounter& operator=(int x) { *d_counter=x; return *this; }
00193 DebugCounter& operator+=(int x) { *d_counter+=x; return *this; }
00194 DebugCounter& operator-=(int x) { *d_counter-=x; return *this; }
00195
00196
00197 DebugCounter& operator=(const DebugCounter& x)
00198 { *d_counter=*x.d_counter; return *this; }
00199
00200 DebugCounter& operator-=(const DebugCounter& x)
00201 { *d_counter-=*x.d_counter; return *this; }
00202
00203 DebugCounter& operator+=(const DebugCounter& x)
00204 { *d_counter+=*x.d_counter; return *this; }
00205
00206 friend bool operator==(const DebugCounter& c1, const DebugCounter& c2);
00207 friend bool operator!=(const DebugCounter& c1, const DebugCounter& c2);
00208 friend bool operator==(int c1, const DebugCounter& c2);
00209 friend bool operator!=(int c1, const DebugCounter& c2);
00210 friend bool operator==(const DebugCounter& c1, int c2);
00211 friend bool operator!=(const DebugCounter& c1, int c2);
00212
00213 friend std::ostream& operator<<(std::ostream& os, const DebugCounter& f);
00214 };
00215
00216 inline bool operator==(const DebugCounter& c1, const DebugCounter& c2) {
00217 return (*c1.d_counter) == (*c2.d_counter);
00218 }
00219 inline bool operator!=(const DebugCounter& c1, const DebugCounter& c2) {
00220 return (*c1.d_counter) != (*c2.d_counter);
00221 }
00222 inline bool operator==(int c1, const DebugCounter& c2) {
00223 return c1 == (*c2.d_counter);
00224 }
00225 inline bool operator!=(int c1, const DebugCounter& c2) {
00226 return c1 != (*c2.d_counter);
00227 }
00228 inline bool operator==(const DebugCounter& c1, int c2) {
00229 return (*c1.d_counter) == c2;
00230 }
00231 inline bool operator!=(const DebugCounter& c1, int c2) {
00232 return (*c1.d_counter) != c2;
00233 }
00234 inline std::ostream& operator<<(std::ostream& os, const DebugCounter& c) {
00235 return (os << *c.d_counter);
00236 }
00237
00238
00239
00240
00241
00242 class DebugTime;
00243
00244
00245
00246
00247
00248 class DebugTimer {
00249 private:
00250 DebugTime* d_time;
00251 bool d_clean_time;
00252 public:
00253
00254
00255
00256 DebugTimer(DebugTime* time, bool take_time = false)
00257 : d_time(time), d_clean_time(take_time) { }
00258
00259
00260
00261
00262
00263
00264
00265 DebugTimer(const DebugTimer& timer);
00266
00267 DebugTimer& operator=(const DebugTimer& timer);
00268
00269
00270 ~DebugTimer();
00271
00272
00273
00274 void reset();
00275 DebugTimer& operator+=(const DebugTimer& timer);
00276 DebugTimer& operator-=(const DebugTimer& timer);
00277
00278 DebugTimer operator+(const DebugTimer& timer);
00279
00280 DebugTimer operator-(const DebugTimer& timer);
00281
00282
00283 friend class Debug;
00284
00285 friend bool operator==(const DebugTimer& t1, const DebugTimer& t2);
00286 friend bool operator!=(const DebugTimer& t1, const DebugTimer& t2);
00287 friend bool operator<(const DebugTimer& t1, const DebugTimer& t2);
00288 friend bool operator>(const DebugTimer& t1, const DebugTimer& t2);
00289 friend bool operator<=(const DebugTimer& t1, const DebugTimer& t2);
00290 friend bool operator>=(const DebugTimer& t1, const DebugTimer& t2);
00291
00292
00293 friend std::ostream& operator<<(std::ostream& os, const DebugTimer& timer);
00294 };
00295
00296
00297
00298
00299
00300
00301
00302 class Debug {
00303 private:
00304
00305 const std::vector<std::pair<std::string,bool> >* d_traceOptions;
00306
00307 const std::string* d_dumpName;
00308
00309 std::ostream* d_os;
00310
00311 std::ostream* d_osDumpTrace;
00312
00313 class stringHash {
00314 public:
00315 size_t operator()(const std::string& s) const {
00316 std::hash<char*> h;
00317 return h(s.c_str());
00318 }
00319 };
00320
00321 typedef std::hash_map<std::string, bool, stringHash> FlagMap;
00322 typedef std::hash_map<std::string, int, stringHash> CounterMap;
00323 typedef std::hash_map<std::string, DebugTime*, stringHash> TimerMap;
00324 FlagMap d_flags;
00325 FlagMap d_traceFlags;
00326 CounterMap d_counters;
00327
00328
00329
00330 TimerMap d_timers;
00331
00332 public:
00333
00334 Debug(): d_traceOptions(NULL), d_os(&std::cerr), d_osDumpTrace(NULL) { }
00335
00336 ~Debug();
00337
00338 void init(const std::vector<std::pair<std::string,bool> >* traceOptions,
00339 const std::string* dumpName);
00340
00341
00342
00343 DebugFlag flag(const std::string& name)
00344 { return DebugFlag(d_flags[name]); }
00345
00346
00347
00348 DebugFlag traceFlag(const std::string& name)
00349 { return DebugFlag(d_traceFlags[name]); }
00350
00351 DebugFlag traceFlag(char* name);
00352
00353 void traceAll(bool enable = true);
00354
00355
00356 DebugCounter counter(const std::string& name)
00357 { return DebugCounter(d_counters[name]); }
00358
00359
00360 DebugTimer timer(const std::string& name);
00361
00362
00363
00364
00365 bool trace(const std::string& name);
00366
00367
00368
00369
00370
00371
00372
00373
00374 static DebugTimer newTimer();
00375
00376
00377 void setCurrentTime(DebugTimer& timer);
00378 void setCurrentTime(const std::string& name) {
00379 DebugTimer t(timer(name));
00380 setCurrentTime(t);
00381 }
00382
00383
00384
00385
00386
00387 void setElapsed(DebugTimer& timer);
00388
00389
00390 std::ostream& getOS() { return *d_os; }
00391
00392 std::ostream& getOSDumpTrace();
00393
00394
00395 void dumpTrace(const std::string& title,
00396 const std::vector<std::pair<std::string,std::string> >&
00397 fields);
00398
00399 void setOS(std::ostream& os) { d_os = &os; }
00400
00401
00402 void printAll(std::ostream& os);
00403
00404
00405 void printAll() { printAll(*d_os); }
00406
00407
00408
00409 int scopeLevel();
00410
00411 };
00412
00413 extern Debug debugger;
00414
00415 }
00416
00417 #else // if DEBUG is not defined
00418
00419
00420
00421 #define IF_DEBUG(code)
00422
00423 #define DebugAssert(cond, str)
00424
00425 #define DBG_PRINT(cond, pre, v, post)
00426 #define TRACE(cond, pre, v, post)
00427
00428 #define DBG_PRINT_MSG(cond, msg)
00429 #define TRACE_MSG(flag, msg)
00430
00431
00432 namespace CVC3 {
00433 class DebugException: public Exception { };
00434 }
00435
00436 #endif // DEBUG
00437
00438 #include "cvc_util.h"
00439
00440 #endif // _cvc3__debug_h