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