<!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: expr_stream.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">expr_stream.h</div> </div>
</div>
<div class="contents">
<a href="expr__stream_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 expr_stream.h</span>
<a name="l00004"></a>00004 <span class="comment"> * </span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00006"></a>00006 <span class="comment"> * </span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Mon Jun 16 10:59:18 2003</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> * </span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> * </span>
<a name="l00018"></a>00018 <span class="comment"> * Declaration of class ExprStream, an output stream to pretty-print</span>
<a name="l00019"></a>00019 <span class="comment"> * Expr in various nice output formats (presentation/internal/other</span>
<a name="l00020"></a>00020 <span class="comment"> * languages, outo-indentation, bounded depth printing, DAG-ified</span>
<a name="l00021"></a>00021 <span class="comment"> * printing, etc, etc...).</span>
<a name="l00022"></a>00022 <span class="comment"> * </span>
<a name="l00023"></a>00023 <span class="comment"> * This stream is most useful for the decision procedure designer when</span>
<a name="l00024"></a>00024 <span class="comment"> * writing a pretty-printer (Theory::print() method). ExprStream</span>
<a name="l00025"></a>00025 <span class="comment"> * carries information about the current output language, and all the</span>
<a name="l00026"></a>00026 <span class="comment"> * indentation and depth pretty-printing is done automagically by the</span>
<a name="l00027"></a>00027 <span class="comment"> * operator<<().</span>
<a name="l00028"></a>00028 <span class="comment"> * </span>
<a name="l00029"></a>00029 <span class="comment"> */</span>
<a name="l00030"></a>00030 <span class="comment">/*****************************************************************************/</span>
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="preprocessor">#ifndef _cvc3__expr_stream_h_</span>
<a name="l00033"></a>00033 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__expr_stream_h_</span>
<a name="l00034"></a>00034 <span class="preprocessor"></span>
<a name="l00035"></a>00035 <span class="preprocessor">#include "<a class="code" href="os_8h.html" title="Abstraction over different operating systems.">os.h</a>"</span>
<a name="l00036"></a>00036 <span class="preprocessor">#include "<a class="code" href="expr_8h.html" title="Definition of the API to expression package. See class Expr for details.">expr.h</a>"</span>
<a name="l00037"></a>00037
<a name="l00038"></a>00038 <span class="keyword">namespace </span>CVC3 {
<a name="l00039"></a>00039 <span class="keyword">class </span>ExprStream;
<a name="l00040"></a>00040 }
<a name="l00041"></a>00041
<a name="l00042"></a>00042 <span class="keyword">namespace </span>std {
<a name="l00043"></a>00043 <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">CVC3::ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">CVC3::ExprStream</a>& os);
<a name="l00044"></a>00044 }
<a name="l00045"></a>00045
<a name="l00046"></a>00046 <span class="keyword">namespace </span>CVC3 {
<a name="l00047"></a>00047 <span class="comment"></span>
<a name="l00048"></a>00048 <span class="comment"> /*! \defgroup PrettyPrinting Pretty-printing related classes and methods</span>
<a name="l00049"></a>00049 <span class="comment"> * \ingroup BuildingBlocks</span>
<a name="l00050"></a>00050 <span class="comment"> * If you are writing a theory-specific pretty-printer, please read</span>
<a name="l00051"></a>00051 <span class="comment"> * carefully all the documentation about class ExprStream and its</span>
<a name="l00052"></a>00052 <span class="comment"> * manipulators.</span>
<a name="l00053"></a>00053 <span class="comment"> * </span>
<a name="l00054"></a>00054 <span class="comment"> * @{</span>
<a name="l00055"></a>00055 <span class="comment"> */</span>
<a name="l00056"></a>00056 <span class="comment"></span>
<a name="l00057"></a>00057 <span class="comment"> //! Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!</span>
<a name="l00058"></a>00058 <span class="comment"></span><span class="comment"> /*! Use this class as a standard ostream for Expr, string, int,</span>
<a name="l00059"></a>00059 <span class="comment"> Rational, manipulators like endl, and it will do the expected</span>
<a name="l00060"></a>00060 <span class="comment"> thing. Additionally, it has methods to access the current</span>
<a name="l00061"></a>00061 <span class="comment"> printing flags.</span>
<a name="l00062"></a>00062 <span class="comment"> </span>
<a name="l00063"></a>00063 <span class="comment"> In order for the indentation engine to work correctly, you must</span>
<a name="l00064"></a>00064 <span class="comment"> use the manipulators properly.</span>
<a name="l00065"></a>00065 <span class="comment"></span>
<a name="l00066"></a>00066 <span class="comment"> Never use "\\n" in a string; always use endl manipulator, which</span>
<a name="l00067"></a>00067 <span class="comment"> knows about indentation and will do the right thing.</span>
<a name="l00068"></a>00068 <span class="comment"></span>
<a name="l00069"></a>00069 <span class="comment"> Always assume that the object you are printing may start printing</span>
<a name="l00070"></a>00070 <span class="comment"> on a new line from the current indentation position. Therefore,</span>
<a name="l00071"></a>00071 <span class="comment"> no string should start with an empty space (otherwise parts of</span>
<a name="l00072"></a>00072 <span class="comment"> your expression will be mis-indented). If you need a white space</span>
<a name="l00073"></a>00073 <span class="comment"> separator, or an operator surrounded by spaces, like os << " = ",</span>
<a name="l00074"></a>00074 <span class="comment"> use os << space << "= " instead. The 'space' manipulator adds one</span>
<a name="l00075"></a>00075 <span class="comment"> white space only if it's not at the beginning of a newly indented</span>
<a name="l00076"></a>00076 <span class="comment"> line. Think of it as a logical white-space separator with</span>
<a name="l00077"></a>00077 <span class="comment"> intelligent behavior, rather than a stupid hard space like " ".</span>
<a name="l00078"></a>00078 <span class="comment"></span>
<a name="l00079"></a>00079 <span class="comment"> Indentation can be set to the current position with os << push,</span>
<a name="l00080"></a>00080 <span class="comment"> and restored to the previous with os << pop. You do not need to</span>
<a name="l00081"></a>00081 <span class="comment"> restore it before exiting your print function, ExprStream knows</span>
<a name="l00082"></a>00082 <span class="comment"> how to restore it automatically. For example, you can write:</span>
<a name="l00083"></a>00083 <span class="comment"></span>
<a name="l00084"></a>00084 <span class="comment"> os << "(" << push << e[0] << space << "+ " << e[1] << push << ")";</span>
<a name="l00085"></a>00085 <span class="comment"></span>
<a name="l00086"></a>00086 <span class="comment"> to print (PLUS a b) as "(a + b)". Notice the second 'push' before</span>
<a name="l00087"></a>00087 <span class="comment"> the closing paren. This is intentional (not a typo), and prevents</span>
<a name="l00088"></a>00088 <span class="comment"> the paren ")" from jumping to the next line by itself. ExprStream</span>
<a name="l00089"></a>00089 <span class="comment"> will not go to the next line if the current position is too close</span>
<a name="l00090"></a>00090 <span class="comment"> to the indentation, since this will not give the expression a</span>
<a name="l00091"></a>00091 <span class="comment"> better look.</span>
<a name="l00092"></a>00092 <span class="comment"></span>
<a name="l00093"></a>00093 <span class="comment"> The indentation level is not restored in this example, and that is</span>
<a name="l00094"></a>00094 <span class="comment"> fine, ExprStream will take care of that.</span>
<a name="l00095"></a>00095 <span class="comment"></span>
<a name="l00096"></a>00096 <span class="comment"> For complex expressions like IF-THEN-ELSE, you may want to</span>
<a name="l00097"></a>00097 <span class="comment"> remember the indentation to which you want to return later. You</span>
<a name="l00098"></a>00098 <span class="comment"> can save the current indentation position with os << popSave, and</span>
<a name="l00099"></a>00099 <span class="comment"> restore it later with os << pushRestore. These manipulators are</span>
<a name="l00100"></a>00100 <span class="comment"> similar to pop and push, but 'pushRestore' will set the new</span>
<a name="l00101"></a>00101 <span class="comment"> indentation level to the one popped by the last popSave instead of</span>
<a name="l00102"></a>00102 <span class="comment"> the current one. At the moment, there is only one register for</span>
<a name="l00103"></a>00103 <span class="comment"> saving an indentation position, so multiple pushRestore will not</span>
<a name="l00104"></a>00104 <span class="comment"> work as you would expect (maybe this should be fixed?..).</span>
<a name="l00105"></a>00105 <span class="comment"></span>
<a name="l00106"></a>00106 <span class="comment"> For concrete examples, see TheoryCore::print() and</span>
<a name="l00107"></a>00107 <span class="comment"> TheoryArith::print().</span>
<a name="l00108"></a>00108 <span class="comment"> </span>
<a name="l00109"></a>00109 <span class="comment"> */</span>
<a name="l00110"></a><a class="code" href="classCVC3_1_1ExprStream.html">00110</a> <span class="keyword">class </span><a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> {
<a name="l00111"></a>00111 <span class="keyword">private</span>:
<a name="l00112"></a><a class="code" href="classCVC3_1_1ExprStream.html#a7ab1b6602b49bf13867877bf5f7a5873">00112</a> <a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* <a class="code" href="classCVC3_1_1ExprStream.html#a7ab1b6602b49bf13867877bf5f7a5873" title="The ExprManager to use.">d_em</a>; <span class="comment">//!< The ExprManager to use</span>
<a name="l00113"></a><a class="code" href="classCVC3_1_1ExprStream.html#acc3438cd65369ea0dad38ea59c93343a">00113</a> <span class="comment"></span> std::ostream* <a class="code" href="classCVC3_1_1ExprStream.html#acc3438cd65369ea0dad38ea59c93343a" title="The ostream to print into.">d_os</a>; <span class="comment">//!< The ostream to print into</span>
<a name="l00114"></a><a class="code" href="classCVC3_1_1ExprStream.html#a82d42f256f0775a3b4c9c3a4bed346d0">00114</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ExprStream.html#a82d42f256f0775a3b4c9c3a4bed346d0" title="Printing only upto this depth; -1 == unlimited.">d_depth</a>; <span class="comment">//!< Printing only upto this depth; -1 == unlimited</span>
<a name="l00115"></a><a class="code" href="classCVC3_1_1ExprStream.html#a83bf8b10c32e6a579ace151f35ce7e08">00115</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ExprStream.html#a83bf8b10c32e6a579ace151f35ce7e08" title="Current depth of Expr.">d_currDepth</a>; <span class="comment">//!< Current depth of Expr</span>
<a name="l00116"></a><a class="code" href="classCVC3_1_1ExprStream.html#a0db5c8c81be1cdcdeba4c2873572b519">00116</a> <span class="comment"></span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a> <a class="code" href="classCVC3_1_1ExprStream.html#a0db5c8c81be1cdcdeba4c2873572b519" title="Output language.">d_lang</a>; <span class="comment">//!< Output language</span>
<a name="l00117"></a><a class="code" href="classCVC3_1_1ExprStream.html#a376d7f29bf587b712bc9302ed27d8b77">00117</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprStream.html#a376d7f29bf587b712bc9302ed27d8b77" title="Whether to print with indentations.">d_indent</a>; <span class="comment">//!< Whether to print with indentations</span>
<a name="l00118"></a><a class="code" href="classCVC3_1_1ExprStream.html#a92f85002e3bc476e5879b9012ff4c2c9">00118</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ExprStream.html#a92f85002e3bc476e5879b9012ff4c2c9" title="Current column in a line.">d_col</a>; <span class="comment">//!< Current column in a line</span>
<a name="l00119"></a><a class="code" href="classCVC3_1_1ExprStream.html#aa954bdbaf953b6f059d2cd6252130095">00119</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ExprStream.html#aa954bdbaf953b6f059d2cd6252130095">d_lineWidth</a>; <span class="comment">//!< Try to format/indent for this line width</span>
<a name="l00120"></a>00120 <span class="comment"></span><span class="comment"> //! Indentation stack</span>
<a name="l00121"></a>00121 <span class="comment"></span><span class="comment"> /*! The user code can set the indentation to the current d_col by</span>
<a name="l00122"></a>00122 <span class="comment"> pushing the new value on the stack. This value is popped</span>
<a name="l00123"></a>00123 <span class="comment"> automatically when returning from the recursive call. */</span>
<a name="l00124"></a><a class="code" href="classCVC3_1_1ExprStream.html#a3141312e4ccf7ea7d15adf6af193a6db">00124</a> std::vector<int> <a class="code" href="classCVC3_1_1ExprStream.html#a3141312e4ccf7ea7d15adf6af193a6db" title="Indentation stack.">d_indentStack</a>;<span class="comment"></span>
<a name="l00125"></a>00125 <span class="comment"> //! The lowest position of the indent stack the user can pop</span>
<a name="l00126"></a><a class="code" href="classCVC3_1_1ExprStream.html#aa77050ac6ae56a6d4a45736e89521e0f">00126</a> <span class="comment"></span> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1ExprStream.html#aa77050ac6ae56a6d4a45736e89521e0f" title="The lowest position of the indent stack the user can pop.">d_indentLast</a>;<span class="comment"></span>
<a name="l00127"></a>00127 <span class="comment"> //! Indentation register for popSave() and pushRestore()</span>
<a name="l00128"></a><a class="code" href="classCVC3_1_1ExprStream.html#a6961d32e92cc350b1fd591888f037289">00128</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ExprStream.html#a6961d32e92cc350b1fd591888f037289" title="Indentation register for popSave() and pushRestore()">d_indentReg</a>;<span class="comment"></span>
<a name="l00129"></a>00129 <span class="comment"> //! Whether it is a beginning of line (for eating up extra spaces)</span>
<a name="l00130"></a><a class="code" href="classCVC3_1_1ExprStream.html#a0e9d4e03372235a23da6a965aa05f742">00130</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprStream.html#a0e9d4e03372235a23da6a965aa05f742" title="Whether it is a beginning of line (for eating up extra spaces)">d_beginningOfLine</a>;
<a name="l00131"></a><a class="code" href="classCVC3_1_1ExprStream.html#abc448835fcc31cd355c90606822ed42c">00131</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprStream.html#abc448835fcc31cd355c90606822ed42c">d_dag</a>; <span class="comment">//!< Print Expr as a DAG</span>
<a name="l00132"></a>00132 <span class="comment"></span><span class="comment"> //! Mapping subexpressions to names for DAG printing</span>
<a name="l00133"></a><a class="code" href="classCVC3_1_1ExprStream.html#a5613bd2f13161fe6846776dbb328bd34">00133</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::string></a> <a class="code" href="classCVC3_1_1ExprStream.html#a5613bd2f13161fe6846776dbb328bd34" title="Mapping subexpressions to names for DAG printing.">d_dagMap</a>;<span class="comment"></span>
<a name="l00134"></a>00134 <span class="comment"> //! New subexpressions not yet printed in a LET header</span>
<a name="l00135"></a><a class="code" href="classCVC3_1_1ExprStream.html#a8281aa65a9abe1cbbb3b1b43f9ab28c5">00135</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::string></a> <a class="code" href="classCVC3_1_1ExprStream.html#a8281aa65a9abe1cbbb3b1b43f9ab28c5" title="New subexpressions not yet printed in a LET header.">d_newDagMap</a>;<span class="comment"></span>
<a name="l00136"></a>00136 <span class="comment"> //! Stack of shared subexpressions (same as in d_dagMap)</span>
<a name="l00137"></a><a class="code" href="classCVC3_1_1ExprStream.html#ad1dc7ed42d81dd3de3a3ec4328c1d6c2">00137</a> <span class="comment"></span> std::vector<Expr> <a class="code" href="classCVC3_1_1ExprStream.html#ad1dc7ed42d81dd3de3a3ec4328c1d6c2" title="Stack of shared subexpressions (same as in d_dagMap)">d_dagStack</a>;<span class="comment"></span>
<a name="l00138"></a>00138 <span class="comment"> //! Stack of pointers to d_dagStack for pushing/popping shared subexprs</span>
<a name="l00139"></a><a class="code" href="classCVC3_1_1ExprStream.html#a78aa8e292d7555fdfb7a94c00c0b3a6f">00139</a> <span class="comment"></span> std::vector<size_t> <a class="code" href="classCVC3_1_1ExprStream.html#a78aa8e292d7555fdfb7a94c00c0b3a6f" title="Stack of pointers to d_dagStack for pushing/popping shared subexprs.">d_dagPtr</a>;<span class="comment"></span>
<a name="l00140"></a>00140 <span class="comment"> //! The smallest size of d_dagPtr the user can `popDag'</span>
<a name="l00141"></a><a class="code" href="classCVC3_1_1ExprStream.html#ae19d943560a35d7b9f4042a152420262">00141</a> <span class="comment"></span> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1ExprStream.html#ae19d943560a35d7b9f4042a152420262" title="The smallest size of d_dagPtr the user can `popDag'.">d_lastDagSize</a>;<span class="comment"></span>
<a name="l00142"></a>00142 <span class="comment"> //! Flag whether the dagMap is already built</span>
<a name="l00143"></a><a class="code" href="classCVC3_1_1ExprStream.html#a5fb7d3cacc87b22ea0ca79efd35a038f">00143</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprStream.html#a5fb7d3cacc87b22ea0ca79efd35a038f" title="Flag whether the dagMap is already built.">d_dagBuilt</a>;<span class="comment"></span>
<a name="l00144"></a>00144 <span class="comment"> //! Counter for generating unique LET var names</span>
<a name="l00145"></a><a class="code" href="classCVC3_1_1ExprStream.html#aa2a427ab0f2adc805cfd3cab42b8363a">00145</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ExprStream.html#aa2a427ab0f2adc805cfd3cab42b8363a" title="Counter for generating unique LET var names.">d_idCounter</a>;<span class="comment"></span>
<a name="l00146"></a>00146 <span class="comment"> //! nodag() manipulator has been applied</span>
<a name="l00147"></a><a class="code" href="classCVC3_1_1ExprStream.html#a00ed22d62da899833285f2bbf20754fd">00147</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprStream.html#a00ed22d62da899833285f2bbf20754fd" title="nodag() manipulator has been applied">d_nodag</a>;<span class="comment"></span>
<a name="l00148"></a>00148 <span class="comment"> //! Generating unique names in DAG expr</span>
<a name="l00149"></a>00149 <span class="comment"></span> std::string newName();<span class="comment"></span>
<a name="l00150"></a>00150 <span class="comment"> //! Traverse the Expr, collect shared subexpressions in d_dagMap</span>
<a name="l00151"></a>00151 <span class="comment"></span> <span class="keywordtype">void</span> collectShared(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a>& cache);<span class="comment"></span>
<a name="l00152"></a>00152 <span class="comment"> //! Wrap e into the top-level LET ... IN header from the dagMap</span>
<a name="l00153"></a>00153 <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> addLetHeader(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00154"></a>00154 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00155"></a>00155 <span class="comment"> //! Default constructor</span>
<a name="l00156"></a>00156 <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>(<a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a> *em);<span class="comment"></span>
<a name="l00157"></a>00157 <span class="comment"> //! Destructor</span>
<a name="l00158"></a><a class="code" href="classCVC3_1_1ExprStream.html#a2a945bdadc46720c472dc3bd75e4c250">00158</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprStream.html#a2a945bdadc46720c472dc3bd75e4c250" title="Destructor.">~ExprStream</a>() { }<span class="comment"></span>
<a name="l00159"></a>00159 <span class="comment"> //! Set a new output stream</span>
<a name="l00160"></a>00160 <span class="comment"></span><span class="comment"> /*! Note, that there is no method to access the ostream. This is</span>
<a name="l00161"></a>00161 <span class="comment"> done on purpose, so that DP designers had to use only ExprStream</span>
<a name="l00162"></a>00162 <span class="comment"> to print everything in their versions of Theory::print(). */</span>
<a name="l00163"></a><a class="code" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">00163</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512" title="Set a new output stream.">os</a>(std::ostream& os) { d_os = &<a class="code" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512" title="Set a new output stream.">os</a>; }<span class="comment"></span>
<a name="l00164"></a>00164 <span class="comment"> //! Get the current output language</span>
<a name="l00165"></a><a class="code" href="classCVC3_1_1ExprStream.html#ac2b2872228aff3fd5d08bbd69c672543">00165</a> <span class="comment"></span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a> <a class="code" href="classCVC3_1_1ExprStream.html#ac2b2872228aff3fd5d08bbd69c672543" title="Get the current output language.">lang</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_lang; }<span class="comment"></span>
<a name="l00166"></a>00166 <span class="comment"> //! Set the output language</span>
<a name="l00167"></a><a class="code" href="classCVC3_1_1ExprStream.html#af47217b350ebc0ba17f419d397165fe1">00167</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprStream.html#af47217b350ebc0ba17f419d397165fe1" title="Set the output language.">lang</a>(<a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a> l) { d_lang = l; }<span class="comment"></span>
<a name="l00168"></a>00168 <span class="comment"> //! Get the printing depth</span>
<a name="l00169"></a><a class="code" href="classCVC3_1_1ExprStream.html#a6ae01341aa0512bfad472ba3d68065a6">00169</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ExprStream.html#a6ae01341aa0512bfad472ba3d68065a6" title="Get the printing depth.">depth</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_depth; }<span class="comment"></span>
<a name="l00170"></a>00170 <span class="comment"> //! Set the printing depth</span>
<a name="l00171"></a><a class="code" href="classCVC3_1_1ExprStream.html#af49621de37fe228a2f7b3f2d372cea44">00171</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprStream.html#af49621de37fe228a2f7b3f2d372cea44" title="Set the printing depth.">depth</a>(<span class="keywordtype">int</span> d) { d_depth = d; }<span class="comment"></span>
<a name="l00172"></a>00172 <span class="comment"> //! Set the line width</span>
<a name="l00173"></a><a class="code" href="classCVC3_1_1ExprStream.html#ae408e31b8c24a7a808985f6874cd5059">00173</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprStream.html#ae408e31b8c24a7a808985f6874cd5059" title="Set the line width.">lineWidth</a>(<span class="keywordtype">int</span> w) { d_lineWidth = w; }<span class="comment"></span>
<a name="l00174"></a>00174 <span class="comment"> //! Set the DAG flag (return previous value)</span>
<a name="l00175"></a><a class="code" href="classCVC3_1_1ExprStream.html#a2d4ff13cb98b358eb02dfbf149ae03ae">00175</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprStream.html#a2d4ff13cb98b358eb02dfbf149ae03ae" title="Set the DAG flag (return previous value)">dagFlag</a>(<span class="keywordtype">bool</span> flag = <span class="keyword">true</span>) { <span class="keywordtype">bool</span> old = d_dag; d_dag = flag; <span class="keywordflow">return</span> old; }<span class="comment"></span>
<a name="l00176"></a>00176 <span class="comment"> //! Set the indentation to the current column</span>
<a name="l00177"></a>00177 <span class="comment"></span><span class="comment"> /*! The value will be restorted automatically after the DP print()</span>
<a name="l00178"></a>00178 <span class="comment"> function returns */</span>
<a name="l00179"></a><a class="code" href="classCVC3_1_1ExprStream.html#a92fe55e5f00f52ac00db56afcaaba80c">00179</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprStream.html#a92fe55e5f00f52ac00db56afcaaba80c" title="Set the indentation to the current column.">pushIndent</a>() { d_indentStack.push_back(d_col); }<span class="comment"></span>
<a name="l00180"></a>00180 <span class="comment"> //! Set the indentation to the given absolute position</span>
<a name="l00181"></a>00181 <span class="comment"></span><span class="comment"> /*! The value will be restorted automatically after the DP print()</span>
<a name="l00182"></a>00182 <span class="comment"> function returns */</span>
<a name="l00183"></a><a class="code" href="classCVC3_1_1ExprStream.html#a45fc9ca3545f65f62e6c255d2b108782">00183</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprStream.html#a45fc9ca3545f65f62e6c255d2b108782" title="Set the indentation to the given absolute position.">pushIndent</a>(<span class="keywordtype">int</span> pos) { d_indentStack.push_back(pos); }<span class="comment"></span>
<a name="l00184"></a>00184 <span class="comment"> //! Restore the indentation (user cannot pop more than pushed)</span>
<a name="l00185"></a>00185 <span class="comment"></span> <span class="keywordtype">void</span> popIndent();<span class="comment"></span>
<a name="l00186"></a>00186 <span class="comment"> //! Reset indentation to what it was at this level</span>
<a name="l00187"></a>00187 <span class="comment"></span> <span class="keywordtype">void</span> resetIndent();<span class="comment"></span>
<a name="l00188"></a>00188 <span class="comment"> //! Return the current column position</span>
<a name="l00189"></a><a class="code" href="classCVC3_1_1ExprStream.html#a1f3ea8ff58dfb9cab4471d157decfae5">00189</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ExprStream.html#a1f3ea8ff58dfb9cab4471d157decfae5" title="Return the current column position.">column</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_col; }<span class="comment"></span>
<a name="l00190"></a>00190 <span class="comment"> //! Recompute shared subexpression for the next Expr</span>
<a name="l00191"></a>00191 <span class="comment"></span> <span class="keywordtype">void</span> pushDag();<span class="comment"></span>
<a name="l00192"></a>00192 <span class="comment"> //! Delete shared subexpressions previously added with pushdag</span>
<a name="l00193"></a>00193 <span class="comment"></span> <span class="keywordtype">void</span> popDag();<span class="comment"></span>
<a name="l00194"></a>00194 <span class="comment"> //! Reset the DAG to what it was at this level</span>
<a name="l00195"></a>00195 <span class="comment"></span> <span class="keywordtype">void</span> resetDag();
<a name="l00196"></a>00196
<a name="l00197"></a>00197 <span class="comment">// The printing action</span>
<a name="l00198"></a>00198 <span class="comment"></span>
<a name="l00199"></a>00199 <span class="comment"> //! Use manipulators which are functions over ExprStream&</span>
<a name="l00200"></a>00200 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os,
<a name="l00201"></a>00201 <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& (*manip)(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>&));<span class="comment"></span>
<a name="l00202"></a>00202 <span class="comment"> //! Print Expr</span>
<a name="l00203"></a>00203 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span>
<a name="l00204"></a>00204 <span class="comment"> //! Print Type</span>
<a name="l00205"></a>00205 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t);<span class="comment"></span>
<a name="l00206"></a>00206 <span class="comment"> //! Print string</span>
<a name="l00207"></a>00207 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <span class="keyword">const</span> std::string& s);<span class="comment"></span>
<a name="l00208"></a>00208 <span class="comment"> //! Print char* string</span>
<a name="l00209"></a>00209 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <span class="keyword">const</span> <span class="keywordtype">char</span>* s);<span class="comment"></span>
<a name="l00210"></a>00210 <span class="comment"> //! Print Rational</span>
<a name="l00211"></a>00211 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& r);<span class="comment"></span>
<a name="l00212"></a>00212 <span class="comment"> //! Print int</span>
<a name="l00213"></a>00213 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <span class="keywordtype">int</span> i);
<a name="l00214"></a>00214 <span class="comment"></span>
<a name="l00215"></a>00215 <span class="comment"> //! Set the indentation to the current position</span>
<a name="l00216"></a>00216 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os);<span class="comment"></span>
<a name="l00217"></a>00217 <span class="comment"> //! Restore the indentation to the previous position</span>
<a name="l00218"></a>00218 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os);<span class="comment"></span>
<a name="l00219"></a>00219 <span class="comment"> //! Remember the current indentation and pop to the previous position</span>
<a name="l00220"></a>00220 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#gacf04af76c8233f27762ad6ebb73a58c0" title="Remember the current indentation and pop to the previous position.">popSave</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os);<span class="comment"></span>
<a name="l00221"></a>00221 <span class="comment"> //! Set the indentation to the position saved by popSave()</span>
<a name="l00222"></a>00222 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#ga7a2134042b4ae9b096b0003d8f3c869a" title="Set the indentation to the position saved by popSave()">pushRestore</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os);<span class="comment"></span>
<a name="l00223"></a>00223 <span class="comment"> //! Reset the indentation to the default at this level</span>
<a name="l00224"></a>00224 <span class="comment"></span> <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#ga90deb7348703ae1a59a11d9af77aa8ad" title="Reset the indentation to the default at this level.">reset</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os);<span class="comment"></span>
<a name="l00225"></a>00225 <span class="comment"> //! Insert a single white space separator</span>
<a name="l00226"></a>00226 <span class="comment"></span><span class="comment"> /*! It is preferred to use 'space' rather than a string of spaces</span>
<a name="l00227"></a>00227 <span class="comment"> (" ") because ExprStream needs to delete extra white space if it</span>
<a name="l00228"></a>00228 <span class="comment"> decides to end the line. If you use strings for spaces, you'll</span>
<a name="l00229"></a>00229 <span class="comment"> mess up the indentation. */</span>
<a name="l00230"></a>00230 <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os);<span class="comment"></span>
<a name="l00231"></a>00231 <span class="comment"> //! Print the next top-level expression node without DAG-ifying</span>
<a name="l00232"></a>00232 <span class="comment"></span><span class="comment"> /*! </span>
<a name="l00233"></a>00233 <span class="comment"> * DAG-printing will resume for the children of the node. This is</span>
<a name="l00234"></a>00234 <span class="comment"> * useful when printing definitions in the header of a DAGified</span>
<a name="l00235"></a>00235 <span class="comment"> * LET expressions: defs have names, but must be printed expanded.</span>
<a name="l00236"></a>00236 <span class="comment"> */</span>
<a name="l00237"></a>00237 <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#gab9909b3108229b630956179ebd71f3ef">nodag</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os);<span class="comment"></span>
<a name="l00238"></a>00238 <span class="comment"> //! Recompute shared subexpression for the next Expr</span>
<a name="l00239"></a>00239 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00240"></a>00240 <span class="comment"> * For some constructs with bound variables (notably,</span>
<a name="l00241"></a>00241 <span class="comment"> * quantifiers), shared subexpressions are not computed, because</span>
<a name="l00242"></a>00242 <span class="comment"> * they cannot be defined outside the scope of bound variables.</span>
<a name="l00243"></a>00243 <span class="comment"> * If this manipulator is applied before an expression within the</span>
<a name="l00244"></a>00244 <span class="comment"> * scope of bound vars, these internal subexpressions will then be</span>
<a name="l00245"></a>00245 <span class="comment"> * computed.</span>
<a name="l00246"></a>00246 <span class="comment"> */</span>
<a name="l00247"></a>00247 <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#ga1475185296de10fdbe07f0b498e8ed36">pushdag</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os);<span class="comment"></span>
<a name="l00248"></a>00248 <span class="comment"> //! Delete shared subexpressions previously added with pushdag</span>
<a name="l00249"></a>00249 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00250"></a>00250 <span class="comment"> * Similar to push/pop, shared subexpressions are automatically</span>
<a name="l00251"></a>00251 <span class="comment"> * deleted upon a return from a recursive call, so popdag is not</span>
<a name="l00252"></a>00252 <span class="comment"> * necessary after a pushdag in theory-specific print() functions.</span>
<a name="l00253"></a>00253 <span class="comment"> * Also, you cannot pop more than you pushed an the current</span>
<a name="l00254"></a>00254 <span class="comment"> * recursion level.</span>
<a name="l00255"></a>00255 <span class="comment"> */</span>
<a name="l00256"></a>00256 <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#ga07ae0c39b4082065891134536f2fa91c">popdag</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os);<span class="comment"></span>
<a name="l00257"></a>00257 <span class="comment"> //! Print the end-of-line</span>
<a name="l00258"></a>00258 <span class="comment"></span><span class="comment"> /*! The new line will not necessarily start at column 0 because of</span>
<a name="l00259"></a>00259 <span class="comment"> indentation. </span>
<a name="l00260"></a>00260 <span class="comment"> </span>
<a name="l00261"></a>00261 <span class="comment"> The name endl will be introduced in namespace std, otherwise</span>
<a name="l00262"></a>00262 <span class="comment"> CVC3::endl would overshadow std::endl, wreaking havoc...</span>
<a name="l00263"></a>00263 <span class="comment"> */</span>
<a name="l00264"></a>00264 <span class="keyword">friend</span> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">std::endl</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os);
<a name="l00265"></a>00265 }; <span class="comment">// end of class ExprStream</span>
<a name="l00266"></a>00266 <span class="comment"></span>
<a name="l00267"></a>00267 <span class="comment"> /*! @} */</span> <span class="comment">// End of group PrettyPrinting</span>
<a name="l00268"></a>00268
<a name="l00269"></a>00269 ExprStream& <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>(ExprStream& os);
<a name="l00270"></a>00270 ExprStream& <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>(ExprStream& os);
<a name="l00271"></a>00271 ExprStream& <a class="code" href="group__ExprStream__Manip.html#gacf04af76c8233f27762ad6ebb73a58c0" title="Remember the current indentation and pop to the previous position.">popSave</a>(ExprStream& os);
<a name="l00272"></a>00272 ExprStream& <a class="code" href="group__ExprStream__Manip.html#ga7a2134042b4ae9b096b0003d8f3c869a" title="Set the indentation to the position saved by popSave()">pushRestore</a>(ExprStream& os);
<a name="l00273"></a>00273 ExprStream& <a class="code" href="group__ExprStream__Manip.html#ga90deb7348703ae1a59a11d9af77aa8ad" title="Reset the indentation to the default at this level.">reset</a>(ExprStream& os);
<a name="l00274"></a>00274 ExprStream& <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a>(ExprStream& os);
<a name="l00275"></a>00275 ExprStream& <a class="code" href="group__ExprStream__Manip.html#gab9909b3108229b630956179ebd71f3ef">nodag</a>(ExprStream& os);
<a name="l00276"></a>00276 ExprStream& <a class="code" href="group__ExprStream__Manip.html#ga1475185296de10fdbe07f0b498e8ed36">pushdag</a>(ExprStream& os);
<a name="l00277"></a>00277 ExprStream& <a class="code" href="group__ExprStream__Manip.html#ga07ae0c39b4082065891134536f2fa91c">popdag</a>(ExprStream& os);
<a name="l00278"></a>00278
<a name="l00279"></a>00279
<a name="l00280"></a>00280 } <span class="comment">// End of namespace CVC3</span>
<a name="l00281"></a>00281
<a name="l00282"></a>00282 <span class="comment">/*</span>
<a name="l00283"></a>00283 <span class="comment">namespace std {</span>
<a name="l00284"></a>00284 <span class="comment"> CVC3::ExprStream& endl(CVC3::ExprStream& os);</span>
<a name="l00285"></a>00285 <span class="comment">}</span>
<a name="l00286"></a>00286 <span class="comment">*/</span>
<a name="l00287"></a>00287
<a name="l00288"></a>00288 <span class="preprocessor">#endif</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>
