<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: CVC3::ExprManager Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-types">Private Types</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="#friends">Friends</a> </div>
<div class="headertitle">
<div class="title">CVC3::ExprManager Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::ExprManager" -->
<p><code>#include <<a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>></code></p>
<p><a href="classCVC3_1_1ExprManager-members.html">List of all members.</a></p>
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1ExprManager_1_1EqEV.html">EqEV</a>
<dl class="el"><dd class="mdescRight">Private class for d_exprSet. <a href="classCVC3_1_1ExprManager_1_1EqEV.html#details">More...</a><br/></dl><li>class <a class="el" href="classCVC3_1_1ExprManager_1_1HashEV.html">HashEV</a>
<dl class="el"><dd class="mdescRight">Private class for d_exprSet. <a href="classCVC3_1_1ExprManager_1_1HashEV.html#details">More...</a><br/></dl><li>class <a class="el" href="classCVC3_1_1ExprManager_1_1HashString.html">HashString</a>
<dl class="el"><dd class="mdescRight">Private class for hashing strings. <a href="classCVC3_1_1ExprManager_1_1HashString.html#details">More...</a><br/></dl><li>class <a class="el" href="classCVC3_1_1ExprManager_1_1TypeComputer.html">TypeComputer</a>
<dl class="el"><dd class="mdescRight">Abstract class for computing expr type. <a href="classCVC3_1_1ExprManager_1_1TypeComputer.html#details">More...</a><br/></dl></ul>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="group__EM__Priv.html#gaf3af8657f4b2c64f189f0a50147d3589">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)
<dl class="el"><dd class="mdescRight">Constructor. <a href="group__EM__Priv.html#gaf3af8657f4b2c64f189f0a50147d3589"></a><br/></dl><li><a class="el" href="group__EM__Priv.html#ga318254064b65faf57e1657b680688bc7">~ExprManager</a> ()
<dl class="el"><dd class="mdescRight">Destructor. <a href="group__EM__Priv.html#ga318254064b65faf57e1657b680688bc7"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga9bddd7eaf6f198476eda3cd55227f384">clear</a> ()
<dl class="el"><dd class="mdescRight">Free up all memory and delete all the expressions. <a href="group__EM__Priv.html#ga9bddd7eaf6f198476eda3cd55227f384"></a><br/></dl><li>bool <a class="el" href="group__EM__Priv.html#gaaec477005a23531fa15d27282658aab8">isActive</a> ()
<dl class="el"><dd 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="group__EM__Priv.html#gaaec477005a23531fa15d27282658aab8"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga5878c4fbe700243540dc835b965fd01b">gc</a> (<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *ev)
<dl class="el"><dd 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="group__EM__Priv.html#ga5878c4fbe700243540dc835b965fd01b"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga9c35426ab6885b609e84a4be9b30effc">postponeGC</a> ()
<dl class="el"><dd class="mdescRight">Postpone deletion of garbage-collected expressions. <a href="group__EM__Priv.html#ga9c35426ab6885b609e84a4be9b30effc"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#gafd44d7be33c1111722aa7bb9f3b8b2e9">resumeGC</a> ()
<dl class="el"><dd class="mdescRight">Resume deletion of garbage-collected expressions. <a href="group__EM__Priv.html#gafd44d7be33c1111722aa7bb9f3b8b2e9"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#gacaab5ccf5cf81d11185979051d301d5e">rebuild</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd 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="group__EM__Priv.html#gacaab5ccf5cf81d11185979051d301d5e"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a4233916514848331ee104548acbab912">ExprIndex</a> <a class="el" href="group__EM__Priv.html#ga212f07de6befabee47e4f9a1813e7c44">nextIndex</a> ()
<dl class="el"><dd 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="group__EM__Priv.html#ga212f07de6befabee47e4f9a1813e7c44"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a4233916514848331ee104548acbab912">ExprIndex</a> <a class="el" href="group__EM__Priv.html#gac64badd3988c01f34e43f227902e80f1">lastIndex</a> ()
<li>void <a class="el" href="group__EM__Priv.html#gab4b3f2259b5c0af2251741139ea9d952">clearFlags</a> ()
<dl class="el"><dd 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="group__EM__Priv.html#gab4b3f2259b5c0af2251741139ea9d952"></a><br/></dl><li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="group__EM__Priv.html#gab01fe102500e6b4e266299bf4bbb8a20">boolExpr</a> ()
<dl class="el"><dd class="mdescRight">BOOLEAN <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__EM__Priv.html#gab01fe102500e6b4e266299bf4bbb8a20"></a><br/></dl><li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae">falseExpr</a> ()
<dl class="el"><dd class="mdescRight">FALSE <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae"></a><br/></dl><li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a">trueExpr</a> ()
<dl class="el"><dd class="mdescRight">TRUE <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a"></a><br/></dl><li>const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & <a class="el" href="group__EM__Priv.html#ga4619bc6e35a273b89d30908c45d73348">getEmptyVector</a> ()
<dl class="el"><dd 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="group__EM__Priv.html#ga4619bc6e35a273b89d30908c45d73348"></a><br/></dl><li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="group__EM__Priv.html#ga5b9a6dbadfbed96662a5b5d72e6001e2">getNullExpr</a> ()
<dl class="el"><dd 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="group__EM__Priv.html#ga5b9a6dbadfbed96662a5b5d72e6001e2"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43">newExpr</a> (<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *ev)
<dl class="el"><dd 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="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#gacd77df1dbcc429e06a75047e2f609822">newLeafExpr</a> (const <a class="el" href="classCVC3_1_1Op.html">Op</a> &op)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">newStringExpr</a> (const std::string &s)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">newRatExpr</a> (const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> &r)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#gaf392ed0e07e505e56e551ce9cdaa76fe">newSkolemExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int i)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">newVarExpr</a> (const std::string &s)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#gafddb4551e9dbb163823b1162248e58f0">newSymbolExpr</a> (const std::string &s, int kind)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga22dbb23f716cc73378d4c69d564e38dd">newBoundVarExpr</a> (const std::string &name, const std::string &uid)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga53f1a8180e8fcfead2537dd876c80682">newBoundVarExpr</a> (const std::string &name, const std::string &uid, const <a class="el" href="classCVC3_1_1Type.html">Type</a> &type)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga4a47e11b69e5a197d0437be8a632fa08">newBoundVarExpr</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &type)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a> (int kind, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &var, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &body)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga349cd5c632090f97d1f03effcbb3ebe4">newClosureExpr</a> (int kind, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &vars, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &body)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga99ccea65cb5a86a0ac3f671777f8812d">newClosureExpr</a> (int kind, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &vars, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &body, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &trigger)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga9793cd1d6b44062a5ae5b8bd5e5f548d">newClosureExpr</a> (int kind, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &vars, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &body, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &triggers)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga47dd127b6737e1c0163fdf34cb5f1f15">newClosureExpr</a> (int kind, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &vars, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &body, const std::vector< std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > &triggers)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga305b349b572c311b55a121e28392a714">andExpr</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &children)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#ga65c227873c06b36c509832506d690aaa">orExpr</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &children)
<li>size_t <a class="el" href="group__EM__Priv.html#gaa6b885e5372d6072b670831c4e577eff">hash</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const
<dl class="el"><dd 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="group__EM__Priv.html#gaa6b885e5372d6072b670831c4e577eff"></a><br/></dl><li><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a> * <a class="el" href="group__EM__Priv.html#ga50b20f4e775e01da9045fbea0762855b">getCM</a> () const
<dl class="el"><dd 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="group__EM__Priv.html#ga50b20f4e775e01da9045fbea0762855b"></a><br/></dl><li><a class="el" href="classCVC3_1_1Context.html">Context</a> * <a class="el" href="group__EM__Priv.html#ga5f8daa1f01a0b3f30a3a147243411e5a">getCurrentContext</a> () const
<dl class="el"><dd 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="group__EM__Priv.html#ga5f8daa1f01a0b3f30a3a147243411e5a"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#gafd98497270fdbd403d52b09cf95d0839">scopelevel</a> ()
<dl class="el"><dd class="mdescRight">Get current scope level. <a href="group__EM__Priv.html#gafd98497270fdbd403d52b09cf95d0839"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga3a3060cbeb64eb97ac935f8f05a60f9b">setTM</a> (<a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> *tm)
<dl class="el"><dd class="mdescRight">Set the <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. <a href="group__EM__Priv.html#ga3a3060cbeb64eb97ac935f8f05a60f9b"></a><br/></dl><li><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * <a class="el" href="group__EM__Priv.html#ga4aa1269ec9df849a4b7654742408d2ca">getTM</a> () const
<dl class="el"><dd class="mdescRight">Fetch the <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. <a href="group__EM__Priv.html#ga4aa1269ec9df849a4b7654742408d2ca"></a><br/></dl><li><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * <a class="el" href="group__EM__Priv.html#ga721fc26fe37460f80e6d614cfe0d6fd8">getMM</a> (size_t MMIndex)
<dl class="el"><dd 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="group__EM__Priv.html#ga721fc26fe37460f80e6d614cfe0d6fd8"></a><br/></dl><li>unsigned <a class="el" href="group__EM__Priv.html#gacacaaf5083e198a6014c2407c7f09cc0">getSimpCacheTag</a> () const
<dl class="el"><dd class="mdescRight">Get the simplifier's cache tag. <a href="group__EM__Priv.html#gacacaaf5083e198a6014c2407c7f09cc0"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#gaba358e1731ad9309e52e64eb9ce60755">invalidateSimpCache</a> ()
<dl class="el"><dd class="mdescRight">Invalidate the simplifier's cache tag. <a href="group__EM__Priv.html#gaba358e1731ad9309e52e64eb9ce60755"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga39c8449d567e83ccd711cb2ff1a91dbf">registerTypeComputer</a> (<a class="el" href="classCVC3_1_1ExprManager_1_1TypeComputer.html">TypeComputer</a> *typeComputer)
<dl class="el"><dd class="mdescRight">Register type computer. <a href="group__EM__Priv.html#ga39c8449d567e83ccd711cb2ff1a91dbf"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#ga56fe351db38c3cc509ae6b1b9c2de000">printDepth</a> () const
<dl class="el"><dd class="mdescRight">Get printing depth. <a href="group__EM__Priv.html#ga56fe351db38c3cc509ae6b1b9c2de000"></a><br/></dl><li>bool <a class="el" href="group__EM__Priv.html#ga3576f0cdcb0ab043d0612c7d9aff7ba1">withIndentation</a> () const
<dl class="el"><dd class="mdescRight">Whether to print with indentation. <a href="group__EM__Priv.html#ga3576f0cdcb0ab043d0612c7d9aff7ba1"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#gab624bd63ef4b189802f1708a41b2b3da">lineWidth</a> () const
<dl class="el"><dd class="mdescRight">Suggested line width for printing with indentation. <a href="group__EM__Priv.html#gab624bd63ef4b189802f1708a41b2b3da"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#ga54ddb950b6bd35316d1cefe3fd506149">indent</a> () const
<dl class="el"><dd class="mdescRight">Get initial indentation. <a href="group__EM__Priv.html#ga54ddb950b6bd35316d1cefe3fd506149"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#ga787e95a252f54b5fdb7c4d387ea49fae">indent</a> (int n, bool permanent=false)
<dl class="el"><dd class="mdescRight">Set initial indentation. Returns the previous permanent value. <a href="group__EM__Priv.html#ga787e95a252f54b5fdb7c4d387ea49fae"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#gaf1a5a30e0f0ed0a3e59201530d39d49a">incIndent</a> (int n, bool permanent=false)
<dl class="el"><dd class="mdescRight">Increment the current transient indentation by n. <a href="group__EM__Priv.html#gaf1a5a30e0f0ed0a3e59201530d39d49a"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga3fe43b71bb148045c114e054934f5304">restoreIndent</a> ()
<dl class="el"><dd class="mdescRight">Set transient indentation to permanent. <a href="group__EM__Priv.html#ga3fe43b71bb148045c114e054934f5304"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> <a class="el" href="group__EM__Priv.html#gae33e1c95930679cde944e2d2d5984db1">getInputLang</a> () const
<dl class="el"><dd class="mdescRight">Get the input language for printing. <a href="group__EM__Priv.html#gae33e1c95930679cde944e2d2d5984db1"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> <a class="el" href="group__EM__Priv.html#gaeef110905b00e6e89f54c082e3c4c1a3">getOutputLang</a> () const
<dl class="el"><dd class="mdescRight">Get the output language for printing. <a href="group__EM__Priv.html#gaeef110905b00e6e89f54c082e3c4c1a3"></a><br/></dl><li>bool <a class="el" href="group__EM__Priv.html#gab24afcec7ae8e33808eebf608193efd9">dagPrinting</a> () const
<dl class="el"><dd class="mdescRight">Whether to print Expr's as DAGs. <a href="group__EM__Priv.html#gab24afcec7ae8e33808eebf608193efd9"></a><br/></dl><li><a class="el" href="classCVC3_1_1PrettyPrinter.html">PrettyPrinter</a> * <a class="el" href="group__EM__Priv.html#ga3762b5bfe4264bd35b4e887084835fa6">getPrinter</a> () const
<dl class="el"><dd class="mdescRight">Return the pretty-printer if there is one; otherwise return NULL. <a href="group__EM__Priv.html#ga3762b5bfe4264bd35b4e887084835fa6"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1">newKind</a> (int kind, const std::string &name, bool isType=false)
<dl class="el"><dd class="mdescRight">Register a new kind. <a href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#gacd01e4de3a171218d0192a9450fb7605">registerPrettyPrinter</a> (<a class="el" href="classCVC3_1_1PrettyPrinter.html">PrettyPrinter</a> &printer)
<dl class="el"><dd class="mdescRight">Register the pretty-printer (can only do it if none registered) <a href="group__EM__Priv.html#gacd01e4de3a171218d0192a9450fb7605"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga4662ac518622beab3379f6da23380a75">unregisterPrettyPrinter</a> ()
<dl class="el"><dd class="mdescRight">Tell <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> that the printer is no longer valid. <a href="group__EM__Priv.html#ga4662ac518622beab3379f6da23380a75"></a><br/></dl><li>bool <a class="el" href="group__EM__Priv.html#gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c">isKindRegistered</a> (int kind)
<dl class="el"><dd class="mdescRight">Returns true if kind is built into CVC or has been registered via newKind. <a href="group__EM__Priv.html#gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c"></a><br/></dl><li>bool <a class="el" href="group__EM__Priv.html#ga8e91326852cd6030a390fa3a29f6c8f9">isTypeKind</a> (int kind)
<dl class="el"><dd class="mdescRight">Check if a kind represents a type. <a href="group__EM__Priv.html#ga8e91326852cd6030a390fa3a29f6c8f9"></a><br/></dl><li>const std::string & <a class="el" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b">getKindName</a> (int kind)
<dl class="el"><dd class="mdescRight">Return the name associated with a kind. The kind must already be registered. <a href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#ga9e7929fab9329724812e74b066a3c90a">getKind</a> (const std::string &name)
<dl class="el"><dd class="mdescRight">Return a kind associated with a name. Returns NULL_KIND if not found. <a href="group__EM__Priv.html#ga9e7929fab9329724812e74b066a3c90a"></a><br/></dl><li>size_t <a class="el" href="group__EM__Priv.html#ga10284641fda307d52345f73e8ad5def0">registerSubclass</a> (size_t sizeOfSubclass)
<dl class="el"><dd 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="group__EM__Priv.html#ga10284641fda307d52345f73e8ad5def0"></a><br/></dl><li>unsigned long <a class="el" href="group__EM__Priv.html#gaa4b16553ca47bb59c3978be771a5766b">getMemory</a> (int verbosity)
<dl class="el"><dd class="mdescRight">Calculate memory usage. <a href="group__EM__Priv.html#gaa4b16553ca47bb59c3978be771a5766b"></a><br/></dl></ul>
<h2><a name="pri-types"></a>
Private Types</h2>
<ul>
<li>typedef <a class="el" href="classHash_1_1hash__set.html">std::hash_set</a><br class="typebreak"/>
< <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *, <a class="el" href="classCVC3_1_1ExprManager_1_1HashEV.html">HashEV</a>, <a class="el" href="classCVC3_1_1ExprManager_1_1EqEV.html">EqEV</a> > <a class="el" href="classCVC3_1_1ExprManager.html#ac77431b2fe56b930edd5961b1f6eb14d">ExprValueSet</a>
<dl class="el"><dd class="mdescRight"><a class="el" href="namespaceHash.html">Hash</a> set type for uniquifying expressions. <a href="#ac77431b2fe56b930edd5961b1f6eb14d"></a><br/></dl></ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li>size_t <a class="el" href="classCVC3_1_1ExprManager.html#ac4a0d5785aa3427b482ab07dff8b5609">hash</a> (const <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *ev) const
<li>void <a class="el" href="classCVC3_1_1ExprManager.html#a8719f1580a1e4bde43738f5d349f0e4a">installExprValue</a> (<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *ev)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__EM__Priv.html#gaa86d7ed7800549f1621d2d5ce64ce643">rebuildRec</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd 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="group__EM__Priv.html#gaa86d7ed7800549f1621d2d5ce64ce643"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * <a class="el" href="group__EM__Priv.html#ga3c693890e6e6e1610c44dda553dbf803">newExprValue</a> (<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *ev)
<dl class="el"><dd 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="group__EM__Priv.html#ga3c693890e6e6e1610c44dda553dbf803"></a><br/></dl><li>unsigned <a class="el" href="group__EM__Priv.html#gacaa71017958e2e9d069c055248c8dd78">getFlag</a> ()
<dl class="el"><dd 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="group__EM__Priv.html#gacaa71017958e2e9d069c055248c8dd78"></a><br/></dl><li>unsigned <a class="el" href="group__EM__Priv.html#gab5336831e8006e69a57f9c1b728138f6">nextFlag</a> ()
<dl class="el"><dd 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="group__EM__Priv.html#gab5336831e8006e69a57f9c1b728138f6"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga15e87e829f86a1dcf2c5e05be6f4d182">computeType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd 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="group__EM__Priv.html#ga15e87e829f86a1dcf2c5e05be6f4d182"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga51109c3e331615c510c964798b38ee95">checkType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd 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="group__EM__Priv.html#ga51109c3e331615c510c964798b38ee95"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> <a class="el" href="group__EM__Priv.html#gae5cc4c6a7dfcc718c7c931e6b160d9d1">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)
<dl class="el"><dd class="mdescRight">Get information related to finiteness of a type. <a href="group__EM__Priv.html#gae5cc4c6a7dfcc718c7c931e6b160d9d1"></a><br/></dl></ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a> * <a class="el" href="classCVC3_1_1ExprManager.html#ab4503774f636c29f72d680289f2783dc">d_cm</a>
<dl class="el"><dd class="mdescRight">For backtracking attributes. <a href="#ab4503774f636c29f72d680289f2783dc"></a><br/></dl><li><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * <a class="el" href="classCVC3_1_1ExprManager.html#a144ee6ab8333d5a1c79b304abe296e89">d_tm</a>
<dl class="el"><dd class="mdescRight">Needed for Refl Theorems. <a href="#a144ee6ab8333d5a1c79b304abe296e89"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprManagerNotifyObj.html">ExprManagerNotifyObj</a> * <a class="el" href="classCVC3_1_1ExprManager.html#abf2f3e04c70fc71ba01170007e3a0831">d_notifyObj</a>
<dl class="el"><dd class="mdescRight">Notification on <a class="el" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop()</a> <a href="#abf2f3e04c70fc71ba01170007e3a0831"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a4233916514848331ee104548acbab912">ExprIndex</a> <a class="el" href="classCVC3_1_1ExprManager.html#abc472a0164e86abb54806342ce2020fd">d_index</a>
<dl class="el"><dd class="mdescRight">Index counter for <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="el" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare()</a> <a href="#abc472a0164e86abb54806342ce2020fd"></a><br/></dl><li>unsigned <a class="el" href="classCVC3_1_1ExprManager.html#a0e8b6ba08f3b0cdf44457240da091100">d_flagCounter</a>
<dl class="el"><dd class="mdescRight">Counter for a generic <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> flag. <a href="#a0e8b6ba08f3b0cdf44457240da091100"></a><br/></dl><li><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< int, std::string > <a class="el" href="classCVC3_1_1ExprManager.html#a07ec9cfbc5aa8fbc09b7844a4a7ad34e">d_kindMap</a>
<dl class="el"><dd class="mdescRight">The database of registered kinds. <a href="#a07ec9cfbc5aa8fbc09b7844a4a7ad34e"></a><br/></dl><li><a class="el" href="classHash_1_1hash__set.html">std::hash_set</a>< int > <a class="el" href="classCVC3_1_1ExprManager.html#a77f4cd27ea691329a3c01285c116eebd">d_typeKinds</a>
<dl class="el"><dd class="mdescRight">The set of kinds representing a type. <a href="#a77f4cd27ea691329a3c01285c116eebd"></a><br/></dl><li><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< std::string, <br class="typebreak"/>
int, <a class="el" href="classCVC3_1_1ExprManager_1_1HashString.html">HashString</a> > <a class="el" href="classCVC3_1_1ExprManager.html#aeab702ffe6838b75b285df2d1cd0f8fb">d_kindMapByName</a>
<dl class="el"><dd class="mdescRight">The reverse map of names to kinds. <a href="#aeab702ffe6838b75b285df2d1cd0f8fb"></a><br/></dl><li><a class="el" href="classCVC3_1_1PrettyPrinter.html">PrettyPrinter</a> * <a class="el" href="classCVC3_1_1ExprManager.html#a12e3e4bb896c10134908607b528512de">d_prettyPrinter</a>
<dl class="el"><dd class="mdescRight">The registered pretty-printer, a connector to theory-specific pretty-printers. <a href="#a12e3e4bb896c10134908607b528512de"></a><br/></dl><li>const int * <a class="el" href="classCVC3_1_1ExprManager.html#ac51aa6e1a689046daae9591ffdf7a6fe">d_printDepth</a>
<dl class="el"><dd class="mdescRight">Print upto the given depth, replace the rest with "...". -1==unlimited depth. <a href="#ac51aa6e1a689046daae9591ffdf7a6fe"></a><br/></dl><li>const bool * <a class="el" href="classCVC3_1_1ExprManager.html#ad6daa0d62357b8c7b8e17e9cbe627936">d_withIndentation</a>
<dl class="el"><dd class="mdescRight">Whether to print with indentation. <a href="#ad6daa0d62357b8c7b8e17e9cbe627936"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1ExprManager.html#a74ef690ec61d40be41b784246ecd32c4">d_indent</a>
<dl class="el"><dd class="mdescRight">Permanent indentation. <a href="#a74ef690ec61d40be41b784246ecd32c4"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1ExprManager.html#a84f7afd3443e0b6998db69cea8340b38">d_indentTransient</a>
<dl class="el"><dd class="mdescRight">Transient indentation. <a href="#a84f7afd3443e0b6998db69cea8340b38"></a><br/></dl><li>const int * <a class="el" href="classCVC3_1_1ExprManager.html#acc7d0bb165528fd61ae7a1015cd28dfe">d_lineWidth</a>
<dl class="el"><dd class="mdescRight">Suggested line width for printing with indentation. <a href="#acc7d0bb165528fd61ae7a1015cd28dfe"></a><br/></dl><li>const std::string * <a class="el" href="classCVC3_1_1ExprManager.html#ac323f030431b1f87c9201117486f2fd6">d_inputLang</a>
<dl class="el"><dd class="mdescRight">Input language (printing) <a href="#ac323f030431b1f87c9201117486f2fd6"></a><br/></dl><li>const std::string * <a class="el" href="classCVC3_1_1ExprManager.html#ac2d8f75464d06456fa0b2111df849d70">d_outputLang</a>
<dl class="el"><dd class="mdescRight">Output language (printing) <a href="#ac2d8f75464d06456fa0b2111df849d70"></a><br/></dl><li>const bool * <a class="el" href="classCVC3_1_1ExprManager.html#a002213c66d24e953c75d7f1238849c87">d_dagPrinting</a>
<dl class="el"><dd class="mdescRight">Whether to print Expr's as DAGs. <a href="#a002213c66d24e953c75d7f1238849c87"></a><br/></dl><li>const std::string <a class="el" href="classCVC3_1_1ExprManager.html#a5cfe801f6ae8f9fd7a51477a219685e8">d_mmFlag</a>
<dl class="el"><dd class="mdescRight">Which memory manager to use (copy the flag value and keep it the same) <a href="#a5cfe801f6ae8f9fd7a51477a219685e8"></a><br/></dl><li><a class="el" href="classHash_1_1hash__set.html">ExprValueSet</a> <a class="el" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c">d_exprSet</a>
<dl class="el"><dd class="mdescRight"><a class="el" href="namespaceHash.html">Hash</a> set for uniquifying expressions. <a href="#a007da346931bbc8d2dafafaa81c4ea9c"></a><br/></dl><li>std::vector< <a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * > <a class="el" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d">d_mm</a>
<dl class="el"><dd class="mdescRight">Array of memory managers for subclasses of <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>. <a href="#aa5eefdcd1d9d304dec3553908c76f10d"></a><br/></dl><li><a class="el" href="structHash_1_1hash.html">std::hash</a>< void * > <a class="el" href="classCVC3_1_1ExprManager.html#a5ab1d84efde75b4ed4d5c1f4b47c2601">d_pointerHash</a>
<dl class="el"><dd class="mdescRight">A hash function for hashing pointers. <a href="#a5ab1d84efde75b4ed4d5c1f4b47c2601"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprManager.html#a8f6f7143ab2a62f58ed86d296fa23be4">d_bool</a>
<dl class="el"><dd class="mdescRight"><a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> constants cached for fast access. <a href="#a8f6f7143ab2a62f58ed86d296fa23be4"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprManager.html#a4b0a44de15c4b3de63233d824a2058bd">d_false</a>
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprManager.html#a6c341a4de2d1e1189e9a1a67430a508c">d_true</a>
<li>std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1ExprManager.html#a20b3e13cca9564afd32e3df2537bdb24">d_emptyVec</a>
<dl class="el"><dd class="mdescRight">Empty vector of <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> to return by reference as empty vector of children. <a href="#a20b3e13cca9564afd32e3df2537bdb24"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprManager.html#afd9f8cac32e3acbbf7bbb18506cb2350">d_nullExpr</a>
<dl class="el"><dd class="mdescRight">Null <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> to return by reference, for efficiency. <a href="#afd9f8cac32e3acbbf7bbb18506cb2350"></a><br/></dl><li>unsigned <a class="el" href="classCVC3_1_1ExprManager.html#a8770381a9e54320b15897ad4757d6c5e">d_simpCacheTagCurrent</a>
<dl class="el"><dd class="mdescRight">Current value of the simplifier cache tag. <a href="#a8770381a9e54320b15897ad4757d6c5e"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1ExprManager.html#a9c4e054fd961a0910bbf03b8bbccb04a">d_disableGC</a>
<dl class="el"><dd class="mdescRight">Disable garbage collection. <a href="#a9c4e054fd961a0910bbf03b8bbccb04a"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1ExprManager.html#a7ee8efeb3b86e7b044290ad543792db2">d_postponeGC</a>
<dl class="el"><dd class="mdescRight">Postpone deleting garbage-collected expressions. <a href="#a7ee8efeb3b86e7b044290ad543792db2"></a><br/></dl><li>std::vector< <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * > <a class="el" href="classCVC3_1_1ExprManager.html#a679888b2e2e5cb92645ec6bd0701f7ec">d_postponed</a>
<dl class="el"><dd class="mdescRight">Vector of postponed garbage-collected expressions. <a href="#a679888b2e2e5cb92645ec6bd0701f7ec"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1ExprManager.html#a6ae99a5eb75cee11d7f638c1ea17a201">d_inGC</a>
<dl class="el"><dd class="mdescRight">Flag for whether GC is already running. <a href="#a6ae99a5eb75cee11d7f638c1ea17a201"></a><br/></dl><li>std::deque< <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * > <a class="el" href="classCVC3_1_1ExprManager.html#a99533eeb3df944329cf62d97c86fc43c">d_pending</a>
<dl class="el"><dd class="mdescRight">Queue of pending exprs to GC. <a href="#a99533eeb3df944329cf62d97c86fc43c"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a">d_rebuildCache</a>
<dl class="el"><dd class="mdescRight">Rebuild cache. <a href="#a841b8a48adc1372b7d99e3f93dd9620a"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprManager_1_1TypeComputer.html">TypeComputer</a> * <a class="el" href="classCVC3_1_1ExprManager.html#a3b4356ae8ebb7c1fc561188920ae7d03">d_typeComputer</a>
<dl class="el"><dd class="mdescRight">Instance of <a class="el" href="classCVC3_1_1ExprManager_1_1TypeComputer.html" title="Abstract class for computing expr type.">TypeComputer</a>: must be registered. <a href="#a3b4356ae8ebb7c1fc561188920ae7d03"></a><br/></dl></ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1ExprManager.html#aa33520359f6cc0f51b476790d39ed869">Expr</a>
<li>class <a class="el" href="classCVC3_1_1ExprManager.html#a6b4e0ce748563841be8fe35c34ee7975">ExprValue</a>
<li>class <a class="el" href="classCVC3_1_1ExprManager.html#a2c31e8a3c11caeb061d69db14ebb0e95">Op</a>
<li>class <a class="el" href="classCVC3_1_1ExprManager.html#a5027bd09c010f0a1fdc060a3064b1c7c">HashEV</a>
<li>class <a class="el" href="classCVC3_1_1ExprManager.html#a18dba29b4f3e91d6d2bc53472a6bb7cc">Type</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock"><p>Expression Manager</p>
<p>Class: <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a></p>
<p>Author: Sergey Berezin</p>
<p>Created: Wed Dec 4 14:26:35 2002</p>
<p>Description: Global state of the <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> package for a particular instance of <a class="el" href="namespaceCVC3.html">CVC3</a>. Each instance of the <a class="el" href="namespaceCVC3.html">CVC3</a> library has its own expression manager, for thread-safety. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00058">58</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div><hr/><h2>Member Typedef Documentation</h2>
<a class="anchor" id="ac77431b2fe56b930edd5961b1f6eb14d"></a><!-- doxytag: member="CVC3::ExprManager::ExprValueSet" ref="ac77431b2fe56b930edd5961b1f6eb14d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef <a class="el" href="classHash_1_1hash__set.html">std::hash_set</a><<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a>*, <a class="el" href="classCVC3_1_1ExprManager_1_1HashEV.html">HashEV</a>, <a class="el" href="classCVC3_1_1ExprManager_1_1EqEV.html">EqEV</a>> <a class="el" href="classHash_1_1hash__set.html">CVC3::ExprManager::ExprValueSet</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><a class="el" href="namespaceHash.html">Hash</a> set type for uniquifying expressions. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00129">129</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="ac4a0d5785aa3427b482ab07dff8b5609"></a><!-- doxytag: member="CVC3::ExprManager::hash" ref="ac4a0d5785aa3427b482ab07dff8b5609" args="(const ExprValue *ev) const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline, private]</code></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>
<a class="anchor" id="a8719f1580a1e4bde43738f5d349f0e4a"></a><!-- doxytag: member="CVC3::ExprManager::installExprValue" ref="a8719f1580a1e4bde43738f5d349f0e4a" args="(ExprValue *ev)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprManager::installExprValue </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><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8cpp_source.html#l00036">36</a> of file <a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
</div>
</div>
<hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="aa33520359f6cc0f51b476790d39ed869"></a><!-- doxytag: member="CVC3::ExprManager::Expr" ref="aa33520359f6cc0f51b476790d39ed869" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Expr.html">Expr</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00059">59</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#l00141">clear()</a>.</p>
</div>
</div>
<a class="anchor" id="a6b4e0ce748563841be8fe35c34ee7975"></a><!-- doxytag: member="CVC3::ExprManager::ExprValue" ref="a6b4e0ce748563841be8fe35c34ee7975" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00060">60</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a2c31e8a3c11caeb061d69db14ebb0e95"></a><!-- doxytag: member="CVC3::ExprManager::Op" ref="a2c31e8a3c11caeb061d69db14ebb0e95" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Op.html">Op</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00061">61</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a5027bd09c010f0a1fdc060a3064b1c7c"></a><!-- doxytag: member="CVC3::ExprManager::HashEV" ref="a5027bd09c010f0a1fdc060a3064b1c7c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ExprManager_1_1HashEV.html">HashEV</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00062">62</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a18dba29b4f3e91d6d2bc53472a6bb7cc"></a><!-- doxytag: member="CVC3::ExprManager::Type" ref="a18dba29b4f3e91d6d2bc53472a6bb7cc" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Type.html">Type</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00063">63</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#l00251">rebuildRec()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="ab4503774f636c29f72d680289f2783dc"></a><!-- doxytag: member="CVC3::ExprManager::d_cm" ref="ab4503774f636c29f72d680289f2783dc" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a>* <a class="el" href="classCVC3_1_1ExprManager.html#ab4503774f636c29f72d680289f2783dc">CVC3::ExprManager::d_cm</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>For backtracking attributes. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00065">65</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#l00070">ExprManager()</a>.</p>
</div>
</div>
<a class="anchor" id="a144ee6ab8333d5a1c79b304abe296e89"></a><!-- doxytag: member="CVC3::ExprManager::d_tm" ref="a144ee6ab8333d5a1c79b304abe296e89" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* <a class="el" href="classCVC3_1_1ExprManager.html#a144ee6ab8333d5a1c79b304abe296e89">CVC3::ExprManager::d_tm</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Needed for Refl Theorems. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00066">66</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="abf2f3e04c70fc71ba01170007e3a0831"></a><!-- doxytag: member="CVC3::ExprManager::d_notifyObj" ref="abf2f3e04c70fc71ba01170007e3a0831" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprManagerNotifyObj.html">ExprManagerNotifyObj</a>* <a class="el" href="classCVC3_1_1ExprManager.html#abf2f3e04c70fc71ba01170007e3a0831">CVC3::ExprManager::d_notifyObj</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Notification on <a class="el" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop()</a> </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00067">67</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#l00070">ExprManager()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00125">~ExprManager()</a>.</p>
</div>
</div>
<a class="anchor" id="abc472a0164e86abb54806342ce2020fd"></a><!-- doxytag: member="CVC3::ExprManager::d_index" ref="abc472a0164e86abb54806342ce2020fd" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a4233916514848331ee104548acbab912">ExprIndex</a> <a class="el" href="classCVC3_1_1ExprManager.html#abc472a0164e86abb54806342ce2020fd">CVC3::ExprManager::d_index</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Index counter for <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="el" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare()</a> </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00068">68</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a0e8b6ba08f3b0cdf44457240da091100"></a><!-- doxytag: member="CVC3::ExprManager::d_flagCounter" ref="a0e8b6ba08f3b0cdf44457240da091100" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned <a class="el" href="classCVC3_1_1ExprManager.html#a0e8b6ba08f3b0cdf44457240da091100">CVC3::ExprManager::d_flagCounter</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Counter for a generic <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> flag. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00069">69</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a07ec9cfbc5aa8fbc09b7844a4a7ad34e"></a><!-- doxytag: member="CVC3::ExprManager::d_kindMap" ref="a07ec9cfbc5aa8fbc09b7844a4a7ad34e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><int, std::string> <a class="el" href="classCVC3_1_1ExprManager.html#a07ec9cfbc5aa8fbc09b7844a4a7ad34e">CVC3::ExprManager::d_kindMap</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The database of registered kinds. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00072">72</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#l00405">getKindName()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00367">newKind()</a>.</p>
</div>
</div>
<a class="anchor" id="a77f4cd27ea691329a3c01285c116eebd"></a><!-- doxytag: member="CVC3::ExprManager::d_typeKinds" ref="a77f4cd27ea691329a3c01285c116eebd" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__set.html">std::hash_set</a><int> <a class="el" href="classCVC3_1_1ExprManager.html#a77f4cd27ea691329a3c01285c116eebd">CVC3::ExprManager::d_typeKinds</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The set of kinds representing a type. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00074">74</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#l00367">newKind()</a>.</p>
</div>
</div>
<a class="anchor" id="aeab702ffe6838b75b285df2d1cd0f8fb"></a><!-- doxytag: member="CVC3::ExprManager::d_kindMapByName" ref="aeab702ffe6838b75b285df2d1cd0f8fb" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><std::string, int, <a class="el" href="classCVC3_1_1ExprManager_1_1HashString.html">HashString</a>> <a class="el" href="classCVC3_1_1ExprManager.html#aeab702ffe6838b75b285df2d1cd0f8fb">CVC3::ExprManager::d_kindMapByName</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The reverse map of names to kinds. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00084">84</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#l00412">getKind()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00367">newKind()</a>.</p>
</div>
</div>
<a class="anchor" id="a12e3e4bb896c10134908607b528512de"></a><!-- doxytag: member="CVC3::ExprManager::d_prettyPrinter" ref="a12e3e4bb896c10134908607b528512de" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1PrettyPrinter.html">PrettyPrinter</a>* <a class="el" href="classCVC3_1_1ExprManager.html#a12e3e4bb896c10134908607b528512de">CVC3::ExprManager::d_prettyPrinter</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The registered pretty-printer, a connector to theory-specific pretty-printers. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00087">87</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#l00391">registerPrettyPrinter()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00398">unregisterPrettyPrinter()</a>.</p>
</div>
</div>
<a class="anchor" id="ac51aa6e1a689046daae9591ffdf7a6fe"></a><!-- doxytag: member="CVC3::ExprManager::d_printDepth" ref="ac51aa6e1a689046daae9591ffdf7a6fe" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int* <a class="el" href="classCVC3_1_1ExprManager.html#ac51aa6e1a689046daae9591ffdf7a6fe">CVC3::ExprManager::d_printDepth</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Print upto the given depth, replace the rest with "...". -1==unlimited depth. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00095">95</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ad6daa0d62357b8c7b8e17e9cbe627936"></a><!-- doxytag: member="CVC3::ExprManager::d_withIndentation" ref="ad6daa0d62357b8c7b8e17e9cbe627936" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const bool* <a class="el" href="classCVC3_1_1ExprManager.html#ad6daa0d62357b8c7b8e17e9cbe627936">CVC3::ExprManager::d_withIndentation</a><code> [private]</code></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#l00097">97</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a74ef690ec61d40be41b784246ecd32c4"></a><!-- doxytag: member="CVC3::ExprManager::d_indent" ref="a74ef690ec61d40be41b784246ecd32c4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCVC3_1_1ExprManager.html#a74ef690ec61d40be41b784246ecd32c4">CVC3::ExprManager::d_indent</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Permanent indentation. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00099">99</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#l00345">incIndent()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00334">indent()</a>.</p>
</div>
</div>
<a class="anchor" id="a84f7afd3443e0b6998db69cea8340b38"></a><!-- doxytag: member="CVC3::ExprManager::d_indentTransient" ref="a84f7afd3443e0b6998db69cea8340b38" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCVC3_1_1ExprManager.html#a84f7afd3443e0b6998db69cea8340b38">CVC3::ExprManager::d_indentTransient</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Transient indentation. </p>
<p>Normally is the same as d_indent, but may temporarily be different for printing one 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#l00103">103</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#l00345">incIndent()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00334">indent()</a>.</p>
</div>
</div>
<a class="anchor" id="acc7d0bb165528fd61ae7a1015cd28dfe"></a><!-- doxytag: member="CVC3::ExprManager::d_lineWidth" ref="acc7d0bb165528fd61ae7a1015cd28dfe" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int* <a class="el" href="classCVC3_1_1ExprManager.html#acc7d0bb165528fd61ae7a1015cd28dfe">CVC3::ExprManager::d_lineWidth</a><code> [private]</code></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#l00105">105</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="ac323f030431b1f87c9201117486f2fd6"></a><!-- doxytag: member="CVC3::ExprManager::d_inputLang" ref="ac323f030431b1f87c9201117486f2fd6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::string* <a class="el" href="classCVC3_1_1ExprManager.html#ac323f030431b1f87c9201117486f2fd6">CVC3::ExprManager::d_inputLang</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Input language (printing) </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00107">107</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#l00354">getInputLang()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00360">getOutputLang()</a>.</p>
</div>
</div>
<a class="anchor" id="ac2d8f75464d06456fa0b2111df849d70"></a><!-- doxytag: member="CVC3::ExprManager::d_outputLang" ref="ac2d8f75464d06456fa0b2111df849d70" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::string* <a class="el" href="classCVC3_1_1ExprManager.html#ac2d8f75464d06456fa0b2111df849d70">CVC3::ExprManager::d_outputLang</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Output language (printing) </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00109">109</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#l00360">getOutputLang()</a>.</p>
</div>
</div>
<a class="anchor" id="a002213c66d24e953c75d7f1238849c87"></a><!-- doxytag: member="CVC3::ExprManager::d_dagPrinting" ref="a002213c66d24e953c75d7f1238849c87" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const bool* <a class="el" href="classCVC3_1_1ExprManager.html#a002213c66d24e953c75d7f1238849c87">CVC3::ExprManager::d_dagPrinting</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Whether to print Expr's as DAGs. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00111">111</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a5cfe801f6ae8f9fd7a51477a219685e8"></a><!-- doxytag: member="CVC3::ExprManager::d_mmFlag" ref="a5cfe801f6ae8f9fd7a51477a219685e8" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::string <a class="el" href="classCVC3_1_1ExprManager.html#a5cfe801f6ae8f9fd7a51477a219685e8">CVC3::ExprManager::d_mmFlag</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Which memory manager to use (copy the flag value and keep it the same) </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00113">113</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#l00070">ExprManager()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00433">getMemory()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00421">registerSubclass()</a>.</p>
</div>
</div>
<a class="anchor" id="a007da346931bbc8d2dafafaa81c4ea9c"></a><!-- doxytag: member="CVC3::ExprManager::d_exprSet" ref="a007da346931bbc8d2dafafaa81c4ea9c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__set.html">ExprValueSet</a> <a class="el" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c">CVC3::ExprManager::d_exprSet</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><a class="el" href="namespaceHash.html">Hash</a> set for uniquifying expressions. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00131">131</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#l00141">clear()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00188">gc()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00288">newExprValue()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00251">rebuildRec()</a>.</p>
</div>
</div>
<a class="anchor" id="aa5eefdcd1d9d304dec3553908c76f10d"></a><!-- doxytag: member="CVC3::ExprManager::d_mm" ref="aa5eefdcd1d9d304dec3553908c76f10d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>*> <a class="el" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d">CVC3::ExprManager::d_mm</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Array of memory managers for subclasses of <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#l00133">133</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#l00141">clear()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00070">ExprManager()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00188">gc()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00421">registerSubclass()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00212">resumeGC()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00125">~ExprManager()</a>.</p>
</div>
</div>
<a class="anchor" id="a5ab1d84efde75b4ed4d5c1f4b47c2601"></a><!-- doxytag: member="CVC3::ExprManager::d_pointerHash" ref="a5ab1d84efde75b4ed4d5c1f4b47c2601" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="structHash_1_1hash.html">std::hash</a><void*> <a class="el" href="classCVC3_1_1ExprManager.html#a5ab1d84efde75b4ed4d5c1f4b47c2601">CVC3::ExprManager::d_pointerHash</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>A hash function for hashing pointers. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00136">136</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a8f6f7143ab2a62f58ed86d296fa23be4"></a><!-- doxytag: member="CVC3::ExprManager::d_bool" ref="a8f6f7143ab2a62f58ed86d296fa23be4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprManager.html#a8f6f7143ab2a62f58ed86d296fa23be4">CVC3::ExprManager::d_bool</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> constants cached for fast access. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00139">139</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#l00141">clear()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00070">ExprManager()</a>.</p>
</div>
</div>
<a class="anchor" id="a4b0a44de15c4b3de63233d824a2058bd"></a><!-- doxytag: member="CVC3::ExprManager::d_false" ref="a4b0a44de15c4b3de63233d824a2058bd" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprManager.html#a4b0a44de15c4b3de63233d824a2058bd">CVC3::ExprManager::d_false</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00140">140</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#l00141">clear()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00070">ExprManager()</a>.</p>
</div>
</div>
<a class="anchor" id="a6c341a4de2d1e1189e9a1a67430a508c"></a><!-- doxytag: member="CVC3::ExprManager::d_true" ref="a6c341a4de2d1e1189e9a1a67430a508c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprManager.html#a6c341a4de2d1e1189e9a1a67430a508c">CVC3::ExprManager::d_true</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00141">141</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#l00141">clear()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00070">ExprManager()</a>.</p>
</div>
</div>
<a class="anchor" id="a20b3e13cca9564afd32e3df2537bdb24"></a><!-- doxytag: member="CVC3::ExprManager::d_emptyVec" ref="a20b3e13cca9564afd32e3df2537bdb24" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> <a class="el" href="classCVC3_1_1ExprManager.html#a20b3e13cca9564afd32e3df2537bdb24">CVC3::ExprManager::d_emptyVec</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Empty vector of <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> to return by reference as empty vector of children. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00143">143</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#l00125">~ExprManager()</a>.</p>
</div>
</div>
<a class="anchor" id="afd9f8cac32e3acbbf7bbb18506cb2350"></a><!-- doxytag: member="CVC3::ExprManager::d_nullExpr" ref="afd9f8cac32e3acbbf7bbb18506cb2350" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprManager.html#afd9f8cac32e3acbbf7bbb18506cb2350">CVC3::ExprManager::d_nullExpr</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Null <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> to return by reference, for efficiency. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00145">145</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#l00141">clear()</a>.</p>
</div>
</div>
<a class="anchor" id="a8770381a9e54320b15897ad4757d6c5e"></a><!-- doxytag: member="CVC3::ExprManager::d_simpCacheTagCurrent" ref="a8770381a9e54320b15897ad4757d6c5e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned <a class="el" href="classCVC3_1_1ExprManager.html#a8770381a9e54320b15897ad4757d6c5e">CVC3::ExprManager::d_simpCacheTagCurrent</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Current value of the simplifier cache tag. </p>
<p>The cached values of calls to Simplify are valid as long as their cache tag matches this tag. Caches can then be invalidated by incrementing this tag. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00153">153</a> of file <a class="el" href="expr__manager_8h_source.html">expr_manager.h</a>.</p>
</div>
</div>
<a class="anchor" id="a9c4e054fd961a0910bbf03b8bbccb04a"></a><!-- doxytag: member="CVC3::ExprManager::d_disableGC" ref="a9c4e054fd961a0910bbf03b8bbccb04a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1ExprManager.html#a9c4e054fd961a0910bbf03b8bbccb04a">CVC3::ExprManager::d_disableGC</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Disable garbage collection. </p>
<p>This flag disables the garbage collection. Normally, it's set in the destructor, so that we can delete all remaining expressions without GC getting in the way. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00159">159</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#l00141">clear()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00188">gc()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00184">isActive()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00125">~ExprManager()</a>.</p>
</div>
</div>
<a class="anchor" id="a7ee8efeb3b86e7b044290ad543792db2"></a><!-- doxytag: member="CVC3::ExprManager::d_postponeGC" ref="a7ee8efeb3b86e7b044290ad543792db2" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1ExprManager.html#a7ee8efeb3b86e7b044290ad543792db2">CVC3::ExprManager::d_postponeGC</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Postpone deleting garbage-collected expressions. </p>
<p>Useful during manipulation of context, especially at the time of backtracking, since we may have objects with circular dependencies (like find pointers).</p>
<p>The postponed expressions will be deleted the next time the garbage collector is called after this flag is cleared. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00168">168</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#l00188">gc()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00212">resumeGC()</a>.</p>
</div>
</div>
<a class="anchor" id="a679888b2e2e5cb92645ec6bd0701f7ec"></a><!-- doxytag: member="CVC3::ExprManager::d_postponed" ref="a679888b2e2e5cb92645ec6bd0701f7ec" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a>*> <a class="el" href="classCVC3_1_1ExprManager.html#a679888b2e2e5cb92645ec6bd0701f7ec">CVC3::ExprManager::d_postponed</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Vector of postponed garbage-collected expressions. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00170">170</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#l00188">gc()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00212">resumeGC()</a>.</p>
</div>
</div>
<a class="anchor" id="a6ae99a5eb75cee11d7f638c1ea17a201"></a><!-- doxytag: member="CVC3::ExprManager::d_inGC" ref="a6ae99a5eb75cee11d7f638c1ea17a201" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1ExprManager.html#a6ae99a5eb75cee11d7f638c1ea17a201">CVC3::ExprManager::d_inGC</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Flag for whether GC is already running. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00173">173</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#l00188">gc()</a>.</p>
</div>
</div>
<a class="anchor" id="a99533eeb3df944329cf62d97c86fc43c"></a><!-- doxytag: member="CVC3::ExprManager::d_pending" ref="a99533eeb3df944329cf62d97c86fc43c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::deque<<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a>*> <a class="el" href="classCVC3_1_1ExprManager.html#a99533eeb3df944329cf62d97c86fc43c">CVC3::ExprManager::d_pending</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Queue of pending exprs to GC. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00175">175</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#l00188">gc()</a>.</p>
</div>
</div>
<a class="anchor" id="a841b8a48adc1372b7d99e3f93dd9620a"></a><!-- doxytag: member="CVC3::ExprManager::d_rebuildCache" ref="a841b8a48adc1372b7d99e3f93dd9620a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> <a class="el" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a">CVC3::ExprManager::d_rebuildCache</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Rebuild cache. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00178">178</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#l00226">rebuild()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00251">rebuildRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a3b4356ae8ebb7c1fc561188920ae7d03"></a><!-- doxytag: member="CVC3::ExprManager::d_typeComputer" ref="a3b4356ae8ebb7c1fc561188920ae7d03" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprManager_1_1TypeComputer.html">TypeComputer</a>* <a class="el" href="classCVC3_1_1ExprManager.html#a3b4356ae8ebb7c1fc561188920ae7d03">CVC3::ExprManager::d_typeComputer</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Instance of <a class="el" href="classCVC3_1_1ExprManager_1_1TypeComputer.html" title="Abstract class for computing expr type.">TypeComputer</a>: must be registered. </p>
<p>Definition at line <a class="el" href="expr__manager_8h_source.html#l00197">197</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#l00472">checkType()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00465">computeType()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00479">finiteTypeInfo()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="expr__manager_8h_source.html">expr_manager.h</a></li>
<li><a class="el" href="expr__manager_8cpp_source.html">expr_manager.cpp</a></li>
</ul>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
