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