<!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: Private methods</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><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#func-members">Functions</a> |
<a href="#var-members">Variables</a> </div>
<div class="headertitle">
<div class="title">Private methods</div> </div>
<div class="ingroups"><a class="el" href="group__ExprPkg.html">Expression Package</a></div></div><!--header-->
<div class="contents">
<div class="dynheader">
Collaboration diagram for Private methods:</div>
<div class="dyncontent">
<center><table><tr><td><img src="group__EM__Priv.gif" border="0" alt="" usemap="#group____EM____Priv"/>
<map name="group____EM____Priv" id="group____EM____Priv">
<area shape="rect" id="node1" href="group__ExprPkg.html" title="Expression Package" alt="" coords="6,5,149,32"/></map>
</td></tr></table></center>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="func-members"></a>
Functions</h2></td></tr>
<tr class="memitem:ga9fe970ca9a02174a617bce9797d41815"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga9fe970ca9a02174a617bce9797d41815">CVC3::ExprManager::HashString::operator()</a> (const std::string &s) const </td></tr>
<tr class="separator:ga9fe970ca9a02174a617bce9797d41815"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaabb82d3abf0072c71761ca599ba9a8fa"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaabb82d3abf0072c71761ca599ba9a8fa">CVC3::ExprManager::HashEV::HashEV</a> (ExprManager *em)</td></tr>
<tr class="separator:gaabb82d3abf0072c71761ca599ba9a8fa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac8adf717113c11ce0bc84160d17bea7a"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gac8adf717113c11ce0bc84160d17bea7a">CVC3::ExprManager::HashEV::operator()</a> (ExprValue *ev) const </td></tr>
<tr class="separator:gac8adf717113c11ce0bc84160d17bea7a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4a8fa9169728473cc4db3f96d467544f"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga4a8fa9169728473cc4db3f96d467544f">CVC3::ExprManager::EqEV::operator()</a> (const ExprValue *ev1, const ExprValue *ev2) const </td></tr>
<tr class="separator:ga4a8fa9169728473cc4db3f96d467544f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf4397d9b6d23d0e4b9112b509d9dfad4"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaf4397d9b6d23d0e4b9112b509d9dfad4">CVC3::ExprManager::TypeComputer::TypeComputer</a> ()</td></tr>
<tr class="separator:gaf4397d9b6d23d0e4b9112b509d9dfad4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaee11e07336c1b8704409d42c0aaeafad"><td class="memItemLeft" align="right" valign="top">virtual </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaee11e07336c1b8704409d42c0aaeafad">CVC3::ExprManager::TypeComputer::~TypeComputer</a> ()</td></tr>
<tr class="separator:gaee11e07336c1b8704409d42c0aaeafad"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga670ca72899c66da598ea568af7389407"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga670ca72899c66da598ea568af7389407">CVC3::ExprManager::TypeComputer::computeType</a> (const Expr &e)=0</td></tr>
<tr class="memdesc:ga670ca72899c66da598ea568af7389407"><td class="mdescLeft"> </td><td class="mdescRight">Compute the type of e. <a href="#ga670ca72899c66da598ea568af7389407"></a><br/></td></tr>
<tr class="separator:ga670ca72899c66da598ea568af7389407"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae679c021fb433f86c28c5eec68e5b5ee"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gae679c021fb433f86c28c5eec68e5b5ee">CVC3::ExprManager::TypeComputer::checkType</a> (const Expr &e)=0</td></tr>
<tr class="memdesc:gae679c021fb433f86c28c5eec68e5b5ee"><td class="mdescLeft"> </td><td class="mdescRight">Check that e is a valid <a class="el" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> expr. <a href="#gae679c021fb433f86c28c5eec68e5b5ee"></a><br/></td></tr>
<tr class="separator:gae679c021fb433f86c28c5eec68e5b5ee"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga13e9c0f4a23614e99705f60e3913c2b1"><td class="memItemLeft" align="right" valign="top">virtual Cardinality </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga13e9c0f4a23614e99705f60e3913c2b1">CVC3::ExprManager::TypeComputer::finiteTypeInfo</a> (Expr &e, Unsigned &n, bool enumerate, bool computeSize)=0</td></tr>
<tr class="memdesc:ga13e9c0f4a23614e99705f60e3913c2b1"><td class="mdescLeft"> </td><td class="mdescRight">Get information related to finiteness of a type. <a href="#ga13e9c0f4a23614e99705f60e3913c2b1"></a><br/></td></tr>
<tr class="separator:ga13e9c0f4a23614e99705f60e3913c2b1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa86d7ed7800549f1621d2d5ce64ce643"><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="group__EM__Priv.html#gaa86d7ed7800549f1621d2d5ce64ce643">CVC3::ExprManager::rebuildRec</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:gaa86d7ed7800549f1621d2d5ce64ce643"><td class="mdescLeft"> </td><td class="mdescRight">Cached recursive descent. Must be called only during <a class="el" href="group__EM__Priv.html#gacaab5ccf5cf81d11185979051d301d5e" title="Rebuild the Expr with this ExprManager if it belongs to another ExprManager.">rebuild()</a> <a href="#gaa86d7ed7800549f1621d2d5ce64ce643"></a><br/></td></tr>
<tr class="separator:gaa86d7ed7800549f1621d2d5ce64ce643"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3c693890e6e6e1610c44dda553dbf803"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga3c693890e6e6e1610c44dda553dbf803">CVC3::ExprManager::newExprValue</a> (<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *ev)</td></tr>
<tr class="memdesc:ga3c693890e6e6e1610c44dda553dbf803"><td class="mdescLeft"> </td><td class="mdescRight">Return either an existing or a new <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> matching ev. <a href="#ga3c693890e6e6e1610c44dda553dbf803"></a><br/></td></tr>
<tr class="separator:ga3c693890e6e6e1610c44dda553dbf803"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacaa71017958e2e9d069c055248c8dd78"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gacaa71017958e2e9d069c055248c8dd78">CVC3::ExprManager::getFlag</a> ()</td></tr>
<tr class="memdesc:gacaa71017958e2e9d069c055248c8dd78"><td class="mdescLeft"> </td><td class="mdescRight">Return the current <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> flag counter. <a href="#gacaa71017958e2e9d069c055248c8dd78"></a><br/></td></tr>
<tr class="separator:gacaa71017958e2e9d069c055248c8dd78"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab5336831e8006e69a57f9c1b728138f6"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gab5336831e8006e69a57f9c1b728138f6">CVC3::ExprManager::nextFlag</a> ()</td></tr>
<tr class="memdesc:gab5336831e8006e69a57f9c1b728138f6"><td class="mdescLeft"> </td><td class="mdescRight">Increment and return the <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> flag counter (this clears all the flags) <a href="#gab5336831e8006e69a57f9c1b728138f6"></a><br/></td></tr>
<tr class="separator:gab5336831e8006e69a57f9c1b728138f6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga15e87e829f86a1dcf2c5e05be6f4d182"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga15e87e829f86a1dcf2c5e05be6f4d182">CVC3::ExprManager::computeType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga15e87e829f86a1dcf2c5e05be6f4d182"><td class="mdescLeft"> </td><td class="mdescRight">Compute the type of the <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="#ga15e87e829f86a1dcf2c5e05be6f4d182"></a><br/></td></tr>
<tr class="separator:ga15e87e829f86a1dcf2c5e05be6f4d182"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga51109c3e331615c510c964798b38ee95"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga51109c3e331615c510c964798b38ee95">CVC3::ExprManager::checkType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga51109c3e331615c510c964798b38ee95"><td class="mdescLeft"> </td><td class="mdescRight">Check well-formedness of a type <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="#ga51109c3e331615c510c964798b38ee95"></a><br/></td></tr>
<tr class="separator:ga51109c3e331615c510c964798b38ee95"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae5cc4c6a7dfcc718c7c931e6b160d9d1"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gae5cc4c6a7dfcc718c7c931e6b160d9d1">CVC3::ExprManager::finiteTypeInfo</a> (<a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> &n, bool enumerate, bool computeSize)</td></tr>
<tr class="memdesc:gae5cc4c6a7dfcc718c7c931e6b160d9d1"><td class="mdescLeft"> </td><td class="mdescRight">Get information related to finiteness of a type. <a href="#gae5cc4c6a7dfcc718c7c931e6b160d9d1"></a><br/></td></tr>
<tr class="separator:gae5cc4c6a7dfcc718c7c931e6b160d9d1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf3af8657f4b2c64f189f0a50147d3589"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaf3af8657f4b2c64f189f0a50147d3589">CVC3::ExprManager::ExprManager</a> (<a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a> *cm, const <a class="el" href="classCVC3_1_1CLFlags.html">CLFlags</a> &flags)</td></tr>
<tr class="memdesc:gaf3af8657f4b2c64f189f0a50147d3589"><td class="mdescLeft"> </td><td class="mdescRight">Constructor. <a href="#gaf3af8657f4b2c64f189f0a50147d3589"></a><br/></td></tr>
<tr class="separator:gaf3af8657f4b2c64f189f0a50147d3589"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga318254064b65faf57e1657b680688bc7"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga318254064b65faf57e1657b680688bc7">CVC3::ExprManager::~ExprManager</a> ()</td></tr>
<tr class="memdesc:ga318254064b65faf57e1657b680688bc7"><td class="mdescLeft"> </td><td class="mdescRight">Destructor. <a href="#ga318254064b65faf57e1657b680688bc7"></a><br/></td></tr>
<tr class="separator:ga318254064b65faf57e1657b680688bc7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9bddd7eaf6f198476eda3cd55227f384"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga9bddd7eaf6f198476eda3cd55227f384">CVC3::ExprManager::clear</a> ()</td></tr>
<tr class="memdesc:ga9bddd7eaf6f198476eda3cd55227f384"><td class="mdescLeft"> </td><td class="mdescRight">Free up all memory and delete all the expressions. <a href="#ga9bddd7eaf6f198476eda3cd55227f384"></a><br/></td></tr>
<tr class="separator:ga9bddd7eaf6f198476eda3cd55227f384"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaaec477005a23531fa15d27282658aab8"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaaec477005a23531fa15d27282658aab8">CVC3::ExprManager::isActive</a> ()</td></tr>
<tr class="memdesc:gaaec477005a23531fa15d27282658aab8"><td class="mdescLeft"> </td><td class="mdescRight">Check if the <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> is still active (<a class="el" href="group__EM__Priv.html#ga9bddd7eaf6f198476eda3cd55227f384" title="Free up all memory and delete all the expressions.">clear()</a> was not called) <a href="#gaaec477005a23531fa15d27282658aab8"></a><br/></td></tr>
<tr class="separator:gaaec477005a23531fa15d27282658aab8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5878c4fbe700243540dc835b965fd01b"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga5878c4fbe700243540dc835b965fd01b">CVC3::ExprManager::gc</a> (<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *ev)</td></tr>
<tr class="memdesc:ga5878c4fbe700243540dc835b965fd01b"><td class="mdescLeft"> </td><td class="mdescRight">Garbage collect the <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> pointer. <a href="#ga5878c4fbe700243540dc835b965fd01b"></a><br/></td></tr>
<tr class="separator:ga5878c4fbe700243540dc835b965fd01b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9c35426ab6885b609e84a4be9b30effc"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga9c35426ab6885b609e84a4be9b30effc">CVC3::ExprManager::postponeGC</a> ()</td></tr>
<tr class="memdesc:ga9c35426ab6885b609e84a4be9b30effc"><td class="mdescLeft"> </td><td class="mdescRight">Postpone deletion of garbage-collected expressions. <a href="#ga9c35426ab6885b609e84a4be9b30effc"></a><br/></td></tr>
<tr class="separator:ga9c35426ab6885b609e84a4be9b30effc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gafd44d7be33c1111722aa7bb9f3b8b2e9"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gafd44d7be33c1111722aa7bb9f3b8b2e9">CVC3::ExprManager::resumeGC</a> ()</td></tr>
<tr class="memdesc:gafd44d7be33c1111722aa7bb9f3b8b2e9"><td class="mdescLeft"> </td><td class="mdescRight">Resume deletion of garbage-collected expressions. <a href="#gafd44d7be33c1111722aa7bb9f3b8b2e9"></a><br/></td></tr>
<tr class="separator:gafd44d7be33c1111722aa7bb9f3b8b2e9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacaab5ccf5cf81d11185979051d301d5e"><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="group__EM__Priv.html#gacaab5ccf5cf81d11185979051d301d5e">CVC3::ExprManager::rebuild</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:gacaab5ccf5cf81d11185979051d301d5e"><td class="mdescLeft"> </td><td class="mdescRight">Rebuild the <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> with this <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> if it belongs to another <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a>. <a href="#gacaab5ccf5cf81d11185979051d301d5e"></a><br/></td></tr>
<tr class="separator:gacaab5ccf5cf81d11185979051d301d5e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga212f07de6befabee47e4f9a1813e7c44"><td class="memItemLeft" align="right" valign="top">ExprIndex </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga212f07de6befabee47e4f9a1813e7c44">CVC3::ExprManager::nextIndex</a> ()</td></tr>
<tr class="memdesc:ga212f07de6befabee47e4f9a1813e7c44"><td class="mdescLeft"> </td><td class="mdescRight">Return the next <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> index. <a href="#ga212f07de6befabee47e4f9a1813e7c44"></a><br/></td></tr>
<tr class="separator:ga212f07de6befabee47e4f9a1813e7c44"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac64badd3988c01f34e43f227902e80f1"><td class="memItemLeft" align="right" valign="top">ExprIndex </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gac64badd3988c01f34e43f227902e80f1">CVC3::ExprManager::lastIndex</a> ()</td></tr>
<tr class="separator:gac64badd3988c01f34e43f227902e80f1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab4b3f2259b5c0af2251741139ea9d952"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gab4b3f2259b5c0af2251741139ea9d952">CVC3::ExprManager::clearFlags</a> ()</td></tr>
<tr class="memdesc:gab4b3f2259b5c0af2251741139ea9d952"><td class="mdescLeft"> </td><td class="mdescRight">Clears the generic <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> flag in all Exprs. <a href="#gab4b3f2259b5c0af2251741139ea9d952"></a><br/></td></tr>
<tr class="separator:gab4b3f2259b5c0af2251741139ea9d952"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab01fe102500e6b4e266299bf4bbb8a20"><td class="memItemLeft" align="right" valign="top">const Expr & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gab01fe102500e6b4e266299bf4bbb8a20">CVC3::ExprManager::boolExpr</a> ()</td></tr>
<tr class="memdesc:gab01fe102500e6b4e266299bf4bbb8a20"><td class="mdescLeft"> </td><td class="mdescRight">BOOLEAN <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="#gab01fe102500e6b4e266299bf4bbb8a20"></a><br/></td></tr>
<tr class="separator:gab01fe102500e6b4e266299bf4bbb8a20"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaae9db4c93c67cbf8bbf5d1e60e94f1ae"><td class="memItemLeft" align="right" valign="top">const Expr & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae">CVC3::ExprManager::falseExpr</a> ()</td></tr>
<tr class="memdesc:gaae9db4c93c67cbf8bbf5d1e60e94f1ae"><td class="mdescLeft"> </td><td class="mdescRight">FALSE <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="#gaae9db4c93c67cbf8bbf5d1e60e94f1ae"></a><br/></td></tr>
<tr class="separator:gaae9db4c93c67cbf8bbf5d1e60e94f1ae"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4471fca49c2acbb7b4cf71e72bc55d6a"><td class="memItemLeft" align="right" valign="top">const Expr & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a">CVC3::ExprManager::trueExpr</a> ()</td></tr>
<tr class="memdesc:ga4471fca49c2acbb7b4cf71e72bc55d6a"><td class="mdescLeft"> </td><td class="mdescRight">TRUE <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="#ga4471fca49c2acbb7b4cf71e72bc55d6a"></a><br/></td></tr>
<tr class="separator:ga4471fca49c2acbb7b4cf71e72bc55d6a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4619bc6e35a273b89d30908c45d73348"><td class="memItemLeft" align="right" valign="top">const std::vector< Expr > & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga4619bc6e35a273b89d30908c45d73348">CVC3::ExprManager::getEmptyVector</a> ()</td></tr>
<tr class="memdesc:ga4619bc6e35a273b89d30908c45d73348"><td class="mdescLeft"> </td><td class="mdescRight">References to empty objects (used in <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>) <a href="#ga4619bc6e35a273b89d30908c45d73348"></a><br/></td></tr>
<tr class="separator:ga4619bc6e35a273b89d30908c45d73348"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5b9a6dbadfbed96662a5b5d72e6001e2"><td class="memItemLeft" align="right" valign="top">const Expr & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga5b9a6dbadfbed96662a5b5d72e6001e2">CVC3::ExprManager::getNullExpr</a> ()</td></tr>
<tr class="memdesc:ga5b9a6dbadfbed96662a5b5d72e6001e2"><td class="mdescLeft"> </td><td class="mdescRight">References to empty objects (used in <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>) <a href="#ga5b9a6dbadfbed96662a5b5d72e6001e2"></a><br/></td></tr>
<tr class="separator:ga5b9a6dbadfbed96662a5b5d72e6001e2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga603f0df90a7c9695e010355f8ad8df43"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43">CVC3::ExprManager::newExpr</a> (ExprValue *ev)</td></tr>
<tr class="memdesc:ga603f0df90a7c9695e010355f8ad8df43"><td class="mdescLeft"> </td><td class="mdescRight">Return either an existing or a new <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> matching ev. <a href="#ga603f0df90a7c9695e010355f8ad8df43"></a><br/></td></tr>
<tr class="separator:ga603f0df90a7c9695e010355f8ad8df43"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacd77df1dbcc429e06a75047e2f609822"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gacd77df1dbcc429e06a75047e2f609822">CVC3::ExprManager::newLeafExpr</a> (const Op &op)</td></tr>
<tr class="separator:gacd77df1dbcc429e06a75047e2f609822"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3c1f298d2fdd7aaba48d000ca27df636"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">CVC3::ExprManager::newStringExpr</a> (const std::string &s)</td></tr>
<tr class="separator:ga3c1f298d2fdd7aaba48d000ca27df636"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga18423a42ce6557dc33287d3979ccc3c6"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">CVC3::ExprManager::newRatExpr</a> (const Rational &r)</td></tr>
<tr class="separator:ga18423a42ce6557dc33287d3979ccc3c6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf392ed0e07e505e56e551ce9cdaa76fe"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaf392ed0e07e505e56e551ce9cdaa76fe">CVC3::ExprManager::newSkolemExpr</a> (const Expr &e, int i)</td></tr>
<tr class="separator:gaf392ed0e07e505e56e551ce9cdaa76fe"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4d52ed373636679c2dd651d10822a3ee"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">CVC3::ExprManager::newVarExpr</a> (const std::string &s)</td></tr>
<tr class="separator:ga4d52ed373636679c2dd651d10822a3ee"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gafddb4551e9dbb163823b1162248e58f0"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gafddb4551e9dbb163823b1162248e58f0">CVC3::ExprManager::newSymbolExpr</a> (const std::string &s, int kind)</td></tr>
<tr class="separator:gafddb4551e9dbb163823b1162248e58f0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga22dbb23f716cc73378d4c69d564e38dd"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga22dbb23f716cc73378d4c69d564e38dd">CVC3::ExprManager::newBoundVarExpr</a> (const std::string &name, const std::string &uid)</td></tr>
<tr class="separator:ga22dbb23f716cc73378d4c69d564e38dd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga53f1a8180e8fcfead2537dd876c80682"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga53f1a8180e8fcfead2537dd876c80682">CVC3::ExprManager::newBoundVarExpr</a> (const std::string &name, const std::string &uid, const Type &type)</td></tr>
<tr class="separator:ga53f1a8180e8fcfead2537dd876c80682"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4a47e11b69e5a197d0437be8a632fa08"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga4a47e11b69e5a197d0437be8a632fa08">CVC3::ExprManager::newBoundVarExpr</a> (const Type &type)</td></tr>
<tr class="separator:ga4a47e11b69e5a197d0437be8a632fa08"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga0d2ff7603a249b30b2df4e549607ad6e"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">CVC3::ExprManager::newClosureExpr</a> (int kind, const Expr &var, const Expr &body)</td></tr>
<tr class="separator:ga0d2ff7603a249b30b2df4e549607ad6e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga349cd5c632090f97d1f03effcbb3ebe4"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga349cd5c632090f97d1f03effcbb3ebe4">CVC3::ExprManager::newClosureExpr</a> (int kind, const std::vector< Expr > &vars, const Expr &body)</td></tr>
<tr class="separator:ga349cd5c632090f97d1f03effcbb3ebe4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga99ccea65cb5a86a0ac3f671777f8812d"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga99ccea65cb5a86a0ac3f671777f8812d">CVC3::ExprManager::newClosureExpr</a> (int kind, const std::vector< Expr > &vars, const Expr &body, const Expr &trigger)</td></tr>
<tr class="separator:ga99ccea65cb5a86a0ac3f671777f8812d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9793cd1d6b44062a5ae5b8bd5e5f548d"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga9793cd1d6b44062a5ae5b8bd5e5f548d">CVC3::ExprManager::newClosureExpr</a> (int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers)</td></tr>
<tr class="separator:ga9793cd1d6b44062a5ae5b8bd5e5f548d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga47dd127b6737e1c0163fdf34cb5f1f15"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga47dd127b6737e1c0163fdf34cb5f1f15">CVC3::ExprManager::newClosureExpr</a> (int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers)</td></tr>
<tr class="separator:ga47dd127b6737e1c0163fdf34cb5f1f15"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga305b349b572c311b55a121e28392a714"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga305b349b572c311b55a121e28392a714">CVC3::ExprManager::andExpr</a> (const std::vector< Expr > &children)</td></tr>
<tr class="separator:ga305b349b572c311b55a121e28392a714"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga65c227873c06b36c509832506d690aaa"><td class="memItemLeft" align="right" valign="top">Expr </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga65c227873c06b36c509832506d690aaa">CVC3::ExprManager::orExpr</a> (const std::vector< Expr > &children)</td></tr>
<tr class="separator:ga65c227873c06b36c509832506d690aaa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa6b885e5372d6072b670831c4e577eff"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaa6b885e5372d6072b670831c4e577eff">CVC3::ExprManager::hash</a> (const Expr &e) const </td></tr>
<tr class="memdesc:gaa6b885e5372d6072b670831c4e577eff"><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="namespaceHash.html">Hash</a> function for a single <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="#gaa6b885e5372d6072b670831c4e577eff"></a><br/></td></tr>
<tr class="separator:gaa6b885e5372d6072b670831c4e577eff"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga50b20f4e775e01da9045fbea0762855b"><td class="memItemLeft" align="right" valign="top">ContextManager * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga50b20f4e775e01da9045fbea0762855b">CVC3::ExprManager::getCM</a> () const </td></tr>
<tr class="memdesc:ga50b20f4e775e01da9045fbea0762855b"><td class="mdescLeft"> </td><td class="mdescRight">Fetch our <a class="el" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>. <a href="#ga50b20f4e775e01da9045fbea0762855b"></a><br/></td></tr>
<tr class="separator:ga50b20f4e775e01da9045fbea0762855b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5f8daa1f01a0b3f30a3a147243411e5a"><td class="memItemLeft" align="right" valign="top">Context * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga5f8daa1f01a0b3f30a3a147243411e5a">CVC3::ExprManager::getCurrentContext</a> () const </td></tr>
<tr class="memdesc:ga5f8daa1f01a0b3f30a3a147243411e5a"><td class="mdescLeft"> </td><td class="mdescRight">Get the current context from our <a class="el" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>. <a href="#ga5f8daa1f01a0b3f30a3a147243411e5a"></a><br/></td></tr>
<tr class="separator:ga5f8daa1f01a0b3f30a3a147243411e5a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gafd98497270fdbd403d52b09cf95d0839"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gafd98497270fdbd403d52b09cf95d0839">CVC3::ExprManager::scopelevel</a> ()</td></tr>
<tr class="memdesc:gafd98497270fdbd403d52b09cf95d0839"><td class="mdescLeft"> </td><td class="mdescRight">Get current scope level. <a href="#gafd98497270fdbd403d52b09cf95d0839"></a><br/></td></tr>
<tr class="separator:gafd98497270fdbd403d52b09cf95d0839"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3a3060cbeb64eb97ac935f8f05a60f9b"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga3a3060cbeb64eb97ac935f8f05a60f9b">CVC3::ExprManager::setTM</a> (TheoremManager *tm)</td></tr>
<tr class="memdesc:ga3a3060cbeb64eb97ac935f8f05a60f9b"><td class="mdescLeft"> </td><td class="mdescRight">Set the <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. <a href="#ga3a3060cbeb64eb97ac935f8f05a60f9b"></a><br/></td></tr>
<tr class="separator:ga3a3060cbeb64eb97ac935f8f05a60f9b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4aa1269ec9df849a4b7654742408d2ca"><td class="memItemLeft" align="right" valign="top">TheoremManager * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga4aa1269ec9df849a4b7654742408d2ca">CVC3::ExprManager::getTM</a> () const </td></tr>
<tr class="memdesc:ga4aa1269ec9df849a4b7654742408d2ca"><td class="mdescLeft"> </td><td class="mdescRight">Fetch the <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. <a href="#ga4aa1269ec9df849a4b7654742408d2ca"></a><br/></td></tr>
<tr class="separator:ga4aa1269ec9df849a4b7654742408d2ca"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga721fc26fe37460f80e6d614cfe0d6fd8"><td class="memItemLeft" align="right" valign="top">MemoryManager * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga721fc26fe37460f80e6d614cfe0d6fd8">CVC3::ExprManager::getMM</a> (size_t MMIndex)</td></tr>
<tr class="memdesc:ga721fc26fe37460f80e6d614cfe0d6fd8"><td class="mdescLeft"> </td><td class="mdescRight">Return a <a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> for the given <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> type. <a href="#ga721fc26fe37460f80e6d614cfe0d6fd8"></a><br/></td></tr>
<tr class="separator:ga721fc26fe37460f80e6d614cfe0d6fd8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacacaaf5083e198a6014c2407c7f09cc0"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gacacaaf5083e198a6014c2407c7f09cc0">CVC3::ExprManager::getSimpCacheTag</a> () const </td></tr>
<tr class="memdesc:gacacaaf5083e198a6014c2407c7f09cc0"><td class="mdescLeft"> </td><td class="mdescRight">Get the simplifier's cache tag. <a href="#gacacaaf5083e198a6014c2407c7f09cc0"></a><br/></td></tr>
<tr class="separator:gacacaaf5083e198a6014c2407c7f09cc0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaba358e1731ad9309e52e64eb9ce60755"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaba358e1731ad9309e52e64eb9ce60755">CVC3::ExprManager::invalidateSimpCache</a> ()</td></tr>
<tr class="memdesc:gaba358e1731ad9309e52e64eb9ce60755"><td class="mdescLeft"> </td><td class="mdescRight">Invalidate the simplifier's cache tag. <a href="#gaba358e1731ad9309e52e64eb9ce60755"></a><br/></td></tr>
<tr class="separator:gaba358e1731ad9309e52e64eb9ce60755"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga39c8449d567e83ccd711cb2ff1a91dbf"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga39c8449d567e83ccd711cb2ff1a91dbf">CVC3::ExprManager::registerTypeComputer</a> (TypeComputer *typeComputer)</td></tr>
<tr class="memdesc:ga39c8449d567e83ccd711cb2ff1a91dbf"><td class="mdescLeft"> </td><td class="mdescRight">Register type computer. <a href="#ga39c8449d567e83ccd711cb2ff1a91dbf"></a><br/></td></tr>
<tr class="separator:ga39c8449d567e83ccd711cb2ff1a91dbf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga56fe351db38c3cc509ae6b1b9c2de000"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga56fe351db38c3cc509ae6b1b9c2de000">CVC3::ExprManager::printDepth</a> () const </td></tr>
<tr class="memdesc:ga56fe351db38c3cc509ae6b1b9c2de000"><td class="mdescLeft"> </td><td class="mdescRight">Get printing depth. <a href="#ga56fe351db38c3cc509ae6b1b9c2de000"></a><br/></td></tr>
<tr class="separator:ga56fe351db38c3cc509ae6b1b9c2de000"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3576f0cdcb0ab043d0612c7d9aff7ba1"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga3576f0cdcb0ab043d0612c7d9aff7ba1">CVC3::ExprManager::withIndentation</a> () const </td></tr>
<tr class="memdesc:ga3576f0cdcb0ab043d0612c7d9aff7ba1"><td class="mdescLeft"> </td><td class="mdescRight">Whether to print with indentation. <a href="#ga3576f0cdcb0ab043d0612c7d9aff7ba1"></a><br/></td></tr>
<tr class="separator:ga3576f0cdcb0ab043d0612c7d9aff7ba1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab624bd63ef4b189802f1708a41b2b3da"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gab624bd63ef4b189802f1708a41b2b3da">CVC3::ExprManager::lineWidth</a> () const </td></tr>
<tr class="memdesc:gab624bd63ef4b189802f1708a41b2b3da"><td class="mdescLeft"> </td><td class="mdescRight">Suggested line width for printing with indentation. <a href="#gab624bd63ef4b189802f1708a41b2b3da"></a><br/></td></tr>
<tr class="separator:gab624bd63ef4b189802f1708a41b2b3da"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga54ddb950b6bd35316d1cefe3fd506149"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga54ddb950b6bd35316d1cefe3fd506149">CVC3::ExprManager::indent</a> () const </td></tr>
<tr class="memdesc:ga54ddb950b6bd35316d1cefe3fd506149"><td class="mdescLeft"> </td><td class="mdescRight">Get initial indentation. <a href="#ga54ddb950b6bd35316d1cefe3fd506149"></a><br/></td></tr>
<tr class="separator:ga54ddb950b6bd35316d1cefe3fd506149"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga787e95a252f54b5fdb7c4d387ea49fae"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga787e95a252f54b5fdb7c4d387ea49fae">CVC3::ExprManager::indent</a> (int n, bool permanent=false)</td></tr>
<tr class="memdesc:ga787e95a252f54b5fdb7c4d387ea49fae"><td class="mdescLeft"> </td><td class="mdescRight">Set initial indentation. Returns the previous permanent value. <a href="#ga787e95a252f54b5fdb7c4d387ea49fae"></a><br/></td></tr>
<tr class="separator:ga787e95a252f54b5fdb7c4d387ea49fae"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf1a5a30e0f0ed0a3e59201530d39d49a"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaf1a5a30e0f0ed0a3e59201530d39d49a">CVC3::ExprManager::incIndent</a> (int n, bool permanent=false)</td></tr>
<tr class="memdesc:gaf1a5a30e0f0ed0a3e59201530d39d49a"><td class="mdescLeft"> </td><td class="mdescRight">Increment the current transient indentation by n. <a href="#gaf1a5a30e0f0ed0a3e59201530d39d49a"></a><br/></td></tr>
<tr class="separator:gaf1a5a30e0f0ed0a3e59201530d39d49a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3fe43b71bb148045c114e054934f5304"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga3fe43b71bb148045c114e054934f5304">CVC3::ExprManager::restoreIndent</a> ()</td></tr>
<tr class="memdesc:ga3fe43b71bb148045c114e054934f5304"><td class="mdescLeft"> </td><td class="mdescRight">Set transient indentation to permanent. <a href="#ga3fe43b71bb148045c114e054934f5304"></a><br/></td></tr>
<tr class="separator:ga3fe43b71bb148045c114e054934f5304"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae33e1c95930679cde944e2d2d5984db1"><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="group__EM__Priv.html#gae33e1c95930679cde944e2d2d5984db1">CVC3::ExprManager::getInputLang</a> () const </td></tr>
<tr class="memdesc:gae33e1c95930679cde944e2d2d5984db1"><td class="mdescLeft"> </td><td class="mdescRight">Get the input language for printing. <a href="#gae33e1c95930679cde944e2d2d5984db1"></a><br/></td></tr>
<tr class="separator:gae33e1c95930679cde944e2d2d5984db1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaeef110905b00e6e89f54c082e3c4c1a3"><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="group__EM__Priv.html#gaeef110905b00e6e89f54c082e3c4c1a3">CVC3::ExprManager::getOutputLang</a> () const </td></tr>
<tr class="memdesc:gaeef110905b00e6e89f54c082e3c4c1a3"><td class="mdescLeft"> </td><td class="mdescRight">Get the output language for printing. <a href="#gaeef110905b00e6e89f54c082e3c4c1a3"></a><br/></td></tr>
<tr class="separator:gaeef110905b00e6e89f54c082e3c4c1a3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab24afcec7ae8e33808eebf608193efd9"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gab24afcec7ae8e33808eebf608193efd9">CVC3::ExprManager::dagPrinting</a> () const </td></tr>
<tr class="memdesc:gab24afcec7ae8e33808eebf608193efd9"><td class="mdescLeft"> </td><td class="mdescRight">Whether to print <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>'s as DAGs. <a href="#gab24afcec7ae8e33808eebf608193efd9"></a><br/></td></tr>
<tr class="separator:gab24afcec7ae8e33808eebf608193efd9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3762b5bfe4264bd35b4e887084835fa6"><td class="memItemLeft" align="right" valign="top">PrettyPrinter * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga3762b5bfe4264bd35b4e887084835fa6">CVC3::ExprManager::getPrinter</a> () const </td></tr>
<tr class="memdesc:ga3762b5bfe4264bd35b4e887084835fa6"><td class="mdescLeft"> </td><td class="mdescRight">Return the pretty-printer if there is one; otherwise return NULL. <a href="#ga3762b5bfe4264bd35b4e887084835fa6"></a><br/></td></tr>
<tr class="separator:ga3762b5bfe4264bd35b4e887084835fa6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga2b0c6f8e83135e82ebe084188e390da1"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1">CVC3::ExprManager::newKind</a> (int kind, const std::string &name, bool isType=false)</td></tr>
<tr class="memdesc:ga2b0c6f8e83135e82ebe084188e390da1"><td class="mdescLeft"> </td><td class="mdescRight">Register a new kind. <a href="#ga2b0c6f8e83135e82ebe084188e390da1"></a><br/></td></tr>
<tr class="separator:ga2b0c6f8e83135e82ebe084188e390da1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacd01e4de3a171218d0192a9450fb7605"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gacd01e4de3a171218d0192a9450fb7605">CVC3::ExprManager::registerPrettyPrinter</a> (<a class="el" href="classCVC3_1_1PrettyPrinter.html">PrettyPrinter</a> &printer)</td></tr>
<tr class="memdesc:gacd01e4de3a171218d0192a9450fb7605"><td class="mdescLeft"> </td><td class="mdescRight">Register the pretty-printer (can only do it if none registered) <a href="#gacd01e4de3a171218d0192a9450fb7605"></a><br/></td></tr>
<tr class="separator:gacd01e4de3a171218d0192a9450fb7605"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4662ac518622beab3379f6da23380a75"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga4662ac518622beab3379f6da23380a75">CVC3::ExprManager::unregisterPrettyPrinter</a> ()</td></tr>
<tr class="memdesc:ga4662ac518622beab3379f6da23380a75"><td class="mdescLeft"> </td><td class="mdescRight">Tell <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> that the printer is no longer valid. <a href="#ga4662ac518622beab3379f6da23380a75"></a><br/></td></tr>
<tr class="separator:ga4662ac518622beab3379f6da23380a75"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c">CVC3::ExprManager::isKindRegistered</a> (int kind)</td></tr>
<tr class="memdesc:gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c"><td class="mdescLeft"> </td><td class="mdescRight">Returns true if kind is built into CVC or has been registered via newKind. <a href="#gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c"></a><br/></td></tr>
<tr class="separator:gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8e91326852cd6030a390fa3a29f6c8f9"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga8e91326852cd6030a390fa3a29f6c8f9">CVC3::ExprManager::isTypeKind</a> (int kind)</td></tr>
<tr class="memdesc:ga8e91326852cd6030a390fa3a29f6c8f9"><td class="mdescLeft"> </td><td class="mdescRight">Check if a kind represents a type. <a href="#ga8e91326852cd6030a390fa3a29f6c8f9"></a><br/></td></tr>
<tr class="separator:ga8e91326852cd6030a390fa3a29f6c8f9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad129f2ecc362f60ca43e06ff46b8521b"><td class="memItemLeft" align="right" valign="top">const std::string & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b">CVC3::ExprManager::getKindName</a> (int kind)</td></tr>
<tr class="memdesc:gad129f2ecc362f60ca43e06ff46b8521b"><td class="mdescLeft"> </td><td class="mdescRight">Return the name associated with a kind. The kind must already be registered. <a href="#gad129f2ecc362f60ca43e06ff46b8521b"></a><br/></td></tr>
<tr class="separator:gad129f2ecc362f60ca43e06ff46b8521b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9e7929fab9329724812e74b066a3c90a"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga9e7929fab9329724812e74b066a3c90a">CVC3::ExprManager::getKind</a> (const std::string &name)</td></tr>
<tr class="memdesc:ga9e7929fab9329724812e74b066a3c90a"><td class="mdescLeft"> </td><td class="mdescRight">Return a kind associated with a name. Returns NULL_KIND if not found. <a href="#ga9e7929fab9329724812e74b066a3c90a"></a><br/></td></tr>
<tr class="separator:ga9e7929fab9329724812e74b066a3c90a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga10284641fda307d52345f73e8ad5def0"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga10284641fda307d52345f73e8ad5def0">CVC3::ExprManager::registerSubclass</a> (size_t sizeOfSubclass)</td></tr>
<tr class="memdesc:ga10284641fda307d52345f73e8ad5def0"><td class="mdescLeft"> </td><td class="mdescRight">Register a new subclass of <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>. <a href="#ga10284641fda307d52345f73e8ad5def0"></a><br/></td></tr>
<tr class="separator:ga10284641fda307d52345f73e8ad5def0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa4b16553ca47bb59c3978be771a5766b"><td class="memItemLeft" align="right" valign="top">unsigned long </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaa4b16553ca47bb59c3978be771a5766b">CVC3::ExprManager::getMemory</a> (int verbosity)</td></tr>
<tr class="memdesc:gaa4b16553ca47bb59c3978be771a5766b"><td class="mdescLeft"> </td><td class="mdescRight">Calculate memory usage. <a href="#gaa4b16553ca47bb59c3978be771a5766b"></a><br/></td></tr>
<tr class="separator:gaa4b16553ca47bb59c3978be771a5766b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8150de408f4d5aec9ceddabf86b30cf3"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga8150de408f4d5aec9ceddabf86b30cf3">CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj</a> (ExprManager *em, Context *cxt)</td></tr>
<tr class="memdesc:ga8150de408f4d5aec9ceddabf86b30cf3"><td class="mdescLeft"> </td><td class="mdescRight">Constructor. <a href="#ga8150de408f4d5aec9ceddabf86b30cf3"></a><br/></td></tr>
<tr class="separator:ga8150de408f4d5aec9ceddabf86b30cf3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac681a5cd1f70dda8a7a391439d887c2d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gac681a5cd1f70dda8a7a391439d887c2d">CVC3::ExprManagerNotifyObj::notifyPre</a> (void)</td></tr>
<tr class="separator:gac681a5cd1f70dda8a7a391439d887c2d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gadd71c522283037f94526bda8f73a8bbd"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gadd71c522283037f94526bda8f73a8bbd">CVC3::ExprManagerNotifyObj::notify</a> (void)</td></tr>
<tr class="separator:gadd71c522283037f94526bda8f73a8bbd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga083141d49f93f86b917f6a99f239d2c8"><td class="memItemLeft" align="right" valign="top">unsigned long </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga083141d49f93f86b917f6a99f239d2c8">CVC3::ExprManagerNotifyObj::getMemory</a> (int verbosity)</td></tr>
<tr class="separator:ga083141d49f93f86b917f6a99f239d2c8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac4a0d5785aa3427b482ab07dff8b5609"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gac4a0d5785aa3427b482ab07dff8b5609">CVC3::ExprManager::hash</a> (const ExprValue *ev) const </td></tr>
<tr class="separator:gac4a0d5785aa3427b482ab07dff8b5609"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="var-members"></a>
Variables</h2></td></tr>
<tr class="memitem:ga727d1263f81f01e526042f38ec668caa"><td class="memItemLeft" align="right" valign="top"><a class="el" href="structHash_1_1hash.html">std::hash</a>< char * > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga727d1263f81f01e526042f38ec668caa">CVC3::ExprManager::HashString::h</a></td></tr>
<tr class="separator:ga727d1263f81f01e526042f38ec668caa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa8b0387e58616954916858e296de4449"><td class="memItemLeft" align="right" valign="top">ExprManager * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#gaa8b0387e58616954916858e296de4449">CVC3::ExprManager::HashEV::d_em</a></td></tr>
<tr class="separator:gaa8b0387e58616954916858e296de4449"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5b95d2473f4230b72cc27b090500552f"><td class="memItemLeft" align="right" valign="top">ExprManager * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__EM__Priv.html#ga5b95d2473f4230b72cc27b090500552f">CVC3::ExprManagerNotifyObj::d_em</a></td></tr>
<tr class="separator:ga5b95d2473f4230b72cc27b090500552f"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<h2 class="groupheader">Function Documentation</h2>
<a class="anchor" id="ga9fe970ca9a02174a617bce9797d41815"></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::ExprManager::HashString::operator() </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>s</em></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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00079">79</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="gaabb82d3abf0072c71761ca599ba9a8fa"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::ExprManager::HashEV::HashEV </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>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00119">119</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="gac8adf717113c11ce0bc84160d17bea7a"></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::ExprManager::HashEV::operator() </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * </td>
<td class="paramname"><em>ev</em></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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00120">120</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga4a8fa9169728473cc4db3f96d467544f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprManager::EqEV::operator() </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * </td>
<td class="paramname"><em>ev1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * </td>
<td class="paramname"><em>ev2</em> </td>
</tr>
<tr>
<td></td>
<td>)</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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00537">537</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="gaf4397d9b6d23d0e4b9112b509d9dfad4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::ExprManager::TypeComputer::TypeComputer </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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00185">185</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="gaee11e07336c1b8704409d42c0aaeafad"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::ExprManager::TypeComputer::~TypeComputer </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 class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00186">186</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga670ca72899c66da598ea568af7389407"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::ExprManager::TypeComputer::computeType </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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Compute the type of e. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1TypeComputerCore.html#a9223b9b2cd88316afa84855a698b1c4c">CVC3::TypeComputerCore</a>.</p>
<p>Referenced by <a class="el" href="expr__manager_8cpp_source.html#l00465">CVC3::ExprManager::computeType()</a>.</p>
</div>
</div>
<a class="anchor" id="gae679c021fb433f86c28c5eec68e5b5ee"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::ExprManager::TypeComputer::checkType </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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Check that e is a valid <a class="el" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> expr. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1TypeComputerCore.html#a13bfb35575699b39b635e7eefce51c6a">CVC3::TypeComputerCore</a>.</p>
<p>Referenced by <a class="el" href="expr__manager_8cpp_source.html#l00472">CVC3::ExprManager::checkType()</a>.</p>
</div>
</div>
<a class="anchor" id="ga13e9c0f4a23614e99705f60e3913c2b1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual Cardinality CVC3::ExprManager::TypeComputer::finiteTypeInfo </td>
<td>(</td>
<td class="paramtype"><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_1Unsigned.html">Unsigned</a> & </td>
<td class="paramname"><em>n</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>enumerate</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>computeSize</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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get information related to finiteness of a type. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1TypeComputerCore.html#a6ee7730c9d296140e2870359967cb8f5">CVC3::TypeComputerCore</a>.</p>
<p>Referenced by <a class="el" href="expr__manager_8cpp_source.html#l00479">CVC3::ExprManager::finiteTypeInfo()</a>.</p>
</div>
</div>
<a class="anchor" id="gaa86d7ed7800549f1621d2d5ce64ce643"></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> ExprManager::rebuildRec </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>Cached recursive descent. Must be called only during <a class="el" href="group__EM__Priv.html#gacaab5ccf5cf81d11185979051d301d5e" title="Rebuild the Expr with this ExprManager if it belongs to another ExprManager.">rebuild()</a> </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00251">251</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00197">CVC3::Expr::d_expr</a>, <a class="el" href="expr__manager_8h_source.html#l00131">CVC3::ExprManager::d_exprSet</a>, <a class="el" href="expr__manager_8h_source.html#l00178">CVC3::ExprManager::d_rebuildCache</a>, <a class="el" href="expr__value_8h_source.html#l00094">CVC3::ExprValue::d_type</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">CVC3::MemoryManager::deleteData()</a>, <a class="el" href="hash__set_8h_source.html#l00235">Hash::hash_set< _Key, _HashFcn, _EqualKey >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00326">CVC3::ExprHashMap< Data >::end()</a>, <a class="el" href="hash__set_8h_source.html#l00161">Hash::hash_set< _Key, _HashFcn, _EqualKey >::find()</a>, <a class="el" href="expr__map_8h_source.html#l00329">CVC3::ExprHashMap< Data >::find()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr__manager_8h_source.html#l00334">CVC3::ExprManager::getMM()</a>, <a class="el" href="hash__set_8h_source.html#l00173">Hash::hash_set< _Key, _HashFcn, _EqualKey >::insert()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="expr__manager_8h_source.html#l00268">CVC3::ExprManager::nextIndex()</a>, <a class="el" href="expr__value_8h_source.html#l00201">CVC3::ExprValue::rebuild()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="expr__manager_8h_source.html#l00063">CVC3::ExprManager::Type</a>.</p>
<p>Referenced by <a class="el" href="expr__value_8h_source.html#l00205">CVC3::ExprValue::rebuild()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00226">CVC3::ExprManager::rebuild()</a>.</p>
</div>
</div>
<a class="anchor" id="ga3c693890e6e6e1610c44dda553dbf803"></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_1ExprValue.html">ExprValue</a> * ExprManager::newExprValue </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * </td>
<td class="paramname"><em>ev</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>Return either an existing or a new <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> matching ev. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00288">288</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8cpp_source.html#l00078">CVC3::ExprValue::copy()</a>, <a class="el" href="expr__manager_8h_source.html#l00131">CVC3::ExprManager::d_exprSet</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="hash__set_8h_source.html#l00235">Hash::hash_set< _Key, _HashFcn, _EqualKey >::end()</a>, <a class="el" href="hash__set_8h_source.html#l00161">Hash::hash_set< _Key, _HashFcn, _EqualKey >::find()</a>, <a class="el" href="hash__set_8h_source.html#l00173">Hash::hash_set< _Key, _HashFcn, _EqualKey >::insert()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00184">CVC3::ExprManager::isActive()</a>, and <a class="el" href="expr__manager_8h_source.html#l00268">CVC3::ExprManager::nextIndex()</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l00830">CVC3::Expr::Expr()</a>.</p>
</div>
</div>
<a class="anchor" id="gacaa71017958e2e9d069c055248c8dd78"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::ExprManager::getFlag </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 class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Return the current <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> flag counter. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00213">213</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l01395">CVC3::Expr::setFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="gab5336831e8006e69a57f9c1b728138f6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::ExprManager::nextFlag </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 class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Increment and return the <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> flag counter (this clears all the flags) </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00215">215</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>.</p>
</div>
</div>
<a class="anchor" id="ga15e87e829f86a1dcf2c5e05be6f4d182"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void ExprManager::computeType </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>Compute the type of the <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__manager_8cpp_source.html#l00465">465</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="group__EM__Priv.html#ga670ca72899c66da598ea568af7389407">CVC3::ExprManager::TypeComputer::computeType()</a>, <a class="el" href="expr__manager_8h_source.html#l00197">CVC3::ExprManager::d_typeComputer</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, and <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>.</p>
</div>
</div>
<a class="anchor" id="ga51109c3e331615c510c964798b38ee95"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void ExprManager::checkType </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>Check well-formedness of a type <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__manager_8cpp_source.html#l00472">472</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="group__EM__Priv.html#gae679c021fb433f86c28c5eec68e5b5ee">CVC3::ExprManager::TypeComputer::checkType()</a>, <a class="el" href="expr__manager_8h_source.html#l00197">CVC3::ExprManager::d_typeComputer</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="expr_8h_source.html#l01302">CVC3::Expr::isValidType()</a>.</p>
<p>Referenced by <a class="el" href="expr_8cpp_source.html#l00634">CVC3::Type::Type()</a>.</p>
</div>
</div>
<a class="anchor" id="gae5cc4c6a7dfcc718c7c931e6b160d9d1"></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#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> ExprManager::finiteTypeInfo </td>
<td>(</td>
<td class="paramtype"><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_1Unsigned.html">Unsigned</a> & </td>
<td class="paramname"><em>n</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>enumerate</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>computeSize</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>Get information related to finiteness of a type. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00479">479</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00197">CVC3::ExprManager::d_typeComputer</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="group__EM__Priv.html#ga13e9c0f4a23614e99705f60e3913c2b1">CVC3::ExprManager::TypeComputer::finiteTypeInfo()</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l01270">CVC3::Expr::typeCard()</a>, <a class="el" href="expr_8h_source.html#l01277">CVC3::Expr::typeEnumerateFinite()</a>, and <a class="el" href="expr_8h_source.html#l01285">CVC3::Expr::typeSizeFinite()</a>.</p>
</div>
</div>
<a class="anchor" id="gaf3af8657f4b2c64f189f0a50147d3589"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprManager::ExprManager </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a> * </td>
<td class="paramname"><em>cm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1CLFlags.html">CLFlags</a> & </td>
<td class="paramname"><em>flags</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Constructor. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00070">70</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00048">BOOLEAN</a>, <a class="el" href="expr__manager_8h_source.html#l00139">CVC3::ExprManager::d_bool</a>, <a class="el" href="expr__manager_8h_source.html#l00065">CVC3::ExprManager::d_cm</a>, <a class="el" href="expr__manager_8h_source.html#l00140">CVC3::ExprManager::d_false</a>, <a class="el" href="expr__manager_8h_source.html#l00133">CVC3::ExprManager::d_mm</a>, <a class="el" href="expr__manager_8h_source.html#l00113">CVC3::ExprManager::d_mmFlag</a>, <a class="el" href="expr__manager_8h_source.html#l00067">CVC3::ExprManager::d_notifyObj</a>, <a class="el" href="expr__manager_8h_source.html#l00141">CVC3::ExprManager::d_true</a>, <a class="el" href="expr_8h_source.html#l00068">CVC3::EXPR_APPLY</a>, <a class="el" href="expr_8h_source.html#l00074">CVC3::EXPR_BOUND_VAR</a>, <a class="el" href="expr_8h_source.html#l00075">CVC3::EXPR_CLOSURE</a>, <a class="el" href="expr_8h_source.html#l00067">CVC3::EXPR_NODE</a>, <a class="el" href="expr_8h_source.html#l00070">CVC3::EXPR_RATIONAL</a>, <a class="el" href="expr_8h_source.html#l00071">CVC3::EXPR_SKOLEM</a>, <a class="el" href="expr_8h_source.html#l00069">CVC3::EXPR_STRING</a>, <a class="el" href="expr_8h_source.html#l00073">CVC3::EXPR_SYMBOL</a>, <a class="el" href="expr_8h_source.html#l00072">CVC3::EXPR_UCONST</a>, <a class="el" href="expr_8h_source.html#l00066">CVC3::EXPR_VALUE</a>, <a class="el" href="kinds_8h_source.html#l00036">FALSE_EXPR</a>, <a class="el" href="context_8h_source.html#l00406">CVC3::ContextManager::getCurrentContext()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="expr__manager_8h_source.html#l00454">CVC3::ExprManager::newLeafExpr()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00493">registerKinds()</a>, <a class="el" href="expr_8h_source.html#l01427">CVC3::Expr::setType()</a>, <a class="el" href="kinds_8h_source.html#l00035">TRUE_EXPR</a>, and <a class="el" href="type_8h_source.html#l00073">CVC3::Type::typeBool()</a>.</p>
<p>Referenced by <a class="el" href="expr__manager_8cpp_source.html#l00433">CVC3::ExprManager::getMemory()</a>.</p>
</div>
</div>
<a class="anchor" id="ga318254064b65faf57e1657b680688bc7"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprManager::~ExprManager </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Destructor. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00125">125</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8cpp_source.html#l00141">CVC3::ExprManager::clear()</a>, <a class="el" href="expr__manager_8h_source.html#l00159">CVC3::ExprManager::d_disableGC</a>, <a class="el" href="expr__manager_8h_source.html#l00143">CVC3::ExprManager::d_emptyVec</a>, <a class="el" href="expr__manager_8h_source.html#l00133">CVC3::ExprManager::d_mm</a>, <a class="el" href="expr__manager_8h_source.html#l00067">CVC3::ExprManager::d_notifyObj</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
</div>
</div>
<a class="anchor" id="ga9bddd7eaf6f198476eda3cd55227f384"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprManager::clear </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Free up all memory and delete all the expressions. </p>
<p>No more expressions can be created after this point, only destructors ~Expr() can be called.</p>
<p>This method is needed to dis-entangle the mutual dependency of <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> and <a class="el" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>, when destructors of <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> (sub)classes need to delete backtracking objects, and deleting the <a class="el" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a> requires destruction of some remaining Exprs. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00141">141</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="hash__set_8h_source.html#l00224">Hash::hash_set< _Key, _HashFcn, _EqualKey >::begin()</a>, <a class="el" href="hash__set_8h_source.html#l00151">Hash::hash_set< _Key, _HashFcn, _EqualKey >::clear()</a>, <a class="el" href="expr__manager_8h_source.html#l00139">CVC3::ExprManager::d_bool</a>, <a class="el" href="expr__manager_8h_source.html#l00159">CVC3::ExprManager::d_disableGC</a>, <a class="el" href="expr__manager_8h_source.html#l00131">CVC3::ExprManager::d_exprSet</a>, <a class="el" href="expr__manager_8h_source.html#l00140">CVC3::ExprManager::d_false</a>, <a class="el" href="expr__manager_8h_source.html#l00133">CVC3::ExprManager::d_mm</a>, <a class="el" href="expr__manager_8h_source.html#l00145">CVC3::ExprManager::d_nullExpr</a>, <a class="el" href="expr__manager_8h_source.html#l00141">CVC3::ExprManager::d_true</a>, <a class="el" href="hash__set_8h_source.html#l00235">Hash::hash_set< _Key, _HashFcn, _EqualKey >::end()</a>, <a class="el" href="expr__manager_8h_source.html#l00059">CVC3::ExprManager::Expr</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="expr__value_8h_source.html#l00263">CVC3::ExprValue::getMMIndex()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="expr__manager_8cpp_source.html#l00184">CVC3::ExprManager::isActive()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="hash__set_8h_source.html#l00205">Hash::hash_set< _Key, _HashFcn, _EqualKey >::size()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
<p>Referenced by <a class="el" href="expr__manager_8cpp_source.html#l00125">CVC3::ExprManager::~ExprManager()</a>.</p>
</div>
</div>
<a class="anchor" id="gaaec477005a23531fa15d27282658aab8"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool ExprManager::isActive </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Check if the <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> is still active (<a class="el" href="group__EM__Priv.html#ga9bddd7eaf6f198476eda3cd55227f384" title="Free up all memory and delete all the expressions.">clear()</a> was not called) </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00184">184</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00159">CVC3::ExprManager::d_disableGC</a>.</p>
<p>Referenced by <a class="el" href="expr__manager_8cpp_source.html#l00141">CVC3::ExprManager::clear()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00288">CVC3::ExprManager::newExprValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">CVC3::Theorem::print()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00226">CVC3::ExprManager::rebuild()</a>.</p>
</div>
</div>
<a class="anchor" id="ga5878c4fbe700243540dc835b965fd01b"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprManager::gc </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * </td>
<td class="paramname"><em>ev</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Garbage collect the <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> pointer. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00188">188</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00159">CVC3::ExprManager::d_disableGC</a>, <a class="el" href="expr__manager_8h_source.html#l00131">CVC3::ExprManager::d_exprSet</a>, <a class="el" href="expr__manager_8h_source.html#l00173">CVC3::ExprManager::d_inGC</a>, <a class="el" href="expr__manager_8h_source.html#l00133">CVC3::ExprManager::d_mm</a>, <a class="el" href="expr__manager_8h_source.html#l00175">CVC3::ExprManager::d_pending</a>, <a class="el" href="expr__manager_8h_source.html#l00170">CVC3::ExprManager::d_postponed</a>, <a class="el" href="expr__manager_8h_source.html#l00168">CVC3::ExprManager::d_postponeGC</a>, <a class="el" href="hash__set_8h_source.html#l00180">Hash::hash_set< _Key, _HashFcn, _EqualKey >::erase()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="expr__value_8h_source.html#l00263">CVC3::ExprValue::getMMIndex()</a>, and <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l00985">CVC3::Expr::~Expr()</a>.</p>
</div>
</div>
<a class="anchor" id="ga9c35426ab6885b609e84a4be9b30effc"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprManager::postponeGC </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>Postpone deletion of garbage-collected expressions. </p>
<dl class="section see"><dt>See Also</dt><dd><a class="el" href="group__EM__Priv.html#gafd44d7be33c1111722aa7bb9f3b8b2e9" title="Resume deletion of garbage-collected expressions.">resumeGC()</a> </dd></dl>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00257">257</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="gafd44d7be33c1111722aa7bb9f3b8b2e9"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprManager::resumeGC </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Resume deletion of garbage-collected expressions. </p>
<dl class="section see"><dt>See Also</dt><dd><a class="el" href="group__EM__Priv.html#ga9c35426ab6885b609e84a4be9b30effc" title="Postpone deletion of garbage-collected expressions.">postponeGC()</a> </dd></dl>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00212">212</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00133">CVC3::ExprManager::d_mm</a>, <a class="el" href="expr__manager_8h_source.html#l00170">CVC3::ExprManager::d_postponed</a>, <a class="el" href="expr__manager_8h_source.html#l00168">CVC3::ExprManager::d_postponeGC</a>, and <a class="el" href="expr__value_8h_source.html#l00263">CVC3::ExprValue::getMMIndex()</a>.</p>
</div>
</div>
<a class="anchor" id="gacaab5ccf5cf81d11185979051d301d5e"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> ExprManager::rebuild </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>
</div><div class="memdoc">
<p>Rebuild the <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> with this <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> if it belongs to another <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a>. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00226">226</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__map_8h_source.html#l00310">CVC3::ExprHashMap< Data >::clear()</a>, <a class="el" href="expr__manager_8h_source.html#l00178">CVC3::ExprManager::d_rebuildCache</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01156">CVC3::Expr::getEM()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="expr__manager_8cpp_source.html#l00184">CVC3::ExprManager::isActive()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00251">CVC3::ExprManager::rebuildRec()</a>, and <a class="el" href="expr__map_8h_source.html#l00306">CVC3::ExprHashMap< Data >::size()</a>.</p>
<p>Referenced by <a class="el" href="expr__op_8cpp_source.html#l00027">CVC3::Op::Op()</a>, and <a class="el" href="expr_8h_source.html#l00981">CVC3::Expr::rebuild()</a>.</p>
</div>
</div>
<a class="anchor" id="ga212f07de6befabee47e4f9a1813e7c44"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">ExprIndex CVC3::ExprManager::nextIndex </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>Return the next <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> index. </p>
<p>It should be used only by <a class="el" href="classCVC3_1_1ExprManager.html#a6b4e0ce748563841be8fe35c34ee7975">ExprValue()</a> constructor </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00268">268</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr__manager_8cpp_source.html#l00288">CVC3::ExprManager::newExprValue()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00251">CVC3::ExprManager::rebuildRec()</a>.</p>
</div>
</div>
<a class="anchor" id="gac64badd3988c01f34e43f227902e80f1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">ExprIndex CVC3::ExprManager::lastIndex </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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00269">269</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l01175">CVC3::Expr::hasLastIndex()</a>.</p>
</div>
</div>
<a class="anchor" id="gab4b3f2259b5c0af2251741139ea9d952"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprManager::clearFlags </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>Clears the generic <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> flag in all Exprs. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00272">272</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l01400">CVC3::Expr::clearFlags()</a>, and <a class="el" href="theory__core_8cpp_source.html#l04204">IF_DEBUG()</a>.</p>
</div>
</div>
<a class="anchor" id="gab01fe102500e6b4e266299bf4bbb8a20"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const Expr& CVC3::ExprManager::boolExpr </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>BOOLEAN <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__manager_8h_source.html#l00276">276</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l01724">CVC3::TheoryCore::parseExprOp()</a>, and <a class="el" href="type_8h_source.html#l00073">CVC3::Type::typeBool()</a>.</p>
</div>
</div>
<a class="anchor" id="gaae9db4c93c67cbf8bbf5d1e60e94f1ae"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const Expr& CVC3::ExprManager::falseExpr </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>FALSE <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__manager_8h_source.html#l00278">278</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theory__simulate_8cpp_source.html#l00164">CVC3::TheorySimulate::computeTCC()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00744">CVC3::SearchEngineTheoremProducer::confAndrAF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00711">CVC3::SearchEngineTheoremProducer::confAndrAT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00834">CVC3::SearchEngineTheoremProducer::confIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01059">CVC3::SearchEngineTheoremProducer::confIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01012">CVC3::SearchEngineTheoremProducer::confIterThenElse()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01109">CVC3::SearchEngineTheoremProducer::conflictRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00561">CVC3::CommonTheoremProducer::contradictionRule()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="theory_8h_source.html#l00579">CVC3::Theory::falseExpr()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00602">CVC3::CommonTheoremProducer::iffNotFalse()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00906">CVC3::CommonTheoremProducer::notToIff()</a>, <a class="el" href="theory__core_8cpp_source.html#l01724">CVC3::TheoryCore::parseExprOp()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00365">LFSCObj::queryAtomic()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00989">CVC3::CommonTheoremProducer::rewriteAnd()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00941">CVC3::CommonTheoremProducer::rewriteIff()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01066">CVC3::CommonTheoremProducer::rewriteNotTrue()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01028">CVC3::CommonTheoremProducer::rewriteOr()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00476">CVC3::ExprTransform::simplifyWithCare()</a>, and <a class="el" href="LFSCObject_8cpp_source.html#l00539">LFSCObj::what_is_proven()</a>.</p>
</div>
</div>
<a class="anchor" id="ga4471fca49c2acbb7b4cf71e72bc55d6a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const Expr& CVC3::ExprManager::trueExpr </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>TRUE <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__manager_8h_source.html#l00280">280</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l03449">CVC3::TheoryCore::computeModelBasic()</a>, <a class="el" href="theory__simulate_8cpp_source.html#l00164">CVC3::TheorySimulate::computeTCC()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01860">CVC3::TheoryArithNew::computeTypePred()</a>, <a class="el" href="theory_8h_source.html#l00275">CVC3::Theory::computeTypePred()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03411">CVC3::TheoryBitvector::computeTypePred()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02625">CVC3::TheoryArith3::computeTypePred()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03603">CVC3::TheoryArithOld::computeTypePred()</a>, <a class="el" href="theory__core_8cpp_source.html#l01704">CVC3::TheoryCore::computeTypePred()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00448">LFSCObj::getY()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00591">CVC3::CommonTheoremProducer::iffTrue()</a>, <a class="el" href="theory__core_8cpp_source.html#l01724">CVC3::TheoryCore::parseExprOp()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00408">CVC3::QuantTheoremProducer::partialUniversalInst()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00365">LFSCObj::queryAtomic()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00989">CVC3::CommonTheoremProducer::rewriteAnd()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00297">CVC3::CoreTheoremProducer::rewriteDistinct()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01078">CVC3::CommonTheoremProducer::rewriteNotFalse()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01028">CVC3::CommonTheoremProducer::rewriteOr()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00168">CVC3::CommonTheoremProducer::rewriteReflexivity()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00476">CVC3::ExprTransform::simplifyWithCare()</a>, <a class="el" href="theory_8h_source.html#l00582">CVC3::Theory::trueExpr()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01280">CVC3::CommonTheoremProducer::trueTheorem()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00154">CVC3::QuantTheoremProducer::universalInst()</a>, and <a class="el" href="LFSCObject_8cpp_source.html#l00539">LFSCObj::what_is_proven()</a>.</p>
</div>
</div>
<a class="anchor" id="ga4619bc6e35a273b89d30908c45d73348"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const std::vector<Expr>& CVC3::ExprManager::getEmptyVector </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>References to empty objects (used in <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>) </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00282">282</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, and <a class="el" href="expr_8h_source.html#l01162">CVC3::Expr::getKids()</a>.</p>
</div>
</div>
<a class="anchor" id="ga5b9a6dbadfbed96662a5b5d72e6001e2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const Expr& CVC3::ExprManager::getNullExpr </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>References to empty objects (used in <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>) </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00284">284</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga603f0df90a7c9695e010355f8ad8df43"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newExpr </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * </td>
<td class="paramname"><em>ev</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>Return either an existing or a new <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> matching ev. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00289">289</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr__manager_8h_source.html#l00484">CVC3::ExprManager::newBoundVarExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05172">CVC3::TheoryBitvector::newBVConstExpr()</a>, <a class="el" href="expr__manager_8h_source.html#l00506">CVC3::ExprManager::newClosureExpr()</a>, <a class="el" href="expr__manager_8h_source.html#l00454">CVC3::ExprManager::newLeafExpr()</a>, <a class="el" href="expr__manager_8h_source.html#l00471">CVC3::ExprManager::newRatExpr()</a>, <a class="el" href="expr__manager_8h_source.html#l00474">CVC3::ExprManager::newSkolemExpr()</a>, <a class="el" href="expr__manager_8h_source.html#l00468">CVC3::ExprManager::newStringExpr()</a>, <a class="el" href="expr__manager_8h_source.html#l00481">CVC3::ExprManager::newSymbolExpr()</a>, and <a class="el" href="expr__manager_8h_source.html#l00478">CVC3::ExprManager::newVarExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="gacd77df1dbcc429e06a75047e2f609822"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newLeafExpr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Op.html">Op</a> & </td>
<td class="paramname"><em>op</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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00454">454</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00090">APPLY</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01156">CVC3::Expr::getEM()</a>, <a class="el" href="expr__op_8h_source.html#l00084">CVC3::Op::getExpr()</a>, <a class="el" href="expr__op_8h_source.html#l00082">CVC3::Op::getKind()</a>, and <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00093">CVC3::ExprStream::addLetHeader()</a>, <a class="el" href="type_8h_source.html#l00074">CVC3::Type::anyType()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00454">CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00070">CVC3::ExprManager::ExprManager()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l02040">CVC3::TheoryArithNew::parseExprOp()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02855">CVC3::TheoryArith3::parseExprOp()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03833">CVC3::TheoryArithOld::parseExprOp()</a>, <a class="el" href="theory__core_8cpp_source.html#l01724">CVC3::TheoryCore::parseExprOp()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00373">CVC3::CommonTheoremProducer::substitutivityRule()</a>, and <a class="el" href="theorem__producer_8cpp_source.html#l00044">CVC3::TheoremProducer::TheoremProducer()</a>.</p>
</div>
</div>
<a class="anchor" id="ga3c1f298d2fdd7aaba48d000ca27df636"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newStringExpr </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>s</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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00468">468</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">CVC3::Translator::finish()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00104">LFSCObj::initialize()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l00140">CVC3::TheoryQuant::TheoryQuant()</a>.</p>
</div>
</div>
<a class="anchor" id="ga18423a42ce6557dc33287d3979ccc3c6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newRatExpr </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><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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00471">471</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l00718">CVC3::CommonTheoremProducer::andElim()</a>, <a class="el" href="LFSCConvert_8cpp_source.html#l00093">LFSCConvert::cvc3_to_lfsc()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02229">CVC3::CompleteInstPreProcessor::inst()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01827">CVC3::CompleteInstPreProcessor::minusOne()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01822">CVC3::CompleteInstPreProcessor::plusOne()</a>, <a class="el" href="arith__theorem__producer3_8h_source.html#l00070">CVC3::ArithTheoremProducer3::rat()</a>, <a class="el" href="arith__theorem__producer__old_8h_source.html#l00070">CVC3::ArithTheoremProducerOld::rat()</a>, <a class="el" href="arith__theorem__producer_8h_source.html#l00071">CVC3::ArithTheoremProducer::rat()</a>, <a class="el" href="theory__arith_8h_source.html#l00156">CVC3::TheoryArith::rat()</a>, <a class="el" href="theory__bitvector_8h_source.html#l00300">CVC3::TheoryBitvector::rat()</a>, <a class="el" href="bitvector__theorem__producer_8h_source.html#l00486">CVC3::BitvectorTheoremProducer::rat()</a>, and <a class="el" href="LFSCObject_8cpp_source.html#l00539">LFSCObj::what_is_proven()</a>.</p>
</div>
</div>
<a class="anchor" id="gaf392ed0e07e505e56e551ce9cdaa76fe"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newSkolemExpr </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">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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00474">474</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01156">CVC3::Expr::getEM()</a>, and <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l00977">CVC3::Expr::skolemExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="ga4d52ed373636679c2dd651d10822a3ee"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newVarExpr </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>s</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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00478">478</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00093">CVC3::ExprStream::addLetHeader()</a>, <a class="el" href="theory__quant_8cpp_source.html#l07647">CVC3::TheoryQuant::checkSat()</a>, <a class="el" href="LFSCObject_8cpp_source.html#l00104">LFSCObj::initialize()</a>, <a class="el" href="theory_8cpp_source.html#l00776">CVC3::Theory::lookupVar()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, and <a class="el" href="theory_8cpp_source.html#l00569">CVC3::Theory::newVar()</a>.</p>
</div>
</div>
<a class="anchor" id="gafddb4551e9dbb163823b1162248e58f0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newSymbolExpr </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>s</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00481">481</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00878">CVC3::TheoryDatatype::dataType()</a>, <a class="el" href="theory_8cpp_source.html#l00697">CVC3::Theory::lookupFunction()</a>, <a class="el" href="theory_8cpp_source.html#l00647">CVC3::Theory::newFunction()</a>, <a class="el" href="theory_8cpp_source.html#l00569">CVC3::Theory::newVar()</a>, and <a class="el" href="translator_8cpp_source.html#l01850">CVC3::Translator::printArrayExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="ga22dbb23f716cc73378d4c69d564e38dd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newBoundVarExpr </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>name</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>uid</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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00484">484</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>.</p>
<p>Referenced by <a class="el" href="array__theorem__producer_8cpp_source.html#l00338">CVC3::ArrayTheoremProducer::arrayNotEq()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06272">CVC3::BitvectorTheoremProducer::bvUDivTheorem()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00509">CVC3::TheoryUF::computeModel()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01382">CVC3::SearchEngineTheoremProducer::findInLocalCache()</a>, <a class="el" href="expr__manager_8h_source.html#l00488">CVC3::ExprManager::newBoundVarExpr()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00052">CVC3::TheoremProducer::newLabel()</a>, <a class="el" href="theory_8cpp_source.html#l00816">CVC3::Theory::newSubtypeExpr()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00082">CVC3::QuantTheoremProducer::normalizeQuant()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l05609">CVC3::BitvectorTheoremProducer::processExtract()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06713">CVC3::BitvectorTheoremProducer::solveExtractOverlap()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00140">CVC3::TheoryQuant::TheoryQuant()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l01202">CVC3::CommonTheoremProducer::varIntroRule()</a>.</p>
</div>
</div>
<a class="anchor" id="ga53f1a8180e8fcfead2537dd876c80682"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newBoundVarExpr </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>name</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>uid</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>type</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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00488">488</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00051">ARROW</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="expr_8h_source.html#l01265">CVC3::Expr::lookupType()</a>, <a class="el" href="expr__manager_8h_source.html#l00484">CVC3::ExprManager::newBoundVarExpr()</a>, and <a class="el" href="expr_8h_source.html#l01427">CVC3::Expr::setType()</a>.</p>
</div>
</div>
<a class="anchor" id="ga4a47e11b69e5a197d0437be8a632fa08"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newBoundVarExpr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>type</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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00499">499</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, and <a class="el" href="expr__manager_8h_source.html#l00484">CVC3::ExprManager::newBoundVarExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="ga0d2ff7603a249b30b2df4e549607ad6e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newClosureExpr </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</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>var</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>body</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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00506">506</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>.</p>
<p>Referenced by <a class="el" href="quant__theorem__producer_8cpp_source.html#l00510">CVC3::QuantTheoremProducer::adjustVarUniv()</a>, <a class="el" href="theory__array_8cpp_source.html#l01261">CVC3::arrayLiteral()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00338">CVC3::ArrayTheoremProducer::arrayNotEq()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00748">CVC3::QuantTheoremProducer::boundVarElim()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06272">CVC3::BitvectorTheoremProducer::bvUDivTheorem()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08714">CVC3::TheoryQuant::computeTCC()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00050">CVC3::TheoryDatatypeLazy::instantiate()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00075">CVC3::TheoryDatatype::instantiate()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01373">CVC3::CompleteInstPreProcessor::isMacro()</a>, <a class="el" href="theory__uf_8cpp_source.html#l01129">CVC3::TheoryUF::lambdaExpr()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00234">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theory_8cpp_source.html#l00816">CVC3::Theory::newSubtypeExpr()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00082">CVC3::QuantTheoremProducer::normalizeQuant()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">CVC3::SearchEngineTheoremProducer::opCNFRule()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00568">CVC3::QuantTheoremProducer::packVar()</a>, <a class="el" href="theory__array_8cpp_source.html#l01193">CVC3::TheoryArray::parseExprOp()</a>, <a class="el" href="theory__quant_8cpp_source.html#l09009">CVC3::TheoryQuant::parseExprOp()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00408">CVC3::QuantTheoremProducer::partialUniversalInst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l05609">CVC3::BitvectorTheoremProducer::processExtract()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00612">CVC3::QuantTheoremProducer::pullVarOut()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01249">CVC3::CompleteInstPreProcessor::pullVarOut()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01499">CVC3::CompleteInstPreProcessor::recInstMacros()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01763">CVC3::CompleteInstPreProcessor::recRewriteNot()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01693">CVC3::CompleteInstPreProcessor::recSkolemize()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00139">CVC3::QuantTheoremProducer::rewriteNotExists()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01117">CVC3::CommonTheoremProducer::rewriteNotExists()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00049">CVC3::QuantTheoremProducer::rewriteNotForall()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01102">CVC3::CommonTheoremProducer::rewriteNotForall()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01462">CVC3::CompleteInstPreProcessor::simplifyEq()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06713">CVC3::BitvectorTheoremProducer::solveExtractOverlap()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l01202">CVC3::CommonTheoremProducer::varIntroRule()</a>.</p>
</div>
</div>
<a class="anchor" id="ga349cd5c632090f97d1f03effcbb3ebe4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newClosureExpr </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>vars</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>body</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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00511">511</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="ga99ccea65cb5a86a0ac3f671777f8812d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newClosureExpr </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>vars</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>body</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>trigger</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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00530">530</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>, and <a class="el" href="expr_8h_source.html#l01096">CVC3::Expr::setTrigger()</a>.</p>
</div>
</div>
<a class="anchor" id="ga9793cd1d6b44062a5ae5b8bd5e5f548d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newClosureExpr </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>vars</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>body</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>triggers</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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00516">516</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>, and <a class="el" href="expr_8h_source.html#l01076">CVC3::Expr::setTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="ga47dd127b6737e1c0163fdf34cb5f1f15"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::newClosureExpr </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>vars</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>body</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > & </td>
<td class="paramname"><em>triggers</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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00523">523</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00289">CVC3::ExprManager::newExpr()</a>, and <a class="el" href="expr_8h_source.html#l01076">CVC3::Expr::setTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="ga305b349b572c311b55a121e28392a714"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::andExpr </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>children</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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00312">312</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>.</p>
</div>
</div>
<a class="anchor" id="ga65c227873c06b36c509832506d690aaa"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Expr CVC3::ExprManager::orExpr </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>children</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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00314">314</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00068">OR</a>.</p>
</div>
</div>
<a class="anchor" id="gaa6b885e5372d6072b670831c4e577eff"></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::ExprManager::hash </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> 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><a class="el" href="namespaceHash.html">Hash</a> function for a single <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__manager_8h_source.html#l00542">542</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00197">CVC3::Expr::d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__value_8h_source.html#l00155">CVC3::ExprValue::hash()</a>, and <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="ga50b20f4e775e01da9045fbea0762855b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">ContextManager* CVC3::ExprManager::getCM </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>Fetch our <a class="el" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00322">322</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga5f8daa1f01a0b3f30a3a147243411e5a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Context* CVC3::ExprManager::getCurrentContext </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 context from our <a class="el" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00324">324</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l01416">CVC3::Expr::setEqNext()</a>, <a class="el" href="expr_8h_source.html#l01405">CVC3::Expr::setFind()</a>, <a class="el" href="expr_8h_source.html#l01589">CVC3::Expr::setRep()</a>, and <a class="el" href="expr_8h_source.html#l01578">CVC3::Expr::setSig()</a>.</p>
</div>
</div>
<a class="anchor" id="gafd98497270fdbd403d52b09cf95d0839"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprManager::scopelevel </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>Get current scope level. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00326">326</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga3a3060cbeb64eb97ac935f8f05a60f9b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprManager::setTM </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * </td>
<td class="paramname"><em>tm</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 <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00329">329</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga4aa1269ec9df849a4b7654742408d2ca"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">TheoremManager* CVC3::ExprManager::getTM </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>Fetch the <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00331">331</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00422">CVC3::Theorem::clearAllFlags()</a>, <a class="el" href="theorem_8cpp_source.html#l00441">CVC3::Theorem::getCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00464">CVC3::Theorem::getExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00476">CVC3::Theorem::getLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">CVC3::Theorem::isFlagged()</a>, <a class="el" href="theorem_8cpp_source.html#l00435">CVC3::Theorem::setCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00458">CVC3::Theorem::setExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00429">CVC3::Theorem::setFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00470">CVC3::Theorem::setLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00219">CVC3::Theorem::withAssumptions()</a>, and <a class="el" href="theorem_8cpp_source.html#l00214">CVC3::Theorem::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ga721fc26fe37460f80e6d614cfe0d6fd8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">MemoryManager* CVC3::ExprManager::getMM </td>
<td>(</td>
<td class="paramtype">size_t </td>
<td class="paramname"><em>MMIndex</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>Return a <a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> for the given <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> type. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00334">334</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
<p>Referenced by <a class="el" href="bitvector__expr__value_8h_source.html#l00046">CVC3::BVConstExpr::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00078">CVC3::ExprValue::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00131">CVC3::ExprNode::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00091">CVC3::ExprNodeTmp::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00254">CVC3::ExprApplyTmp::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00231">CVC3::ExprApply::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00151">CVC3::ExprString::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00164">CVC3::ExprSkolem::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00181">CVC3::ExprRational::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00193">CVC3::ExprVar::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00205">CVC3::ExprSymbol::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00218">CVC3::ExprBoundVar::copy()</a>, <a class="el" href="expr__value_8cpp_source.html#l00278">CVC3::ExprClosure::copy()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00251">CVC3::ExprManager::rebuildRec()</a>.</p>
</div>
</div>
<a class="anchor" id="gacacaaf5083e198a6014c2407c7f09cc0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::ExprManager::getSimpCacheTag </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 simplifier's cache tag. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00339">339</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l01432">CVC3::Expr::setSimpCache()</a>, and <a class="el" href="expr_8h_source.html#l01294">CVC3::Expr::validSimpCache()</a>.</p>
</div>
</div>
<a class="anchor" id="gaba358e1731ad9309e52e64eb9ce60755"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprManager::invalidateSimpCache </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>Invalidate the simplifier's cache tag. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00341">341</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l04093">CVC3::TheoryCore::assertEqualities()</a>, <a class="el" href="theory__core_8h_source.html#l00181">CVC3::TheoryCore::CoreNotifyObj::notify()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00267">CVC3::TheoryDatatypeLazy::update()</a>, <a class="el" href="theory__array_8cpp_source.html#l00550">CVC3::TheoryArray::update()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00359">CVC3::TheoryDatatype::update()</a>, and <a class="el" href="theory_8cpp_source.html#l00473">CVC3::Theory::updateCC()</a>.</p>
</div>
</div>
<a class="anchor" id="ga39c8449d567e83ccd711cb2ff1a91dbf"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprManager::registerTypeComputer </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprManager_1_1TypeComputer.html">TypeComputer</a> * </td>
<td class="paramname"><em>typeComputer</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>Register type computer. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00344">344</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l00698">CVC3::TheoryCore::TheoryCore()</a>.</p>
</div>
</div>
<a class="anchor" id="ga56fe351db38c3cc509ae6b1b9c2de000"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprManager::printDepth </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 printing depth. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00348">348</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga3576f0cdcb0ab043d0612c7d9aff7ba1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprManager::withIndentation </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>Whether to print with indentation. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00350">350</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="gab624bd63ef4b189802f1708a41b2b3da"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprManager::lineWidth </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>Suggested line width for printing with indentation. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00352">352</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga54ddb950b6bd35316d1cefe3fd506149"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::ExprManager::indent </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 initial indentation. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00354">354</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr__stream_8cpp_source.html#l00029">CVC3::ExprStream::ExprStream()</a>, and <a class="el" href="theorem_8cpp_source.html#l00580">CVC3::Theorem::print()</a>.</p>
</div>
</div>
<a class="anchor" id="ga787e95a252f54b5fdb7c4d387ea49fae"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int ExprManager::indent </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>n</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>permanent</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Set initial indentation. Returns the previous permanent value. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00334">334</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00099">CVC3::ExprManager::d_indent</a>, and <a class="el" href="expr__manager_8h_source.html#l00103">CVC3::ExprManager::d_indentTransient</a>.</p>
</div>
</div>
<a class="anchor" id="gaf1a5a30e0f0ed0a3e59201530d39d49a"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int ExprManager::incIndent </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>n</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>permanent</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Increment the current transient indentation by n. </p>
<p>If the second argument is true, sets the result as permanent. </p>
<dl class="section return"><dt>Returns</dt><dd>previous permanent value. </dd></dl>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00345">345</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00099">CVC3::ExprManager::d_indent</a>, and <a class="el" href="expr__manager_8h_source.html#l00103">CVC3::ExprManager::d_indentTransient</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00580">CVC3::Theorem::print()</a>.</p>
</div>
</div>
<a class="anchor" id="ga3fe43b71bb148045c114e054934f5304"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprManager::restoreIndent </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 transient indentation to permanent. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00362">362</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8cpp_source.html#l00621">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="gae33e1c95930679cde944e2d2d5984db1"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> ExprManager::getInputLang </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Get the input language for printing. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00354">354</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00107">CVC3::ExprManager::d_inputLang</a>, and <a class="el" href="lang_8h_source.html#l00061">CVC3::getLanguage()</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00267">CVC3::VCCmd::evaluateCommand()</a>, and <a class="el" href="main_8cpp_source.html#l00092">main()</a>.</p>
</div>
</div>
<a class="anchor" id="gaeef110905b00e6e89f54c082e3c4c1a3"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> ExprManager::getOutputLang </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Get the output language for printing. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00360">360</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00107">CVC3::ExprManager::d_inputLang</a>, <a class="el" href="expr__manager_8h_source.html#l00109">CVC3::ExprManager::d_outputLang</a>, and <a class="el" href="lang_8h_source.html#l00061">CVC3::getLanguage()</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l00986">CVC3::Translator::dumpQueryResult()</a>, <a class="el" href="translator_8cpp_source.html#l01816">CVC3::Translator::escapeSymbol()</a>, <a class="el" href="translator_8cpp_source.html#l01145">CVC3::Translator::finish()</a>, <a class="el" href="translator_8cpp_source.html#l01804">CVC3::Translator::fixConstName()</a>, <a class="el" href="main_8cpp_source.html#l00092">main()</a>, <a class="el" href="translator_8cpp_source.html#l01850">CVC3::Translator::printArrayExpr()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00102">CVC3::VCCmd::reportResult()</a>, and <a class="el" href="translator_8cpp_source.html#l00845">CVC3::Translator::start()</a>.</p>
</div>
</div>
<a class="anchor" id="gab24afcec7ae8e33808eebf608193efd9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprManager::dagPrinting </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>Whether to print <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>'s as DAGs. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00368">368</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga3762b5bfe4264bd35b4e887084835fa6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">PrettyPrinter* CVC3::ExprManager::getPrinter </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 pretty-printer if there is one; otherwise return NULL. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00371">371</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.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="ga2b0c6f8e83135e82ebe084188e390da1"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprManager::newKind </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>name</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>isType</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Register a new kind. </p>
<p>The kind may already be registered under the same name, but if the name is different, it's an error.</p>
<p>If the new kind is supposed to represent a type, set isType to true. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00367">367</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="hash__map_8h_source.html#l00217">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count()</a>, <a class="el" href="expr__manager_8h_source.html#l00072">CVC3::ExprManager::d_kindMap</a>, <a class="el" href="expr__manager_8h_source.html#l00084">CVC3::ExprManager::d_kindMapByName</a>, <a class="el" href="expr__manager_8h_source.html#l00074">CVC3::ExprManager::d_typeKinds</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="hash__set_8h_source.html#l00173">Hash::hash_set< _Key, _HashFcn, _EqualKey >::insert()</a>, and <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>.</p>
<p>Referenced by <a class="el" href="expr__manager_8cpp_source.html#l00493">registerKinds()</a>, <a class="el" href="theorem__manager_8cpp_source.html#l00046">CVC3::TheoremManager::TheoremManager()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01809">CVC3::TheoryArith3::TheoryArith3()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01055">CVC3::TheoryArithNew::TheoryArithNew()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02227">CVC3::TheoryArithOld::TheoryArithOld()</a>, <a class="el" href="theory__array_8cpp_source.html#l00042">CVC3::TheoryArray::TheoryArray()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l01708">CVC3::TheoryBitvector::TheoryBitvector()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00041">CVC3::TheoryDatatype::TheoryDatatype()</a>, <a class="el" href="theory__records_8cpp_source.html#l00096">CVC3::TheoryRecords::TheoryRecords()</a>, and <a class="el" href="theory__uf_8cpp_source.html#l00042">CVC3::TheoryUF::TheoryUF()</a>.</p>
</div>
</div>
<a class="anchor" id="gacd01e4de3a171218d0192a9450fb7605"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprManager::registerPrettyPrinter </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1PrettyPrinter.html">PrettyPrinter</a> & </td>
<td class="paramname"><em>printer</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Register the pretty-printer (can only do it if none registered) </p>
<p>The pointer is NOT owned by <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a>. Delete it yourself. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00391">391</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00087">CVC3::ExprManager::d_prettyPrinter</a>, and <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l00698">CVC3::TheoryCore::TheoryCore()</a>.</p>
</div>
</div>
<a class="anchor" id="ga4662ac518622beab3379f6da23380a75"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprManager::unregisterPrettyPrinter </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Tell <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> that the printer is no longer valid. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00398">398</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00087">CVC3::ExprManager::d_prettyPrinter</a>, and <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l00847">CVC3::TheoryCore::~TheoryCore()</a>.</p>
</div>
</div>
<a class="anchor" id="gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprManager::isKindRegistered </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</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>Returns true if kind is built into CVC or has been registered via newKind. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00392">392</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr__value_8h_source.html#l00223">CVC3::ExprValue::ExprValue()</a>.</p>
</div>
</div>
<a class="anchor" id="ga8e91326852cd6030a390fa3a29f6c8f9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::ExprManager::isTypeKind </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</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>Check if a kind represents a type. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00394">394</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l01020">CVC3::Expr::isType()</a>.</p>
</div>
</div>
<a class="anchor" id="gad129f2ecc362f60ca43e06ff46b8521b"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const string & ExprManager::getKindName </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Return the name associated with a kind. The kind must already be registered. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00405">405</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="hash__map_8h_source.html#l00217">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count()</a>, <a class="el" href="expr__manager_8h_source.html#l00072">CVC3::ExprManager::d_kindMap</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="bitvector__theorem__producer_8cpp_source.html#l01575">CVC3::BitvectorTheoremProducer::bitExtractBitwise()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01936">CVC3::TheoryArithNew::computeType()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02747">CVC3::TheoryArith3::computeType()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03725">CVC3::TheoryArithOld::computeType()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02532">CVC3::BitvectorTheoremProducer::extractBitwise()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">CVC3::SearchEngineTheoremProducer::opCNFRule()</a>, <a class="el" href="theory_8cpp_source.html#l00177">CVC3::Theory::registerKinds()</a>, and <a class="el" href="theory_8cpp_source.html#l00252">CVC3::Theory::theoryOf()</a>.</p>
</div>
</div>
<a class="anchor" id="ga9e7929fab9329724812e74b066a3c90a"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int ExprManager::getKind </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>name</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Return a kind associated with a name. Returns NULL_KIND if not found. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00412">412</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00084">CVC3::ExprManager::d_kindMapByName</a>, <a class="el" href="hash__map_8h_source.html#l00257">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end()</a>, <a class="el" href="hash__map_8h_source.html#l00171">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find()</a>, and <a class="el" href="kinds_8h_source.html#l00032">NULL_KIND</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00267">CVC3::VCCmd::evaluateCommand()</a>, <a class="el" href="theory__core_8cpp_source.html#l03589">CVC3::TheoryCore::parseExpr()</a>, <a class="el" href="theory__simulate_8cpp_source.html#l00131">CVC3::TheorySimulate::parseExprOp()</a>, <a class="el" href="theory__records_8cpp_source.html#l00880">CVC3::TheoryRecords::parseExprOp()</a>, <a class="el" href="theory__uf_8cpp_source.html#l01015">CVC3::TheoryUF::parseExprOp()</a>, <a class="el" href="theory__array_8cpp_source.html#l01193">CVC3::TheoryArray::parseExprOp()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00731">CVC3::TheoryDatatype::parseExprOp()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l02040">CVC3::TheoryArithNew::parseExprOp()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04087">CVC3::TheoryBitvector::parseExprOp()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02855">CVC3::TheoryArith3::parseExprOp()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03833">CVC3::TheoryArithOld::parseExprOp()</a>, <a class="el" href="theory__core_8cpp_source.html#l01724">CVC3::TheoryCore::parseExprOp()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l09009">CVC3::TheoryQuant::parseExprOp()</a>.</p>
</div>
</div>
<a class="anchor" id="ga10284641fda307d52345f73e8ad5def0"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">size_t ExprManager::registerSubclass </td>
<td>(</td>
<td class="paramtype">size_t </td>
<td class="paramname"><em>sizeOfSubclass</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Register a new subclass of <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>. </p>
<p>Takes the size (in bytes) of the new subclass and returns the unique index of that subclass. Subsequent calls to the subclass's getMMIndex() must return that index. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00421">421</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00133">CVC3::ExprManager::d_mm</a>, <a class="el" href="expr__manager_8h_source.html#l00113">CVC3::ExprManager::d_mmFlag</a>, and <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>.</p>
<p>Referenced by <a class="el" href="theory__bitvector_8cpp_source.html#l01708">CVC3::TheoryBitvector::TheoryBitvector()</a>.</p>
</div>
</div>
<a class="anchor" id="gaa4b16553ca47bb59c3978be771a5766b"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned long ExprManager::getMemory </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>verbosity</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Calculate memory usage. </p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00433">433</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00113">CVC3::ExprManager::d_mmFlag</a>, <a class="el" href="expr__manager_8cpp_source.html#l00070">CVC3::ExprManager::ExprManager()</a>, <a class="el" href="cvc__util_8h_source.html#l00163">CVC3::MemoryTracker::getString()</a>, and <a class="el" href="cvc__util_8h_source.html#l00120">CVC3::MemoryTracker::print()</a>.</p>
</div>
</div>
<a class="anchor" id="ga8150de408f4d5aec9ceddabf86b30cf3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * </td>
<td class="paramname"><em>em</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Context.html">Context</a> * </td>
<td class="paramname"><em>cxt</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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Constructor. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00433">433</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>Referenced by <a class="el" href="expr__manager_8h_source.html#l00438">CVC3::ExprManagerNotifyObj::getMemory()</a>.</p>
</div>
</div>
<a class="anchor" id="gac681a5cd1f70dda8a7a391439d887c2d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void ExprManagerNotifyObj::notifyPre </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Reimplemented from <a class="el" href="classCVC3_1_1ContextNotifyObj.html#a71e8fc4cf1ab52a2cba9708dfe74633e">CVC3::ContextNotifyObj</a>.</p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00659">659</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="gadd71c522283037f94526bda8f73a8bbd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void ExprManagerNotifyObj::notify </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Reimplemented from <a class="el" href="classCVC3_1_1ContextNotifyObj.html#abad0e373f144d6004cc61ff4604b54c0">CVC3::ContextNotifyObj</a>.</p>
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00664">664</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ga083141d49f93f86b917f6a99f239d2c8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned long CVC3::ExprManagerNotifyObj::getMemory </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>verbosity</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Reimplemented from <a class="el" href="classCVC3_1_1ContextNotifyObj.html#aa5be41ab0c2f9dfd4d5f86d7cda3b85e">CVC3::ContextNotifyObj</a>.</p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00438">438</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00433">CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj()</a>.</p>
</div>
</div>
<a class="anchor" id="gac4a0d5785aa3427b482ab07dff8b5609"></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::ExprManager::hash </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * </td>
<td class="paramname"><em>ev</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00449">449</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="expr__value_8h_source.html#l00155">CVC3::ExprValue::hash()</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l00992">CVC3::Expr::hash()</a>.</p>
</div>
</div>
<h2 class="groupheader">Variable Documentation</h2>
<a class="anchor" id="ga727d1263f81f01e526042f38ec668caa"></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="structHash_1_1hash.html">std::hash</a><char*> CVC3::ExprManager::HashString::h</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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00077">77</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="gaa8b0387e58616954916858e296de4449"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">ExprManager* CVC3::ExprManager::HashEV::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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00117">117</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga5b95d2473f4230b72cc27b090500552f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">ExprManager* CVC3::ExprManagerNotifyObj::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>Definition at line <a class="el" href="expr__manager_8h_source.html#l00430">430</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:16 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>
