<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: Manipulators</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#func-members">Functions</a> </div>
<div class="headertitle">
<div class="title">Manipulators</div> </div>
<div class="ingroups"><a class="el" href="group__PrettyPrinting.html">Pretty-printing related classes and methods</a></div></div>
<div class="contents">
<h2><a name="func-members"></a>
Functions</h2>
<ul>
<li>ExprStream & <a class="el" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218">CVC3::push</a> (ExprStream &os)
<dl class="el"><dd class="mdescRight">Set the indentation to the current position. <a href="#ga2a0348c6d3f94f2f8febc6dd0a9c3218"></a><br/></dl><li>ExprStream & <a class="el" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be">CVC3::pop</a> (ExprStream &os)
<dl class="el"><dd class="mdescRight">Restore the indentation. <a href="#gaddb050a787be87116afc51791293d3be"></a><br/></dl><li>ExprStream & <a class="el" href="group__ExprStream__Manip.html#gacf04af76c8233f27762ad6ebb73a58c0">CVC3::popSave</a> (ExprStream &os)
<dl class="el"><dd class="mdescRight">Remember the current indentation and pop to the previous position. <a href="#gacf04af76c8233f27762ad6ebb73a58c0"></a><br/></dl><li>ExprStream & <a class="el" href="group__ExprStream__Manip.html#ga7a2134042b4ae9b096b0003d8f3c869a">CVC3::pushRestore</a> (ExprStream &os)
<dl class="el"><dd class="mdescRight">Set the indentation to the position saved by <a class="el" href="group__ExprStream__Manip.html#gacf04af76c8233f27762ad6ebb73a58c0" title="Remember the current indentation and pop to the previous position.">popSave()</a> <a href="#ga7a2134042b4ae9b096b0003d8f3c869a"></a><br/></dl><li>ExprStream & <a class="el" href="group__ExprStream__Manip.html#ga90deb7348703ae1a59a11d9af77aa8ad">CVC3::reset</a> (ExprStream &os)
<dl class="el"><dd class="mdescRight">Reset the indentation to the default at this level. <a href="#ga90deb7348703ae1a59a11d9af77aa8ad"></a><br/></dl><li>ExprStream & <a class="el" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810">CVC3::space</a> (ExprStream &os)
<dl class="el"><dd class="mdescRight">Insert a single white space separator. <a href="#ga02670eb229648e9e2d888f21f91b6810"></a><br/></dl><li>ExprStream & <a class="el" href="group__ExprStream__Manip.html#gab9909b3108229b630956179ebd71f3ef">CVC3::nodag</a> (ExprStream &os)
<li>ExprStream & <a class="el" href="group__ExprStream__Manip.html#ga1475185296de10fdbe07f0b498e8ed36">CVC3::pushdag</a> (ExprStream &os)
<li>ExprStream & <a class="el" href="group__ExprStream__Manip.html#ga07ae0c39b4082065891134536f2fa91c">CVC3::popdag</a> (ExprStream &os)
<li><a class="el" href="classCVC3_1_1ExprStream.html">CVC3::ExprStream</a> & <a class="el" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8">std::endl</a> (<a class="el" href="classCVC3_1_1ExprStream.html">CVC3::ExprStream</a> &os)
<dl class="el"><dd class="mdescRight">Print the end-of-line. <a href="#ga05b0ea7353ec24fa8e7e272d7a7875d8"></a><br/></dl></ul>
<hr/><h2>Function Documentation</h2>
<a class="anchor" id="ga2a0348c6d3f94f2f8febc6dd0a9c3218"></a><!-- doxytag: member="CVC3::push" ref="ga2a0348c6d3f94f2f8febc6dd0a9c3218" args="(ExprStream &os)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprStream & CVC3::push </td>
<td>(</td>
<td class="paramtype">ExprStream & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></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>
<p>References <a class="el" href="expr__stream_8h_source.html#l00179">CVC3::ExprStream::pushIndent()</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00638">CVC3::SearchSat::check()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00700">CVC3::TheoryUF::print()</a>, <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__quant_8cpp_source.html#l08729">CVC3::TheoryQuant::print()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00639">CVC3::TheoryDatatype::print()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03662">CVC3::TheoryBitvector::print()</a>, <a class="el" href="theory__array_8cpp_source.html#l01072">CVC3::TheoryArray::print()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03952">CVC3::TheoryArithOld::print()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l02150">CVC3::TheoryArithNew::print()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02966">CVC3::TheoryArith3::print()</a>, <a class="el" href="expr_8cpp_source.html#l00458">CVC3::Expr::print()</a>, <a class="el" href="translator_8cpp_source.html#l01850">CVC3::Translator::printArrayExpr()</a>, <a class="el" href="expr_8cpp_source.html#l00400">CVC3::Expr::printAST()</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>, <a class="el" href="theory__bitvector_8cpp_source.html#l03429">CVC3::TheoryBitvector::printSmtLibShared()</a>, <a class="el" href="vcl_8cpp_source.html#l01929">CVC3::VCL::query()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00326">CVC3::space()</a>.</p>
</div>
</div>
<a class="anchor" id="gaddb050a787be87116afc51791293d3be"></a><!-- doxytag: member="CVC3::pop" ref="gaddb050a787be87116afc51791293d3be" args="(ExprStream &os)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprStream & CVC3::pop </td>
<td>(</td>
<td class="paramtype">ExprStream & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Restore the indentation. </p>
<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>References <a class="el" href="expr__stream_8cpp_source.html#l00110">CVC3::ExprStream::popIndent()</a>.</p>
<p>Referenced by <a class="el" href="vcl_8cpp_source.html#l01848">CVC3::VCL::assertFormula()</a>, <a class="el" href="search__sat_8cpp_source.html#l00638">CVC3::SearchSat::check()</a>, <a class="el" href="vcl_8cpp_source.html#l02294">CVC3::VCL::pop()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00700">CVC3::TheoryUF::print()</a>, <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__quant_8cpp_source.html#l08729">CVC3::TheoryQuant::print()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00639">CVC3::TheoryDatatype::print()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03662">CVC3::TheoryBitvector::print()</a>, <a class="el" href="theory__array_8cpp_source.html#l01072">CVC3::TheoryArray::print()</a>, <a class="el" href="expr_8cpp_source.html#l00458">CVC3::Expr::print()</a>, <a class="el" href="translator_8cpp_source.html#l01850">CVC3::Translator::printArrayExpr()</a>, <a class="el" href="expr_8cpp_source.html#l00400">CVC3::Expr::printAST()</a>, <a class="el" href="theory__core_8cpp_source.html#l01915">CVC3::TheoryCore::printSmtLibShared()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03429">CVC3::TheoryBitvector::printSmtLibShared()</a>, <a class="el" href="vcl_8cpp_source.html#l02281">CVC3::VCL::push()</a>, <a class="el" href="vcl_8cpp_source.html#l01929">CVC3::VCL::query()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00326">CVC3::space()</a>.</p>
</div>
</div>
<a class="anchor" id="gacf04af76c8233f27762ad6ebb73a58c0"></a><!-- doxytag: member="CVC3::popSave" ref="gacf04af76c8233f27762ad6ebb73a58c0" args="(ExprStream &os)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprStream & CVC3::popSave </td>
<td>(</td>
<td class="paramtype">ExprStream & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></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="group__ExprStream__Manip.html#gacf04af76c8233f27762ad6ebb73a58c0" 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="group__ExprStream__Manip.html#ga7a2134042b4ae9b096b0003d8f3c869a" 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>
<p>References <a class="el" href="expr__stream_8h_source.html#l00128">CVC3::ExprStream::d_indentReg</a>, <a class="el" href="expr__stream_8h_source.html#l00124">CVC3::ExprStream::d_indentStack</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00110">CVC3::ExprStream::popIndent()</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>.</p>
</div>
</div>
<a class="anchor" id="ga7a2134042b4ae9b096b0003d8f3c869a"></a><!-- doxytag: member="CVC3::pushRestore" ref="ga7a2134042b4ae9b096b0003d8f3c869a" args="(ExprStream &os)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprStream & CVC3::pushRestore </td>
<td>(</td>
<td class="paramtype">ExprStream & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set the indentation to the position saved by <a class="el" href="group__ExprStream__Manip.html#gacf04af76c8233f27762ad6ebb73a58c0" 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="group__ExprStream__Manip.html#ga7a2134042b4ae9b096b0003d8f3c869a" 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>
<p>References <a class="el" href="expr__stream_8h_source.html#l00128">CVC3::ExprStream::d_indentReg</a>, and <a class="el" href="expr__stream_8h_source.html#l00179">CVC3::ExprStream::pushIndent()</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>.</p>
</div>
</div>
<a class="anchor" id="ga90deb7348703ae1a59a11d9af77aa8ad"></a><!-- doxytag: member="CVC3::reset" ref="ga90deb7348703ae1a59a11d9af77aa8ad" args="(ExprStream &os)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprStream & CVC3::reset </td>
<td>(</td>
<td class="paramtype">ExprStream & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></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>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00121">CVC3::ExprStream::resetIndent()</a>.</p>
</div>
</div>
<a class="anchor" id="ga02670eb229648e9e2d888f21f91b6810"></a><!-- doxytag: member="CVC3::space" ref="ga02670eb229648e9e2d888f21f91b6810" args="(ExprStream &os)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprStream & CVC3::space </td>
<td>(</td>
<td class="paramtype">ExprStream & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></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>
<p>References <a class="el" href="expr__stream_8h_source.html#l00130">CVC3::ExprStream::d_beginningOfLine</a>, <a class="el" href="expr__stream_8cpp_source.html#l00301">CVC3::pop()</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00298">CVC3::push()</a>.</p>
<p>Referenced by <a class="el" href="theory__uf_8cpp_source.html#l00700">CVC3::TheoryUF::print()</a>, <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__quant_8cpp_source.html#l08729">CVC3::TheoryQuant::print()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00639">CVC3::TheoryDatatype::print()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03662">CVC3::TheoryBitvector::print()</a>, <a class="el" href="theory__array_8cpp_source.html#l01072">CVC3::TheoryArray::print()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03952">CVC3::TheoryArithOld::print()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l02150">CVC3::TheoryArithNew::print()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02966">CVC3::TheoryArith3::print()</a>, <a class="el" href="expr_8cpp_source.html#l00458">CVC3::Expr::print()</a>, <a class="el" href="translator_8cpp_source.html#l01850">CVC3::Translator::printArrayExpr()</a>, <a class="el" href="expr_8cpp_source.html#l00400">CVC3::Expr::printAST()</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="theory__bitvector_8cpp_source.html#l03429">CVC3::TheoryBitvector::printSmtLibShared()</a>.</p>
</div>
</div>
<a class="anchor" id="gab9909b3108229b630956179ebd71f3ef"></a><!-- doxytag: member="CVC3::nodag" ref="gab9909b3108229b630956179ebd71f3ef" args="(ExprStream &os)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprStream & CVC3::nodag </td>
<td>(</td>
<td class="paramtype">ExprStream & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<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>
<p>References <a class="el" href="expr__stream_8h_source.html#l00147">CVC3::ExprStream::d_nodag</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l08729">CVC3::TheoryQuant::print()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="translator_8cpp_source.html#l01850">CVC3::Translator::printArrayExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00400">CVC3::Expr::printAST()</a>.</p>
</div>
</div>
<a class="anchor" id="ga1475185296de10fdbe07f0b498e8ed36"></a><!-- doxytag: member="CVC3::pushdag" ref="ga1475185296de10fdbe07f0b498e8ed36" args="(ExprStream &os)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprStream & CVC3::pushdag </td>
<td>(</td>
<td class="paramtype">ExprStream & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<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>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00127">CVC3::ExprStream::pushDag()</a>.</p>
<p>Referenced by <a class="el" href="theory__uf_8cpp_source.html#l00700">CVC3::TheoryUF::print()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08729">CVC3::TheoryQuant::print()</a>, and <a class="el" href="theory__array_8cpp_source.html#l01072">CVC3::TheoryArray::print()</a>.</p>
</div>
</div>
<a class="anchor" id="ga07ae0c39b4082065891134536f2fa91c"></a><!-- doxytag: member="CVC3::popdag" ref="ga07ae0c39b4082065891134536f2fa91c" args="(ExprStream &os)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprStream & CVC3::popdag </td>
<td>(</td>
<td class="paramtype">ExprStream & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<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>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00132">CVC3::ExprStream::popDag()</a>.</p>
<p>Referenced by <a class="el" href="theory__uf_8cpp_source.html#l00700">CVC3::TheoryUF::print()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08729">CVC3::TheoryQuant::print()</a>, and <a class="el" href="theory__array_8cpp_source.html#l01072">CVC3::TheoryArray::print()</a>.</p>
</div>
</div>
<a class="anchor" id="ga05b0ea7353ec24fa8e7e272d7a7875d8"></a><!-- doxytag: member="std::endl" ref="ga05b0ea7353ec24fa8e7e272d7a7875d8" args="(CVC3::ExprStream &os)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">CVC3::ExprStream</a> & std::endl </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">CVC3::ExprStream</a> & </td>
<td class="paramname"><em>os</em></td><td>)</td>
<td></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>Definition at line <a class="el" href="expr__stream_8cpp_source.html#l00353">353</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#l00130">CVC3::ExprStream::d_beginningOfLine</a>, <a class="el" href="expr__stream_8h_source.html#l00118">CVC3::ExprStream::d_col</a>, <a class="el" href="expr__stream_8h_source.html#l00117">CVC3::ExprStream::d_indent</a>, <a class="el" href="expr__stream_8h_source.html#l00124">CVC3::ExprStream::d_indentStack</a>, and <a class="el" href="expr__stream_8h_source.html#l00113">CVC3::ExprStream::d_os</a>.</p>
<p>Referenced by <a class="el" href="xchaff__utils_8cpp_source.html#l00043">Abort()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02313">MiniSat::Solver::allClausesSatisfied()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="theory__core_8cpp_source.html#l00321">CVC3::TheoryCore::assertFactCore()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00830">CSolver::back_track()</a>, <a class="el" href="search__sat_8cpp_source.html#l00638">CVC3::SearchSat::check()</a>, <a class="el" href="context_8cpp_source.html#l00055">CVC3::Scope::check()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02398">MiniSat::Solver::checkClause()</a>, <a class="el" href="theory__quant_8cpp_source.html#l07647">CVC3::TheoryQuant::checkSat()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02574">CVC3::TheoryBitvector::checkSat()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02606">CVC3::TheoryArithOld::checkSat()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02359">MiniSat::Solver::checkWatched()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01861">CVC3::CompleteInstPreProcessor::collect_forall_index()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">CDatabase::compact_lit_pool()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00916">CSolver::conflict_analysis_zchaff()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00221">CVC3::SearchEngineTheoremProducer::conflictClause()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00018">LFSCConvert::convert()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00351">MiniSat::Solver::curAssigns()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00360">MiniSat::Solver::curClauses()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00343">CVC3::TheoryQuant::debug()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">CSolver::decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00513">CSolver::delete_unrelevant_clauses()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00176">CDatabase::detail_dump_cl()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01718">LFSCConvert::do_bso()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00197">CDatabase::dump()</a>, <a class="el" href="xchaff__base_8h_source.html#l00300">CVariable::dump()</a>, <a class="el" href="xchaff__base_8h_source.html#l00199">CClause::dump()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00463">CSolver::dump_assignment_stack()</a>, <a class="el" href="translator_8cpp_source.html#l00986">CVC3::Translator::dumpQueryResult()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">CDatabase::enlarge_lit_pool()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00267">CVC3::VCCmd::evaluateCommand()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00073">CVC3::VCCmd::evaluateNext()</a>, <a class="el" href="debug_8cpp_source.html#l00035">CVC3::fatalError()</a>, <a class="el" href="search__sat_8cpp_source.html#l00364">CVC3::SearchSat::findSplitterRec()</a>, <a class="el" href="translator_8cpp_source.html#l01145">CVC3::Translator::finish()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00258">generateSatProof()</a>, <a class="el" href="Util_8cpp_source.html#l00111">get_knd_result()</a>, <a class="el" href="context_8cpp_source.html#l00082">CVC3::Scope::getMemory()</a>, <a class="el" href="search__sat_8h_source.html#l00289">CVC3::SearchSat::getValue()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00448">LFSCObj::getY()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00170">SAT::DPLLTBasic::handle_result()</a>, <a class="el" href="Object_8h_source.html#l00073">Obj::indent()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00186">CVC3::TheoryArithOld::kidsCanonical()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00094">CVC3::TheoryArithNew::kidsCanonical()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00180">CVC3::TheoryArith3::kidsCanonical()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00106">CVC3::CNF_TheoremProducer::learnedClauses()</a>, <a class="el" href="main_8cpp_source.html#l00092">main()</a>, <a class="el" href="LFSCLraProof_8cpp_source.html#l00117">LFSCLraPoly::Make()</a>, <a class="el" href="LFSCProof_8cpp_source.html#l00104">LFSCProof::Make_CNF()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l01663">LFSCConvert::make_let_proof()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04592">CVC3::TheoryQuant::newTopMatch()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04671">CVC3::TheoryQuant::newTopMatchSig()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="TReturn_8cpp_source.html#l00423">TReturn::normalize_to_tf()</a>, <a class="el" href="TReturn_8cpp_source.html#l00125">TReturn::normalize_tr()</a>, <a class="el" href="TReturn_8cpp_source.html#l00084">TReturn::normalize_tret()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08621">CVC3::TheoryQuant::notifyInconsistent()</a>, <a class="el" href="theory__arith__new_8h_source.html#l00550">CVC3::TheoryArithNew::BoundInfo::operator<()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00251">CVC3::operator<<()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00167">CDatabase::output_lit_pool_state()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00408">CVC3::QuantTheoremProducer::partialUniversalInst()</a>, <a class="el" href="vcl_8cpp_source.html#l02343">CVC3::VCL::popScope()</a>, <a class="el" href="expr_8cpp_source.html#l00373">CVC3::Expr::pprint()</a>, <a class="el" href="expr_8cpp_source.html#l00383">CVC3::Expr::pprintnodag()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">CSolver::preprocess()</a>, <a class="el" href="translator_8cpp_source.html#l00549">CVC3::Translator::preprocess()</a>, <a class="el" href="translator_8cpp_source.html#l00783">CVC3::Translator::preprocess2()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00639">CVC3::TheoryDatatype::print()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03952">CVC3::TheoryArithOld::print()</a>, <a class="el" href="theorem_8cpp_source.html#l00211">CVC3::Theorem::print()</a>, <a class="el" href="expr_8cpp_source.html#l00362">CVC3::Expr::print()</a>, <a class="el" href="cvc__util_8h_source.html#l00120">CVC3::MemoryTracker::print()</a>, <a class="el" href="cnf_8cpp_source.html#l00042">SAT::Clause::print()</a>, <a class="el" href="assumptions_8cpp_source.html#l00257">CVC3::Assumptions::print()</a>, <a class="el" href="Object_8h_source.html#l00095">Obj::print_error()</a>, <a class="el" href="LFSCPrinter_8cpp_source.html#l00026">LFSCPrinter::print_LFSC()</a>, <a class="el" href="LFSCUtilProof_8cpp_source.html#l00153">LFSCPfLet::print_pf()</a>, <a class="el" href="LFSCPrinter_8cpp_source.html#l00378">LFSCPrinter::print_terms_h()</a>, <a class="el" href="Object_8h_source.html#l00104">Obj::print_warning()</a>, <a class="el" href="statistics_8cpp_source.html#l00032">CVC3::Statistics::printAll()</a>, <a class="el" href="expr_8cpp_source.html#l00400">CVC3::Expr::printAST()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00228">CVC3::VCCmd::printCounterExample()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00343">MiniSat::Derivation::printDerivation()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00405">MiniSat::Solver::printDIMACS()</a>, <a class="el" href="vcl_8cpp_source.html#l01050">CVC3::VCL::printExpr()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00157">CVC3::VCCmd::printModel()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00330">printSatProof()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00375">MiniSat::Solver::printState()</a>, <a class="el" href="vcl_8h_source.html#l00416">CVC3::VCL::printStatistics()</a>, <a class="el" href="sat__api_8cpp_source.html#l00021">SatSolver::PrintStatistics()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00188">CVC3::VCCmd::printSymbols()</a>, <a class="el" href="main_8cpp_source.html#l00217">printUsage()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00944">CVC3::VCCmd::processCommands()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01937">MiniSat::Solver::protocolPropagation()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">MiniSat::Solver::push()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00418">LFSCObj::queryMt()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00345">CSolver::queue_implication()</a>, <a class="el" href="theorem_8cpp_source.html#l00516">CVC3::Theorem::recursivePrint()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00102">CVC3::VCCmd::reportResult()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00358">CSolver::restart()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00109">CSolver::run_periodic_functions()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01419">CVC3::SearchEngineTheoremProducer::satProof()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">MiniSat::Solver::search()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">SAT::DPLLTMiniSat::search()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00296">CSolver::set_var_value()</a>, <a class="el" href="main_8cpp_source.html#l00055">sighandler()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01462">CVC3::CompleteInstPreProcessor::simplifyEq()</a>, <a class="el" href="translator_8cpp_source.html#l00845">CVC3::Translator::start()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00509">CVC3::CommonTheoremProducer::substitutivityRule()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00334">MiniSat::Solver::toString()</a>, <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>, <a class="el" href="TReturn_8cpp_source.html#l00008">TReturn::TReturn()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00433">CSolver::unset_var_value()</a>, <a class="el" href="xchaff__utils_8cpp_source.html#l00049">Warning()</a>, and <a class="el" href="theory__arith__old_8cpp_source.html#l05872">CVC3::TheoryArithOld::DifferenceLogicGraph::writeGraph()</a>.</p>
</div>
</div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
