00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #include <fstream>
00023
00024 #include "debug.h"
00025
00026 using namespace std;
00027
00028 namespace CVC3 {
00029
00030
00031
00032
00033 void fatalError(const std::string& file, int line,
00034 const std::string& cond, const std::string& msg) {
00035 cerr << "\n**** Fatal error in " << file << ":" << line
00036 << " (" << cond << ")\n" << msg << endl << flush;
00037 exit(1);
00038 }
00039
00040 }
00041
00042 #ifdef DEBUG
00043
00044 #include <ctime>
00045 #include <iomanip>
00046
00047 namespace CVC3 {
00048
00049
00050 void debugError(const std::string& file, int line,
00051 const std::string& cond, const std::string& msg) {
00052 ostringstream ss;
00053 ss << "in " << file << ":" << line << " (" << cond << ")\n" << msg;
00054 throw DebugException(ss.str());
00055 }
00056
00057
00058 class DebugTime {
00059 public:
00060 clock_t d_clock;
00061
00062
00063 DebugTime() {
00064 d_clock = 0;
00065 }
00066 DebugTime(const clock_t& clock): d_clock(clock) { }
00067
00068
00069 void reset() {
00070 d_clock = 0;
00071 }
00072
00073
00074 DebugTime& operator+=(const DebugTime& t) {
00075 d_clock += t.d_clock;
00076 return *this;
00077 }
00078 DebugTime& operator-=(const DebugTime& t) {
00079 d_clock -= t.d_clock;
00080 return *this;
00081 }
00082
00083 friend bool operator==(const DebugTime& t1, const DebugTime& t2);
00084 friend bool operator!=(const DebugTime& t1, const DebugTime& t2);
00085
00086 friend bool operator<(const DebugTime& t1, const DebugTime& t2);
00087 friend bool operator>(const DebugTime& t1, const DebugTime& t2);
00088 friend bool operator<=(const DebugTime& t1, const DebugTime& t2);
00089 friend bool operator>=(const DebugTime& t1, const DebugTime& t2);
00090
00091 friend ostream& operator<<(ostream& os, const DebugTime& t);
00092 };
00093
00094 DebugTime operator+(const DebugTime& t1, const DebugTime& t2) {
00095 DebugTime res(t1);
00096 res += t2;
00097 return res;
00098 }
00099 DebugTime operator-(const DebugTime& t1, const DebugTime& t2) {
00100 DebugTime res(t1);
00101 res -= t2;
00102 return res;
00103 }
00104
00105 bool operator==(const DebugTime& t1, const DebugTime& t2) {
00106 return t1.d_clock == t2.d_clock;
00107 }
00108
00109 bool operator!=(const DebugTime& t1, const DebugTime& t2) {
00110 return !(t1 == t2);
00111 }
00112
00113 bool operator<(const DebugTime& t1, const DebugTime& t2) {
00114 return t1.d_clock < t2.d_clock;
00115 }
00116
00117 bool operator>(const DebugTime& t1, const DebugTime& t2) {
00118 return t1.d_clock > t2.d_clock;
00119 }
00120
00121 bool operator<=(const DebugTime& t1, const DebugTime& t2) {
00122 return t1.d_clock <= t2.d_clock;
00123 }
00124
00125 bool operator>=(const DebugTime& t1, const DebugTime& t2) {
00126 return t1.d_clock >= t2.d_clock;
00127 }
00128
00129
00130
00131
00132
00133
00134 DebugTimer::~DebugTimer() {
00135 if(d_clean_time)
00136 delete d_time;
00137 }
00138
00139 void Debug::init(const std::vector<std::pair<std::string,bool> >* traceOptions,
00140 const std::string* dumpName)
00141 {
00142 d_traceOptions = traceOptions;
00143 d_dumpName = dumpName;
00144 }
00145
00146
00147 DebugFlag
00148 Debug::traceFlag(char* name) { return traceFlag(std::string(name)); }
00149
00150 void
00151 Debug::traceAll(bool enable) { traceFlag("ALL") = enable; }
00152
00153
00154
00155
00156
00157
00158 DebugTimer::DebugTimer(const DebugTimer& timer) {
00159 d_clean_time = timer.d_clean_time;
00160 if(d_clean_time) {
00161
00162 d_time = new DebugTime(*timer.d_time);
00163 d_clean_time = true;
00164 } else {
00165
00166 d_time = timer.d_time;
00167 }
00168 }
00169
00170
00171 DebugTimer& DebugTimer::operator=(const DebugTimer& timer) {
00172
00173 if(&timer == this) return *this;
00174
00175 if(timer.d_clean_time) {
00176
00177 if(d_clean_time)
00178 *d_time = *timer.d_time;
00179 else {
00180 d_time = new DebugTime(*timer.d_time);
00181 d_clean_time = true;
00182 }
00183 } else {
00184
00185 if(d_clean_time)
00186 delete d_time;
00187 d_time = timer.d_time;
00188 d_clean_time = false;
00189 }
00190 return *this;
00191 }
00192
00193 void DebugTimer::reset() {
00194 d_time->reset();
00195 }
00196
00197 DebugTimer& DebugTimer::operator+=(const DebugTimer& timer) {
00198 (*d_time) += *(timer.d_time);
00199 return *this;
00200 }
00201
00202 DebugTimer& DebugTimer::operator-=(const DebugTimer& timer) {
00203 (*d_time) -= *(timer.d_time);
00204 return *this;
00205 }
00206
00207
00208 DebugTimer DebugTimer::operator+(const DebugTimer& timer) {
00209 return DebugTimer(new DebugTime((*d_time) + (*timer.d_time)),
00210 true );
00211 }
00212
00213 DebugTimer DebugTimer::operator-(const DebugTimer& timer) {
00214 return DebugTimer(new DebugTime((*d_time) - (*timer.d_time)),
00215 true );
00216 }
00217
00218
00219 bool operator==(const DebugTimer& t1, const DebugTimer& t2) {
00220 return(*t1.d_time == *t2.d_time);
00221 }
00222 bool operator!=(const DebugTimer& t1, const DebugTimer& t2) {
00223 return(*t1.d_time != *t2.d_time);
00224 }
00225 bool operator<(const DebugTimer& t1, const DebugTimer& t2) {
00226 return *t1.d_time < *t2.d_time;
00227 }
00228 bool operator>(const DebugTimer& t1, const DebugTimer& t2) {
00229 return *t1.d_time > *t2.d_time;
00230 }
00231 bool operator<=(const DebugTimer& t1, const DebugTimer& t2) {
00232 return *t1.d_time <= *t2.d_time;
00233 }
00234 bool operator>=(const DebugTimer& t1, const DebugTimer& t2) {
00235 return *t1.d_time >= *t2.d_time;
00236 }
00237
00238
00239 ostream& operator<<(ostream& os, const DebugTime& t) {
00240 int seconds = (int)(t.d_clock / CLOCKS_PER_SEC);
00241 int milliseconds = 1000 * int((((double)(t.d_clock % CLOCKS_PER_SEC)) / CLOCKS_PER_SEC));
00242 os << seconds << "." << setfill('0') << setw(6) << milliseconds;
00243 return os;
00244 }
00245 ostream& operator<<(ostream& os, const DebugTimer& timer) {
00246 return(os << *timer.d_time);
00247 }
00248
00249
00250
00251
00252
00253
00254 Debug::~Debug() {
00255 TimerMap::iterator i, iend;
00256 for(i = d_timers.begin(), iend = d_timers.end(); i != iend; ++i)
00257 delete (*i).second;
00258 if(d_osDumpTrace != NULL)
00259 delete d_osDumpTrace;
00260 }
00261
00262 bool
00263 Debug::trace(const string& name) {
00264
00265
00266 if(d_traceOptions != NULL) {
00267 vector<pair<string,bool> >::const_reverse_iterator i, iend;
00268 for(i=d_traceOptions->rbegin(), iend=d_traceOptions->rend(); i!=iend; ++i)
00269 if((*i).first == name || (*i).first == "ALL") return (*i).second;
00270 }
00271 return traceFlag(name) || traceFlag("ALL");
00272 }
00273
00274
00275 DebugTimer Debug::timer(const string& name) {
00276
00277 if(d_timers.count(name) > 0) return(DebugTimer(d_timers[name]));
00278 else {
00279
00280 DebugTime *t = new DebugTime();
00281 d_timers[name] = t;
00282 return DebugTimer(t);
00283 }
00284 }
00285
00286 DebugTimer Debug::newTimer() {
00287 return DebugTimer(new DebugTime(), true );
00288 }
00289
00290 void Debug::setCurrentTime(DebugTimer& timer) {
00291 *timer.d_time = clock();
00292 }
00293
00294
00295
00296
00297
00298 void Debug::setElapsed(DebugTimer& timer) {
00299 *timer.d_time -= DebugTime(clock());
00300 }
00301
00302
00303
00304
00305
00306
00307 ostream& Debug::getOSDumpTrace() {
00308 if(d_osDumpTrace != NULL) return *d_osDumpTrace;
00309
00310 if(*d_dumpName == "" || *d_dumpName == "-") return cout;
00311 d_osDumpTrace = new ofstream(d_dumpName->c_str());
00312 return *d_osDumpTrace;
00313 }
00314
00315
00316
00317 void Debug::dumpTrace(const std::string& title,
00318 const std::vector<std::pair<std::string,std::string> >& fields) {
00319 ostream& os = getOSDumpTrace();
00320 os << "[" << title << "]\n";
00321 for(size_t i=0, iend=fields.size(); i<iend; ++i)
00322 os << fields[i].first << " = " << fields[i].second << "\n";
00323 os << endl;
00324 }
00325
00326
00327
00328 void Debug::printAll(ostream& os) {
00329 if(!trace("DEBUG")) return;
00330
00331 os << endl
00332 << "********************************" << endl
00333 << "******* Debugging Info *********" << endl
00334 << "********************************" << endl;
00335
00336 if(d_flags.size() > 0) {
00337 os << endl << "************ Flags *************" << endl << endl;
00338 for(FlagMap::iterator
00339 i = d_flags.begin(), iend = d_flags.end(); i != iend; ++i)
00340 os << (*i).first << " = " << (*i).second << endl;
00341 }
00342
00343 if(d_counters.size() > 0) {
00344 os << endl << "*********** Counters ***********" << endl << endl;
00345 for(CounterMap::iterator
00346 i = d_counters.begin(), iend = d_counters.end(); i != iend; ++i)
00347 os << (*i).first << " = " << (*i).second << endl;
00348 }
00349
00350 if(d_timers.size() > 0) {
00351 os << endl << "************ Timers ************" << endl << endl;
00352 for(TimerMap::iterator
00353 i = d_timers.begin(), iend = d_timers.end(); i != iend; ++i)
00354 os << (*i).first << " = " << *((*i).second) << endl;
00355 }
00356
00357 os << endl
00358 << "********************************" << endl
00359 << "**** End of Debugging Info *****" << endl
00360 << "********************************" << endl;
00361 }
00362
00363
00364
00365 Debug debugger;
00366
00367 }
00368
00369 #endif