<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: CVC3::TheoremManager Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a></li><li class="navelem"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="classCVC3_1_1TheoremManager-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::TheoremManager Class Reference</div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>></code></p>
<div class="dynheader">
Collaboration diagram for CVC3::TheoremManager:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1TheoremManager__coll__graph.gif" border="0" usemap="#CVC3_1_1TheoremManager_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1TheoremManager_coll__map" id="CVC3_1_1TheoremManager_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:adb9bd094a9bf2abbd1cbe2c6c5e449b6"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#adb9bd094a9bf2abbd1cbe2c6c5e449b6">TheoremManager</a> (<a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a> *cm, <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> *em, const <a class="el" href="classCVC3_1_1CLFlags.html">CLFlags</a> &flags)</td></tr>
<tr class="memdesc:adb9bd094a9bf2abbd1cbe2c6c5e449b6"><td class="mdescLeft"> </td><td class="mdescRight">Constructor. <a href="#adb9bd094a9bf2abbd1cbe2c6c5e449b6"></a><br/></td></tr>
<tr class="separator:adb9bd094a9bf2abbd1cbe2c6c5e449b6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8dc7e598beb64d9bc8fbc2a5f4f77e18"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a8dc7e598beb64d9bc8fbc2a5f4f77e18">~TheoremManager</a> ()</td></tr>
<tr class="memdesc:a8dc7e598beb64d9bc8fbc2a5f4f77e18"><td class="mdescLeft"> </td><td class="mdescRight">Destructor. <a href="#a8dc7e598beb64d9bc8fbc2a5f4f77e18"></a><br/></td></tr>
<tr class="separator:a8dc7e598beb64d9bc8fbc2a5f4f77e18"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a51c95d2a0f7596e7093a1f8332fdc85e"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a51c95d2a0f7596e7093a1f8332fdc85e">clear</a> ()</td></tr>
<tr class="memdesc:a51c95d2a0f7596e7093a1f8332fdc85e"><td class="mdescLeft"> </td><td class="mdescRight">Deactivate <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. <a href="#a51c95d2a0f7596e7093a1f8332fdc85e"></a><br/></td></tr>
<tr class="separator:a51c95d2a0f7596e7093a1f8332fdc85e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae1b25a77c570ef32031f982dc67a5ce1"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#ae1b25a77c570ef32031f982dc67a5ce1">isActive</a> ()</td></tr>
<tr class="memdesc:ae1b25a77c570ef32031f982dc67a5ce1"><td class="mdescLeft"> </td><td class="mdescRight">Test whether the <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> is still active. <a href="#ae1b25a77c570ef32031f982dc67a5ce1"></a><br/></td></tr>
<tr class="separator:ae1b25a77c570ef32031f982dc67a5ce1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab7f4c16522ac05cca1ca83ff79fc3e0f"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#ab7f4c16522ac05cca1ca83ff79fc3e0f">getCM</a> () const </td></tr>
<tr class="separator:ab7f4c16522ac05cca1ca83ff79fc3e0f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a12fd5db0a56006d3cd4123fec058b2ca"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a12fd5db0a56006d3cd4123fec058b2ca">getEM</a> () const </td></tr>
<tr class="separator:a12fd5db0a56006d3cd4123fec058b2ca"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aac1a2b8c8dbec2d6e92c08fb0eaf2ec7"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1CLFlags.html">CLFlags</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#aac1a2b8c8dbec2d6e92c08fb0eaf2ec7">getFlags</a> () const </td></tr>
<tr class="separator:aac1a2b8c8dbec2d6e92c08fb0eaf2ec7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a62b8cd3f917ca0fb580dde6c483db361"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a62b8cd3f917ca0fb580dde6c483db361">getMM</a> () const </td></tr>
<tr class="separator:a62b8cd3f917ca0fb580dde6c483db361"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1ab310c8d6cfd68063379902b371a924"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a1ab310c8d6cfd68063379902b371a924">getRWMM</a> () const </td></tr>
<tr class="separator:a1ab310c8d6cfd68063379902b371a924"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa251dab2bc6004cef7be350f668a4d8c"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#aa251dab2bc6004cef7be350f668a4d8c">getRules</a> () const </td></tr>
<tr class="separator:aa251dab2bc6004cef7be350f668a4d8c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a146426ed876d276baeeb2b50a9bd7b4b"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a146426ed876d276baeeb2b50a9bd7b4b">getFlag</a> () const </td></tr>
<tr class="separator:a146426ed876d276baeeb2b50a9bd7b4b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a53386d08efa4d0f18524129b3d653bef"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a53386d08efa4d0f18524129b3d653bef">clearAllFlags</a> ()</td></tr>
<tr class="separator:a53386d08efa4d0f18524129b3d653bef"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a462f27eb0eca420b334354a9ddc7a257"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a462f27eb0eca420b334354a9ddc7a257">withProof</a> ()</td></tr>
<tr class="separator:a462f27eb0eca420b334354a9ddc7a257"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0a4f7d2aac078ca32b1dacb5d0af25c4"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a0a4f7d2aac078ca32b1dacb5d0af25c4">withAssumptions</a> ()</td></tr>
<tr class="separator:a0a4f7d2aac078ca32b1dacb5d0af25c4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a510895405d8502401bb6715e54ee58a3"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a510895405d8502401bb6715e54ee58a3">setFlag</a> (long ptr)</td></tr>
<tr class="separator:a510895405d8502401bb6715e54ee58a3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae44dabfc954acbba69c98ac56fc09600"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#ae44dabfc954acbba69c98ac56fc09600">isFlagged</a> (long ptr)</td></tr>
<tr class="separator:ae44dabfc954acbba69c98ac56fc09600"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1412941ea97bc56950827c7d28c6ba54"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a1412941ea97bc56950827c7d28c6ba54">setCachedValue</a> (long ptr, int value)</td></tr>
<tr class="separator:a1412941ea97bc56950827c7d28c6ba54"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa0bc4b6cb911dd5e40efcab60c3f1255"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#aa0bc4b6cb911dd5e40efcab60c3f1255">getCachedValue</a> (long ptr)</td></tr>
<tr class="separator:aa0bc4b6cb911dd5e40efcab60c3f1255"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab70781500f12974614ac06e1118d502f"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#ab70781500f12974614ac06e1118d502f">setExpandFlag</a> (long ptr, bool value)</td></tr>
<tr class="separator:ab70781500f12974614ac06e1118d502f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:abd4fa692d21d8d1a4ba9db570c615847"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#abd4fa692d21d8d1a4ba9db570c615847">getExpandFlag</a> (long ptr)</td></tr>
<tr class="separator:abd4fa692d21d8d1a4ba9db570c615847"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0e3e5bbc0f9539fe1e45f4091602e66a"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a0e3e5bbc0f9539fe1e45f4091602e66a">setLitFlag</a> (long ptr, bool value)</td></tr>
<tr class="separator:a0e3e5bbc0f9539fe1e45f4091602e66a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a57daffd1ce5675f8d58694213e89fb93"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a57daffd1ce5675f8d58694213e89fb93">getLitFlag</a> (long ptr)</td></tr>
<tr class="separator:a57daffd1ce5675f8d58694213e89fb93"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-methods"></a>
Private Member Functions</h2></td></tr>
<tr class="memitem:af0be44f4f9e3e746bcde0ec605f1edc9"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#af0be44f4f9e3e746bcde0ec605f1edc9">createProofRules</a> ()</td></tr>
<tr class="separator:af0be44f4f9e3e746bcde0ec605f1edc9"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-attribs"></a>
Private Attributes</h2></td></tr>
<tr class="memitem:a3b263e6731a9f0382f2368b3a435e80c"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a3b263e6731a9f0382f2368b3a435e80c">d_cm</a></td></tr>
<tr class="separator:a3b263e6731a9f0382f2368b3a435e80c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ace573cbad87f7f05c08d4df5bb135f9b"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#ace573cbad87f7f05c08d4df5bb135f9b">d_em</a></td></tr>
<tr class="separator:ace573cbad87f7f05c08d4df5bb135f9b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acf9119862571d1e1c78a84c0d3a2c86e"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1CLFlags.html">CLFlags</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#acf9119862571d1e1c78a84c0d3a2c86e">d_flags</a></td></tr>
<tr class="separator:acf9119862571d1e1c78a84c0d3a2c86e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a30bfd878f40351acd2ddb5c0d3b26c15"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a30bfd878f40351acd2ddb5c0d3b26c15">d_mm</a></td></tr>
<tr class="separator:a30bfd878f40351acd2ddb5c0d3b26c15"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a690ce8fc2ea52273be727a4153f57a99"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a690ce8fc2ea52273be727a4153f57a99">d_rwmm</a></td></tr>
<tr class="separator:a690ce8fc2ea52273be727a4153f57a99"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a063d9709485420fe4ba62678be167724"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a063d9709485420fe4ba62678be167724">d_withProof</a></td></tr>
<tr class="separator:a063d9709485420fe4ba62678be167724"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8b9e2df67e057c865c9fbc2e26400c03"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a8b9e2df67e057c865c9fbc2e26400c03">d_withAssump</a></td></tr>
<tr class="separator:a8b9e2df67e057c865c9fbc2e26400c03"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4709a80a0ecd282dbdc9d66fa57772fb"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a4709a80a0ecd282dbdc9d66fa57772fb">d_flag</a></td></tr>
<tr class="separator:a4709a80a0ecd282dbdc9d66fa57772fb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4321fbe372c0f2fb6cf409cd8fed2c29"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a4321fbe372c0f2fb6cf409cd8fed2c29">d_active</a></td></tr>
<tr class="memdesc:a4321fbe372c0f2fb6cf409cd8fed2c29"><td class="mdescLeft"> </td><td class="mdescRight">Whether <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> is active. See also <a class="el" href="classCVC3_1_1TheoremManager.html#a51c95d2a0f7596e7093a1f8332fdc85e" title="Deactivate TheoremManager.">clear()</a> <a href="#a4321fbe372c0f2fb6cf409cd8fed2c29"></a><br/></td></tr>
<tr class="separator:a4321fbe372c0f2fb6cf409cd8fed2c29"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6357578327d823837e87ae5cc94bc4c7"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a6357578327d823837e87ae5cc94bc4c7">d_rules</a></td></tr>
<tr class="separator:a6357578327d823837e87ae5cc94bc4c7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad747841b9ddd1fd27ab2d029ac93ab52"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< long, bool > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#ad747841b9ddd1fd27ab2d029ac93ab52">d_reflFlags</a></td></tr>
<tr class="separator:ad747841b9ddd1fd27ab2d029ac93ab52"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a87b85aed87edec2b76d4093922d8d618"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< long, int > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a87b85aed87edec2b76d4093922d8d618">d_cachedValues</a></td></tr>
<tr class="separator:a87b85aed87edec2b76d4093922d8d618"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a56084d2a96b227c28f0a3ca74f5fd088"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< long, bool > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a56084d2a96b227c28f0a3ca74f5fd088">d_expandFlags</a></td></tr>
<tr class="separator:a56084d2a96b227c28f0a3ca74f5fd088"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a228b3c5064ff6c3d1c8bfa31363c1555"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< long, bool > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremManager.html#a228b3c5064ff6c3d1c8bfa31363c1555">d_litFlags</a></td></tr>
<tr class="separator:a228b3c5064ff6c3d1c8bfa31363c1555"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00039">39</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="adb9bd094a9bf2abbd1cbe2c6c5e449b6"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">TheoremManager::TheoremManager </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"><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">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="theorem__manager_8cpp_source.html#l00046">46</a> of file <a class="el" href="theorem__manager_8cpp_source.html">theorem_manager.cpp</a>.</p>
<p>References <a class="el" href="common__theorem__producer_8cpp_source.html#l00035">createProofRules()</a>, <a class="el" href="theorem__manager_8h_source.html#l00042">d_em</a>, <a class="el" href="theorem__manager_8h_source.html#l00044">d_mm</a>, <a class="el" href="theorem__manager_8h_source.html#l00050">d_rules</a>, <a class="el" href="theorem__manager_8h_source.html#l00045">d_rwmm</a>, <a class="el" href="theorem__manager_8h_source.html#l00047">d_withAssump</a>, <a class="el" href="theorem__manager_8h_source.html#l00046">d_withProof</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__manager_8cpp_source.html#l00367">CVC3::ExprManager::newKind()</a>, <a class="el" href="kinds_8h_source.html#l00275">PF_APPLY</a>, and <a class="el" href="kinds_8h_source.html#l00276">PF_HOLE</a>.</p>
</div>
</div>
<a class="anchor" id="a8dc7e598beb64d9bc8fbc2a5f4f77e18"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">TheoremManager::~TheoremManager </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="theorem__manager_8cpp_source.html#l00069">69</a> of file <a class="el" href="theorem__manager_8cpp_source.html">theorem_manager.cpp</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00044">d_mm</a>, and <a class="el" href="theorem__manager_8h_source.html#l00045">d_rwmm</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="af0be44f4f9e3e746bcde0ec605f1edc9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a> * TheoremManager::createProofRules </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="common__theorem__producer_8cpp_source.html#l00035">35</a> of file <a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8cpp_source.html#l00046">TheoremManager()</a>.</p>
</div>
</div>
<a class="anchor" id="a51c95d2a0f7596e7093a1f8332fdc85e"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoremManager::clear </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Deactivate <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. </p>
<p>No more Theorems can be created after this call, only deleted. The purpose of this call is to dis-entangle the mutual dependency of <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> and <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> during destruction time. </p>
<p>Definition at line <a class="el" href="theorem__manager_8cpp_source.html#l00076">76</a> of file <a class="el" href="theorem__manager_8cpp_source.html">theorem_manager.cpp</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00049">d_active</a>, and <a class="el" href="theorem__manager_8h_source.html#l00050">d_rules</a>.</p>
</div>
</div>
<a class="anchor" id="ae1b25a77c570ef32031f982dc67a5ce1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::isActive </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Test whether the <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> is still active. </p>
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00073">73</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00049">d_active</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00444">CVC3::RWTheoremValue::init()</a>, and <a class="el" href="theorem__value_8h_source.html#l00354">CVC3::RegTheoremValue::RegTheoremValue()</a>.</p>
</div>
</div>
<a class="anchor" id="ab7f4c16522ac05cca1ca83ff79fc3e0f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a>* CVC3::TheoremManager::getCM </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00075">75</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00041">d_cm</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00444">CVC3::RWTheoremValue::init()</a>, and <a class="el" href="theorem__value_8h_source.html#l00354">CVC3::RegTheoremValue::RegTheoremValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a12fd5db0a56006d3cd4123fec058b2ca"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a>* CVC3::TheoremManager::getEM </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00076">76</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00042">d_em</a>.</p>
<p>Referenced by <a class="el" href="theorem__producer_8cpp_source.html#l00052">CVC3::TheoremProducer::newLabel()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00234">CVC3::TheoremProducer::newPf()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l00373">CVC3::CommonTheoremProducer::substitutivityRule()</a>.</p>
</div>
</div>
<a class="anchor" id="aac1a2b8c8dbec2d6e92c08fb0eaf2ec7"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1CLFlags.html">CLFlags</a>& CVC3::TheoremManager::getFlags </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00077">77</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00043">d_flags</a>.</p>
<p>Referenced by <a class="el" href="theorem__producer_8cpp_source.html#l00052">CVC3::TheoremProducer::newLabel()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01419">CVC3::SearchEngineTheoremProducer::satProof()</a>, and <a class="el" href="search_8cpp_source.html#l00035">CVC3::SearchEngine::SearchEngine()</a>.</p>
</div>
</div>
<a class="anchor" id="a62b8cd3f917ca0fb580dde6c483db361"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* CVC3::TheoremManager::getMM </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00078">78</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00044">d_mm</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00408">CVC3::RegTheoremValue::getMM()</a>, and <a class="el" href="theorem_8cpp_source.html#l00131">CVC3::Theorem::Theorem()</a>.</p>
</div>
</div>
<a class="anchor" id="a1ab310c8d6cfd68063379902b371a924"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* CVC3::TheoremManager::getRWMM </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00079">79</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00045">d_rwmm</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00532">CVC3::RWTheoremValue::getMM()</a>, and <a class="el" href="theorem_8cpp_source.html#l00131">CVC3::Theorem::Theorem()</a>.</p>
</div>
</div>
<a class="anchor" id="aa251dab2bc6004cef7be350f668a4d8c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a>* CVC3::TheoremManager::getRules </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00080">80</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00050">d_rules</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="a146426ed876d276baeeb2b50a9bd7b4b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremManager::getFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00082">82</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00048">d_flag</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00125">CVC3::TheoremValue::isFlagged()</a>, and <a class="el" href="theorem__value_8h_source.html#l00133">CVC3::TheoremValue::setFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a53386d08efa4d0f18524129b3d653bef"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremManager::clearAllFlags </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00086">86</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="hash__map_8h_source.html#l00161">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::clear()</a>, <a class="el" href="theorem__manager_8h_source.html#l00048">d_flag</a>, <a class="el" href="theorem__manager_8h_source.html#l00052">d_reflFlags</a>, and <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00129">CVC3::TheoremValue::clearAllFlags()</a>, and <a class="el" href="theorem_8cpp_source.html#l00422">CVC3::Theorem::clearAllFlags()</a>.</p>
</div>
</div>
<a class="anchor" id="a462f27eb0eca420b334354a9ddc7a257"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::withProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00091">91</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00046">d_withProof</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00282">CVC3::SearchImplBase::getProof()</a>, <a class="el" href="search__sat_8cpp_source.html#l01178">CVC3::SearchSat::getProof()</a>, <a class="el" href="search__sat_8cpp_source.html#l00936">CVC3::SearchSat::SearchSat()</a>, <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>, and <a class="el" href="theorem_8cpp_source.html#l00214">CVC3::Theorem::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a0a4f7d2aac078ca32b1dacb5d0af25c4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::withAssumptions </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00094">94</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00047">d_withAssump</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00297">CVC3::SearchImplBase::getAssumptionsUsed()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00247">CVC3::SearchImplBase::getCounterExample()</a>, <a class="el" href="theorem_8cpp_source.html#l00219">CVC3::Theorem::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>.</p>
</div>
</div>
<a class="anchor" id="a510895405d8502401bb6715e54ee58a3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremManager::setFlag </td>
<td>(</td>
<td class="paramtype">long </td>
<td class="paramname"><em>ptr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00099">99</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00052">d_reflFlags</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00429">CVC3::Theorem::setFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="ae44dabfc954acbba69c98ac56fc09600"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::isFlagged </td>
<td>(</td>
<td class="paramtype">long </td>
<td class="paramname"><em>ptr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00100">100</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="hash__map_8h_source.html#l00217">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00052">d_reflFlags</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00416">CVC3::Theorem::isFlagged()</a>.</p>
</div>
</div>
<a class="anchor" id="a1412941ea97bc56950827c7d28c6ba54"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremManager::setCachedValue </td>
<td>(</td>
<td class="paramtype">long </td>
<td class="paramname"><em>ptr</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>value</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00101">101</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00053">d_cachedValues</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00435">CVC3::Theorem::setCachedValue()</a>.</p>
</div>
</div>
<a class="anchor" id="aa0bc4b6cb911dd5e40efcab60c3f1255"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::TheoremManager::getCachedValue </td>
<td>(</td>
<td class="paramtype">long </td>
<td class="paramname"><em>ptr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00102">102</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00053">d_cachedValues</a>, <a class="el" href="hash__map_8h_source.html#l00257">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end()</a>, and <a class="el" href="hash__map_8h_source.html#l00171">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00441">CVC3::Theorem::getCachedValue()</a>.</p>
</div>
</div>
<a class="anchor" id="ab70781500f12974614ac06e1118d502f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremManager::setExpandFlag </td>
<td>(</td>
<td class="paramtype">long </td>
<td class="paramname"><em>ptr</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>value</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00107">107</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00054">d_expandFlags</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00458">CVC3::Theorem::setExpandFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="abd4fa692d21d8d1a4ba9db570c615847"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::getExpandFlag </td>
<td>(</td>
<td class="paramtype">long </td>
<td class="paramname"><em>ptr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00108">108</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00054">d_expandFlags</a>, <a class="el" href="hash__map_8h_source.html#l00257">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end()</a>, and <a class="el" href="hash__map_8h_source.html#l00171">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00464">CVC3::Theorem::getExpandFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a0e3e5bbc0f9539fe1e45f4091602e66a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremManager::setLitFlag </td>
<td>(</td>
<td class="paramtype">long </td>
<td class="paramname"><em>ptr</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>value</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00113">113</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00055">d_litFlags</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00470">CVC3::Theorem::setLitFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a57daffd1ce5675f8d58694213e89fb93"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::getLitFlag </td>
<td>(</td>
<td class="paramtype">long </td>
<td class="paramname"><em>ptr</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00114">114</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00055">d_litFlags</a>, <a class="el" href="hash__map_8h_source.html#l00257">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end()</a>, and <a class="el" href="hash__map_8h_source.html#l00171">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00476">CVC3::Theorem::getLitFlag()</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="a3b263e6731a9f0382f2368b3a435e80c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a>* CVC3::TheoremManager::d_cm</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00041">41</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8h_source.html#l00075">getCM()</a>.</p>
</div>
</div>
<a class="anchor" id="ace573cbad87f7f05c08d4df5bb135f9b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a>* CVC3::TheoremManager::d_em</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00042">42</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8h_source.html#l00076">getEM()</a>, and <a class="el" href="theorem__manager_8cpp_source.html#l00046">TheoremManager()</a>.</p>
</div>
</div>
<a class="anchor" id="acf9119862571d1e1c78a84c0d3a2c86e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1CLFlags.html">CLFlags</a>& CVC3::TheoremManager::d_flags</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00043">43</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8h_source.html#l00077">getFlags()</a>.</p>
</div>
</div>
<a class="anchor" id="a30bfd878f40351acd2ddb5c0d3b26c15"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* CVC3::TheoremManager::d_mm</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00044">44</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8h_source.html#l00078">getMM()</a>, <a class="el" href="theorem__manager_8cpp_source.html#l00046">TheoremManager()</a>, and <a class="el" href="theorem__manager_8cpp_source.html#l00069">~TheoremManager()</a>.</p>
</div>
</div>
<a class="anchor" id="a690ce8fc2ea52273be727a4153f57a99"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* CVC3::TheoremManager::d_rwmm</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00045">45</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8h_source.html#l00079">getRWMM()</a>, <a class="el" href="theorem__manager_8cpp_source.html#l00046">TheoremManager()</a>, and <a class="el" href="theorem__manager_8cpp_source.html#l00069">~TheoremManager()</a>.</p>
</div>
</div>
<a class="anchor" id="a063d9709485420fe4ba62678be167724"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::d_withProof</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00046">46</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8cpp_source.html#l00046">TheoremManager()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00091">withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a8b9e2df67e057c865c9fbc2e26400c03"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::d_withAssump</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00047">47</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8cpp_source.html#l00046">TheoremManager()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00094">withAssumptions()</a>.</p>
</div>
</div>
<a class="anchor" id="a4709a80a0ecd282dbdc9d66fa57772fb"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremManager::d_flag</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00048">48</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8h_source.html#l00086">clearAllFlags()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00082">getFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a4321fbe372c0f2fb6cf409cd8fed2c29"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::d_active</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Whether <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> is active. See also <a class="el" href="classCVC3_1_1TheoremManager.html#a51c95d2a0f7596e7093a1f8332fdc85e" title="Deactivate TheoremManager.">clear()</a> </p>
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00049">49</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8cpp_source.html#l00076">clear()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00073">isActive()</a>.</p>
</div>
</div>
<a class="anchor" id="a6357578327d823837e87ae5cc94bc4c7"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a>* CVC3::TheoremManager::d_rules</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00050">50</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8cpp_source.html#l00076">clear()</a>, <a class="el" href="theorem__manager_8h_source.html#l00080">getRules()</a>, and <a class="el" href="theorem__manager_8cpp_source.html#l00046">TheoremManager()</a>.</p>
</div>
</div>
<a class="anchor" id="ad747841b9ddd1fd27ab2d029ac93ab52"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><long, bool> CVC3::TheoremManager::d_reflFlags</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00052">52</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8h_source.html#l00086">clearAllFlags()</a>, <a class="el" href="theorem__manager_8h_source.html#l00100">isFlagged()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00099">setFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a87b85aed87edec2b76d4093922d8d618"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><long, int> CVC3::TheoremManager::d_cachedValues</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00053">53</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8h_source.html#l00102">getCachedValue()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00101">setCachedValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a56084d2a96b227c28f0a3ca74f5fd088"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><long, bool> CVC3::TheoremManager::d_expandFlags</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00054">54</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8h_source.html#l00108">getExpandFlag()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00107">setExpandFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a228b3c5064ff6c3d1c8bfa31363c1555"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><long, bool> CVC3::TheoremManager::d_litFlags</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__manager_8h_source.html#l00055">55</a> of file <a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__manager_8h_source.html#l00114">getLitFlag()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00113">setLitFlag()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a></li>
<li><a class="el" href="common__theorem__producer_8cpp_source.html">common_theorem_producer.cpp</a></li>
<li><a class="el" href="theorem__manager_8cpp_source.html">theorem_manager.cpp</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:18 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
