<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: debug.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">debug.h</div> </div>
</div>
<div class="contents">
<a href="debug_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file debug.h</span>
<a name="l00004"></a>00004 <span class="comment"> * \brief Description: Collection of debugging macros and functions.</span>
<a name="l00005"></a>00005 <span class="comment"> *</span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00007"></a>00007 <span class="comment"> *</span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Thu Dec 5 13:12:59 2002</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * <hr></span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> *</span>
<a name="l00017"></a>00017 <span class="comment"> * <hr></span>
<a name="l00018"></a>00018 <span class="comment"> *</span>
<a name="l00019"></a>00019 <span class="comment"> */</span>
<a name="l00020"></a>00020 <span class="comment">/*****************************************************************************/</span>
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="preprocessor">#ifndef _cvc3__debug_h</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__debug_h</span>
<a name="l00024"></a>00024 <span class="preprocessor"></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include <string></span>
<a name="l00026"></a>00026 <span class="preprocessor">#include <iostream></span>
<a name="l00027"></a>00027 <span class="preprocessor">#include <sstream></span>
<a name="l00028"></a>00028 <span class="preprocessor">#include <vector></span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="os_8h.html" title="Abstraction over different operating systems.">os.h</a>"</span>
<a name="l00030"></a>00030 <span class="preprocessor">#include "<a class="code" href="exception_8h.html">exception.h</a>"</span>
<a name="l00031"></a>00031 <span class="comment"></span>
<a name="l00032"></a>00032 <span class="comment">/*! @brief If something goes horribly wrong, print a message and abort</span>
<a name="l00033"></a>00033 <span class="comment"> immediately with exit(1). */</span><span class="comment"></span>
<a name="l00034"></a>00034 <span class="comment">/*! This macro stays even in the non-debug build, so the end users can</span>
<a name="l00035"></a>00035 <span class="comment"> send us meaningful bug reports. */</span>
<a name="l00036"></a>00036
<a name="l00037"></a><a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce">00037</a> <span class="preprocessor">#define FatalAssert(cond, msg) if(!(cond)) \</span>
<a name="l00038"></a>00038 <span class="preprocessor"> CVC3::fatalError(__FILE__, __LINE__, #cond, msg)</span>
<a name="l00039"></a>00039 <span class="preprocessor"></span>
<a name="l00040"></a>00040 <span class="keyword">namespace </span>CVC3 {<span class="comment"></span>
<a name="l00041"></a>00041 <span class="comment"> //! Function for fatal exit.</span>
<a name="l00042"></a>00042 <span class="comment"></span><span class="comment"> /*! It just exits with code 1, but is provided here for the debugger</span>
<a name="l00043"></a>00043 <span class="comment"> to set a breakpoint to. For this reason, it is not inlined. */</span>
<a name="l00044"></a>00044 <span class="keyword">extern</span> <a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> <span class="keywordtype">void</span> <a class="code" href="namespaceCVC3.html#af191ea335afe222795ad4f508a5be267" title="Function for fatal exit.">fatalError</a>(<span class="keyword">const</span> std::string& file, <span class="keywordtype">int</span> line,
<a name="l00045"></a>00045 <span class="keyword">const</span> std::string& cond, <span class="keyword">const</span> std::string& msg);
<a name="l00046"></a>00046 }
<a name="l00047"></a>00047
<a name="l00048"></a>00048 <span class="preprocessor">#ifdef _CVC3_DEBUG_MODE</span>
<a name="l00049"></a>00049 <span class="preprocessor"></span>
<a name="l00050"></a>00050 <span class="preprocessor">#include "<a class="code" href="compat__hash__map_8h.html">compat_hash_map.h</a>"</span>
<a name="l00051"></a>00051 <span class="preprocessor">#include "<a class="code" href="compat__hash__set_8h.html">compat_hash_set.h</a>"</span>
<a name="l00052"></a>00052 <span class="comment"></span>
<a name="l00053"></a>00053 <span class="comment">//! Any debugging code must be within IF_DEBUG(...)</span>
<a name="l00054"></a>00054 <span class="comment"></span><span class="preprocessor">#define IF_DEBUG(code) code</span>
<a name="l00055"></a>00055 <span class="preprocessor"></span><span class="comment"></span>
<a name="l00056"></a>00056 <span class="comment">//! Print a value conditionally.</span>
<a name="l00057"></a>00057 <span class="comment"></span><span class="comment">/*! If 'cond' is true, print 'pre', then 'v', then 'post'. The type</span>
<a name="l00058"></a>00058 <span class="comment"> of v must have overloaded operator<<. It expects a ';' after it. */</span>
<a name="l00059"></a>00059 <span class="preprocessor">#define DBG_PRINT(cond, pre, v, post) if(cond) CVC3::debugger.getOS() \</span>
<a name="l00060"></a>00060 <span class="preprocessor"> << (pre) << (v) << (post) << std::endl</span>
<a name="l00061"></a>00061 <span class="preprocessor"></span><span class="comment"></span>
<a name="l00062"></a>00062 <span class="comment">//! Print a message conditionally</span>
<a name="l00063"></a>00063 <span class="comment"></span><span class="preprocessor">#define DBG_PRINT_MSG(cond, msg) \</span>
<a name="l00064"></a>00064 <span class="preprocessor"> if(cond) CVC3::debugger.getOS() << (msg) << std::endl</span>
<a name="l00065"></a>00065 <span class="preprocessor"></span><span class="comment"></span>
<a name="l00066"></a>00066 <span class="comment">/*! @brief Same as DBG_PRINT, only takes a flag name instead of a</span>
<a name="l00067"></a>00067 <span class="comment"> general condition */</span>
<a name="l00068"></a>00068 <span class="preprocessor">#define TRACE(flag, pre, v, post) \</span>
<a name="l00069"></a>00069 <span class="preprocessor"> DBG_PRINT(CVC3::debugger.trace(flag), pre, v, post)</span>
<a name="l00070"></a>00070 <span class="preprocessor"></span><span class="comment"></span>
<a name="l00071"></a>00071 <span class="comment">//! Same as TRACE, but for a simple message</span>
<a name="l00072"></a>00072 <span class="comment"></span><span class="preprocessor">#define TRACE_MSG(flag, msg) \</span>
<a name="l00073"></a>00073 <span class="preprocessor"> DBG_PRINT_MSG(CVC3::debugger.trace(flag), msg)</span>
<a name="l00074"></a>00074 <span class="preprocessor"></span><span class="comment"></span>
<a name="l00075"></a>00075 <span class="comment">//! Sanity check for debug build. It disappears in the production code.</span>
<a name="l00076"></a>00076 <span class="comment"></span><span class="preprocessor">#define DebugAssert(cond, str) if(!(cond)) \</span>
<a name="l00077"></a>00077 <span class="preprocessor"> CVC3::debugError(__FILE__, __LINE__, #cond, str)</span>
<a name="l00078"></a>00078 <span class="preprocessor"></span>
<a name="l00079"></a>00079
<a name="l00080"></a>00080 <span class="keyword">namespace </span>CVC3 {
<a name="l00081"></a>00081
<a name="l00082"></a>00082 <span class="keyword">class </span>Expr;<span class="comment"></span>
<a name="l00083"></a>00083 <span class="comment"> //! Our exception to throw</span>
<a name="l00084"></a>00084 <span class="comment"></span> <span class="keyword">class </span>DebugException: <span class="keyword">public</span> Exception {
<a name="l00085"></a>00085 <span class="keyword">public</span>:
<a name="l00086"></a>00086 <span class="comment">// Constructor</span>
<a name="l00087"></a>00087 DebugException(<span class="keyword">const</span> std::string& msg): <a class="code" href="classCVC3_1_1Exception.html#abc21464834c8a8d18063b7a3685f773c">Exception</a>(msg) { }
<a name="l00088"></a>00088 <span class="comment">// Printing</span>
<a name="l00089"></a>00089 <span class="keyword">virtual</span> std::string <a class="code" href="classCVC3_1_1Exception.html#a1c8a5ddbb45b98059454efc839394f96">toString</a>()<span class="keyword"> const </span>{
<a name="l00090"></a>00090 <span class="keywordflow">return</span> <span class="stringliteral">"Assertion violation "</span> + <a class="code" href="classCVC3_1_1Exception.html#ae4c896c4f9db2cded61761aace45b397">d_msg</a>;
<a name="l00091"></a>00091 }
<a name="l00092"></a>00092 }; <span class="comment">// end of class DebugException</span>
<a name="l00093"></a>00093 <span class="comment"></span>
<a name="l00094"></a>00094 <span class="comment"> //! Similar to fatalError to raise an exception when DebugAssert fires.</span>
<a name="l00095"></a>00095 <span class="comment"></span><span class="comment"> /*! This does not necessarily cause the program to quit. */</span>
<a name="l00096"></a>00096 <span class="keyword">extern</span> <a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> <span class="keywordtype">void</span> debugError(<span class="keyword">const</span> std::string& file, <span class="keywordtype">int</span> line,
<a name="l00097"></a>00097 <span class="keyword">const</span> std::string& cond, <span class="keyword">const</span> std::string& msg);
<a name="l00098"></a>00098
<a name="l00099"></a>00099 <span class="comment">// First, wrapper classes for flags, counters, and timers. Later,</span>
<a name="l00100"></a>00100 <span class="comment">// we overload some operators like '=', '++', etc. for those</span>
<a name="l00101"></a>00101 <span class="comment">// classes.</span><span class="comment"></span>
<a name="l00102"></a>00102 <span class="comment"> //! Boolean flag (can only be true or false)</span>
<a name="l00103"></a>00103 <span class="comment"></span> <span class="keyword">class </span>DebugFlag {
<a name="l00104"></a>00104 <span class="keyword">private</span>:
<a name="l00105"></a>00105 <span class="keywordtype">bool</span>* d_flag; <span class="comment">// We don't own the pointer</span>
<a name="l00106"></a>00106 <span class="keyword">public</span>:
<a name="l00107"></a>00107 <span class="comment">// Constructor: takes the pointer to the actual flag, normally</span>
<a name="l00108"></a>00108 <span class="comment">// stored in class Debug below.</span>
<a name="l00109"></a>00109 DebugFlag(<span class="keywordtype">bool</span>& flag) : d_flag(&flag) { }
<a name="l00110"></a>00110 <span class="comment">// Destructor</span>
<a name="l00111"></a>00111 ~DebugFlag() { }
<a name="l00112"></a>00112 <span class="comment">// Auto-cast to boolean</span>
<a name="l00113"></a>00113 operator bool() { <span class="keywordflow">return</span> *d_flag; }
<a name="l00114"></a>00114
<a name="l00115"></a>00115 <span class="comment">// Setting and resetting by ++ and --</span>
<a name="l00116"></a>00116 <span class="comment">// Prefix versions:</span>
<a name="l00117"></a>00117 <span class="keywordtype">bool</span> operator--() { *d_flag = <span class="keyword">false</span>; <span class="keywordflow">return</span> <span class="keyword">false</span>; }
<a name="l00118"></a>00118 <span class="keywordtype">bool</span> operator++() { *d_flag = <span class="keyword">true</span>; <span class="keywordflow">return</span> <span class="keyword">true</span>; }
<a name="l00119"></a>00119 <span class="comment">// Postfix versions:</span>
<a name="l00120"></a>00120 <span class="keywordtype">bool</span> operator--(<span class="keywordtype">int</span>) { <span class="keywordtype">bool</span> x=*d_flag; *d_flag=<span class="keyword">false</span>; <span class="keywordflow">return</span> x; }
<a name="l00121"></a>00121 <span class="keywordtype">bool</span> operator++(<span class="keywordtype">int</span>) { <span class="keywordtype">bool</span> x=*d_flag; *d_flag=<span class="keyword">true</span>; <span class="keywordflow">return</span> x; }
<a name="l00122"></a>00122 <span class="comment">// Can be assigned only a boolean value</span>
<a name="l00123"></a>00123 DebugFlag& operator=(<span class="keywordtype">bool</span> x) { *d_flag=(x!=<span class="keyword">false</span>); <span class="keywordflow">return</span> *<span class="keyword">this</span>; }
<a name="l00124"></a>00124 <span class="comment">// Comparisons</span>
<a name="l00125"></a>00125 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8e164436388f2d87c971d9bbde973c58">operator==</a>(<span class="keyword">const</span> DebugFlag& f1, <span class="keyword">const</span> DebugFlag& f2);
<a name="l00126"></a>00126 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a5aa953c549c2e103f3834c48bf6cb9a1">operator!=</a>(<span class="keyword">const</span> DebugFlag& f1, <span class="keyword">const</span> DebugFlag& f2);
<a name="l00127"></a>00127 <span class="comment">// Printing</span>
<a name="l00128"></a>00128 <span class="keyword">friend</span> std::ostream& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(std::ostream& os, <span class="keyword">const</span> DebugFlag& f);
<a name="l00129"></a>00129 }; <span class="comment">// end of class DebugFlag</span>
<a name="l00130"></a>00130 <span class="comment"></span>
<a name="l00131"></a>00131 <span class="comment"> //! Checks if the *values* of the flags are equal</span>
<a name="l00132"></a>00132 <span class="comment"></span> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8e164436388f2d87c971d9bbde973c58">operator==</a>(<span class="keyword">const</span> DebugFlag& f1, <span class="keyword">const</span> DebugFlag& f2) {
<a name="l00133"></a>00133 <span class="keywordflow">return</span> (*f1.d_flag) == (*f2.d_flag);
<a name="l00134"></a>00134 }<span class="comment"></span>
<a name="l00135"></a>00135 <span class="comment"> //! Checks if the *values* of the flags are disequal</span>
<a name="l00136"></a>00136 <span class="comment"></span> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a5aa953c549c2e103f3834c48bf6cb9a1">operator!=</a>(<span class="keyword">const</span> DebugFlag& f1, <span class="keyword">const</span> DebugFlag& f2) {
<a name="l00137"></a>00137 <span class="keywordflow">return</span> (*f1.d_flag) != (*f2.d_flag);
<a name="l00138"></a>00138 }<span class="comment"></span>
<a name="l00139"></a>00139 <span class="comment"> //! Printing flags</span>
<a name="l00140"></a>00140 <span class="comment"></span> <span class="keyword">inline</span> std::ostream& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(std::ostream& os, <span class="keyword">const</span> DebugFlag& f) {
<a name="l00141"></a>00141 <span class="keywordflow">if</span>(*f.d_flag) <span class="keywordflow">return</span>(os << <span class="stringliteral">"true"</span>);
<a name="l00142"></a>00142 <span class="keywordflow">else</span> <span class="keywordflow">return</span>(os << <span class="stringliteral">"false"</span>);
<a name="l00143"></a>00143 }
<a name="l00144"></a>00144 <span class="comment"></span>
<a name="l00145"></a>00145 <span class="comment"> //! Integer counter for debugging purposes.</span>
<a name="l00146"></a>00146 <span class="comment"></span><span class="comment"> /*! Intended use is to count events (e.g. number of function calls),</span>
<a name="l00147"></a>00147 <span class="comment"> but can be used to store any integer value (e.g. size of some data</span>
<a name="l00148"></a>00148 <span class="comment"> structure) */</span>
<a name="l00149"></a>00149 <span class="keyword">class </span>DebugCounter {
<a name="l00150"></a>00150 <span class="keyword">private</span>:
<a name="l00151"></a>00151 <span class="keywordtype">int</span>* d_counter; <span class="comment">//!< We don't own the pointer</span>
<a name="l00152"></a>00152 <span class="comment"></span> <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00153"></a>00153 <span class="comment"> //! Constructor</span>
<a name="l00154"></a>00154 <span class="comment"></span><span class="comment"> /*! Takes the pointer to the actual counter, normally stored in</span>
<a name="l00155"></a>00155 <span class="comment"> class Debug below. */</span>
<a name="l00156"></a>00156 DebugCounter(<span class="keywordtype">int</span>& c) : d_counter(&c) { }<span class="comment"></span>
<a name="l00157"></a>00157 <span class="comment"> //! Destructor</span>
<a name="l00158"></a>00158 <span class="comment"></span> ~DebugCounter() { }<span class="comment"></span>
<a name="l00159"></a>00159 <span class="comment"> //! Auto-cast to int.</span>
<a name="l00160"></a>00160 <span class="comment"></span><span class="comment"> /*! In particular, arithmetic comparisons like <, >, <=, >= will</span>
<a name="l00161"></a>00161 <span class="comment"> work because of this. */</span>
<a name="l00162"></a>00162 operator int() { <span class="keywordflow">return</span> *d_counter; }
<a name="l00163"></a>00163
<a name="l00164"></a>00164 <span class="comment">// Auto-increment operators</span>
<a name="l00165"></a>00165 <span class="comment"></span>
<a name="l00166"></a>00166 <span class="comment"> //! Prefix auto-decrement</span>
<a name="l00167"></a>00167 <span class="comment"></span> <span class="keywordtype">int</span> operator--() { <span class="keywordflow">return</span> --(*d_counter); }<span class="comment"></span>
<a name="l00168"></a>00168 <span class="comment"> //! Prefix auto-increment</span>
<a name="l00169"></a>00169 <span class="comment"></span> <span class="keywordtype">int</span> operator++() { <span class="keywordflow">return</span> ++(*d_counter); }<span class="comment"></span>
<a name="l00170"></a>00170 <span class="comment"> //! Postfix auto-decrement</span>
<a name="l00171"></a>00171 <span class="comment"></span> <span class="keywordtype">int</span> operator--(<span class="keywordtype">int</span>) { <span class="keywordflow">return</span> (*d_counter)--; }<span class="comment"></span>
<a name="l00172"></a>00172 <span class="comment"> //! Postfix auto-increment</span>
<a name="l00173"></a>00173 <span class="comment"></span> <span class="keywordtype">int</span> operator++(<span class="keywordtype">int</span>) { <span class="keywordflow">return</span> (*d_counter)++; }<span class="comment"></span>
<a name="l00174"></a>00174 <span class="comment"> //! Value assignment.</span>
<a name="l00175"></a>00175 <span class="comment"></span> DebugCounter& operator=(<span class="keywordtype">int</span> x) { *d_counter=x; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }
<a name="l00176"></a>00176 DebugCounter& operator+=(<span class="keywordtype">int</span> x) { *d_counter+=x; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }
<a name="l00177"></a>00177 DebugCounter& operator-=(<span class="keywordtype">int</span> x) { *d_counter-=x; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }<span class="comment"></span>
<a name="l00178"></a>00178 <span class="comment"> //! Assignment from another counter.</span>
<a name="l00179"></a>00179 <span class="comment"></span><span class="comment"> /*! It copies the value, not the pointer */</span>
<a name="l00180"></a>00180 DebugCounter& operator=(<span class="keyword">const</span> DebugCounter& x)
<a name="l00181"></a>00181 { *d_counter=*x.d_counter; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }<span class="comment"></span>
<a name="l00182"></a>00182 <span class="comment"> /*! It copies the value, not the pointer */</span>
<a name="l00183"></a>00183 DebugCounter& operator-=(<span class="keyword">const</span> DebugCounter& x)
<a name="l00184"></a>00184 { *d_counter-=*x.d_counter; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }<span class="comment"></span>
<a name="l00185"></a>00185 <span class="comment"> /*! It copies the value, not the pointer */</span>
<a name="l00186"></a>00186 DebugCounter& operator+=(<span class="keyword">const</span> DebugCounter& x)
<a name="l00187"></a>00187 { *d_counter+=*x.d_counter; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }
<a name="l00188"></a>00188 <span class="comment">// Comparisons to integers and other DebugCounters</span>
<a name="l00189"></a>00189 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8e164436388f2d87c971d9bbde973c58">operator==</a>(<span class="keyword">const</span> DebugCounter& c1, <span class="keyword">const</span> DebugCounter& c2);
<a name="l00190"></a>00190 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a5aa953c549c2e103f3834c48bf6cb9a1">operator!=</a>(<span class="keyword">const</span> DebugCounter& c1, <span class="keyword">const</span> DebugCounter& c2);
<a name="l00191"></a>00191 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8e164436388f2d87c971d9bbde973c58">operator==</a>(<span class="keywordtype">int</span> c1, <span class="keyword">const</span> DebugCounter& c2);
<a name="l00192"></a>00192 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a5aa953c549c2e103f3834c48bf6cb9a1">operator!=</a>(<span class="keywordtype">int</span> c1, <span class="keyword">const</span> DebugCounter& c2);
<a name="l00193"></a>00193 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8e164436388f2d87c971d9bbde973c58">operator==</a>(<span class="keyword">const</span> DebugCounter& c1, <span class="keywordtype">int</span> c2);
<a name="l00194"></a>00194 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a5aa953c549c2e103f3834c48bf6cb9a1">operator!=</a>(<span class="keyword">const</span> DebugCounter& c1, <span class="keywordtype">int</span> c2);<span class="comment"></span>
<a name="l00195"></a>00195 <span class="comment"> //! Printing counters</span>
<a name="l00196"></a>00196 <span class="comment"></span> <span class="keyword">friend</span> std::ostream& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(std::ostream& os, <span class="keyword">const</span> DebugCounter& f);
<a name="l00197"></a>00197 }; <span class="comment">// end of class DebugCounter</span>
<a name="l00198"></a>00198
<a name="l00199"></a>00199 <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8e164436388f2d87c971d9bbde973c58">operator==</a>(<span class="keyword">const</span> DebugCounter& c1, <span class="keyword">const</span> DebugCounter& c2) {
<a name="l00200"></a>00200 <span class="keywordflow">return</span> (*c1.d_counter) == (*c2.d_counter);
<a name="l00201"></a>00201 }
<a name="l00202"></a>00202 <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a5aa953c549c2e103f3834c48bf6cb9a1">operator!=</a>(<span class="keyword">const</span> DebugCounter& c1, <span class="keyword">const</span> DebugCounter& c2) {
<a name="l00203"></a>00203 <span class="keywordflow">return</span> (*c1.d_counter) != (*c2.d_counter);
<a name="l00204"></a>00204 }
<a name="l00205"></a>00205 <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8e164436388f2d87c971d9bbde973c58">operator==</a>(<span class="keywordtype">int</span> c1, <span class="keyword">const</span> DebugCounter& c2) {
<a name="l00206"></a>00206 <span class="keywordflow">return</span> c1 == (*c2.d_counter);
<a name="l00207"></a>00207 }
<a name="l00208"></a>00208 <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a5aa953c549c2e103f3834c48bf6cb9a1">operator!=</a>(<span class="keywordtype">int</span> c1, <span class="keyword">const</span> DebugCounter& c2) {
<a name="l00209"></a>00209 <span class="keywordflow">return</span> c1 != (*c2.d_counter);
<a name="l00210"></a>00210 }
<a name="l00211"></a>00211 <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8e164436388f2d87c971d9bbde973c58">operator==</a>(<span class="keyword">const</span> DebugCounter& c1, <span class="keywordtype">int</span> c2) {
<a name="l00212"></a>00212 <span class="keywordflow">return</span> (*c1.d_counter) == c2;
<a name="l00213"></a>00213 }
<a name="l00214"></a>00214 <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a5aa953c549c2e103f3834c48bf6cb9a1">operator!=</a>(<span class="keyword">const</span> DebugCounter& c1, <span class="keywordtype">int</span> c2) {
<a name="l00215"></a>00215 <span class="keywordflow">return</span> (*c1.d_counter) != c2;
<a name="l00216"></a>00216 }
<a name="l00217"></a>00217 <span class="keyword">inline</span> std::ostream& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(std::ostream& os, <span class="keyword">const</span> DebugCounter& c) {
<a name="l00218"></a>00218 <span class="keywordflow">return</span> (os << *c.d_counter);
<a name="l00219"></a>00219 }
<a name="l00220"></a>00220 <span class="comment"></span>
<a name="l00221"></a>00221 <span class="comment"> //! A class holding the time value.</span>
<a name="l00222"></a>00222 <span class="comment"></span><span class="comment"> /*! What exactly is time is not exposed. It can be the system's</span>
<a name="l00223"></a>00223 <span class="comment"> struct timeval, or it can be the (subset of the) user/system/real</span>
<a name="l00224"></a>00224 <span class="comment"> time tuple. */</span>
<a name="l00225"></a>00225 <span class="keyword">class </span>DebugTime;
<a name="l00226"></a>00226 <span class="comment"></span>
<a name="l00227"></a>00227 <span class="comment"> //! Time counter.</span>
<a name="l00228"></a>00228 <span class="comment"></span><span class="comment"> /*! Intended use is to store time intervals or accumulated time for</span>
<a name="l00229"></a>00229 <span class="comment"> multiple events (e.g. time spent to execute certain lines of code,</span>
<a name="l00230"></a>00230 <span class="comment"> or accumulated time spent in a particular function). */</span>
<a name="l00231"></a>00231 <span class="keyword">class </span><a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> DebugTimer {
<a name="l00232"></a>00232 <span class="keyword">private</span>:
<a name="l00233"></a>00233 DebugTime* d_time; <span class="comment">//!< The time value</span>
<a name="l00234"></a>00234 <span class="comment"></span> <span class="keywordtype">bool</span> d_clean_time; <span class="comment">//!< Set if we own *d_time</span>
<a name="l00235"></a>00235 <span class="comment"></span> <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00236"></a>00236 <span class="comment"> //! Constructor: takes the pointer to the actual time value.</span>
<a name="l00237"></a>00237 <span class="comment"></span><span class="comment"> /*! It is either stored in class Debug below (then the timer is</span>
<a name="l00238"></a>00238 <span class="comment"> "public"), or we own it, making the timer "private". */</span>
<a name="l00239"></a>00239 DebugTimer(DebugTime* time, <span class="keywordtype">bool</span> take_time = <span class="keyword">false</span>)
<a name="l00240"></a>00240 : d_time(time), d_clean_time(take_time) { }<span class="comment"></span>
<a name="l00241"></a>00241 <span class="comment"> /*! @brief Copy constructor: copy the *pointer* from public</span>
<a name="l00242"></a>00242 <span class="comment"> timers, and *value* from private. */</span><span class="comment"></span>
<a name="l00243"></a>00243 <span class="comment"> /*! The reason for different behavior for public and private time</span>
<a name="l00244"></a>00244 <span class="comment"> is the following. When you modify a public timer, you want the</span>
<a name="l00245"></a>00245 <span class="comment"> changes to show in the central database and everywhere else,</span>
<a name="l00246"></a>00246 <span class="comment"> whereas private timers are used as independent temporary</span>
<a name="l00247"></a>00247 <span class="comment"> variables holding intermediate time values. */</span>
<a name="l00248"></a>00248 DebugTimer(<span class="keyword">const</span> DebugTimer& timer);<span class="comment"></span>
<a name="l00249"></a>00249 <span class="comment"> //! Assignment: same logistics as for the copy constructor</span>
<a name="l00250"></a>00250 <span class="comment"></span> DebugTimer& operator=(<span class="keyword">const</span> DebugTimer& timer);
<a name="l00251"></a>00251 <span class="comment"></span>
<a name="l00252"></a>00252 <span class="comment"> //! Destructor</span>
<a name="l00253"></a>00253 <span class="comment"></span> ~DebugTimer();
<a name="l00254"></a>00254
<a name="l00255"></a>00255 <span class="comment">// Operators</span><span class="comment"></span>
<a name="l00256"></a>00256 <span class="comment"> //! Set time to zero</span>
<a name="l00257"></a>00257 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__ExprStream__Manip.html#ga90deb7348703ae1a59a11d9af77aa8ad" title="Reset the indentation to the default at this level.">reset</a>();
<a name="l00258"></a>00258 DebugTimer& operator+=(<span class="keyword">const</span> DebugTimer& timer);
<a name="l00259"></a>00259 DebugTimer& operator-=(<span class="keyword">const</span> DebugTimer& timer);<span class="comment"></span>
<a name="l00260"></a>00260 <span class="comment"> //! Produces new "private" timer</span>
<a name="l00261"></a>00261 <span class="comment"></span> DebugTimer <a class="code" href="namespaceCVC3.html#a286cf8699acada708816e72c6b436b90">operator+</a>(<span class="keyword">const</span> DebugTimer& timer);<span class="comment"></span>
<a name="l00262"></a>00262 <span class="comment"> //! Produces new "private" timer</span>
<a name="l00263"></a>00263 <span class="comment"></span> DebugTimer <a class="code" href="namespaceCVC3.html#aacf567dce1c762f957267427472bd959">operator-</a>(<span class="keyword">const</span> DebugTimer& timer);
<a name="l00264"></a>00264
<a name="l00265"></a>00265 <span class="comment">// Our friends</span>
<a name="l00266"></a>00266 <span class="keyword">friend</span> <span class="keyword">class </span>Debug;
<a name="l00267"></a>00267 <span class="comment">// Comparisons</span>
<a name="l00268"></a>00268 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8e164436388f2d87c971d9bbde973c58">operator==</a>(<span class="keyword">const</span> DebugTimer& t1, <span class="keyword">const</span> DebugTimer& t2);
<a name="l00269"></a>00269 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a5aa953c549c2e103f3834c48bf6cb9a1">operator!=</a>(<span class="keyword">const</span> DebugTimer& t1, <span class="keyword">const</span> DebugTimer& t2);
<a name="l00270"></a>00270 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#ad3e3964a0b8cd9e2749de47b053b9d97">operator<</a>(<span class="keyword">const</span> DebugTimer& t1, <span class="keyword">const</span> DebugTimer& t2);
<a name="l00271"></a>00271 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a0d82fd3eb68860cbd01ae86b2b9e3c66">operator></a>(<span class="keyword">const</span> DebugTimer& t1, <span class="keyword">const</span> DebugTimer& t2);
<a name="l00272"></a>00272 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#abccc88aac4f7652def737f1081dc7a89">operator<=</a>(<span class="keyword">const</span> DebugTimer& t1, <span class="keyword">const</span> DebugTimer& t2);
<a name="l00273"></a>00273 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#af997ba8407b661bf2ffe2cb6f52c3e3b">operator>=</a>(<span class="keyword">const</span> DebugTimer& t1, <span class="keyword">const</span> DebugTimer& t2);
<a name="l00274"></a>00274 <span class="comment"></span>
<a name="l00275"></a>00275 <span class="comment"> //! Print the timer's value</span>
<a name="l00276"></a>00276 <span class="comment"></span> <span class="keyword">friend</span> std::ostream& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(std::ostream& os, <span class="keyword">const</span> DebugTimer& timer);
<a name="l00277"></a>00277 }; <span class="comment">// end of class DebugTimer</span>
<a name="l00278"></a>00278 <span class="comment"></span>
<a name="l00279"></a>00279 <span class="comment"> //! The heart of the Bug Extermination Kingdom.</span>
<a name="l00280"></a>00280 <span class="comment"></span><span class="comment"> /*! This class exposes many important components of the entire</span>
<a name="l00281"></a>00281 <span class="comment"> CVC-lite system for use in debugging, keeps all the flags,</span>
<a name="l00282"></a>00282 <span class="comment"> counters, and timers in the central database, and provides timing</span>
<a name="l00283"></a>00283 <span class="comment"> and printing functions. */</span>
<a name="l00284"></a>00284
<a name="l00285"></a>00285 <span class="keyword">class </span><a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> Debug {
<a name="l00286"></a>00286 <span class="keyword">private</span>:<span class="comment"></span>
<a name="l00287"></a>00287 <span class="comment"> //! Command line options for tracing; these override the TRACE command</span>
<a name="l00288"></a>00288 <span class="comment"></span> <span class="keyword">const</span> std::vector<std::pair<std::string,bool> >* d_traceOptions;<span class="comment"></span>
<a name="l00289"></a>00289 <span class="comment"> //! name of dump file</span>
<a name="l00290"></a>00290 <span class="comment"></span> <span class="keyword">const</span> std::string* d_dumpName;
<a name="l00291"></a>00291 <span class="comment">// Output control</span>
<a name="l00292"></a>00292 std::ostream* d_os;
<a name="l00293"></a>00293 <span class="comment">// Stream for dumping trace to file ("dump-trace" option)</span>
<a name="l00294"></a>00294 std::ostream* d_osDumpTrace;<span class="comment"></span>
<a name="l00295"></a>00295 <span class="comment"> //! Private hasher class for strings</span>
<a name="l00296"></a>00296 <span class="comment"></span> <span class="keyword">class </span>stringHash {
<a name="l00297"></a>00297 <span class="keyword">public</span>:
<a name="l00298"></a>00298 <span class="keywordtype">size_t</span> operator()(<span class="keyword">const</span> std::string& s)<span class="keyword"> const </span>{
<a name="l00299"></a>00299 <a class="code" href="structHash_1_1hash_3_01char_01_5_01_4.html">std::hash<char*></a> h;
<a name="l00300"></a>00300 <span class="keywordflow">return</span> h(s.c_str());
<a name="l00301"></a>00301 }
<a name="l00302"></a>00302 }; <span class="comment">// end of stringHash</span>
<a name="l00303"></a>00303 <span class="comment">// Hash tables for storing flags, counters, and timers</span>
<a name="l00304"></a>00304 <span class="keyword">typedef</span> <a class="code" href="classHash_1_1hash__map.html">std::hash_map<std::string, bool, stringHash></a> FlagMap;
<a name="l00305"></a>00305 <span class="keyword">typedef</span> <a class="code" href="classHash_1_1hash__map.html">std::hash_map<std::string, int, stringHash></a> CounterMap;
<a name="l00306"></a>00306 <span class="keyword">typedef</span> <a class="code" href="classHash_1_1hash__map.html">std::hash_map<std::string, DebugTime*, stringHash></a> TimerMap;
<a name="l00307"></a>00307 FlagMap d_flags; <span class="comment">//!< Set of flags</span>
<a name="l00308"></a>00308 <span class="comment"></span> FlagMap d_traceFlags; <span class="comment">//!< Set of trace flags</span>
<a name="l00309"></a>00309 <span class="comment"></span> CounterMap d_counters; <span class="comment">//!< Set of counters</span>
<a name="l00310"></a>00310 <span class="comment"></span><span class="comment"> /*! Note, that the d_timers map does *not* own the pointers; so</span>
<a name="l00311"></a>00311 <span class="comment"> the objects in d_timers must be destroyed explicitly in our</span>
<a name="l00312"></a>00312 <span class="comment"> destructor. */</span>
<a name="l00313"></a>00313 TimerMap d_timers; <span class="comment">//!< Set of timers</span>
<a name="l00314"></a>00314 <span class="comment"></span>
<a name="l00315"></a>00315 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00316"></a>00316 <span class="comment"> //! Constructor</span>
<a name="l00317"></a>00317 <span class="comment"></span> Debug(): d_traceOptions(NULL), d_os(&std::cerr), d_osDumpTrace(NULL) { }<span class="comment"></span>
<a name="l00318"></a>00318 <span class="comment"> //! Destructor (must destroy objects it d_timers)</span>
<a name="l00319"></a>00319 <span class="comment"></span> ~Debug();<span class="comment"></span>
<a name="l00320"></a>00320 <span class="comment"> //! Must be called before Debug class can be safely used</span>
<a name="l00321"></a>00321 <span class="comment"></span> <span class="keywordtype">void</span> init(<span class="keyword">const</span> std::vector<std::pair<std::string,bool> >* traceOptions,
<a name="l00322"></a>00322 <span class="keyword">const</span> std::string* dumpName);<span class="comment"></span>
<a name="l00323"></a>00323 <span class="comment"> //! Must be called before arguments supplied to init are deallocated</span>
<a name="l00324"></a>00324 <span class="comment"></span> <span class="keywordtype">void</span> finalize();<span class="comment"></span>
<a name="l00325"></a>00325 <span class="comment"> //! Accessing flags by name.</span>
<a name="l00326"></a>00326 <span class="comment"></span><span class="comment"> /*! If a flag doesn't exist, it is created and initialized to</span>
<a name="l00327"></a>00327 <span class="comment"> false. */</span>
<a name="l00328"></a>00328 DebugFlag flag(<span class="keyword">const</span> std::string& name)
<a name="l00329"></a>00329 { <span class="keywordflow">return</span> DebugFlag(d_flags[name]); }<span class="comment"></span>
<a name="l00330"></a>00330 <span class="comment"> //! Accessing tracing flags by name.</span>
<a name="l00331"></a>00331 <span class="comment"></span><span class="comment"> /*! If a flag doesn't exist, it is created and initialized to</span>
<a name="l00332"></a>00332 <span class="comment"> false. */</span>
<a name="l00333"></a>00333 DebugFlag traceFlag(<span class="keyword">const</span> std::string& name)
<a name="l00334"></a>00334 { <span class="keywordflow">return</span> DebugFlag(d_traceFlags[name]); }<span class="comment"></span>
<a name="l00335"></a>00335 <span class="comment"> //! Accessing tracing flag by char* name (mostly for GDB)</span>
<a name="l00336"></a>00336 <span class="comment"></span> DebugFlag traceFlag(<span class="keyword">const</span> <span class="keywordtype">char</span>* name);<span class="comment"></span>
<a name="l00337"></a>00337 <span class="comment"> //! Set tracing of everything on (1) and off (0) [for use in GDB]</span>
<a name="l00338"></a>00338 <span class="comment"></span> <span class="keywordtype">void</span> traceAll(<span class="keywordtype">bool</span> enable = <span class="keyword">true</span>);<span class="comment"></span>
<a name="l00339"></a>00339 <span class="comment"> //! Accessing counters by name.</span>
<a name="l00340"></a>00340 <span class="comment"></span><span class="comment"> /*! If a counter doesn't exist, it is created and initialized to 0. */</span>
<a name="l00341"></a>00341 DebugCounter counter(<span class="keyword">const</span> std::string& name)
<a name="l00342"></a>00342 { <span class="keywordflow">return</span> DebugCounter(d_counters[name]); }<span class="comment"></span>
<a name="l00343"></a>00343 <span class="comment"> //! Accessing timers by name.</span>
<a name="l00344"></a>00344 <span class="comment"></span><span class="comment"> /*! If a timer doesn't exist, it is created and initialized to 0. */</span>
<a name="l00345"></a>00345 DebugTimer timer(<span class="keyword">const</span> std::string& name);
<a name="l00346"></a>00346 <span class="comment"></span>
<a name="l00347"></a>00347 <span class="comment"> //! Check whether to print trace info for a particular flag.</span>
<a name="l00348"></a>00348 <span class="comment"></span><span class="comment"> /*! Trace flags are the same DebugFlag objects, but live in a</span>
<a name="l00349"></a>00349 <span class="comment"> different namespace from the normal debug flags */</span>
<a name="l00350"></a>00350 <span class="keywordtype">bool</span> trace(<span class="keyword">const</span> std::string& name);
<a name="l00351"></a>00351
<a name="l00352"></a>00352 <span class="comment">// Timer functions</span>
<a name="l00353"></a>00353 <span class="comment"></span>
<a name="l00354"></a>00354 <span class="comment"> //! Create a new "private" timer, initially set to 0.</span>
<a name="l00355"></a>00355 <span class="comment"></span><span class="comment"> /*! The new timer will not be added to the set of timers, will not</span>
<a name="l00356"></a>00356 <span class="comment"> have a name, and will not be printed by 'printAll()'. It is</span>
<a name="l00357"></a>00357 <span class="comment"> intended to be used to measure time intervals which are later</span>
<a name="l00358"></a>00358 <span class="comment"> added or assigned to the named timers. */</span>
<a name="l00359"></a>00359 <span class="keyword">static</span> DebugTimer newTimer();
<a name="l00360"></a>00360 <span class="comment"></span>
<a name="l00361"></a>00361 <span class="comment"> //! Set the timer to the current time (whatever that means)</span>
<a name="l00362"></a>00362 <span class="comment"></span> <span class="keywordtype">void</span> setCurrentTime(DebugTimer& timer);
<a name="l00363"></a>00363 <span class="keywordtype">void</span> setCurrentTime(<span class="keyword">const</span> std::string& name) {
<a name="l00364"></a>00364 DebugTimer t(timer(name));
<a name="l00365"></a>00365 setCurrentTime(t);
<a name="l00366"></a>00366 }<span class="comment"></span>
<a name="l00367"></a>00367 <span class="comment"> /*! @brief Set the timer to the difference between current time</span>
<a name="l00368"></a>00368 <span class="comment"> and the time stored in the timer: timer = currentTime -</span>
<a name="l00369"></a>00369 <span class="comment"> timer. */</span><span class="comment"></span>
<a name="l00370"></a>00370 <span class="comment"> /*! Intended to obtain the time interval since the last call to</span>
<a name="l00371"></a>00371 <span class="comment"> setCurrentTime() with that timer. */</span>
<a name="l00372"></a>00372 <span class="keywordtype">void</span> setElapsed(DebugTimer& timer);
<a name="l00373"></a>00373 <span class="comment"></span>
<a name="l00374"></a>00374 <span class="comment"> //! Return the ostream used for debugging output</span>
<a name="l00375"></a>00375 <span class="comment"></span> std::ostream& getOS() { <span class="keywordflow">return</span> *d_os; }<span class="comment"></span>
<a name="l00376"></a>00376 <span class="comment"> //! Return the ostream for dumping trace</span>
<a name="l00377"></a>00377 <span class="comment"></span> std::ostream& getOSDumpTrace();
<a name="l00378"></a>00378 <span class="comment"></span>
<a name="l00379"></a>00379 <span class="comment"> //! Print an entry to the dump file</span>
<a name="l00380"></a>00380 <span class="comment"></span> <span class="keywordtype">void</span> dumpTrace(<span class="keyword">const</span> std::string& title,
<a name="l00381"></a>00381 <span class="keyword">const</span> std::vector<std::pair<std::string,std::string> >&
<a name="l00382"></a>00382 fields);<span class="comment"></span>
<a name="l00383"></a>00383 <span class="comment"> //! Set the debugging ostream</span>
<a name="l00384"></a>00384 <span class="comment"></span> <span class="keywordtype">void</span> setOS(std::ostream& os) { d_os = &os; }
<a name="l00385"></a>00385 <span class="comment"></span>
<a name="l00386"></a>00386 <span class="comment"> //! Print all the collected data if "DEBUG" flag is set to 'os'</span>
<a name="l00387"></a>00387 <span class="comment"></span> <span class="keywordtype">void</span> printAll(std::ostream& os);<span class="comment"></span>
<a name="l00388"></a>00388 <span class="comment"> /*! @brief Print all the collected data if "DEBUG" flag is set to</span>
<a name="l00389"></a>00389 <span class="comment"> the default debug stream */</span>
<a name="l00390"></a>00390 <span class="keywordtype">void</span> printAll() { printAll(*d_os); }
<a name="l00391"></a>00391
<a name="l00392"></a>00392 <span class="comment">// Generally useful functions</span><span class="comment"></span>
<a name="l00393"></a>00393 <span class="comment"> //! Get the current scope level</span>
<a name="l00394"></a>00394 <span class="comment"></span> <span class="keywordtype">int</span> scopeLevel();
<a name="l00395"></a>00395
<a name="l00396"></a>00396 }; <span class="comment">// end of class Debug</span>
<a name="l00397"></a>00397
<a name="l00398"></a>00398 <span class="keyword">extern</span> <a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> Debug debugger;
<a name="l00399"></a>00399
<a name="l00400"></a>00400 } <span class="comment">// end of namespace CVC3</span>
<a name="l00401"></a>00401
<a name="l00402"></a>00402 <span class="preprocessor">#else // if _CVC3_DEBUG_MODE is not defined</span>
<a name="l00403"></a>00403 <span class="preprocessor"></span>
<a name="l00404"></a>00404 <span class="comment">// All debugging macros are empty here</span>
<a name="l00405"></a>00405
<a name="l00406"></a><a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">00406</a> <span class="preprocessor">#define IF_DEBUG(code)</span>
<a name="l00407"></a>00407 <span class="preprocessor"></span>
<a name="l00408"></a><a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">00408</a> <span class="preprocessor">#define DebugAssert(cond, str)</span>
<a name="l00409"></a>00409 <span class="preprocessor"></span>
<a name="l00410"></a><a class="code" href="debug_8h.html#a3fbf72853e2eda3afe9cc59c02e82253">00410</a> <span class="preprocessor">#define DBG_PRINT(cond, pre, v, post)</span>
<a name="l00411"></a><a class="code" href="debug_8h.html#aee6dbc9177de2d2b4a1627f6c5c1c03f">00411</a> <span class="preprocessor"></span><span class="preprocessor">#define TRACE(cond, pre, v, post)</span>
<a name="l00412"></a>00412 <span class="preprocessor"></span>
<a name="l00413"></a><a class="code" href="debug_8h.html#a2ccc254164135b52d99b22bde90fb913">00413</a> <span class="preprocessor">#define DBG_PRINT_MSG(cond, msg)</span>
<a name="l00414"></a><a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">00414</a> <span class="preprocessor"></span><span class="preprocessor">#define TRACE_MSG(flag, msg)</span>
<a name="l00415"></a>00415 <span class="preprocessor"></span>
<a name="l00416"></a>00416 <span class="comment">// to make the CLI wrapper happy</span>
<a name="l00417"></a>00417 <span class="keyword">namespace </span>CVC3 {
<a name="l00418"></a><a class="code" href="classCVC3_1_1DebugException.html">00418</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1DebugException.html">DebugException</a>: <span class="keyword">public</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a> { };
<a name="l00419"></a>00419 }
<a name="l00420"></a>00420
<a name="l00421"></a>00421 <span class="preprocessor">#endif // _CVC3_DEBUG_MODE</span>
<a name="l00422"></a>00422 <span class="preprocessor"></span>
<a name="l00423"></a>00423 <span class="preprocessor">#include "<a class="code" href="cvc__util_8h.html" title="basic helper utilities">cvc_util.h</a>"</span>
<a name="l00424"></a>00424
<a name="l00425"></a>00425 <span class="preprocessor">#endif // _cvc3__debug_h</span>
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
