<!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"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: CVC3::ExprStream Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<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 class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a></li><li class="navelem"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="#friends">Friends</a> |
<a href="classCVC3_1_1ExprStream-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::ExprStream Class Reference<div class="ingroups"><a class="el" href="group__PrettyPrinting.html">Pretty-printing related classes and methods</a></div></div> </div>
</div><!--header-->
<div class="contents">
<p>Pretty-printing output stream for <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. READ THE DOCS BEFORE USING!
<a href="classCVC3_1_1ExprStream.html#details">More...</a></p>
<p><code>#include <<a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>></code></p>
<div class="dynheader">
Collaboration diagram for CVC3::ExprStream:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1ExprStream__coll__graph.gif" border="0" usemap="#CVC3_1_1ExprStream_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1ExprStream_coll__map" id="CVC3_1_1ExprStream_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:a758b310ee5459a56722b13b0f18b297f"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a758b310ee5459a56722b13b0f18b297f">ExprStream</a> (<a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> *em)</td></tr>
<tr class="memdesc:a758b310ee5459a56722b13b0f18b297f"><td class="mdescLeft"> </td><td class="mdescRight">Default constructor. <a href="#a758b310ee5459a56722b13b0f18b297f"></a><br/></td></tr>
<tr class="separator:a758b310ee5459a56722b13b0f18b297f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2a945bdadc46720c472dc3bd75e4c250"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a2a945bdadc46720c472dc3bd75e4c250">~ExprStream</a> ()</td></tr>
<tr class="memdesc:a2a945bdadc46720c472dc3bd75e4c250"><td class="mdescLeft"> </td><td class="mdescRight">Destructor. <a href="#a2a945bdadc46720c472dc3bd75e4c250"></a><br/></td></tr>
<tr class="separator:a2a945bdadc46720c472dc3bd75e4c250"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8316bdcfb3ea96317ce9f8b4ebd16512"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a> (std::ostream &os)</td></tr>
<tr class="memdesc:a8316bdcfb3ea96317ce9f8b4ebd16512"><td class="mdescLeft"> </td><td class="mdescRight">Set a new output stream. <a href="#a8316bdcfb3ea96317ce9f8b4ebd16512"></a><br/></td></tr>
<tr class="separator:a8316bdcfb3ea96317ce9f8b4ebd16512"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac2b2872228aff3fd5d08bbd69c672543"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#ac2b2872228aff3fd5d08bbd69c672543">lang</a> () const </td></tr>
<tr class="memdesc:ac2b2872228aff3fd5d08bbd69c672543"><td class="mdescLeft"> </td><td class="mdescRight">Get the current output language. <a href="#ac2b2872228aff3fd5d08bbd69c672543"></a><br/></td></tr>
<tr class="separator:ac2b2872228aff3fd5d08bbd69c672543"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af47217b350ebc0ba17f419d397165fe1"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#af47217b350ebc0ba17f419d397165fe1">lang</a> (<a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> l)</td></tr>
<tr class="memdesc:af47217b350ebc0ba17f419d397165fe1"><td class="mdescLeft"> </td><td class="mdescRight">Set the output language. <a href="#af47217b350ebc0ba17f419d397165fe1"></a><br/></td></tr>
<tr class="separator:af47217b350ebc0ba17f419d397165fe1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6ae01341aa0512bfad472ba3d68065a6"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a6ae01341aa0512bfad472ba3d68065a6">depth</a> () const </td></tr>
<tr class="memdesc:a6ae01341aa0512bfad472ba3d68065a6"><td class="mdescLeft"> </td><td class="mdescRight">Get the printing depth. <a href="#a6ae01341aa0512bfad472ba3d68065a6"></a><br/></td></tr>
<tr class="separator:a6ae01341aa0512bfad472ba3d68065a6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af49621de37fe228a2f7b3f2d372cea44"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#af49621de37fe228a2f7b3f2d372cea44">depth</a> (int d)</td></tr>
<tr class="memdesc:af49621de37fe228a2f7b3f2d372cea44"><td class="mdescLeft"> </td><td class="mdescRight">Set the printing depth. <a href="#af49621de37fe228a2f7b3f2d372cea44"></a><br/></td></tr>
<tr class="separator:af49621de37fe228a2f7b3f2d372cea44"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae408e31b8c24a7a808985f6874cd5059"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#ae408e31b8c24a7a808985f6874cd5059">lineWidth</a> (int w)</td></tr>
<tr class="memdesc:ae408e31b8c24a7a808985f6874cd5059"><td class="mdescLeft"> </td><td class="mdescRight">Set the line width. <a href="#ae408e31b8c24a7a808985f6874cd5059"></a><br/></td></tr>
<tr class="separator:ae408e31b8c24a7a808985f6874cd5059"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2d4ff13cb98b358eb02dfbf149ae03ae"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a2d4ff13cb98b358eb02dfbf149ae03ae">dagFlag</a> (bool flag=true)</td></tr>
<tr class="memdesc:a2d4ff13cb98b358eb02dfbf149ae03ae"><td class="mdescLeft"> </td><td class="mdescRight">Set the DAG flag (return previous value) <a href="#a2d4ff13cb98b358eb02dfbf149ae03ae"></a><br/></td></tr>
<tr class="separator:a2d4ff13cb98b358eb02dfbf149ae03ae"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a92fe55e5f00f52ac00db56afcaaba80c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a92fe55e5f00f52ac00db56afcaaba80c">pushIndent</a> ()</td></tr>
<tr class="memdesc:a92fe55e5f00f52ac00db56afcaaba80c"><td class="mdescLeft"> </td><td class="mdescRight">Set the indentation to the current column. <a href="#a92fe55e5f00f52ac00db56afcaaba80c"></a><br/></td></tr>
<tr class="separator:a92fe55e5f00f52ac00db56afcaaba80c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a45fc9ca3545f65f62e6c255d2b108782"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a45fc9ca3545f65f62e6c255d2b108782">pushIndent</a> (int pos)</td></tr>
<tr class="memdesc:a45fc9ca3545f65f62e6c255d2b108782"><td class="mdescLeft"> </td><td class="mdescRight">Set the indentation to the given absolute position. <a href="#a45fc9ca3545f65f62e6c255d2b108782"></a><br/></td></tr>
<tr class="separator:a45fc9ca3545f65f62e6c255d2b108782"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a32a666cc0a71503770b88e3a7362808c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a32a666cc0a71503770b88e3a7362808c">popIndent</a> ()</td></tr>
<tr class="memdesc:a32a666cc0a71503770b88e3a7362808c"><td class="mdescLeft"> </td><td class="mdescRight">Restore the indentation (user cannot pop more than pushed) <a href="#a32a666cc0a71503770b88e3a7362808c"></a><br/></td></tr>
<tr class="separator:a32a666cc0a71503770b88e3a7362808c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a946110c3457868fe38ce8c1d4cdde916"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a946110c3457868fe38ce8c1d4cdde916">resetIndent</a> ()</td></tr>
<tr class="memdesc:a946110c3457868fe38ce8c1d4cdde916"><td class="mdescLeft"> </td><td class="mdescRight">Reset indentation to what it was at this level. <a href="#a946110c3457868fe38ce8c1d4cdde916"></a><br/></td></tr>
<tr class="separator:a946110c3457868fe38ce8c1d4cdde916"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1f3ea8ff58dfb9cab4471d157decfae5"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a1f3ea8ff58dfb9cab4471d157decfae5">column</a> () const </td></tr>
<tr class="memdesc:a1f3ea8ff58dfb9cab4471d157decfae5"><td class="mdescLeft"> </td><td class="mdescRight">Return the current column position. <a href="#a1f3ea8ff58dfb9cab4471d157decfae5"></a><br/></td></tr>
<tr class="separator:a1f3ea8ff58dfb9cab4471d157decfae5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2c93d862ed9b3cb1480a1d12cb510841"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a2c93d862ed9b3cb1480a1d12cb510841">pushDag</a> ()</td></tr>
<tr class="memdesc:a2c93d862ed9b3cb1480a1d12cb510841"><td class="mdescLeft"> </td><td class="mdescRight">Recompute shared subexpression for the next <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="#a2c93d862ed9b3cb1480a1d12cb510841"></a><br/></td></tr>
<tr class="separator:a2c93d862ed9b3cb1480a1d12cb510841"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7d1aa8566189d9b03a12bc56d3514979"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a7d1aa8566189d9b03a12bc56d3514979">popDag</a> ()</td></tr>
<tr class="memdesc:a7d1aa8566189d9b03a12bc56d3514979"><td class="mdescLeft"> </td><td class="mdescRight">Delete shared subexpressions previously added with pushdag. <a href="#a7d1aa8566189d9b03a12bc56d3514979"></a><br/></td></tr>
<tr class="separator:a7d1aa8566189d9b03a12bc56d3514979"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a004714bd282bfa11595d21bce94e72ec"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a004714bd282bfa11595d21bce94e72ec">resetDag</a> ()</td></tr>
<tr class="memdesc:a004714bd282bfa11595d21bce94e72ec"><td class="mdescLeft"> </td><td class="mdescRight">Reset the DAG to what it was at this level. <a href="#a004714bd282bfa11595d21bce94e72ec"></a><br/></td></tr>
<tr class="separator:a004714bd282bfa11595d21bce94e72ec"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-methods"></a>
Private Member Functions</h2></td></tr>
<tr class="memitem:a1c0a58ef36e93c45d8ee3e7cf58b604b"><td class="memItemLeft" align="right" valign="top">std::string </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a1c0a58ef36e93c45d8ee3e7cf58b604b">newName</a> ()</td></tr>
<tr class="memdesc:a1c0a58ef36e93c45d8ee3e7cf58b604b"><td class="mdescLeft"> </td><td class="mdescRight">Generating unique names in DAG expr. <a href="#a1c0a58ef36e93c45d8ee3e7cf58b604b"></a><br/></td></tr>
<tr class="separator:a1c0a58ef36e93c45d8ee3e7cf58b604b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a26a9afb803961536e2b0f74be900300f"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a26a9afb803961536e2b0f74be900300f">collectShared</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > &cache)</td></tr>
<tr class="memdesc:a26a9afb803961536e2b0f74be900300f"><td class="mdescLeft"> </td><td class="mdescRight">Traverse the <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>, collect shared subexpressions in d_dagMap. <a href="#a26a9afb803961536e2b0f74be900300f"></a><br/></td></tr>
<tr class="separator:a26a9afb803961536e2b0f74be900300f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a44b1833a153b0ecaa46616c557039dd8"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a44b1833a153b0ecaa46616c557039dd8">addLetHeader</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:a44b1833a153b0ecaa46616c557039dd8"><td class="mdescLeft"> </td><td class="mdescRight">Wrap e into the top-level LET ... IN header from the dagMap. <a href="#a44b1833a153b0ecaa46616c557039dd8"></a><br/></td></tr>
<tr class="separator:a44b1833a153b0ecaa46616c557039dd8"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-attribs"></a>
Private Attributes</h2></td></tr>
<tr class="memitem:a7ab1b6602b49bf13867877bf5f7a5873"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a7ab1b6602b49bf13867877bf5f7a5873">d_em</a></td></tr>
<tr class="memdesc:a7ab1b6602b49bf13867877bf5f7a5873"><td class="mdescLeft"> </td><td class="mdescRight">The <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> to use. <a href="#a7ab1b6602b49bf13867877bf5f7a5873"></a><br/></td></tr>
<tr class="separator:a7ab1b6602b49bf13867877bf5f7a5873"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acc3438cd65369ea0dad38ea59c93343a"><td class="memItemLeft" align="right" valign="top">std::ostream * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#acc3438cd65369ea0dad38ea59c93343a">d_os</a></td></tr>
<tr class="memdesc:acc3438cd65369ea0dad38ea59c93343a"><td class="mdescLeft"> </td><td class="mdescRight">The ostream to print into. <a href="#acc3438cd65369ea0dad38ea59c93343a"></a><br/></td></tr>
<tr class="separator:acc3438cd65369ea0dad38ea59c93343a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a82d42f256f0775a3b4c9c3a4bed346d0"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a82d42f256f0775a3b4c9c3a4bed346d0">d_depth</a></td></tr>
<tr class="memdesc:a82d42f256f0775a3b4c9c3a4bed346d0"><td class="mdescLeft"> </td><td class="mdescRight">Printing only upto this depth; -1 == unlimited. <a href="#a82d42f256f0775a3b4c9c3a4bed346d0"></a><br/></td></tr>
<tr class="separator:a82d42f256f0775a3b4c9c3a4bed346d0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a83bf8b10c32e6a579ace151f35ce7e08"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a83bf8b10c32e6a579ace151f35ce7e08">d_currDepth</a></td></tr>
<tr class="memdesc:a83bf8b10c32e6a579ace151f35ce7e08"><td class="mdescLeft"> </td><td class="mdescRight">Current depth of <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="#a83bf8b10c32e6a579ace151f35ce7e08"></a><br/></td></tr>
<tr class="separator:a83bf8b10c32e6a579ace151f35ce7e08"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0db5c8c81be1cdcdeba4c2873572b519"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a0db5c8c81be1cdcdeba4c2873572b519">d_lang</a></td></tr>
<tr class="memdesc:a0db5c8c81be1cdcdeba4c2873572b519"><td class="mdescLeft"> </td><td class="mdescRight">Output language. <a href="#a0db5c8c81be1cdcdeba4c2873572b519"></a><br/></td></tr>
<tr class="separator:a0db5c8c81be1cdcdeba4c2873572b519"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a376d7f29bf587b712bc9302ed27d8b77"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a376d7f29bf587b712bc9302ed27d8b77">d_indent</a></td></tr>
<tr class="memdesc:a376d7f29bf587b712bc9302ed27d8b77"><td class="mdescLeft"> </td><td class="mdescRight">Whether to print with indentations. <a href="#a376d7f29bf587b712bc9302ed27d8b77"></a><br/></td></tr>
<tr class="separator:a376d7f29bf587b712bc9302ed27d8b77"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a92f85002e3bc476e5879b9012ff4c2c9"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a92f85002e3bc476e5879b9012ff4c2c9">d_col</a></td></tr>
<tr class="memdesc:a92f85002e3bc476e5879b9012ff4c2c9"><td class="mdescLeft"> </td><td class="mdescRight">Current column in a line. <a href="#a92f85002e3bc476e5879b9012ff4c2c9"></a><br/></td></tr>
<tr class="separator:a92f85002e3bc476e5879b9012ff4c2c9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa954bdbaf953b6f059d2cd6252130095"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#aa954bdbaf953b6f059d2cd6252130095">d_lineWidth</a></td></tr>
<tr class="separator:aa954bdbaf953b6f059d2cd6252130095"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3141312e4ccf7ea7d15adf6af193a6db"><td class="memItemLeft" align="right" valign="top">std::vector< int > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a3141312e4ccf7ea7d15adf6af193a6db">d_indentStack</a></td></tr>
<tr class="memdesc:a3141312e4ccf7ea7d15adf6af193a6db"><td class="mdescLeft"> </td><td class="mdescRight">Indentation stack. <a href="#a3141312e4ccf7ea7d15adf6af193a6db"></a><br/></td></tr>
<tr class="separator:a3141312e4ccf7ea7d15adf6af193a6db"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa77050ac6ae56a6d4a45736e89521e0f"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#aa77050ac6ae56a6d4a45736e89521e0f">d_indentLast</a></td></tr>
<tr class="memdesc:aa77050ac6ae56a6d4a45736e89521e0f"><td class="mdescLeft"> </td><td class="mdescRight">The lowest position of the indent stack the user can pop. <a href="#aa77050ac6ae56a6d4a45736e89521e0f"></a><br/></td></tr>
<tr class="separator:aa77050ac6ae56a6d4a45736e89521e0f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6961d32e92cc350b1fd591888f037289"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a6961d32e92cc350b1fd591888f037289">d_indentReg</a></td></tr>
<tr class="memdesc:a6961d32e92cc350b1fd591888f037289"><td class="mdescLeft"> </td><td class="mdescRight">Indentation register for <a class="el" href="classCVC3_1_1ExprStream.html#adfda971d718f84fccfd2118f4a2e13ac" title="Remember the current indentation and pop to the previous position.">popSave()</a> and <a class="el" href="classCVC3_1_1ExprStream.html#a97553d34943597156f6a9b4f382cf05f" title="Set the indentation to the position saved by popSave()">pushRestore()</a> <a href="#a6961d32e92cc350b1fd591888f037289"></a><br/></td></tr>
<tr class="separator:a6961d32e92cc350b1fd591888f037289"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0e9d4e03372235a23da6a965aa05f742"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a0e9d4e03372235a23da6a965aa05f742">d_beginningOfLine</a></td></tr>
<tr class="memdesc:a0e9d4e03372235a23da6a965aa05f742"><td class="mdescLeft"> </td><td class="mdescRight">Whether it is a beginning of line (for eating up extra spaces) <a href="#a0e9d4e03372235a23da6a965aa05f742"></a><br/></td></tr>
<tr class="separator:a0e9d4e03372235a23da6a965aa05f742"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:abc448835fcc31cd355c90606822ed42c"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#abc448835fcc31cd355c90606822ed42c">d_dag</a></td></tr>
<tr class="separator:abc448835fcc31cd355c90606822ed42c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5613bd2f13161fe6846776dbb328bd34"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< std::string > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a5613bd2f13161fe6846776dbb328bd34">d_dagMap</a></td></tr>
<tr class="memdesc:a5613bd2f13161fe6846776dbb328bd34"><td class="mdescLeft"> </td><td class="mdescRight">Mapping subexpressions to names for DAG printing. <a href="#a5613bd2f13161fe6846776dbb328bd34"></a><br/></td></tr>
<tr class="separator:a5613bd2f13161fe6846776dbb328bd34"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8281aa65a9abe1cbbb3b1b43f9ab28c5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< std::string > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a8281aa65a9abe1cbbb3b1b43f9ab28c5">d_newDagMap</a></td></tr>
<tr class="memdesc:a8281aa65a9abe1cbbb3b1b43f9ab28c5"><td class="mdescLeft"> </td><td class="mdescRight">New subexpressions not yet printed in a LET header. <a href="#a8281aa65a9abe1cbbb3b1b43f9ab28c5"></a><br/></td></tr>
<tr class="separator:a8281aa65a9abe1cbbb3b1b43f9ab28c5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad1dc7ed42d81dd3de3a3ec4328c1d6c2"><td class="memItemLeft" align="right" valign="top">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#ad1dc7ed42d81dd3de3a3ec4328c1d6c2">d_dagStack</a></td></tr>
<tr class="memdesc:ad1dc7ed42d81dd3de3a3ec4328c1d6c2"><td class="mdescLeft"> </td><td class="mdescRight">Stack of shared subexpressions (same as in d_dagMap) <a href="#ad1dc7ed42d81dd3de3a3ec4328c1d6c2"></a><br/></td></tr>
<tr class="separator:ad1dc7ed42d81dd3de3a3ec4328c1d6c2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a78aa8e292d7555fdfb7a94c00c0b3a6f"><td class="memItemLeft" align="right" valign="top">std::vector< size_t > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a78aa8e292d7555fdfb7a94c00c0b3a6f">d_dagPtr</a></td></tr>
<tr class="memdesc:a78aa8e292d7555fdfb7a94c00c0b3a6f"><td class="mdescLeft"> </td><td class="mdescRight">Stack of pointers to d_dagStack for pushing/popping shared subexprs. <a href="#a78aa8e292d7555fdfb7a94c00c0b3a6f"></a><br/></td></tr>
<tr class="separator:a78aa8e292d7555fdfb7a94c00c0b3a6f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae19d943560a35d7b9f4042a152420262"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#ae19d943560a35d7b9f4042a152420262">d_lastDagSize</a></td></tr>
<tr class="memdesc:ae19d943560a35d7b9f4042a152420262"><td class="mdescLeft"> </td><td class="mdescRight">The smallest size of d_dagPtr the user can `popDag'. <a href="#ae19d943560a35d7b9f4042a152420262"></a><br/></td></tr>
<tr class="separator:ae19d943560a35d7b9f4042a152420262"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5fb7d3cacc87b22ea0ca79efd35a038f"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a5fb7d3cacc87b22ea0ca79efd35a038f">d_dagBuilt</a></td></tr>
<tr class="memdesc:a5fb7d3cacc87b22ea0ca79efd35a038f"><td class="mdescLeft"> </td><td class="mdescRight">Flag whether the dagMap is already built. <a href="#a5fb7d3cacc87b22ea0ca79efd35a038f"></a><br/></td></tr>
<tr class="separator:a5fb7d3cacc87b22ea0ca79efd35a038f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa2a427ab0f2adc805cfd3cab42b8363a"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#aa2a427ab0f2adc805cfd3cab42b8363a">d_idCounter</a></td></tr>
<tr class="memdesc:aa2a427ab0f2adc805cfd3cab42b8363a"><td class="mdescLeft"> </td><td class="mdescRight">Counter for generating unique LET var names. <a href="#aa2a427ab0f2adc805cfd3cab42b8363a"></a><br/></td></tr>
<tr class="separator:aa2a427ab0f2adc805cfd3cab42b8363a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a00ed22d62da899833285f2bbf20754fd"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a00ed22d62da899833285f2bbf20754fd">d_nodag</a></td></tr>
<tr class="memdesc:a00ed22d62da899833285f2bbf20754fd"><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classCVC3_1_1ExprStream.html#a6b0ee540ac9fd476d22ce316a6c9f78d" title="Print the next top-level expression node without DAG-ifying.">nodag()</a> manipulator has been applied <a href="#a00ed22d62da899833285f2bbf20754fd"></a><br/></td></tr>
<tr class="separator:a00ed22d62da899833285f2bbf20754fd"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="friends"></a>
Friends</h2></td></tr>
<tr class="memitem:a2bb78121744c58b0fe429be690099af5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a2bb78121744c58b0fe429be690099af5">operator<<</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>, <a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &(*manip)(<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &))</td></tr>
<tr class="memdesc:a2bb78121744c58b0fe429be690099af5"><td class="mdescLeft"> </td><td class="mdescRight">Use manipulators which are functions over <a class="el" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>&. <a href="#a2bb78121744c58b0fe429be690099af5"></a><br/></td></tr>
<tr class="separator:a2bb78121744c58b0fe429be690099af5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afe31e05cdc0aeb97284d664bfb31afb4"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#afe31e05cdc0aeb97284d664bfb31afb4">operator<<</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:afe31e05cdc0aeb97284d664bfb31afb4"><td class="mdescLeft"> </td><td class="mdescRight">Print <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="#afe31e05cdc0aeb97284d664bfb31afb4"></a><br/></td></tr>
<tr class="separator:afe31e05cdc0aeb97284d664bfb31afb4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aefb83c75e89a7c782e89f485b20bdc74"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#aefb83c75e89a7c782e89f485b20bdc74">operator<<</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>, const <a class="el" href="classCVC3_1_1Type.html">Type</a> &t)</td></tr>
<tr class="memdesc:aefb83c75e89a7c782e89f485b20bdc74"><td class="mdescLeft"> </td><td class="mdescRight">Print <a class="el" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>. <a href="#aefb83c75e89a7c782e89f485b20bdc74"></a><br/></td></tr>
<tr class="separator:aefb83c75e89a7c782e89f485b20bdc74"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac80c6017f4685dddc8c43de3bf72c8f0"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#ac80c6017f4685dddc8c43de3bf72c8f0">operator<<</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>, const std::string &s)</td></tr>
<tr class="memdesc:ac80c6017f4685dddc8c43de3bf72c8f0"><td class="mdescLeft"> </td><td class="mdescRight">Print string. <a href="#ac80c6017f4685dddc8c43de3bf72c8f0"></a><br/></td></tr>
<tr class="separator:ac80c6017f4685dddc8c43de3bf72c8f0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7b3d2ea716f32a02bcbaad87185a620d"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a7b3d2ea716f32a02bcbaad87185a620d">operator<<</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>, const char *s)</td></tr>
<tr class="memdesc:a7b3d2ea716f32a02bcbaad87185a620d"><td class="mdescLeft"> </td><td class="mdescRight">Print char* string. <a href="#a7b3d2ea716f32a02bcbaad87185a620d"></a><br/></td></tr>
<tr class="separator:a7b3d2ea716f32a02bcbaad87185a620d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afc67d7be0ed3251f85bec17aefda9be9"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#afc67d7be0ed3251f85bec17aefda9be9">operator<<</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>, const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> &r)</td></tr>
<tr class="memdesc:afc67d7be0ed3251f85bec17aefda9be9"><td class="mdescLeft"> </td><td class="mdescRight">Print <a class="el" href="classCVC3_1_1Rational.html">Rational</a>. <a href="#afc67d7be0ed3251f85bec17aefda9be9"></a><br/></td></tr>
<tr class="separator:afc67d7be0ed3251f85bec17aefda9be9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab83e67a05d087196ac378d13a7d3cac6"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#ab83e67a05d087196ac378d13a7d3cac6">operator<<</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>, int i)</td></tr>
<tr class="memdesc:ab83e67a05d087196ac378d13a7d3cac6"><td class="mdescLeft"> </td><td class="mdescRight">Print int. <a href="#ab83e67a05d087196ac378d13a7d3cac6"></a><br/></td></tr>
<tr class="separator:ab83e67a05d087196ac378d13a7d3cac6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a02863edb9e23b394e5011f63149ea443"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a02863edb9e23b394e5011f63149ea443">push</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>)</td></tr>
<tr class="memdesc:a02863edb9e23b394e5011f63149ea443"><td class="mdescLeft"> </td><td class="mdescRight">Set the indentation to the current position. <a href="#a02863edb9e23b394e5011f63149ea443"></a><br/></td></tr>
<tr class="separator:a02863edb9e23b394e5011f63149ea443"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa82375e98a075cd85eb04f957b01f3d1"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#aa82375e98a075cd85eb04f957b01f3d1">pop</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>)</td></tr>
<tr class="memdesc:aa82375e98a075cd85eb04f957b01f3d1"><td class="mdescLeft"> </td><td class="mdescRight">Restore the indentation to the previous position. <a href="#aa82375e98a075cd85eb04f957b01f3d1"></a><br/></td></tr>
<tr class="separator:aa82375e98a075cd85eb04f957b01f3d1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adfda971d718f84fccfd2118f4a2e13ac"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#adfda971d718f84fccfd2118f4a2e13ac">popSave</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>)</td></tr>
<tr class="memdesc:adfda971d718f84fccfd2118f4a2e13ac"><td class="mdescLeft"> </td><td class="mdescRight">Remember the current indentation and pop to the previous position. <a href="#adfda971d718f84fccfd2118f4a2e13ac"></a><br/></td></tr>
<tr class="separator:adfda971d718f84fccfd2118f4a2e13ac"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a97553d34943597156f6a9b4f382cf05f"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a97553d34943597156f6a9b4f382cf05f">pushRestore</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>)</td></tr>
<tr class="memdesc:a97553d34943597156f6a9b4f382cf05f"><td class="mdescLeft"> </td><td class="mdescRight">Set the indentation to the position saved by <a class="el" href="classCVC3_1_1ExprStream.html#adfda971d718f84fccfd2118f4a2e13ac" title="Remember the current indentation and pop to the previous position.">popSave()</a> <a href="#a97553d34943597156f6a9b4f382cf05f"></a><br/></td></tr>
<tr class="separator:a97553d34943597156f6a9b4f382cf05f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a49c83f6df078882e63f7834f2d31b6bc"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a49c83f6df078882e63f7834f2d31b6bc">reset</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>)</td></tr>
<tr class="memdesc:a49c83f6df078882e63f7834f2d31b6bc"><td class="mdescLeft"> </td><td class="mdescRight">Reset the indentation to the default at this level. <a href="#a49c83f6df078882e63f7834f2d31b6bc"></a><br/></td></tr>
<tr class="separator:a49c83f6df078882e63f7834f2d31b6bc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a09fb109b45779eeaa0d0d64c2ab46c6f"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a09fb109b45779eeaa0d0d64c2ab46c6f">space</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>)</td></tr>
<tr class="memdesc:a09fb109b45779eeaa0d0d64c2ab46c6f"><td class="mdescLeft"> </td><td class="mdescRight">Insert a single white space separator. <a href="#a09fb109b45779eeaa0d0d64c2ab46c6f"></a><br/></td></tr>
<tr class="separator:a09fb109b45779eeaa0d0d64c2ab46c6f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6b0ee540ac9fd476d22ce316a6c9f78d"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a6b0ee540ac9fd476d22ce316a6c9f78d">nodag</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>)</td></tr>
<tr class="memdesc:a6b0ee540ac9fd476d22ce316a6c9f78d"><td class="mdescLeft"> </td><td class="mdescRight">Print the next top-level expression node without DAG-ifying. <a href="#a6b0ee540ac9fd476d22ce316a6c9f78d"></a><br/></td></tr>
<tr class="separator:a6b0ee540ac9fd476d22ce316a6c9f78d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adaa3f23e99a706464a4842bb872b93a3"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#adaa3f23e99a706464a4842bb872b93a3">pushdag</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>)</td></tr>
<tr class="memdesc:adaa3f23e99a706464a4842bb872b93a3"><td class="mdescLeft"> </td><td class="mdescRight">Recompute shared subexpression for the next <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="#adaa3f23e99a706464a4842bb872b93a3"></a><br/></td></tr>
<tr class="separator:adaa3f23e99a706464a4842bb872b93a3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7a602f53a7718623252748882eb4886b"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#a7a602f53a7718623252748882eb4886b">popdag</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>)</td></tr>
<tr class="memdesc:a7a602f53a7718623252748882eb4886b"><td class="mdescLeft"> </td><td class="mdescRight">Delete shared subexpressions previously added with pushdag. <a href="#a7a602f53a7718623252748882eb4886b"></a><br/></td></tr>
<tr class="separator:a7a602f53a7718623252748882eb4886b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aaedf4f2798091833629c6465bfd360b7"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprStream.html#aaedf4f2798091833629c6465bfd360b7">std::endl</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &<a class="el" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512">os</a>)</td></tr>
<tr class="memdesc:aaedf4f2798091833629c6465bfd360b7"><td class="mdescLeft"> </td><td class="mdescRight">Print the end-of-line. <a href="#aaedf4f2798091833629c6465bfd360b7"></a><br/></td></tr>
<tr class="separator:aaedf4f2798091833629c6465bfd360b7"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock"><p>Pretty-printing output stream for <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. READ THE DOCS BEFORE USING! </p>
<p>Use this class as a standard ostream for <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>, string, int, <a class="el" href="classCVC3_1_1Rational.html">Rational</a>, manipulators like endl, and it will do the expected thing. Additionally, it has methods to access the current printing flags.</p>
<p>In order for the indentation engine to work correctly, you must use the manipulators properly.</p>
<p>Never use "\\n" in a string; always use endl manipulator, which knows about indentation and will do the right thing.</p>
<p>Always assume that the object you are printing may start printing on a new line from the current indentation position. Therefore, no string should start with an empty space (otherwise parts of your expression will be mis-indented). If you need a white space separator, or an operator surrounded by spaces, like os << " = ", use os << space << "= " instead. The 'space' manipulator adds one white space only if it's not at the beginning of a newly indented line. Think of it as a logical white-space separator with intelligent behavior, rather than a stupid hard space like " ".</p>
<p>Indentation can be set to the current position with os << push, and restored to the previous with os << pop. You do not need to restore it before exiting your print function, <a class="el" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> knows how to restore it automatically. For example, you can write:</p>
<p>os << "(" << push << e[0] << space << "+ " << e[1] << push << ")";</p>
<p>to print (PLUS a b) as "(a + b)". Notice the second 'push' before the closing paren. This is intentional (not a typo), and prevents the paren ")" from jumping to the next line by itself. <a class="el" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> will not go to the next line if the current position is too close to the indentation, since this will not give the expression a better look.</p>
<p>The indentation level is not restored in this example, and that is fine, <a class="el" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> will take care of that.</p>
<p>For complex expressions like IF-THEN-ELSE, you may want to remember the indentation to which you want to return later. You can save the current indentation position with os << popSave, and restore it later with os << pushRestore. These manipulators are similar to pop and push, but 'pushRestore' will set the new indentation level to the one popped by the last popSave instead of the current one. At the moment, there is only one register for saving an indentation position, so multiple pushRestore will not work as you would expect (maybe this should be fixed?..).</p>
<p>For concrete examples, see <a class="el" href="classCVC3_1_1TheoryCore.html#ab334f07590ad297ad6daa3383c61de5f" title="Theory-specific pretty-printing.">TheoryCore::print()</a> and <a class="el" href="classCVC3_1_1TheoryArith.html#a879d4967986103b989d7003dd815783f" title="Theory-specific pretty-printing.">TheoryArith::print()</a>. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00110">110</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a758b310ee5459a56722b13b0f18b297f"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::ExprStream::ExprStream </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * </td>
<td class="paramname"><em>em</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Default constructor. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00029">29</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8h_source.html#l00139">d_dagPtr</a>, <a class="el" href="expr__stream_8h_source.html#l00112">d_em</a>, <a class="el" href="expr__stream_8h_source.html#l00126">d_indentLast</a>, <a class="el" href="expr__stream_8h_source.html#l00124">d_indentStack</a>, <a class="el" href="expr__stream_8h_source.html#l00141">d_lastDagSize</a>, and <a class="el" href="expr__manager_8h_source.html#l00354">CVC3::ExprManager::indent()</a>.</p>
</div>
</div>
<a class="anchor" id="a2a945bdadc46720c472dc3bd75e4c250"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::ExprStream::~ExprStream </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Destructor. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00158">158</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="a1c0a58ef36e93c45d8ee3e7cf58b604b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">string CVC3::ExprStream::newName </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Generating unique names in DAG expr. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00043">43</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8h_source.html#l00145">d_idCounter</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00054">collectShared()</a>.</p>
</div>
</div>
<a class="anchor" id="a26a9afb803961536e2b0f74be900300f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::collectShared </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > & </td>
<td class="paramname"><em>cache</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Traverse the <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>, collect shared subexpressions in d_dagMap. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00054">54</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="expr__map_8h_source.html#l00173">CVC3::ExprMap< Data >::count()</a>, <a class="el" href="expr__stream_8h_source.html#l00143">d_dagBuilt</a>, <a class="el" href="expr__stream_8h_source.html#l00133">d_dagMap</a>, <a class="el" href="expr__stream_8h_source.html#l00137">d_dagStack</a>, <a class="el" href="expr__stream_8h_source.html#l00116">d_lang</a>, <a class="el" href="expr__stream_8h_source.html#l00135">d_newDagMap</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00049">CVC3::isTrivialExpr()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00043">newName()</a>, <a class="el" href="lang_8h_source.html#l00034">CVC3::SMTLIB_LANG</a>, <a class="el" href="lang_8h_source.html#l00052">CVC3::SMTLIB_V2_LANG</a>, <a class="el" href="cvc__util_8h_source.html#l00030">CVC3::to_upper()</a>, and <a class="el" href="lang_8h_source.html#l00046">CVC3::TPTP_LANG</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a44b1833a153b0ecaa46616c557039dd8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> CVC3::ExprStream::addLetHeader </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Wrap e into the top-level LET ... IN header from the dagMap. </p>
<p>We rely on the fact that d_dagMap is ordered by the <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> creation order, so earlier expressions cannot depend on later ones. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00093">93</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
<p>References <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="expr__map_8h_source.html#l00175">CVC3::ExprMap< Data >::clear()</a>, <a class="el" href="expr__stream_8h_source.html#l00135">d_newDagMap</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr_8h_source.html#l01156">CVC3::Expr::getEM()</a>, <a class="el" href="kinds_8h_source.html#l00225">LET</a>, <a class="el" href="kinds_8h_source.html#l00227">LETDECL</a>, <a class="el" href="kinds_8h_source.html#l00226">LETDECLS</a>, <a class="el" href="expr__manager_8h_source.html#l00454">CVC3::ExprManager::newLeafExpr()</a>, <a class="el" href="expr__manager_8h_source.html#l00478">CVC3::ExprManager::newVarExpr()</a>, <a class="el" href="expr__map_8h_source.html#l00171">CVC3::ExprMap< Data >::size()</a>, and <a class="el" href="kinds_8h_source.html#l00053">TYPE</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a8316bdcfb3ea96317ce9f8b4ebd16512"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::os </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set a new output stream. </p>
<p>Note, that there is no method to access the ostream. This is done on purpose, so that DP designers had to use only <a class="el" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> to print everything in their versions of <a class="el" href="group__Theory__API.html#ga49009744d64bbc47785f3fc5fa6884ca" title="Theory-specific pretty-printing.">Theory::print()</a>. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00163">163</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>References <a class="el" href="expr__stream_8h_source.html#l00163">os()</a>.</p>
<p>Referenced by <a class="el" href="expr_8cpp_source.html#l00621">CVC3::operator<<()</a>, <a class="el" href="expr__stream_8h_source.html#l00163">os()</a>, and <a class="el" href="expr_8cpp_source.html#l00352">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="ac2b2872228aff3fd5d08bbd69c672543"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> CVC3::ExprStream::lang </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get the current output language. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00165">165</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="theory__simulate_8cpp_source.html#l00215">CVC3::TheorySimulate::print()</a>, <a class="el" href="theory__records_8cpp_source.html#l00584">CVC3::TheoryRecords::print()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00700">CVC3::TheoryUF::print()</a>, <a class="el" href="theory__array_8cpp_source.html#l01072">CVC3::TheoryArray::print()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00639">CVC3::TheoryDatatype::print()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l02150">CVC3::TheoryArithNew::print()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03662">CVC3::TheoryBitvector::print()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02966">CVC3::TheoryArith3::print()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03952">CVC3::TheoryArithOld::print()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="expr_8cpp_source.html#l00362">CVC3::Expr::print()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08729">CVC3::TheoryQuant::print()</a>, <a class="el" href="theory__arith_8cpp_source.html#l00054">CVC3::TheoryArith::printRational()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00657">CVC3::TheoryUF::printSmtLibShared()</a>, <a class="el" href="theory__core_8cpp_source.html#l01915">CVC3::TheoryCore::printSmtLibShared()</a>, and <a class="el" href="expr_8cpp_source.html#l00352">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="af47217b350ebc0ba17f419d397165fe1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::lang </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> </td>
<td class="paramname"><em>l</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set the output language. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00167">167</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
</div>
</div>
<a class="anchor" id="a6ae01341aa0512bfad472ba3d68065a6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprStream::depth </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get the printing depth. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00169">169</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
</div>
</div>
<a class="anchor" id="af49621de37fe228a2f7b3f2d372cea44"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::depth </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>d</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set the printing depth. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00171">171</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
</div>
</div>
<a class="anchor" id="ae408e31b8c24a7a808985f6874cd5059"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::lineWidth </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>w</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set the line width. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00173">173</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
</div>
</div>
<a class="anchor" id="a2d4ff13cb98b358eb02dfbf149ae03ae"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprStream::dagFlag </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>flag</em> = <code>true</code></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set the DAG flag (return previous value) </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00175">175</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8cpp_source.html#l00383">CVC3::Expr::pprintnodag()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00700">CVC3::TheoryUF::print()</a>, <a class="el" href="expr_8cpp_source.html#l00362">CVC3::Expr::print()</a>, and <a class="el" href="vc__cmd_8cpp_source.html#l00188">CVC3::VCCmd::printSymbols()</a>.</p>
</div>
</div>
<a class="anchor" id="a92fe55e5f00f52ac00db56afcaaba80c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::pushIndent </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set the indentation to the current column. </p>
<p>The value will be restorted automatically after the DP print() function returns </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00179">179</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00298">CVC3::push()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00315">CVC3::pushRestore()</a>.</p>
</div>
</div>
<a class="anchor" id="a45fc9ca3545f65f62e6c255d2b108782"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::pushIndent </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>pos</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set the indentation to the given absolute position. </p>
<p>The value will be restorted automatically after the DP print() function returns </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00183">183</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
</div>
</div>
<a class="anchor" id="a32a666cc0a71503770b88e3a7362808c"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::popIndent </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Restore the indentation (user cannot pop more than pushed) </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00110">110</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8h_source.html#l00126">d_indentLast</a>, <a class="el" href="expr__stream_8h_source.html#l00124">d_indentStack</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00301">CVC3::pop()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00306">CVC3::popSave()</a>.</p>
</div>
</div>
<a class="anchor" id="a946110c3457868fe38ce8c1d4cdde916"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::resetIndent </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Reset indentation to what it was at this level. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00121">121</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8h_source.html#l00126">d_indentLast</a>, and <a class="el" href="expr__stream_8h_source.html#l00124">d_indentStack</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>, <a class="el" href="expr_8cpp_source.html#l00458">CVC3::Expr::print()</a>, <a class="el" href="expr_8cpp_source.html#l00400">CVC3::Expr::printAST()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00320">CVC3::reset()</a>.</p>
</div>
</div>
<a class="anchor" id="a1f3ea8ff58dfb9cab4471d157decfae5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprStream::column </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Return the current column position. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00189">189</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
</div>
</div>
<a class="anchor" id="a2c93d862ed9b3cb1480a1d12cb510841"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::pushDag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Recompute shared subexpression for the next <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00127">127</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8h_source.html#l00143">d_dagBuilt</a>, <a class="el" href="expr__stream_8h_source.html#l00139">d_dagPtr</a>, and <a class="el" href="expr__stream_8h_source.html#l00137">d_dagStack</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00337">CVC3::pushdag()</a>.</p>
</div>
</div>
<a class="anchor" id="a7d1aa8566189d9b03a12bc56d3514979"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::popDag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Delete shared subexpressions previously added with pushdag. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00132">132</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
<p>References <a class="el" href="expr__map_8h_source.html#l00175">CVC3::ExprMap< Data >::clear()</a>, <a class="el" href="expr__stream_8h_source.html#l00133">d_dagMap</a>, <a class="el" href="expr__stream_8h_source.html#l00139">d_dagPtr</a>, <a class="el" href="expr__stream_8h_source.html#l00137">d_dagStack</a>, <a class="el" href="expr__stream_8h_source.html#l00141">d_lastDagSize</a>, <a class="el" href="expr__stream_8h_source.html#l00135">d_newDagMap</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="expr__map_8h_source.html#l00178">CVC3::ExprMap< Data >::erase()</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00339">CVC3::popdag()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00147">resetDag()</a>.</p>
</div>
</div>
<a class="anchor" id="a004714bd282bfa11595d21bce94e72ec"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprStream::resetDag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Reset the DAG to what it was at this level. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00147">147</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8h_source.html#l00139">d_dagPtr</a>, <a class="el" href="expr__stream_8h_source.html#l00141">d_lastDagSize</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00132">popDag()</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>.</p>
</div>
</div>
<h2 class="groupheader">Friends And Related Function Documentation</h2>
<a class="anchor" id="a2bb78121744c58b0fe429be690099af5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& operator<< </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &(*)(<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &) </td>
<td class="paramname"><em>manip</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Use manipulators which are functions over <a class="el" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>&. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00156">156</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="afe31e05cdc0aeb97284d664bfb31afb4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& operator<< </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Print <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00162">162</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="aefb83c75e89a7c782e89f485b20bdc74"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& operator<< </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>t</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Print <a class="el" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00226">226</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ac80c6017f4685dddc8c43de3bf72c8f0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& operator<< </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>s</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Print string. </p>
<p>This is where all the indentation is happening.</p>
<p>The algorithm for determining whether to go to the next line is the following:</p>
<ul>
<li>If the new d_col does not exceed d_lineWidth/2 or current indentation, don't bother.</li>
</ul>
<ul>
<li>If the difference between the new d_col and the current indentation is less than d_lineWidth/4, don't bother either, so that we don't get lots of very short lines clumped to the right side.</li>
</ul>
<ul>
<li>Similarly, if the difference between the old d_col and the current indentation is less than d_lineWidth/6, keep the same line. Otherwise, for long atomic strings, we may get useless line breaks.</li>
</ul>
<ul>
<li>Otherwise, go to the next line. </li>
</ul>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00251">251</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a7b3d2ea716f32a02bcbaad87185a620d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& operator<< </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const char * </td>
<td class="paramname"><em>s</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Print char* string. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00273">273</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="afc67d7be0ed3251f85bec17aefda9be9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& operator<< </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> & </td>
<td class="paramname"><em>r</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Print <a class="el" href="classCVC3_1_1Rational.html">Rational</a>. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00278">278</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ab83e67a05d087196ac378d13a7d3cac6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& operator<< </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Print int. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00285">285</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a02863edb9e23b394e5011f63149ea443"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& push </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set the indentation to the current position. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00298">298</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="aa82375e98a075cd85eb04f957b01f3d1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& pop </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Restore the indentation to the previous position. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00301">301</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
<p>Referenced by <a class="el" href="vcl_8cpp_source.html#l02343">CVC3::VCL::popScope()</a>.</p>
</div>
</div>
<a class="anchor" id="adfda971d718f84fccfd2118f4a2e13ac"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& popSave </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Remember the current indentation and pop to the previous position. </p>
<p>There is only one register to save the previous position. If you use <a class="el" href="classCVC3_1_1ExprStream.html#adfda971d718f84fccfd2118f4a2e13ac" title="Remember the current indentation and pop to the previous position.">popSave()</a> more than once, only the latest position can be restored with <a class="el" href="classCVC3_1_1ExprStream.html#a97553d34943597156f6a9b4f382cf05f" title="Set the indentation to the position saved by popSave()">pushRestore()</a>. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00306">306</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a97553d34943597156f6a9b4f382cf05f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& pushRestore </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Set the indentation to the position saved by <a class="el" href="classCVC3_1_1ExprStream.html#adfda971d718f84fccfd2118f4a2e13ac" title="Remember the current indentation and pop to the previous position.">popSave()</a> </p>
<p>There is only one register to save the previous position. Using <a class="el" href="classCVC3_1_1ExprStream.html#a97553d34943597156f6a9b4f382cf05f" title="Set the indentation to the position saved by popSave()">pushRestore()</a> several times will set intendation to the same position. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00315">315</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a49c83f6df078882e63f7834f2d31b6bc"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& reset </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Reset the indentation to the default at this level. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00320">320</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a09fb109b45779eeaa0d0d64c2ab46c6f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& space </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Insert a single white space separator. </p>
<p>It is preferred to use 'space' rather than a string of spaces (" ") because <a class="el" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> needs to delete extra white space if it decides to end the line. If you use strings for spaces, you'll mess up the indentation. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00326">326</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a6b0ee540ac9fd476d22ce316a6c9f78d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& nodag </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Print the next top-level expression node without DAG-ifying. </p>
<p>DAG-printing will resume for the children of the node. This is useful when printing definitions in the header of a DAGified LET expressions: defs have names, but must be printed expanded. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00332">332</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="adaa3f23e99a706464a4842bb872b93a3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& pushdag </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Recompute shared subexpression for the next <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. </p>
<p>For some constructs with bound variables (notably, quantifiers), shared subexpressions are not computed, because they cannot be defined outside the scope of bound variables. If this manipulator is applied before an expression within the scope of bound vars, these internal subexpressions will then be computed. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00337">337</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a7a602f53a7718623252748882eb4886b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& popdag </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Delete shared subexpressions previously added with pushdag. </p>
<p>Similar to push/pop, shared subexpressions are automatically deleted upon a return from a recursive call, so popdag is not necessary after a pushdag in theory-specific print() functions. Also, you cannot pop more than you pushed an the current recursion level. </p>
<p>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00339">339</a> of file <a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="aaedf4f2798091833629c6465bfd360b7"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a>& std::endl </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Print the end-of-line. </p>
<p>The new line will not necessarily start at column 0 because of indentation.</p>
<p>The name endl will be introduced in namespace std, otherwise CVC3::endl would overshadow std::endl, wreaking havoc... </p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="a7ab1b6602b49bf13867877bf5f7a5873"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a>* CVC3::ExprStream::d_em</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>The <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> to use. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00112">112</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00029">ExprStream()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="acc3438cd65369ea0dad38ea59c93343a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::ostream* CVC3::ExprStream::d_os</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>The ostream to print into. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00113">113</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00251">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a82d42f256f0775a3b4c9c3a4bed346d0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprStream::d_depth</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Printing only upto this depth; -1 == unlimited. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00114">114</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a83bf8b10c32e6a579ace151f35ce7e08"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprStream::d_currDepth</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Current depth of <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00115">115</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a0db5c8c81be1cdcdeba4c2873572b519"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> CVC3::ExprStream::d_lang</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Output language. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00116">116</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00054">collectShared()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a376d7f29bf587b712bc9302ed27d8b77"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprStream::d_indent</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Whether to print with indentations. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00117">117</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00251">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a92f85002e3bc476e5879b9012ff4c2c9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprStream::d_col</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Current column in a line. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00118">118</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00251">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="aa954bdbaf953b6f059d2cd6252130095"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprStream::d_lineWidth</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Try to format/indent for this line width </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00119">119</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00251">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a3141312e4ccf7ea7d15adf6af193a6db"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector<int> CVC3::ExprStream::d_indentStack</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Indentation stack. </p>
<p>The user code can set the indentation to the current d_col by pushing the new value on the stack. This value is popped automatically when returning from the recursive call. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00124">124</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00029">ExprStream()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00110">popIndent()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00306">CVC3::popSave()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00121">resetIndent()</a>.</p>
</div>
</div>
<a class="anchor" id="aa77050ac6ae56a6d4a45736e89521e0f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">size_t CVC3::ExprStream::d_indentLast</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>The lowest position of the indent stack the user can pop. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00126">126</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00029">ExprStream()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00110">popIndent()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00121">resetIndent()</a>.</p>
</div>
</div>
<a class="anchor" id="a6961d32e92cc350b1fd591888f037289"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprStream::d_indentReg</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Indentation register for <a class="el" href="classCVC3_1_1ExprStream.html#adfda971d718f84fccfd2118f4a2e13ac" title="Remember the current indentation and pop to the previous position.">popSave()</a> and <a class="el" href="classCVC3_1_1ExprStream.html#a97553d34943597156f6a9b4f382cf05f" title="Set the indentation to the position saved by popSave()">pushRestore()</a> </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00128">128</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00306">CVC3::popSave()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00315">CVC3::pushRestore()</a>.</p>
</div>
</div>
<a class="anchor" id="a0e9d4e03372235a23da6a965aa05f742"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprStream::d_beginningOfLine</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Whether it is a beginning of line (for eating up extra spaces) </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00130">130</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00251">CVC3::operator<<()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00326">CVC3::space()</a>.</p>
</div>
</div>
<a class="anchor" id="abc448835fcc31cd355c90606822ed42c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprStream::d_dag</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Print <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> as a DAG </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00131">131</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a5613bd2f13161fe6846776dbb328bd34"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><std::string> CVC3::ExprStream::d_dagMap</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Mapping subexpressions to names for DAG printing. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00133">133</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00054">collectShared()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00132">popDag()</a>.</p>
</div>
</div>
<a class="anchor" id="a8281aa65a9abe1cbbb3b1b43f9ab28c5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><std::string> CVC3::ExprStream::d_newDagMap</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>New subexpressions not yet printed in a LET header. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00135">135</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00093">addLetHeader()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00054">collectShared()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00132">popDag()</a>.</p>
</div>
</div>
<a class="anchor" id="ad1dc7ed42d81dd3de3a3ec4328c1d6c2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> CVC3::ExprStream::d_dagStack</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Stack of shared subexpressions (same as in d_dagMap) </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00137">137</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00054">collectShared()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00132">popDag()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00127">pushDag()</a>.</p>
</div>
</div>
<a class="anchor" id="a78aa8e292d7555fdfb7a94c00c0b3a6f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector<size_t> CVC3::ExprStream::d_dagPtr</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Stack of pointers to d_dagStack for pushing/popping shared subexprs. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00139">139</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00029">ExprStream()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00132">popDag()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00127">pushDag()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00147">resetDag()</a>.</p>
</div>
</div>
<a class="anchor" id="ae19d943560a35d7b9f4042a152420262"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">size_t CVC3::ExprStream::d_lastDagSize</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>The smallest size of d_dagPtr the user can `popDag'. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00141">141</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00029">ExprStream()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00132">popDag()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00147">resetDag()</a>.</p>
</div>
</div>
<a class="anchor" id="a5fb7d3cacc87b22ea0ca79efd35a038f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprStream::d_dagBuilt</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Flag whether the dagMap is already built. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00143">143</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00054">collectShared()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00127">pushDag()</a>.</p>
</div>
</div>
<a class="anchor" id="aa2a427ab0f2adc805cfd3cab42b8363a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprStream::d_idCounter</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Counter for generating unique LET var names. </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00145">145</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00043">newName()</a>.</p>
</div>
</div>
<a class="anchor" id="a00ed22d62da899833285f2bbf20754fd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprStream::d_nodag</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p><a class="el" href="classCVC3_1_1ExprStream.html#a6b0ee540ac9fd476d22ce316a6c9f78d" title="Print the next top-level expression node without DAG-ifying.">nodag()</a> manipulator has been applied </p>
<p>Definition at line <a class="el" href="expr__stream_8h_source.html#l00147">147</a> of file <a class="el" href="expr__stream_8h_source.html">expr_stream.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00332">CVC3::nodag()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00162">CVC3::operator<<()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="expr__stream_8h_source.html">expr_stream.h</a></li>
<li><a class="el" href="expr__stream_8cpp_source.html">expr_stream.cpp</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:17 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
