<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: CVC3::TheoremManager Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> </li>
</ul>
</div>
</div>
<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> </div>
<div class="headertitle">
<div class="title">CVC3::TheoremManager Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::TheoremManager" -->
<p><code>#include <<a class="el" href="theorem__manager_8h_source.html">theorem_manager.h</a>></code></p>
<p><a href="classCVC3_1_1TheoremManager-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><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)
<dl class="el"><dd class="mdescRight">Constructor. <a href="#adb9bd094a9bf2abbd1cbe2c6c5e449b6"></a><br/></dl><li><a class="el" href="classCVC3_1_1TheoremManager.html#a8dc7e598beb64d9bc8fbc2a5f4f77e18">~TheoremManager</a> ()
<dl class="el"><dd class="mdescRight">Destructor. <a href="#a8dc7e598beb64d9bc8fbc2a5f4f77e18"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoremManager.html#a51c95d2a0f7596e7093a1f8332fdc85e">clear</a> ()
<dl class="el"><dd class="mdescRight">Deactivate <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>. <a href="#a51c95d2a0f7596e7093a1f8332fdc85e"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoremManager.html#ae1b25a77c570ef32031f982dc67a5ce1">isActive</a> ()
<dl class="el"><dd class="mdescRight">Test whether the <a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> is still active. <a href="#ae1b25a77c570ef32031f982dc67a5ce1"></a><br/></dl><li><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#ab7f4c16522ac05cca1ca83ff79fc3e0f">getCM</a> () const
<li><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#a12fd5db0a56006d3cd4123fec058b2ca">getEM</a> () const
<li>const <a class="el" href="classCVC3_1_1CLFlags.html">CLFlags</a> & <a class="el" href="classCVC3_1_1TheoremManager.html#aac1a2b8c8dbec2d6e92c08fb0eaf2ec7">getFlags</a> () const
<li><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#a62b8cd3f917ca0fb580dde6c483db361">getMM</a> () const
<li><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#a1ab310c8d6cfd68063379902b371a924">getRWMM</a> () const
<li><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#aa251dab2bc6004cef7be350f668a4d8c">getRules</a> () const
<li>unsigned <a class="el" href="classCVC3_1_1TheoremManager.html#a146426ed876d276baeeb2b50a9bd7b4b">getFlag</a> () const
<li>void <a class="el" href="classCVC3_1_1TheoremManager.html#a53386d08efa4d0f18524129b3d653bef">clearAllFlags</a> ()
<li>bool <a class="el" href="classCVC3_1_1TheoremManager.html#a462f27eb0eca420b334354a9ddc7a257">withProof</a> ()
<li>bool <a class="el" href="classCVC3_1_1TheoremManager.html#a0a4f7d2aac078ca32b1dacb5d0af25c4">withAssumptions</a> ()
<li>void <a class="el" href="classCVC3_1_1TheoremManager.html#a510895405d8502401bb6715e54ee58a3">setFlag</a> (long ptr)
<li>bool <a class="el" href="classCVC3_1_1TheoremManager.html#ae44dabfc954acbba69c98ac56fc09600">isFlagged</a> (long ptr)
<li>void <a class="el" href="classCVC3_1_1TheoremManager.html#a1412941ea97bc56950827c7d28c6ba54">setCachedValue</a> (long ptr, int value)
<li>int <a class="el" href="classCVC3_1_1TheoremManager.html#aa0bc4b6cb911dd5e40efcab60c3f1255">getCachedValue</a> (long ptr)
<li>void <a class="el" href="classCVC3_1_1TheoremManager.html#ab70781500f12974614ac06e1118d502f">setExpandFlag</a> (long ptr, bool value)
<li>bool <a class="el" href="classCVC3_1_1TheoremManager.html#abd4fa692d21d8d1a4ba9db570c615847">getExpandFlag</a> (long ptr)
<li>void <a class="el" href="classCVC3_1_1TheoremManager.html#a0e3e5bbc0f9539fe1e45f4091602e66a">setLitFlag</a> (long ptr, bool value)
<li>bool <a class="el" href="classCVC3_1_1TheoremManager.html#a57daffd1ce5675f8d58694213e89fb93">getLitFlag</a> (long ptr)
</ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#af0be44f4f9e3e746bcde0ec605f1edc9">createProofRules</a> ()
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#a3b263e6731a9f0382f2368b3a435e80c">d_cm</a>
<li><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#ace573cbad87f7f05c08d4df5bb135f9b">d_em</a>
<li>const <a class="el" href="classCVC3_1_1CLFlags.html">CLFlags</a> & <a class="el" href="classCVC3_1_1TheoremManager.html#acf9119862571d1e1c78a84c0d3a2c86e">d_flags</a>
<li><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#a30bfd878f40351acd2ddb5c0d3b26c15">d_mm</a>
<li><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#a690ce8fc2ea52273be727a4153f57a99">d_rwmm</a>
<li>bool <a class="el" href="classCVC3_1_1TheoremManager.html#a063d9709485420fe4ba62678be167724">d_withProof</a>
<li>bool <a class="el" href="classCVC3_1_1TheoremManager.html#a8b9e2df67e057c865c9fbc2e26400c03">d_withAssump</a>
<li>unsigned <a class="el" href="classCVC3_1_1TheoremManager.html#a4709a80a0ecd282dbdc9d66fa57772fb">d_flag</a>
<li>bool <a class="el" href="classCVC3_1_1TheoremManager.html#a4321fbe372c0f2fb6cf409cd8fed2c29">d_active</a>
<dl class="el"><dd 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/></dl><li><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a> * <a class="el" href="classCVC3_1_1TheoremManager.html#a6357578327d823837e87ae5cc94bc4c7">d_rules</a>
<li><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< long, bool > <a class="el" href="classCVC3_1_1TheoremManager.html#ad747841b9ddd1fd27ab2d029ac93ab52">d_reflFlags</a>
<li><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< long, int > <a class="el" href="classCVC3_1_1TheoremManager.html#a87b85aed87edec2b76d4093922d8d618">d_cachedValues</a>
<li><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< long, bool > <a class="el" href="classCVC3_1_1TheoremManager.html#a56084d2a96b227c28f0a3ca74f5fd088">d_expandFlags</a>
<li><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< long, bool > <a class="el" href="classCVC3_1_1TheoremManager.html#a228b3c5064ff6c3d1c8bfa31363c1555">d_litFlags</a>
</ul>
<hr/><a name="details" id="details"></a><h2>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><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="adb9bd094a9bf2abbd1cbe2c6c5e449b6"></a><!-- doxytag: member="CVC3::TheoremManager::TheoremManager" ref="adb9bd094a9bf2abbd1cbe2c6c5e449b6" args="(ContextManager *cm, ExprManager *em, const CLFlags &flags)" -->
<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><!-- doxytag: member="CVC3::TheoremManager::~TheoremManager" ref="a8dc7e598beb64d9bc8fbc2a5f4f77e18" args="()" -->
<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>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="af0be44f4f9e3e746bcde0ec605f1edc9"></a><!-- doxytag: member="CVC3::TheoremManager::createProofRules" ref="af0be44f4f9e3e746bcde0ec605f1edc9" args="()" -->
<div class="memitem">
<div class="memproto">
<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><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::clear" ref="a51c95d2a0f7596e7093a1f8332fdc85e" args="()" -->
<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><!-- doxytag: member="CVC3::TheoremManager::isActive" ref="ae1b25a77c570ef32031f982dc67a5ce1" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::isActive </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::getCM" ref="ab7f4c16522ac05cca1ca83ff79fc3e0f" args="() const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::getEM" ref="a12fd5db0a56006d3cd4123fec058b2ca" args="() const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::getFlags" ref="aac1a2b8c8dbec2d6e92c08fb0eaf2ec7" args="() const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::getMM" ref="a62b8cd3f917ca0fb580dde6c483db361" args="() const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::getRWMM" ref="a1ab310c8d6cfd68063379902b371a924" args="() const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::getRules" ref="aa251dab2bc6004cef7be350f668a4d8c" args="() const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::getFlag" ref="a146426ed876d276baeeb2b50a9bd7b4b" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremManager::getFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::clearAllFlags" ref="a53386d08efa4d0f18524129b3d653bef" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremManager::clearAllFlags </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="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><!-- doxytag: member="CVC3::TheoremManager::withProof" ref="a462f27eb0eca420b334354a9ddc7a257" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::withProof </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="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__sat_8cpp_source.html#l01178">CVC3::SearchSat::getProof()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00282">CVC3::SearchImplBase::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><!-- doxytag: member="CVC3::TheoremManager::withAssumptions" ref="a0a4f7d2aac078ca32b1dacb5d0af25c4" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremManager::withAssumptions </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="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__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem_8cpp_source.html#l00219">CVC3::Theorem::withAssumptions()</a>.</p>
</div>
</div>
<a class="anchor" id="a510895405d8502401bb6715e54ee58a3"></a><!-- doxytag: member="CVC3::TheoremManager::setFlag" ref="a510895405d8502401bb6715e54ee58a3" args="(long ptr)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::isFlagged" ref="ae44dabfc954acbba69c98ac56fc09600" args="(long ptr)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::setCachedValue" ref="a1412941ea97bc56950827c7d28c6ba54" args="(long ptr, int value)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::getCachedValue" ref="aa0bc4b6cb911dd5e40efcab60c3f1255" args="(long ptr)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::setExpandFlag" ref="ab70781500f12974614ac06e1118d502f" args="(long ptr, bool value)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::getExpandFlag" ref="abd4fa692d21d8d1a4ba9db570c615847" args="(long ptr)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::setLitFlag" ref="a0e3e5bbc0f9539fe1e45f4091602e66a" args="(long ptr, bool value)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::TheoremManager::getLitFlag" ref="a57daffd1ce5675f8d58694213e89fb93" args="(long ptr)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a3b263e6731a9f0382f2368b3a435e80c"></a><!-- doxytag: member="CVC3::TheoremManager::d_cm" ref="a3b263e6731a9f0382f2368b3a435e80c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ContextManager.html">ContextManager</a>* <a class="el" href="classCVC3_1_1TheoremManager.html#a3b263e6731a9f0382f2368b3a435e80c">CVC3::TheoremManager::d_cm</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_em" ref="ace573cbad87f7f05c08d4df5bb135f9b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a>* <a class="el" href="classCVC3_1_1TheoremManager.html#ace573cbad87f7f05c08d4df5bb135f9b">CVC3::TheoremManager::d_em</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_flags" ref="acf9119862571d1e1c78a84c0d3a2c86e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1CLFlags.html">CLFlags</a>& <a class="el" href="classCVC3_1_1TheoremManager.html#acf9119862571d1e1c78a84c0d3a2c86e">CVC3::TheoremManager::d_flags</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_mm" ref="a30bfd878f40351acd2ddb5c0d3b26c15" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* <a class="el" href="classCVC3_1_1TheoremManager.html#a30bfd878f40351acd2ddb5c0d3b26c15">CVC3::TheoremManager::d_mm</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_rwmm" ref="a690ce8fc2ea52273be727a4153f57a99" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* <a class="el" href="classCVC3_1_1TheoremManager.html#a690ce8fc2ea52273be727a4153f57a99">CVC3::TheoremManager::d_rwmm</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_withProof" ref="a063d9709485420fe4ba62678be167724" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1TheoremManager.html#a063d9709485420fe4ba62678be167724">CVC3::TheoremManager::d_withProof</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_withAssump" ref="a8b9e2df67e057c865c9fbc2e26400c03" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1TheoremManager.html#a8b9e2df67e057c865c9fbc2e26400c03">CVC3::TheoremManager::d_withAssump</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_flag" ref="a4709a80a0ecd282dbdc9d66fa57772fb" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned <a class="el" href="classCVC3_1_1TheoremManager.html#a4709a80a0ecd282dbdc9d66fa57772fb">CVC3::TheoremManager::d_flag</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_active" ref="a4321fbe372c0f2fb6cf409cd8fed2c29" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1TheoremManager.html#a4321fbe372c0f2fb6cf409cd8fed2c29">CVC3::TheoremManager::d_active</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_rules" ref="a6357578327d823837e87ae5cc94bc4c7" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a>* <a class="el" href="classCVC3_1_1TheoremManager.html#a6357578327d823837e87ae5cc94bc4c7">CVC3::TheoremManager::d_rules</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_reflFlags" ref="ad747841b9ddd1fd27ab2d029ac93ab52" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><long, bool> <a class="el" href="classCVC3_1_1TheoremManager.html#ad747841b9ddd1fd27ab2d029ac93ab52">CVC3::TheoremManager::d_reflFlags</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_cachedValues" ref="a87b85aed87edec2b76d4093922d8d618" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><long, int> <a class="el" href="classCVC3_1_1TheoremManager.html#a87b85aed87edec2b76d4093922d8d618">CVC3::TheoremManager::d_cachedValues</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_expandFlags" ref="a56084d2a96b227c28f0a3ca74f5fd088" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><long, bool> <a class="el" href="classCVC3_1_1TheoremManager.html#a56084d2a96b227c28f0a3ca74f5fd088">CVC3::TheoremManager::d_expandFlags</a><code> [private]</code></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><!-- doxytag: member="CVC3::TheoremManager::d_litFlags" ref="a228b3c5064ff6c3d1c8bfa31363c1555" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><long, bool> <a class="el" href="classCVC3_1_1TheoremManager.html#a228b3c5064ff6c3d1c8bfa31363c1555">CVC3::TheoremManager::d_litFlags</a><code> [private]</code></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>
<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>
