36 const std::string& cond,
const std::string& msg) {
37 cerr <<
"\n**** Fatal error in " << file <<
":" << line
38 <<
" (" << cond <<
")\n" << msg <<
endl << flush;
44 #ifdef _CVC3_DEBUG_MODE
52 CVC_DLL void debugError(
const std::string& file,
int line,
53 const std::string& cond,
const std::string& msg) {
55 ss <<
"in " << file <<
":" << line <<
" (" << cond <<
")\n" << msg;
56 throw DebugException(ss.str());
68 DebugTime(
const clock_t& clock): d_clock(clock) { }
76 DebugTime& operator+=(
const DebugTime& t) {
80 DebugTime& operator-=(
const DebugTime& t) {
85 friend bool operator==(
const DebugTime& t1,
const DebugTime& t2);
86 friend bool operator!=(
const DebugTime& t1,
const DebugTime& t2);
88 friend bool operator<(
const DebugTime& t1,
const DebugTime& t2);
89 friend bool operator>(
const DebugTime& t1,
const DebugTime& t2);
90 friend bool operator<=(
const DebugTime& t1,
const DebugTime& t2);
91 friend bool operator>=(
const DebugTime& t1,
const DebugTime& t2);
93 friend ostream&
operator<<(ostream& os,
const DebugTime& t);
96 DebugTime
operator+(
const DebugTime& t1,
const DebugTime& t2) {
101 DebugTime
operator-(
const DebugTime& t1,
const DebugTime& t2) {
107 bool operator==(
const DebugTime& t1,
const DebugTime& t2) {
108 return t1.d_clock == t2.d_clock;
111 bool operator!=(
const DebugTime& t1,
const DebugTime& t2) {
115 bool operator<(
const DebugTime& t1,
const DebugTime& t2) {
116 return t1.d_clock < t2.d_clock;
119 bool operator>(
const DebugTime& t1,
const DebugTime& t2) {
120 return t1.d_clock > t2.d_clock;
123 bool operator<=(
const DebugTime& t1,
const DebugTime& t2) {
124 return t1.d_clock <= t2.d_clock;
127 bool operator>=(
const DebugTime& t1,
const DebugTime& t2) {
128 return t1.d_clock >= t2.d_clock;
136 DebugTimer::~DebugTimer() {
141 void Debug::init(
const std::vector<std::pair<std::string,bool> >* traceOptions,
142 const std::string* dumpName)
144 d_traceOptions = traceOptions;
145 d_dumpName = dumpName;
148 void Debug::finalize()
150 d_traceOptions = NULL;
155 Debug::traceFlag(
const char* name) {
return traceFlag(std::string(name)); }
158 Debug::traceAll(
bool enable) { traceFlag(
"ALL") = enable; }
165 DebugTimer::DebugTimer(
const DebugTimer& timer) {
166 d_clean_time = timer.d_clean_time;
169 d_time =
new DebugTime(*timer.d_time);
173 d_time = timer.d_time;
178 DebugTimer& DebugTimer::operator=(
const DebugTimer& timer) {
180 if(&timer ==
this)
return *
this;
182 if(timer.d_clean_time) {
185 *d_time = *timer.d_time;
187 d_time =
new DebugTime(*timer.d_time);
194 d_time = timer.d_time;
195 d_clean_time =
false;
204 DebugTimer& DebugTimer::operator+=(
const DebugTimer& timer) {
205 (*d_time) += *(timer.d_time);
209 DebugTimer& DebugTimer::operator-=(
const DebugTimer& timer) {
210 (*d_time) -= *(timer.d_time);
216 return DebugTimer(
new DebugTime((*d_time) + (*timer.d_time)),
221 return DebugTimer(
new DebugTime((*d_time) - (*timer.d_time)),
226 bool operator==(
const DebugTimer& t1,
const DebugTimer& t2) {
227 return(*t1.d_time == *t2.d_time);
229 bool operator!=(
const DebugTimer& t1,
const DebugTimer& t2) {
230 return(*t1.d_time != *t2.d_time);
232 bool operator<(
const DebugTimer& t1,
const DebugTimer& t2) {
233 return *t1.d_time < *t2.d_time;
235 bool operator>(
const DebugTimer& t1,
const DebugTimer& t2) {
236 return *t1.d_time > *t2.d_time;
238 bool operator<=(
const DebugTimer& t1,
const DebugTimer& t2) {
239 return *t1.d_time <= *t2.d_time;
241 bool operator>=(
const DebugTimer& t1,
const DebugTimer& t2) {
242 return *t1.d_time >= *t2.d_time;
246 ostream&
operator<<(ostream& os,
const DebugTime& t) {
247 int seconds = (int)(t.d_clock / CLOCKS_PER_SEC);
248 int milliseconds = 1000 * int((((
double)(t.d_clock % CLOCKS_PER_SEC)) / CLOCKS_PER_SEC));
249 os << seconds <<
"." << setfill(
'0') << setw(6) << milliseconds;
252 ostream&
operator<<(ostream& os,
const DebugTimer& timer) {
253 return(os << *timer.d_time);
262 TimerMap::iterator i, iend;
263 for(i = d_timers.begin(), iend = d_timers.end(); i != iend; ++i)
265 if(d_osDumpTrace != NULL)
266 delete d_osDumpTrace;
270 Debug::trace(
const string& name) {
273 if(d_traceOptions != NULL) {
274 vector<pair<string,bool> >::const_reverse_iterator i, iend;
275 for(i=d_traceOptions->rbegin(), iend=d_traceOptions->rend(); i!=iend; ++i)
276 if((*i).first == name || (*i).first ==
"ALL")
return (*i).second;
278 return traceFlag(name) || traceFlag(
"ALL");
282 DebugTimer Debug::timer(
const string& name) {
284 if(d_timers.count(name) > 0)
return(DebugTimer(d_timers[name]));
287 DebugTime *t =
new DebugTime();
289 return DebugTimer(t);
293 DebugTimer Debug::newTimer() {
294 return DebugTimer(
new DebugTime(),
true );
297 void Debug::setCurrentTime(DebugTimer& timer) {
298 *timer.d_time = clock();
305 void Debug::setElapsed(DebugTimer& timer) {
306 *timer.d_time -= DebugTime(clock());
314 ostream& Debug::getOSDumpTrace() {
315 if(d_osDumpTrace != NULL)
return *d_osDumpTrace;
317 if(*d_dumpName ==
"" || *d_dumpName ==
"-")
return cout;
318 d_osDumpTrace =
new ofstream(d_dumpName->c_str());
319 return *d_osDumpTrace;
324 void Debug::dumpTrace(
const std::string& title,
325 const std::vector<std::pair<std::string,std::string> >& fields) {
326 ostream& os = getOSDumpTrace();
327 os <<
"[" << title <<
"]\n";
328 for(
size_t i=0, iend=fields.size(); i<iend; ++i)
329 os << fields[i].first <<
" = " << fields[i].second <<
"\n";
335 void Debug::printAll(ostream& os) {
336 if(!trace(
"DEBUG"))
return;
339 <<
"********************************" <<
endl
340 <<
"******* Debugging Info *********" <<
endl
341 <<
"********************************" <<
endl;
343 if(d_flags.size() > 0) {
344 os << endl <<
"************ Flags *************" << endl <<
endl;
345 for(FlagMap::iterator
346 i = d_flags.begin(), iend = d_flags.end(); i != iend; ++i)
347 os << (*i).first <<
" = " << (*i).second << endl;
350 if(d_counters.size() > 0) {
351 os << endl <<
"*********** Counters ***********" << endl <<
endl;
352 for(CounterMap::iterator
353 i = d_counters.begin(), iend = d_counters.end(); i != iend; ++i)
354 os << (*i).first <<
" = " << (*i).second << endl;
357 if(d_timers.size() > 0) {
358 os << endl <<
"************ Timers ************" << endl <<
endl;
359 for(TimerMap::iterator
360 i = d_timers.begin(), iend = d_timers.end(); i != iend; ++i)
361 os << (*i).first <<
" = " << *((*i).second) <<
endl;
365 <<
"********************************" << endl
366 <<
"**** End of Debugging Info *****" << endl
367 <<
"********************************" <<
endl;