<!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: Private methods</title> <link href="tabs.css" rel="stylesheet" type="text/css"/> <link href="doxygen.css" rel="stylesheet" type="text/css"/> </head> <body> <!-- Generated by Doxygen 1.7.4 --> <div id="top"> <div id="titlearea"> <table cellspacing="0" cellpadding="0"> <tbody> <tr style="height: 56px;"> <td style="padding-left: 0.5em;"> <div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div> </td> </tr> </tbody> </table> </div> <div id="navrow1" class="tabs"> <ul class="tablist"> <li><a href="index.html"><span>Main Page</span></a></li> <li><a href="pages.html"><span>Related Pages</span></a></li> <li><a href="modules.html"><span>Modules</span></a></li> <li><a href="namespaces.html"><span>Namespaces</span></a></li> <li><a href="annotated.html"><span>Classes</span></a></li> <li><a href="files.html"><span>Files</span></a></li> </ul> </div> </div> <div class="header"> <div class="summary"> <a href="#func-members">Functions</a> </div> <div class="headertitle"> <div class="title">Private methods</div> </div> <div class="ingroups"><a class="el" href="group__ExprPkg.html">Expression Package</a></div></div> <div class="contents"> <h2><a name="func-members"></a> Functions</h2> <ul> <li>size_t <a class="el" href="group__EM__Priv.html#ga9fe970ca9a02174a617bce9797d41815">CVC3::ExprManager::HashString::operator()</a> (const std::string &s) const <li><a class="el" href="group__EM__Priv.html#gaabb82d3abf0072c71761ca599ba9a8fa">CVC3::ExprManager::HashEV::HashEV</a> (ExprManager *em) <li>size_t <a class="el" href="group__EM__Priv.html#gac8adf717113c11ce0bc84160d17bea7a">CVC3::ExprManager::HashEV::operator()</a> (ExprValue *ev) const <li>virtual <a class="el" href="group__EM__Priv.html#gaee11e07336c1b8704409d42c0aaeafad">CVC3::ExprManager::TypeComputer::~TypeComputer</a> () <li>virtual void <a class="el" href="group__EM__Priv.html#ga670ca72899c66da598ea568af7389407">CVC3::ExprManager::TypeComputer::computeType</a> (const Expr &e)=0 <dl class="el"><dd class="mdescRight">Compute the type of e. <a href="#ga670ca72899c66da598ea568af7389407"></a><br/></dl><li>virtual void <a class="el" href="group__EM__Priv.html#gae679c021fb433f86c28c5eec68e5b5ee">CVC3::ExprManager::TypeComputer::checkType</a> (const Expr &e)=0 <dl class="el"><dd 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/></dl><li>virtual Cardinality <a class="el" href="group__EM__Priv.html#ga13e9c0f4a23614e99705f60e3913c2b1">CVC3::ExprManager::TypeComputer::finiteTypeInfo</a> (Expr &e, Unsigned &n, bool enumerate, bool computeSize)=0 <dl class="el"><dd class="mdescRight">Get information related to finiteness of a type. <a href="#ga13e9c0f4a23614e99705f60e3913c2b1"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <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) <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="#gaa86d7ed7800549f1621d2d5ce64ce643"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * <a class="el" href="group__EM__Priv.html#ga3c693890e6e6e1610c44dda553dbf803">CVC3::ExprManager::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="#ga3c693890e6e6e1610c44dda553dbf803"></a><br/></dl><li>unsigned <a class="el" href="group__EM__Priv.html#gacaa71017958e2e9d069c055248c8dd78">CVC3::ExprManager::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="#gacaa71017958e2e9d069c055248c8dd78"></a><br/></dl><li>unsigned <a class="el" href="group__EM__Priv.html#gab5336831e8006e69a57f9c1b728138f6">CVC3::ExprManager::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="#gab5336831e8006e69a57f9c1b728138f6"></a><br/></dl><li>void <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) <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="#ga15e87e829f86a1dcf2c5e05be6f4d182"></a><br/></dl><li>void <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) <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="#ga51109c3e331615c510c964798b38ee95"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> <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) <dl class="el"><dd class="mdescRight">Get information related to finiteness of a type. <a href="#gae5cc4c6a7dfcc718c7c931e6b160d9d1"></a><br/></dl><li><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) <dl class="el"><dd class="mdescRight">Constructor. <a href="#gaf3af8657f4b2c64f189f0a50147d3589"></a><br/></dl><li><a class="el" href="group__EM__Priv.html#ga318254064b65faf57e1657b680688bc7">CVC3::ExprManager::~ExprManager</a> () <dl class="el"><dd class="mdescRight">Destructor. <a href="#ga318254064b65faf57e1657b680688bc7"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga9bddd7eaf6f198476eda3cd55227f384">CVC3::ExprManager::clear</a> () <dl class="el"><dd class="mdescRight">Free up all memory and delete all the expressions. <a href="#ga9bddd7eaf6f198476eda3cd55227f384"></a><br/></dl><li>bool <a class="el" href="group__EM__Priv.html#gaaec477005a23531fa15d27282658aab8">CVC3::ExprManager::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="#gaaec477005a23531fa15d27282658aab8"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga5878c4fbe700243540dc835b965fd01b">CVC3::ExprManager::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="#ga5878c4fbe700243540dc835b965fd01b"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga9c35426ab6885b609e84a4be9b30effc">CVC3::ExprManager::postponeGC</a> () <dl class="el"><dd class="mdescRight">Postpone deletion of garbage-collected expressions. <a href="#ga9c35426ab6885b609e84a4be9b30effc"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#gafd44d7be33c1111722aa7bb9f3b8b2e9">CVC3::ExprManager::resumeGC</a> () <dl class="el"><dd class="mdescRight">Resume deletion of garbage-collected expressions. <a href="#gafd44d7be33c1111722aa7bb9f3b8b2e9"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <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) <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="#gacaab5ccf5cf81d11185979051d301d5e"></a><br/></dl><li>ExprIndex <a class="el" href="group__EM__Priv.html#ga212f07de6befabee47e4f9a1813e7c44">CVC3::ExprManager::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="#ga212f07de6befabee47e4f9a1813e7c44"></a><br/></dl><li>ExprIndex <a class="el" href="group__EM__Priv.html#gac64badd3988c01f34e43f227902e80f1">CVC3::ExprManager::lastIndex</a> () <li>void <a class="el" href="group__EM__Priv.html#gab4b3f2259b5c0af2251741139ea9d952">CVC3::ExprManager::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="#gab4b3f2259b5c0af2251741139ea9d952"></a><br/></dl><li>const Expr & <a class="el" href="group__EM__Priv.html#gab01fe102500e6b4e266299bf4bbb8a20">CVC3::ExprManager::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="#gab01fe102500e6b4e266299bf4bbb8a20"></a><br/></dl><li>const Expr & <a class="el" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae">CVC3::ExprManager::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="#gaae9db4c93c67cbf8bbf5d1e60e94f1ae"></a><br/></dl><li>const Expr & <a class="el" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a">CVC3::ExprManager::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="#ga4471fca49c2acbb7b4cf71e72bc55d6a"></a><br/></dl><li>const std::vector< Expr > & <a class="el" href="group__EM__Priv.html#ga4619bc6e35a273b89d30908c45d73348">CVC3::ExprManager::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="#ga4619bc6e35a273b89d30908c45d73348"></a><br/></dl><li>const Expr & <a class="el" href="group__EM__Priv.html#ga5b9a6dbadfbed96662a5b5d72e6001e2">CVC3::ExprManager::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="#ga5b9a6dbadfbed96662a5b5d72e6001e2"></a><br/></dl><li>Expr <a class="el" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43">CVC3::ExprManager::newExpr</a> (ExprValue *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="#ga603f0df90a7c9695e010355f8ad8df43"></a><br/></dl><li>Expr <a class="el" href="group__EM__Priv.html#gacd77df1dbcc429e06a75047e2f609822">CVC3::ExprManager::newLeafExpr</a> (const Op &op) <li>Expr <a class="el" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">CVC3::ExprManager::newStringExpr</a> (const std::string &s) <li>Expr <a class="el" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">CVC3::ExprManager::newRatExpr</a> (const Rational &r) <li>Expr <a class="el" href="group__EM__Priv.html#gaf392ed0e07e505e56e551ce9cdaa76fe">CVC3::ExprManager::newSkolemExpr</a> (const Expr &e, int i) <li>Expr <a class="el" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">CVC3::ExprManager::newVarExpr</a> (const std::string &s) <li>Expr <a class="el" href="group__EM__Priv.html#gafddb4551e9dbb163823b1162248e58f0">CVC3::ExprManager::newSymbolExpr</a> (const std::string &s, int kind) <li>Expr <a class="el" href="group__EM__Priv.html#ga22dbb23f716cc73378d4c69d564e38dd">CVC3::ExprManager::newBoundVarExpr</a> (const std::string &name, const std::string &uid) <li>Expr <a class="el" href="group__EM__Priv.html#ga53f1a8180e8fcfead2537dd876c80682">CVC3::ExprManager::newBoundVarExpr</a> (const std::string &name, const std::string &uid, const Type &type) <li>Expr <a class="el" href="group__EM__Priv.html#ga4a47e11b69e5a197d0437be8a632fa08">CVC3::ExprManager::newBoundVarExpr</a> (const Type &type) <li>Expr <a class="el" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">CVC3::ExprManager::newClosureExpr</a> (int kind, const Expr &var, const Expr &body) <li>Expr <a class="el" href="group__EM__Priv.html#ga349cd5c632090f97d1f03effcbb3ebe4">CVC3::ExprManager::newClosureExpr</a> (int kind, const std::vector< Expr > &vars, const Expr &body) <li>Expr <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) <li>Expr <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) <li>Expr <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) <li>Expr <a class="el" href="group__EM__Priv.html#ga305b349b572c311b55a121e28392a714">CVC3::ExprManager::andExpr</a> (const std::vector< Expr > &children) <li>Expr <a class="el" href="group__EM__Priv.html#ga65c227873c06b36c509832506d690aaa">CVC3::ExprManager::orExpr</a> (const std::vector< Expr > &children) <li>size_t <a class="el" href="group__EM__Priv.html#gaa6b885e5372d6072b670831c4e577eff">CVC3::ExprManager::hash</a> (const Expr &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="#gaa6b885e5372d6072b670831c4e577eff"></a><br/></dl><li>ContextManager * <a class="el" href="group__EM__Priv.html#ga50b20f4e775e01da9045fbea0762855b">CVC3::ExprManager::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="#ga50b20f4e775e01da9045fbea0762855b"></a><br/></dl><li>Context * <a class="el" href="group__EM__Priv.html#ga5f8daa1f01a0b3f30a3a147243411e5a">CVC3::ExprManager::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="#ga5f8daa1f01a0b3f30a3a147243411e5a"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#gafd98497270fdbd403d52b09cf95d0839">CVC3::ExprManager::scopelevel</a> () <dl class="el"><dd class="mdescRight">Get current scope level. <a href="#gafd98497270fdbd403d52b09cf95d0839"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga3a3060cbeb64eb97ac935f8f05a60f9b">CVC3::ExprManager::setTM</a> (TheoremManager *tm) <dl class="el"><dd class="mdescRight">Set the <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. <a href="#ga3a3060cbeb64eb97ac935f8f05a60f9b"></a><br/></dl><li>TheoremManager * <a class="el" href="group__EM__Priv.html#ga4aa1269ec9df849a4b7654742408d2ca">CVC3::ExprManager::getTM</a> () const <dl class="el"><dd class="mdescRight">Fetch the <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. <a href="#ga4aa1269ec9df849a4b7654742408d2ca"></a><br/></dl><li>MemoryManager * <a class="el" href="group__EM__Priv.html#ga721fc26fe37460f80e6d614cfe0d6fd8">CVC3::ExprManager::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="#ga721fc26fe37460f80e6d614cfe0d6fd8"></a><br/></dl><li>unsigned <a class="el" href="group__EM__Priv.html#gacacaaf5083e198a6014c2407c7f09cc0">CVC3::ExprManager::getSimpCacheTag</a> () const <dl class="el"><dd class="mdescRight">Get the simplifier's cache tag. <a href="#gacacaaf5083e198a6014c2407c7f09cc0"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#gaba358e1731ad9309e52e64eb9ce60755">CVC3::ExprManager::invalidateSimpCache</a> () <dl class="el"><dd class="mdescRight">Invalidate the simplifier's cache tag. <a href="#gaba358e1731ad9309e52e64eb9ce60755"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga39c8449d567e83ccd711cb2ff1a91dbf">CVC3::ExprManager::registerTypeComputer</a> (TypeComputer *typeComputer) <dl class="el"><dd class="mdescRight">Register type computer. <a href="#ga39c8449d567e83ccd711cb2ff1a91dbf"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#ga56fe351db38c3cc509ae6b1b9c2de000">CVC3::ExprManager::printDepth</a> () const <dl class="el"><dd class="mdescRight">Get printing depth. <a href="#ga56fe351db38c3cc509ae6b1b9c2de000"></a><br/></dl><li>bool <a class="el" href="group__EM__Priv.html#ga3576f0cdcb0ab043d0612c7d9aff7ba1">CVC3::ExprManager::withIndentation</a> () const <dl class="el"><dd class="mdescRight">Whether to print with indentation. <a href="#ga3576f0cdcb0ab043d0612c7d9aff7ba1"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#gab624bd63ef4b189802f1708a41b2b3da">CVC3::ExprManager::lineWidth</a> () const <dl class="el"><dd class="mdescRight">Suggested line width for printing with indentation. <a href="#gab624bd63ef4b189802f1708a41b2b3da"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#ga54ddb950b6bd35316d1cefe3fd506149">CVC3::ExprManager::indent</a> () const <dl class="el"><dd class="mdescRight">Get initial indentation. <a href="#ga54ddb950b6bd35316d1cefe3fd506149"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#ga787e95a252f54b5fdb7c4d387ea49fae">CVC3::ExprManager::indent</a> (int n, bool permanent=false) <dl class="el"><dd class="mdescRight">Set initial indentation. Returns the previous permanent value. <a href="#ga787e95a252f54b5fdb7c4d387ea49fae"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#gaf1a5a30e0f0ed0a3e59201530d39d49a">CVC3::ExprManager::incIndent</a> (int n, bool permanent=false) <dl class="el"><dd class="mdescRight">Increment the current transient indentation by n. <a href="#gaf1a5a30e0f0ed0a3e59201530d39d49a"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga3fe43b71bb148045c114e054934f5304">CVC3::ExprManager::restoreIndent</a> () <dl class="el"><dd class="mdescRight">Set transient indentation to permanent. <a href="#ga3fe43b71bb148045c114e054934f5304"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> <a class="el" href="group__EM__Priv.html#gae33e1c95930679cde944e2d2d5984db1">CVC3::ExprManager::getInputLang</a> () const <dl class="el"><dd class="mdescRight">Get the input language for printing. <a href="#gae33e1c95930679cde944e2d2d5984db1"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> <a class="el" href="group__EM__Priv.html#gaeef110905b00e6e89f54c082e3c4c1a3">CVC3::ExprManager::getOutputLang</a> () const <dl class="el"><dd class="mdescRight">Get the output language for printing. <a href="#gaeef110905b00e6e89f54c082e3c4c1a3"></a><br/></dl><li>bool <a class="el" href="group__EM__Priv.html#gab24afcec7ae8e33808eebf608193efd9">CVC3::ExprManager::dagPrinting</a> () const <dl class="el"><dd class="mdescRight">Whether to print Expr's as DAGs. <a href="#gab24afcec7ae8e33808eebf608193efd9"></a><br/></dl><li>PrettyPrinter * <a class="el" href="group__EM__Priv.html#ga3762b5bfe4264bd35b4e887084835fa6">CVC3::ExprManager::getPrinter</a> () const <dl class="el"><dd class="mdescRight">Return the pretty-printer if there is one; otherwise return NULL. <a href="#ga3762b5bfe4264bd35b4e887084835fa6"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1">CVC3::ExprManager::newKind</a> (int kind, const std::string &name, bool isType=false) <dl class="el"><dd class="mdescRight">Register a new kind. <a href="#ga2b0c6f8e83135e82ebe084188e390da1"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#gacd01e4de3a171218d0192a9450fb7605">CVC3::ExprManager::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="#gacd01e4de3a171218d0192a9450fb7605"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#ga4662ac518622beab3379f6da23380a75">CVC3::ExprManager::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="#ga4662ac518622beab3379f6da23380a75"></a><br/></dl><li>bool <a class="el" href="group__EM__Priv.html#gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c">CVC3::ExprManager::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="#gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c"></a><br/></dl><li>bool <a class="el" href="group__EM__Priv.html#ga8e91326852cd6030a390fa3a29f6c8f9">CVC3::ExprManager::isTypeKind</a> (int kind) <dl class="el"><dd class="mdescRight">Check if a kind represents a type. <a href="#ga8e91326852cd6030a390fa3a29f6c8f9"></a><br/></dl><li>const std::string & <a class="el" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b">CVC3::ExprManager::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="#gad129f2ecc362f60ca43e06ff46b8521b"></a><br/></dl><li>int <a class="el" href="group__EM__Priv.html#ga9e7929fab9329724812e74b066a3c90a">CVC3::ExprManager::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="#ga9e7929fab9329724812e74b066a3c90a"></a><br/></dl><li>size_t <a class="el" href="group__EM__Priv.html#ga10284641fda307d52345f73e8ad5def0">CVC3::ExprManager::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="#ga10284641fda307d52345f73e8ad5def0"></a><br/></dl><li>unsigned long <a class="el" href="group__EM__Priv.html#gaa4b16553ca47bb59c3978be771a5766b">CVC3::ExprManager::getMemory</a> (int verbosity) <dl class="el"><dd class="mdescRight">Calculate memory usage. <a href="#gaa4b16553ca47bb59c3978be771a5766b"></a><br/></dl><li><a class="el" href="group__EM__Priv.html#ga8150de408f4d5aec9ceddabf86b30cf3">CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj</a> (ExprManager *em, Context *cxt) <dl class="el"><dd class="mdescRight">Constructor. <a href="#ga8150de408f4d5aec9ceddabf86b30cf3"></a><br/></dl><li>void <a class="el" href="group__EM__Priv.html#gac681a5cd1f70dda8a7a391439d887c2d">CVC3::ExprManagerNotifyObj::notifyPre</a> (void) <li>void <a class="el" href="group__EM__Priv.html#gadd71c522283037f94526bda8f73a8bbd">CVC3::ExprManagerNotifyObj::notify</a> (void) <li>unsigned long <a class="el" href="group__EM__Priv.html#ga083141d49f93f86b917f6a99f239d2c8">CVC3::ExprManagerNotifyObj::getMemory</a> (int verbosity) <li>bool <a class="el" href="group__EM__Priv.html#ga4a8fa9169728473cc4db3f96d467544f">CVC3::ExprManager::EqEV::operator()</a> (const ExprValue *ev1, const ExprValue *ev2) const </ul> <hr/><h2>Function Documentation</h2> <a class="anchor" id="ga9fe970ca9a02174a617bce9797d41815"></a><!-- doxytag: member="CVC3::ExprManager::HashString::operator()" ref="ga9fe970ca9a02174a617bce9797d41815" args="(const std::string &s) const " --> <div class="memitem"> <div class="memproto"> <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<code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::HashEV::HashEV" ref="gaabb82d3abf0072c71761ca599ba9a8fa" args="(ExprManager *em)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::HashEV::operator()" ref="gac8adf717113c11ce0bc84160d17bea7a" args="(ExprValue *ev) const " --> <div class="memitem"> <div class="memproto"> <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<code> [inline]</code></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="gaee11e07336c1b8704409d42c0aaeafad"></a><!-- doxytag: member="CVC3::ExprManager::TypeComputer::~TypeComputer" ref="gaee11e07336c1b8704409d42c0aaeafad" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">virtual CVC3::ExprManager::TypeComputer::~TypeComputer </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline, virtual]</code></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><!-- doxytag: member="CVC3::ExprManager::TypeComputer::computeType" ref="ga670ca72899c66da598ea568af7389407" args="(const Expr &e)=0" --> <div class="memitem"> <div class="memproto"> <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><code> [pure virtual]</code></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><!-- doxytag: member="CVC3::ExprManager::TypeComputer::checkType" ref="gae679c021fb433f86c28c5eec68e5b5ee" args="(const Expr &e)=0" --> <div class="memitem"> <div class="memproto"> <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><code> [pure virtual]</code></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><!-- doxytag: member="CVC3::ExprManager::TypeComputer::finiteTypeInfo" ref="ga13e9c0f4a23614e99705f60e3913c2b1" args="(Expr &e, Unsigned &n, bool enumerate, bool computeSize)=0" --> <div class="memitem"> <div class="memproto"> <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><code> [pure virtual]</code></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><!-- doxytag: member="CVC3::ExprManager::rebuildRec" ref="gaa86d7ed7800549f1621d2d5ce64ce643" args="(const Expr &e)" --> <div class="memitem"> <div class="memproto"> <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><code> [private]</code></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><!-- doxytag: member="CVC3::ExprManager::newExprValue" ref="ga3c693890e6e6e1610c44dda553dbf803" args="(ExprValue *ev)" --> <div class="memitem"> <div class="memproto"> <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><code> [private]</code></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><!-- doxytag: member="CVC3::ExprManager::getFlag" ref="gacaa71017958e2e9d069c055248c8dd78" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">unsigned CVC3::ExprManager::getFlag </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline, private]</code></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><!-- doxytag: member="CVC3::ExprManager::nextFlag" ref="gab5336831e8006e69a57f9c1b728138f6" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">unsigned CVC3::ExprManager::nextFlag </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline, private]</code></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><!-- doxytag: member="CVC3::ExprManager::computeType" ref="ga15e87e829f86a1dcf2c5e05be6f4d182" args="(const Expr &e)" --> <div class="memitem"> <div class="memproto"> <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><code> [private]</code></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><!-- doxytag: member="CVC3::ExprManager::checkType" ref="ga51109c3e331615c510c964798b38ee95" args="(const Expr &e)" --> <div class="memitem"> <div class="memproto"> <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><code> [private]</code></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><!-- doxytag: member="CVC3::ExprManager::finiteTypeInfo" ref="gae5cc4c6a7dfcc718c7c931e6b160d9d1" args="(Expr &e, Unsigned &n, bool enumerate, bool computeSize)" --> <div class="memitem"> <div class="memproto"> <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><code> [private]</code></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><!-- doxytag: member="CVC3::ExprManager::ExprManager" ref="gaf3af8657f4b2c64f189f0a50147d3589" args="(ContextManager *cm, const CLFlags &flags)" --> <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><!-- doxytag: member="CVC3::ExprManager::~ExprManager" ref="ga318254064b65faf57e1657b680688bc7" args="()" --> <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><!-- doxytag: member="CVC3::ExprManager::clear" ref="ga9bddd7eaf6f198476eda3cd55227f384" args="()" --> <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><!-- doxytag: member="CVC3::ExprManager::isActive" ref="gaaec477005a23531fa15d27282658aab8" args="()" --> <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><!-- doxytag: member="CVC3::ExprManager::gc" ref="ga5878c4fbe700243540dc835b965fd01b" args="(ExprValue *ev)" --> <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><!-- doxytag: member="CVC3::ExprManager::postponeGC" ref="ga9c35426ab6885b609e84a4be9b30effc" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">void CVC3::ExprManager::postponeGC </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></td> </tr> </table> </div> <div class="memdoc"> <p>Postpone deletion of garbage-collected expressions. </p> <dl class="see"><dt><b>See also:</b></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><!-- doxytag: member="CVC3::ExprManager::resumeGC" ref="gafd44d7be33c1111722aa7bb9f3b8b2e9" args="()" --> <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="see"><dt><b>See also:</b></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><!-- doxytag: member="CVC3::ExprManager::rebuild" ref="gacaab5ccf5cf81d11185979051d301d5e" args="(const Expr &e)" --> <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><!-- doxytag: member="CVC3::ExprManager::nextIndex" ref="ga212f07de6befabee47e4f9a1813e7c44" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">ExprIndex CVC3::ExprManager::nextIndex </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::lastIndex" ref="gac64badd3988c01f34e43f227902e80f1" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">ExprIndex CVC3::ExprManager::lastIndex </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::clearFlags" ref="gab4b3f2259b5c0af2251741139ea9d952" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">void CVC3::ExprManager::clearFlags </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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>.</p> </div> </div> <a class="anchor" id="gab01fe102500e6b4e266299bf4bbb8a20"></a><!-- doxytag: member="CVC3::ExprManager::boolExpr" ref="gab01fe102500e6b4e266299bf4bbb8a20" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">const Expr& CVC3::ExprManager::boolExpr </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::falseExpr" ref="gaae9db4c93c67cbf8bbf5d1e60e94f1ae" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">const Expr& CVC3::ExprManager::falseExpr </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::trueExpr" ref="ga4471fca49c2acbb7b4cf71e72bc55d6a" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">const Expr& CVC3::ExprManager::trueExpr </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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__core_8cpp_source.html#l01704">CVC3::TheoryCore::computeTypePred()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03411">CVC3::TheoryBitvector::computeTypePred()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03603">CVC3::TheoryArithOld::computeTypePred()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01860">CVC3::TheoryArithNew::computeTypePred()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02625">CVC3::TheoryArith3::computeTypePred()</a>, <a class="el" href="theory_8h_source.html#l00275">CVC3::Theory::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><!-- doxytag: member="CVC3::ExprManager::getEmptyVector" ref="ga4619bc6e35a273b89d30908c45d73348" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">const std::vector<Expr>& CVC3::ExprManager::getEmptyVector </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::getNullExpr" ref="ga5b9a6dbadfbed96662a5b5d72e6001e2" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">const Expr& CVC3::ExprManager::getNullExpr </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newExpr" ref="ga603f0df90a7c9695e010355f8ad8df43" args="(ExprValue *ev)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newLeafExpr" ref="gacd77df1dbcc429e06a75047e2f609822" args="(const Op &op)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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__core_8cpp_source.html#l01724">CVC3::TheoryCore::parseExprOp()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03833">CVC3::TheoryArithOld::parseExprOp()</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="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><!-- doxytag: member="CVC3::ExprManager::newStringExpr" ref="ga3c1f298d2fdd7aaba48d000ca27df636" args="(const std::string &s)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newRatExpr" ref="ga18423a42ce6557dc33287d3979ccc3c6" args="(const Rational &r)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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="theory__bitvector_8h_source.html#l00300">CVC3::TheoryBitvector::rat()</a>, <a class="el" href="theory__arith_8h_source.html#l00156">CVC3::TheoryArith::rat()</a>, <a class="el" href="bitvector__theorem__producer_8h_source.html#l00486">CVC3::BitvectorTheoremProducer::rat()</a>, <a class="el" href="arith__theorem__producer__old_8h_source.html#l00070">CVC3::ArithTheoremProducerOld::rat()</a>, <a class="el" href="arith__theorem__producer3_8h_source.html#l00070">CVC3::ArithTheoremProducer3::rat()</a>, <a class="el" href="arith__theorem__producer_8h_source.html#l00071">CVC3::ArithTheoremProducer::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><!-- doxytag: member="CVC3::ExprManager::newSkolemExpr" ref="gaf392ed0e07e505e56e551ce9cdaa76fe" args="(const Expr &e, int i)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newVarExpr" ref="ga4d52ed373636679c2dd651d10822a3ee" args="(const std::string &s)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newSymbolExpr" ref="gafddb4551e9dbb163823b1162248e58f0" args="(const std::string &s, int kind)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newBoundVarExpr" ref="ga22dbb23f716cc73378d4c69d564e38dd" args="(const std::string &name, const std::string &uid)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newBoundVarExpr" ref="ga53f1a8180e8fcfead2537dd876c80682" args="(const std::string &name, const std::string &uid, const Type &type)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newBoundVarExpr" ref="ga4a47e11b69e5a197d0437be8a632fa08" args="(const Type &type)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newClosureExpr" ref="ga0d2ff7603a249b30b2df4e549607ad6e" args="(int kind, const Expr &var, const Expr &body)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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__quant_8cpp_source.html#l09009">CVC3::TheoryQuant::parseExprOp()</a>, <a class="el" href="theory__array_8cpp_source.html#l01193">CVC3::TheoryArray::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="theory__quant_8cpp_source.html#l01249">CVC3::CompleteInstPreProcessor::pullVarOut()</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#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><!-- doxytag: member="CVC3::ExprManager::newClosureExpr" ref="ga349cd5c632090f97d1f03effcbb3ebe4" args="(int kind, const std::vector< Expr > &vars, const Expr &body)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newClosureExpr" ref="ga99ccea65cb5a86a0ac3f671777f8812d" args="(int kind, const std::vector< Expr > &vars, const Expr &body, const Expr &trigger)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newClosureExpr" ref="ga9793cd1d6b44062a5ae5b8bd5e5f548d" args="(int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newClosureExpr" ref="ga47dd127b6737e1c0163fdf34cb5f1f15" args="(int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::andExpr" ref="ga305b349b572c311b55a121e28392a714" args="(const std::vector< Expr > &children)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::orExpr" ref="ga65c227873c06b36c509832506d690aaa" args="(const std::vector< Expr > &children)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::hash" ref="gaa6b885e5372d6072b670831c4e577eff" args="(const Expr &e) 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_1Expr.html">Expr</a> & </td> <td class="paramname"><em>e</em></td><td>)</td> <td> const<code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::getCM" ref="ga50b20f4e775e01da9045fbea0762855b" args="() const " --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">ContextManager* CVC3::ExprManager::getCM </td> <td>(</td> <td class="paramname"></td><td>)</td> <td> const<code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::getCurrentContext" ref="ga5f8daa1f01a0b3f30a3a147243411e5a" args="() const " --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">Context* CVC3::ExprManager::getCurrentContext </td> <td>(</td> <td class="paramname"></td><td>)</td> <td> const<code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::scopelevel" ref="gafd98497270fdbd403d52b09cf95d0839" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">int CVC3::ExprManager::scopelevel </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::setTM" ref="ga3a3060cbeb64eb97ac935f8f05a60f9b" args="(TheoremManager *tm)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::getTM" ref="ga4aa1269ec9df849a4b7654742408d2ca" args="() const " --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">TheoremManager* CVC3::ExprManager::getTM </td> <td>(</td> <td class="paramname"></td><td>)</td> <td> const<code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::getMM" ref="ga721fc26fe37460f80e6d614cfe0d6fd8" args="(size_t MMIndex)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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="expr__value_8cpp_source.html#l00278">CVC3::ExprClosure::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#l00218">CVC3::ExprBoundVar::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#l00193">CVC3::ExprVar::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#l00164">CVC3::ExprSkolem::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#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#l00078">CVC3::ExprValue::copy()</a>, <a class="el" href="bitvector__expr__value_8h_source.html#l00046">CVC3::BVConstExpr::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><!-- doxytag: member="CVC3::ExprManager::getSimpCacheTag" ref="gacacaaf5083e198a6014c2407c7f09cc0" args="() const " --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">unsigned CVC3::ExprManager::getSimpCacheTag </td> <td>(</td> <td class="paramname"></td><td>)</td> <td> const<code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::invalidateSimpCache" ref="gaba358e1731ad9309e52e64eb9ce60755" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">void CVC3::ExprManager::invalidateSimpCache </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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__datatype_8cpp_source.html#l00359">CVC3::TheoryDatatype::update()</a>, <a class="el" href="theory__array_8cpp_source.html#l00550">CVC3::TheoryArray::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><!-- doxytag: member="CVC3::ExprManager::registerTypeComputer" ref="ga39c8449d567e83ccd711cb2ff1a91dbf" args="(TypeComputer *typeComputer)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::printDepth" ref="ga56fe351db38c3cc509ae6b1b9c2de000" args="() const " --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">int CVC3::ExprManager::printDepth </td> <td>(</td> <td class="paramname"></td><td>)</td> <td> const<code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::withIndentation" ref="ga3576f0cdcb0ab043d0612c7d9aff7ba1" args="() const " --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">bool CVC3::ExprManager::withIndentation </td> <td>(</td> <td class="paramname"></td><td>)</td> <td> const<code> [inline]</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#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><!-- doxytag: member="CVC3::ExprManager::lineWidth" ref="gab624bd63ef4b189802f1708a41b2b3da" args="() const " --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">int CVC3::ExprManager::lineWidth </td> <td>(</td> <td class="paramname"></td><td>)</td> <td> const<code> [inline]</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#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><!-- doxytag: member="CVC3::ExprManager::indent" ref="ga54ddb950b6bd35316d1cefe3fd506149" args="() const " --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">int CVC3::ExprManager::indent </td> <td>(</td> <td class="paramname"></td><td>)</td> <td> const<code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::indent" ref="ga787e95a252f54b5fdb7c4d387ea49fae" args="(int n, bool permanent=false)" --> <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><!-- doxytag: member="CVC3::ExprManager::incIndent" ref="gaf1a5a30e0f0ed0a3e59201530d39d49a" args="(int n, bool permanent=false)" --> <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="return"><dt><b>Returns:</b></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><!-- doxytag: member="CVC3::ExprManager::restoreIndent" ref="ga3fe43b71bb148045c114e054934f5304" args="()" --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">void CVC3::ExprManager::restoreIndent </td> <td>(</td> <td class="paramname"></td><td>)</td> <td><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::getInputLang" ref="gae33e1c95930679cde944e2d2d5984db1" args="() const " --> <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><!-- doxytag: member="CVC3::ExprManager::getOutputLang" ref="gaeef110905b00e6e89f54c082e3c4c1a3" args="() const " --> <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><!-- doxytag: member="CVC3::ExprManager::dagPrinting" ref="gab24afcec7ae8e33808eebf608193efd9" args="() const " --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">bool CVC3::ExprManager::dagPrinting </td> <td>(</td> <td class="paramname"></td><td>)</td> <td> const<code> [inline]</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#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><!-- doxytag: member="CVC3::ExprManager::getPrinter" ref="ga3762b5bfe4264bd35b4e887084835fa6" args="() const " --> <div class="memitem"> <div class="memproto"> <table class="memname"> <tr> <td class="memname">PrettyPrinter* CVC3::ExprManager::getPrinter </td> <td>(</td> <td class="paramname"></td><td>)</td> <td> const<code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::newKind" ref="ga2b0c6f8e83135e82ebe084188e390da1" args="(int kind, const std::string &name, bool isType=false)" --> <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><!-- doxytag: member="CVC3::ExprManager::registerPrettyPrinter" ref="gacd01e4de3a171218d0192a9450fb7605" args="(PrettyPrinter &printer)" --> <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><!-- doxytag: member="CVC3::ExprManager::unregisterPrettyPrinter" ref="ga4662ac518622beab3379f6da23380a75" args="()" --> <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><!-- doxytag: member="CVC3::ExprManager::isKindRegistered" ref="gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c" args="(int kind)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::isTypeKind" ref="ga8e91326852cd6030a390fa3a29f6c8f9" args="(int kind)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManager::getKindName" ref="gad129f2ecc362f60ca43e06ff46b8521b" args="(int kind)" --> <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__old_8cpp_source.html#l03725">CVC3::TheoryArithOld::computeType()</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="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><!-- doxytag: member="CVC3::ExprManager::getKind" ref="ga9e7929fab9329724812e74b066a3c90a" args="(const std::string &name)" --> <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__uf_8cpp_source.html#l01015">CVC3::TheoryUF::parseExprOp()</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__quant_8cpp_source.html#l09009">CVC3::TheoryQuant::parseExprOp()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00731">CVC3::TheoryDatatype::parseExprOp()</a>, <a class="el" href="theory__core_8cpp_source.html#l01724">CVC3::TheoryCore::parseExprOp()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04087">CVC3::TheoryBitvector::parseExprOp()</a>, <a class="el" href="theory__array_8cpp_source.html#l01193">CVC3::TheoryArray::parseExprOp()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03833">CVC3::TheoryArithOld::parseExprOp()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l02040">CVC3::TheoryArithNew::parseExprOp()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02855">CVC3::TheoryArith3::parseExprOp()</a>.</p> </div> </div> <a class="anchor" id="ga10284641fda307d52345f73e8ad5def0"></a><!-- doxytag: member="CVC3::ExprManager::registerSubclass" ref="ga10284641fda307d52345f73e8ad5def0" args="(size_t sizeOfSubclass)" --> <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><!-- doxytag: member="CVC3::ExprManager::getMemory" ref="gaa4b16553ca47bb59c3978be771a5766b" args="(int verbosity)" --> <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><!-- doxytag: member="CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj" ref="ga8150de408f4d5aec9ceddabf86b30cf3" args="(ExprManager *em, Context *cxt)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline]</code></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><!-- doxytag: member="CVC3::ExprManagerNotifyObj::notifyPre" ref="gac681a5cd1f70dda8a7a391439d887c2d" args="(void)" --> <div class="memitem"> <div class="memproto"> <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><code> [virtual]</code></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><!-- doxytag: member="CVC3::ExprManagerNotifyObj::notify" ref="gadd71c522283037f94526bda8f73a8bbd" args="(void)" --> <div class="memitem"> <div class="memproto"> <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><code> [virtual]</code></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><!-- doxytag: member="CVC3::ExprManagerNotifyObj::getMemory" ref="ga083141d49f93f86b917f6a99f239d2c8" args="(int verbosity)" --> <div class="memitem"> <div class="memproto"> <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><code> [inline, virtual]</code></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="ga4a8fa9169728473cc4db3f96d467544f"></a><!-- doxytag: member="CVC3::ExprManager::EqEV::operator()" ref="ga4a8fa9169728473cc4db3f96d467544f" args="(const ExprValue *ev1, const ExprValue *ev2) const " --> <div class="memitem"> <div class="memproto"> <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<code> [inline]</code></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> </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>