<!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::TheoremValue 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_1TheoremValue.html">TheoremValue</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#friends">Friends</a> </div>
<div class="headertitle">
<div class="title">CVC3::TheoremValue Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::TheoremValue" -->
<p><code>#include <<a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CVC3::TheoremValue:</div>
<div class="dyncontent">
<div class="center">
<img src="classCVC3_1_1TheoremValue.png" usemap="#CVC3::TheoremValue_map" alt=""/>
<map id="CVC3::TheoremValue_map" name="CVC3::TheoremValue_map">
<area href="classCVC3_1_1RegTheoremValue.html" alt="CVC3::RegTheoremValue" shape="rect" coords="0,56,156,80"/>
<area href="classCVC3_1_1RWTheoremValue.html" alt="CVC3::RWTheoremValue" shape="rect" coords="166,56,322,80"/>
</map>
</div></div>
<p><a href="classCVC3_1_1TheoremValue-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li>virtual <a class="el" href="classCVC3_1_1TheoremValue.html#a9b8baaeba9459d6b036086f9d0d67a1b">~TheoremValue</a> ()
<li>std::string <a class="el" href="classCVC3_1_1TheoremValue.html#a6862e6f9c77deced7b0ae841c01af3a8">toString</a> () const
<li>virtual <a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * <a class="el" href="classCVC3_1_1TheoremValue.html#af8bf999e469afe124c04bfbbb6aba1e2">getMM</a> ()=0
</ul>
<h2><a name="pro-attribs"></a>
Protected Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * <a class="el" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845">d_tm</a>
<dl class="el"><dd class="mdescRight"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> Manager. <a href="#af0167eefead6921ed3919808bc0f9845"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4">d_thm</a>
<dl class="el"><dd class="mdescRight">The expression representing a theorem. <a href="#a702623ca8da01e55a811e573a82fd0e4"></a><br/></dl><li><a class="el" href="classCVC3_1_1Proof.html">Proof</a> <a class="el" href="classCVC3_1_1TheoremValue.html#a5cf31c613884270c10170d87ff58817b">d_proof</a>
<dl class="el"><dd class="mdescRight"><a class="el" href="classCVC3_1_1Proof.html">Proof</a> of the theorem. <a href="#a5cf31c613884270c10170d87ff58817b"></a><br/></dl><li>unsigned <a class="el" href="classCVC3_1_1TheoremValue.html#a138c67c7a778d8e0d525a658439f105c">d_refcount</a>
<dl class="el"><dd class="mdescRight">How many pointers to this theorem value. <a href="#a138c67c7a778d8e0d525a658439f105c"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15">d_scopeLevel</a>
<dl class="el"><dd class="mdescRight">Largest scope level of the assumptions. <a href="#a44a5fb4e3e9d28ee1d32c2fa61e05d15"></a><br/></dl><li>unsigned <a class="el" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09">d_quantLevel</a>
<dl class="el"><dd class="mdescRight">Quantification level of this theorem. <a href="#a819e06a02c53175bf33d4d475bd15d09"></a><br/></dl><li>unsigned <a class="el" href="classCVC3_1_1TheoremValue.html#a1cec81e358483c5459d125eed27c5edf">d_flag</a>
<dl class="el"><dd class="mdescRight">debug quantlevel, this one is from proof, not from assumption list <a href="#a1cec81e358483c5459d125eed27c5edf"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1TheoremValue.html#ae5df8e7dcf6660844d291e512b66516d">d_cachedValue</a>: 28
<dl class="el"><dd class="mdescRight">Temporary cache used during traversals. <a href="#ae5df8e7dcf6660844d291e512b66516d"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoremValue.html#aa2eb4713aae1ff702316707578757b7d">d_isSubst</a>: 1
<dl class="el"><dd class="mdescRight">whether this theorem was generated by substitution <a href="#aa2eb4713aae1ff702316707578757b7d"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoremValue.html#aac23fbc1ab6d8e32c7dc13bb11c7884d">d_isAssump</a>: 1
<li>bool <a class="el" href="classCVC3_1_1TheoremValue.html#a74965c0ce02cfba99305eae7fa267ffe">d_expand</a>: 1
<dl class="el"><dd class="mdescRight">whether it should this be expanded in graph traversal <a href="#a74965c0ce02cfba99305eae7fa267ffe"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoremValue.html#a376edd9ad7538621cc0fa2c07017c025">d_clauselit</a>: 1
<dl class="el"><dd class="mdescRight">whether it belongs to the conflict clause <a href="#a376edd9ad7538621cc0fa2c07017c025"></a><br/></dl></ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1TheoremValue.html#a159a1ef9a2ff876cf9d31704ed23f816">TheoremValue</a> (<a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> *tm, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &thm, const <a class="el" href="classCVC3_1_1Proof.html">Proof</a> &pf, bool isAssump)
<li><a class="el" href="classCVC3_1_1TheoremValue.html#ada947e18738c40ed80eb8b2e4fff499b">TheoremValue</a> (const <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> &t)
<li><a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> & <a class="el" href="classCVC3_1_1TheoremValue.html#a217ca4cd1244901bded79a8a8be2692a">operator=</a> (const <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> &t)
<li>bool <a class="el" href="classCVC3_1_1TheoremValue.html#a1b91df4037f8888079646e7aefe174a2">isFlagged</a> () const
<li>void <a class="el" href="classCVC3_1_1TheoremValue.html#ace65848828d3d96490a45a52ff7f8f73">clearAllFlags</a> ()
<li>void <a class="el" href="classCVC3_1_1TheoremValue.html#aee29e499025f39a5b04b610dee9dae0c">setFlag</a> ()
<li>void <a class="el" href="classCVC3_1_1TheoremValue.html#a9d2d00b50cf9eb8f5378cb8d289a412c">setCachedValue</a> (int value)
<li>int <a class="el" href="classCVC3_1_1TheoremValue.html#a223a1c591286bee75524a573bc87518e">getCachedValue</a> () const
<li>void <a class="el" href="classCVC3_1_1TheoremValue.html#a31762e3d339154a150064b0e91c6497d">setSubst</a> ()
<li>bool <a class="el" href="classCVC3_1_1TheoremValue.html#a7bc742af6a03964e8c4d9fc876426e5e">isSubst</a> ()
<li>void <a class="el" href="classCVC3_1_1TheoremValue.html#a67f5136c43e385f2398841f8ad94d18a">setExpandFlag</a> (bool val)
<li>bool <a class="el" href="classCVC3_1_1TheoremValue.html#ae88fe39382cb64565b4a30a0ad170797">getExpandFlag</a> ()
<li>void <a class="el" href="classCVC3_1_1TheoremValue.html#ae9091cd1e351cd1e00f9f57e286e1414">setLitFlag</a> (bool val)
<li>bool <a class="el" href="classCVC3_1_1TheoremValue.html#a74e6ab319ca0b6945ae472ba30698aae">getLitFlag</a> ()
<li>int <a class="el" href="classCVC3_1_1TheoremValue.html#a9c11008cb459d81b618c10913057435c">getScope</a> ()
<li>unsigned <a class="el" href="classCVC3_1_1TheoremValue.html#a5548a7ad205c1fee8fa49309d865cf44">getQuantLevel</a> ()
<li>unsigned <a class="el" href="classCVC3_1_1TheoremValue.html#ae091d4527d043cdf0bd83ba56ab98ca3">getQuantLevelDebug</a> ()
<li>void <a class="el" href="classCVC3_1_1TheoremValue.html#a4a305d7049aab9528a6205250303c574">setQuantLevel</a> (unsigned level)
<li>unsigned <a class="el" href="classCVC3_1_1TheoremValue.html#aa437b081740be2d064d8d71e1db90d04">recQuantLevel</a> (<a class="el" href="classCVC3_1_1Expr.html">Expr</a> proof)
<li>unsigned <a class="el" href="classCVC3_1_1TheoremValue.html#a8f33f1f21c512afeed47e16346dd168c">findQuantLevelDebug</a> ()
<li>virtual bool <a class="el" href="classCVC3_1_1TheoremValue.html#a123ac5cf8dde8d8ba3ca7d47a7d9bfde">isRewrite</a> () const
<li>virtual const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1TheoremValue.html#ada6a2145dda62e6d3bd6781c7ef96141">getExpr</a> () const
<li>virtual const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1TheoremValue.html#a183c518edb1e346997882c5cce931fa3">getLHS</a> () const
<li>virtual const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1TheoremValue.html#ae28c3198351296f187065e78bba73a1f">getRHS</a> () const
<li>virtual const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & <a class="el" href="classCVC3_1_1TheoremValue.html#a375f504a8a9844005b2eb8e055483829">getAssumptionsRef</a> () const =0
<li>bool <a class="el" href="classCVC3_1_1TheoremValue.html#aaaabd2fab47103f9a4574c380c790a11">isAssump</a> () const
<li>const <a class="el" href="classCVC3_1_1Proof.html">Proof</a> & <a class="el" href="classCVC3_1_1TheoremValue.html#af7120729a27c693ca032d176cf33e595">getProof</a> ()
</ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1TheoremValue.html#a51f48d7e14c97707595cfe5f8f6df209">Theorem</a>
<li>class <a class="el" href="classCVC3_1_1TheoremValue.html#a2fc7fcb35dcb6d97f101ffb632ac1dcd">RegTheoremValue</a>
<li>class <a class="el" href="classCVC3_1_1TheoremValue.html#add1e5fec863ffafbd22cac7aa0d1b689">RWTheoremValue</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__value_8h_source.html#l00056">56</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a159a1ef9a2ff876cf9d31704ed23f816"></a><!-- doxytag: member="CVC3::TheoremValue::TheoremValue" ref="a159a1ef9a2ff876cf9d31704ed23f816" args="(TheoremManager *tm, const Expr &thm, const Proof &pf, bool isAssump)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::TheoremValue::TheoremValue </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * </td>
<td class="paramname"><em>tm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>thm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Proof.html">Proof</a> & </td>
<td class="paramname"><em>pf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>isAssump</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>NOTE: it is private; only friend classes can call it.</p>
<p>If the assumptions refer to only one theorem, grab the assumptions of that theorem instead. </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00110">110</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
</div>
</div>
<a class="anchor" id="ada947e18738c40ed80eb8b2e4fff499b"></a><!-- doxytag: member="CVC3::TheoremValue::TheoremValue" ref="ada947e18738c40ed80eb8b2e4fff499b" args="(const TheoremValue &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::TheoremValue::TheoremValue </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> & </td>
<td class="paramname"><em>t</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00117">117</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>.</p>
</div>
</div>
<a class="anchor" id="a9b8baaeba9459d6b036086f9d0d67a1b"></a><!-- doxytag: member="CVC3::TheoremValue::~TheoremValue" ref="a9b8baaeba9459d6b036086f9d0d67a1b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::TheoremValue::~TheoremValue </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00320">320</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00074">d_refcount</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, and <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a217ca4cd1244901bded79a8a8be2692a"></a><!-- doxytag: member="CVC3::TheoremValue::operator=" ref="a217ca4cd1244901bded79a8a8be2692a" args="(const TheoremValue &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>& CVC3::TheoremValue::operator= </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> & </td>
<td class="paramname"><em>t</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00120">120</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>.</p>
</div>
</div>
<a class="anchor" id="a1b91df4037f8888079646e7aefe174a2"></a><!-- doxytag: member="CVC3::TheoremValue::isFlagged" ref="a1b91df4037f8888079646e7aefe174a2" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::isFlagged </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00125">125</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00087">d_flag</a>, <a class="el" href="theorem__value_8h_source.html#l00065">d_tm</a>, and <a class="el" href="theorem__manager_8h_source.html#l00082">CVC3::TheoremManager::getFlag()</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="ace65848828d3d96490a45a52ff7f8f73"></a><!-- doxytag: member="CVC3::TheoremValue::clearAllFlags" ref="ace65848828d3d96490a45a52ff7f8f73" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremValue::clearAllFlags </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00129">129</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__manager_8h_source.html#l00086">CVC3::TheoremManager::clearAllFlags()</a>, and <a class="el" href="theorem__value_8h_source.html#l00065">d_tm</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00422">CVC3::Theorem::clearAllFlags()</a>.</p>
</div>
</div>
<a class="anchor" id="aee29e499025f39a5b04b610dee9dae0c"></a><!-- doxytag: member="CVC3::TheoremValue::setFlag" ref="aee29e499025f39a5b04b610dee9dae0c" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremValue::setFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00133">133</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00087">d_flag</a>, <a class="el" href="theorem__value_8h_source.html#l00065">d_tm</a>, and <a class="el" href="theorem__manager_8h_source.html#l00082">CVC3::TheoremManager::getFlag()</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="a9d2d00b50cf9eb8f5378cb8d289a412c"></a><!-- doxytag: member="CVC3::TheoremValue::setCachedValue" ref="a9d2d00b50cf9eb8f5378cb8d289a412c" args="(int value)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremValue::setCachedValue </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>value</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00137">137</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00090">d_cachedValue</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="a223a1c591286bee75524a573bc87518e"></a><!-- doxytag: member="CVC3::TheoremValue::getCachedValue" ref="a223a1c591286bee75524a573bc87518e" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::TheoremValue::getCachedValue </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00141">141</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00090">d_cachedValue</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="a31762e3d339154a150064b0e91c6497d"></a><!-- doxytag: member="CVC3::TheoremValue::setSubst" ref="a31762e3d339154a150064b0e91c6497d" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremValue::setSubst </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00145">145</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00092">d_isSubst</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00447">CVC3::Theorem::setSubst()</a>.</p>
</div>
</div>
<a class="anchor" id="a7bc742af6a03964e8c4d9fc876426e5e"></a><!-- doxytag: member="CVC3::TheoremValue::isSubst" ref="a7bc742af6a03964e8c4d9fc876426e5e" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::isSubst </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00146">146</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00092">d_isSubst</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00452">CVC3::Theorem::isSubst()</a>.</p>
</div>
</div>
<a class="anchor" id="a67f5136c43e385f2398841f8ad94d18a"></a><!-- doxytag: member="CVC3::TheoremValue::setExpandFlag" ref="a67f5136c43e385f2398841f8ad94d18a" args="(bool val)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremValue::setExpandFlag </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>val</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00148">148</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00094">d_expand</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="ae88fe39382cb64565b4a30a0ad170797"></a><!-- doxytag: member="CVC3::TheoremValue::getExpandFlag" ref="ae88fe39382cb64565b4a30a0ad170797" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::getExpandFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00152">152</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00094">d_expand</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="ae9091cd1e351cd1e00f9f57e286e1414"></a><!-- doxytag: member="CVC3::TheoremValue::setLitFlag" ref="ae9091cd1e351cd1e00f9f57e286e1414" args="(bool val)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremValue::setLitFlag </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>val</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00156">156</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00095">d_clauselit</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="a74e6ab319ca0b6945ae472ba30698aae"></a><!-- doxytag: member="CVC3::TheoremValue::getLitFlag" ref="a74e6ab319ca0b6945ae472ba30698aae" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::getLitFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00160">160</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00095">d_clauselit</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00476">CVC3::Theorem::getLitFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a9c11008cb459d81b618c10913057435c"></a><!-- doxytag: member="CVC3::TheoremValue::getScope" ref="a9c11008cb459d81b618c10913057435c" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::TheoremValue::getScope </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00164">164</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00077">d_scopeLevel</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00486">CVC3::Theorem::getScope()</a>.</p>
</div>
</div>
<a class="anchor" id="a5548a7ad205c1fee8fa49309d865cf44"></a><!-- doxytag: member="CVC3::TheoremValue::getQuantLevel" ref="a5548a7ad205c1fee8fa49309d865cf44" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremValue::getQuantLevel </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00168">168</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00080">d_quantLevel</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00491">CVC3::Theorem::getQuantLevel()</a>.</p>
</div>
</div>
<a class="anchor" id="ae091d4527d043cdf0bd83ba56ab98ca3"></a><!-- doxytag: member="CVC3::TheoremValue::getQuantLevelDebug" ref="ae091d4527d043cdf0bd83ba56ab98ca3" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremValue::getQuantLevelDebug </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00170">170</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00497">CVC3::Theorem::getQuantLevelDebug()</a>.</p>
</div>
</div>
<a class="anchor" id="a4a305d7049aab9528a6205250303c574"></a><!-- doxytag: member="CVC3::TheoremValue::setQuantLevel" ref="a4a305d7049aab9528a6205250303c574" args="(unsigned level)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremValue::setQuantLevel </td>
<td>(</td>
<td class="paramtype">unsigned </td>
<td class="paramname"><em>level</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00175">175</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00080">d_quantLevel</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00504">CVC3::Theorem::setQuantLevel()</a>.</p>
</div>
</div>
<a class="anchor" id="aa437b081740be2d064d8d71e1db90d04"></a><!-- doxytag: member="CVC3::TheoremValue::recQuantLevel" ref="aa437b081740be2d064d8d71e1db90d04" args="(Expr proof)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremValue::recQuantLevel </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td>
<td class="paramname"><em>proof</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00177">177</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00080">d_quantLevel</a>.</p>
</div>
</div>
<a class="anchor" id="a8f33f1f21c512afeed47e16346dd168c"></a><!-- doxytag: member="CVC3::TheoremValue::findQuantLevelDebug" ref="a8f33f1f21c512afeed47e16346dd168c" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremValue::findQuantLevelDebug </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00247">247</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00080">d_quantLevel</a>.</p>
</div>
</div>
<a class="anchor" id="a123ac5cf8dde8d8ba3ca7d47a7d9bfde"></a><!-- doxytag: member="CVC3::TheoremValue::isRewrite" ref="a123ac5cf8dde8d8ba3ca7d47a7d9bfde" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual bool CVC3::TheoremValue::isRewrite </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, private, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCVC3_1_1RWTheoremValue.html#a6fdd9581600000bdb9b521203e20275b">CVC3::RWTheoremValue</a>.</p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00295">295</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00298">getLHS()</a>, <a class="el" href="theorem__value_8h_source.html#l00305">getRHS()</a>, and <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="ada6a2145dda62e6d3bd6781c7ef96141"></a><!-- doxytag: member="CVC3::TheoremValue::getExpr" ref="ada6a2145dda62e6d3bd6781c7ef96141" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual const <a class="el" href="classCVC3_1_1Expr.html">Expr</a>& CVC3::TheoremValue::getExpr </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, private, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCVC3_1_1RWTheoremValue.html#a84ba3b591680ab321aa2f855298a41f2">CVC3::RWTheoremValue</a>.</p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00297">297</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00068">d_thm</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, and <a class="el" href="theorem__value_8h_source.html#l00325">toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a183c518edb1e346997882c5cce931fa3"></a><!-- doxytag: member="CVC3::TheoremValue::getLHS" ref="a183c518edb1e346997882c5cce931fa3" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual const <a class="el" href="classCVC3_1_1Expr.html">Expr</a>& CVC3::TheoremValue::getLHS </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, private, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCVC3_1_1RWTheoremValue.html#ac3a024c1f0a4aa4cf8d8aa6200ac9911">CVC3::RWTheoremValue</a>.</p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00298">298</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00068">d_thm</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem__value_8h_source.html#l00295">isRewrite()</a>, and <a class="el" href="theorem__value_8h_source.html#l00325">toString()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>.</p>
</div>
</div>
<a class="anchor" id="ae28c3198351296f187065e78bba73a1f"></a><!-- doxytag: member="CVC3::TheoremValue::getRHS" ref="ae28c3198351296f187065e78bba73a1f" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual const <a class="el" href="classCVC3_1_1Expr.html">Expr</a>& CVC3::TheoremValue::getRHS </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, private, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCVC3_1_1RWTheoremValue.html#a61466f64bcb5fd3664fe2bed35ad7f97">CVC3::RWTheoremValue</a>.</p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00305">305</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00068">d_thm</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem__value_8h_source.html#l00295">isRewrite()</a>, and <a class="el" href="theorem__value_8h_source.html#l00325">toString()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>.</p>
</div>
</div>
<a class="anchor" id="a375f504a8a9844005b2eb8e055483829"></a><!-- doxytag: member="CVC3::TheoremValue::getAssumptionsRef" ref="a375f504a8a9844005b2eb8e055483829" args="() const =0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a>& CVC3::TheoremValue::getAssumptionsRef </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [private, pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1RegTheoremValue.html#a695377925f8cc4f3607f304bec4cc325">CVC3::RegTheoremValue</a>, and <a class="el" href="classCVC3_1_1RWTheoremValue.html#a90d334b1d81a6ecaed725b689920733c">CVC3::RWTheoremValue</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, and <a class="el" href="theorem__value_8h_source.html#l00325">toString()</a>.</p>
</div>
</div>
<a class="anchor" id="aaaabd2fab47103f9a4574c380c790a11"></a><!-- doxytag: member="CVC3::TheoremValue::isAssump" ref="aaaabd2fab47103f9a4574c380c790a11" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::isAssump </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00315">315</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00093">d_isAssump</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00395">CVC3::Theorem::isAssump()</a>.</p>
</div>
</div>
<a class="anchor" id="af7120729a27c693ca032d176cf33e595"></a><!-- doxytag: member="CVC3::TheoremValue::getProof" ref="af7120729a27c693ca032d176cf33e595" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Proof.html">Proof</a>& CVC3::TheoremValue::getProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00316">316</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00071">d_proof</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a6862e6f9c77deced7b0ae841c01af3a8"></a><!-- doxytag: member="CVC3::TheoremValue::toString" ref="a6862e6f9c77deced7b0ae841c01af3a8" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::TheoremValue::toString </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__value_8h_source.html#l00325">325</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>References <a class="el" href="classCVC3_1_1TheoremValue.html#a375f504a8a9844005b2eb8e055483829">getAssumptionsRef()</a>, <a class="el" href="theorem__value_8h_source.html#l00297">getExpr()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="assumptions_8cpp_source.html#l00250">CVC3::Assumptions::toString()</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00298">getLHS()</a>, and <a class="el" href="theorem__value_8h_source.html#l00305">getRHS()</a>.</p>
</div>
</div>
<a class="anchor" id="af8bf999e469afe124c04bfbbb6aba1e2"></a><!-- doxytag: member="CVC3::TheoremValue::getMM" ref="af8bf999e469afe124c04bfbbb6aba1e2" args="()=0" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual <a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* CVC3::TheoremValue::getMM </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [pure virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1RegTheoremValue.html#a7ee05bf85a8647cfaf296a2d76091bc0">CVC3::RegTheoremValue</a>, and <a class="el" href="classCVC3_1_1RWTheoremValue.html#a4593444ed15ecbd4b1be7b44e5b5bc48">CVC3::RWTheoremValue</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00091">CVC3::Theorem::operator=()</a>, and <a class="el" href="theorem_8cpp_source.html#l00188">CVC3::Theorem::~Theorem()</a>.</p>
</div>
</div>
<hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="a51f48d7e14c97707595cfe5f8f6df209"></a><!-- doxytag: member="CVC3::TheoremValue::Theorem" ref="a51f48d7e14c97707595cfe5f8f6df209" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCVC3_1_1RegTheoremValue.html#a51f48d7e14c97707595cfe5f8f6df209">CVC3::RegTheoremValue</a>, and <a class="el" href="classCVC3_1_1RWTheoremValue.html#a51f48d7e14c97707595cfe5f8f6df209">CVC3::RWTheoremValue</a>.</p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00059">59</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
</div>
</div>
<a class="anchor" id="a2fc7fcb35dcb6d97f101ffb632ac1dcd"></a><!-- doxytag: member="CVC3::TheoremValue::RegTheoremValue" ref="a2fc7fcb35dcb6d97f101ffb632ac1dcd" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1RegTheoremValue.html">RegTheoremValue</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00060">60</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
</div>
</div>
<a class="anchor" id="add1e5fec863ffafbd22cac7aa0d1b689"></a><!-- doxytag: member="CVC3::TheoremValue::RWTheoremValue" ref="add1e5fec863ffafbd22cac7aa0d1b689" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1RWTheoremValue.html">RWTheoremValue</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00061">61</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="af0167eefead6921ed3919808bc0f9845"></a><!-- doxytag: member="CVC3::TheoremValue::d_tm" ref="af0167eefead6921ed3919808bc0f9845" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* <a class="el" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845">CVC3::TheoremValue::d_tm</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> Manager. </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00065">65</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00129">clearAllFlags()</a>, <a class="el" href="theorem__value_8h_source.html#l00532">CVC3::RWTheoremValue::getMM()</a>, <a class="el" href="theorem__value_8h_source.html#l00408">CVC3::RegTheoremValue::getMM()</a>, <a class="el" href="theorem__value_8h_source.html#l00444">CVC3::RWTheoremValue::init()</a>, <a class="el" href="theorem__value_8h_source.html#l00125">isFlagged()</a>, <a class="el" href="theorem__value_8h_source.html#l00354">CVC3::RegTheoremValue::RegTheoremValue()</a>, <a class="el" href="theorem__value_8h_source.html#l00133">setFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00219">CVC3::Theorem::withAssumptions()</a>, and <a class="el" href="theorem_8cpp_source.html#l00214">CVC3::Theorem::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a702623ca8da01e55a811e573a82fd0e4"></a><!-- doxytag: member="CVC3::TheoremValue::d_thm" ref="a702623ca8da01e55a811e573a82fd0e4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4">CVC3::TheoremValue::d_thm</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The expression representing a theorem. </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00068">68</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00500">CVC3::RWTheoremValue::getExpr()</a>, <a class="el" href="theorem__value_8h_source.html#l00297">getExpr()</a>, <a class="el" href="theorem__value_8h_source.html#l00298">getLHS()</a>, and <a class="el" href="theorem__value_8h_source.html#l00305">getRHS()</a>.</p>
</div>
</div>
<a class="anchor" id="a5cf31c613884270c10170d87ff58817b"></a><!-- doxytag: member="CVC3::TheoremValue::d_proof" ref="a5cf31c613884270c10170d87ff58817b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Proof.html">Proof</a> <a class="el" href="classCVC3_1_1TheoremValue.html#a5cf31c613884270c10170d87ff58817b">CVC3::TheoremValue::d_proof</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><a class="el" href="classCVC3_1_1Proof.html">Proof</a> of the theorem. </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00071">71</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00316">getProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a138c67c7a778d8e0d525a658439f105c"></a><!-- doxytag: member="CVC3::TheoremValue::d_refcount" ref="a138c67c7a778d8e0d525a658439f105c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned <a class="el" href="classCVC3_1_1TheoremValue.html#a138c67c7a778d8e0d525a658439f105c">CVC3::TheoremValue::d_refcount</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>How many pointers to this theorem value. </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00074">74</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00444">CVC3::RWTheoremValue::init()</a>, <a class="el" href="theorem_8cpp_source.html#l00091">CVC3::Theorem::operator=()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">CVC3::Theorem::print()</a>, <a class="el" href="theorem__value_8h_source.html#l00354">CVC3::RegTheoremValue::RegTheoremValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00131">CVC3::Theorem::Theorem()</a>, <a class="el" href="theorem_8cpp_source.html#l00188">CVC3::Theorem::~Theorem()</a>, and <a class="el" href="theorem__value_8h_source.html#l00320">~TheoremValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a44a5fb4e3e9d28ee1d32c2fa61e05d15"></a><!-- doxytag: member="CVC3::TheoremValue::d_scopeLevel" ref="a44a5fb4e3e9d28ee1d32c2fa61e05d15" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15">CVC3::TheoremValue::d_scopeLevel</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Largest scope level of the assumptions. </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00077">77</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00164">getScope()</a>, <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="a819e06a02c53175bf33d4d475bd15d09"></a><!-- doxytag: member="CVC3::TheoremValue::d_quantLevel" ref="a819e06a02c53175bf33d4d475bd15d09" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned <a class="el" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09">CVC3::TheoremValue::d_quantLevel</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Quantification level of this theorem. </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00080">80</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00247">findQuantLevelDebug()</a>, <a class="el" href="theorem__value_8h_source.html#l00168">getQuantLevel()</a>, <a class="el" href="theorem__value_8h_source.html#l00444">CVC3::RWTheoremValue::init()</a>, <a class="el" href="theorem__value_8h_source.html#l00177">recQuantLevel()</a>, <a class="el" href="theorem__value_8h_source.html#l00354">CVC3::RegTheoremValue::RegTheoremValue()</a>, and <a class="el" href="theorem__value_8h_source.html#l00175">setQuantLevel()</a>.</p>
</div>
</div>
<a class="anchor" id="a1cec81e358483c5459d125eed27c5edf"></a><!-- doxytag: member="CVC3::TheoremValue::d_flag" ref="a1cec81e358483c5459d125eed27c5edf" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned <a class="el" href="classCVC3_1_1TheoremValue.html#a1cec81e358483c5459d125eed27c5edf">CVC3::TheoremValue::d_flag</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>debug quantlevel, this one is from proof, not from assumption list </p>
<p>Temporary flag used during traversals </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00087">87</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00125">isFlagged()</a>, and <a class="el" href="theorem__value_8h_source.html#l00133">setFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="ae5df8e7dcf6660844d291e512b66516d"></a><!-- doxytag: member="CVC3::TheoremValue::d_cachedValue" ref="ae5df8e7dcf6660844d291e512b66516d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCVC3_1_1TheoremValue.html#ae5df8e7dcf6660844d291e512b66516d">CVC3::TheoremValue::d_cachedValue</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Temporary cache used during traversals. </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00090">90</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00141">getCachedValue()</a>, and <a class="el" href="theorem__value_8h_source.html#l00137">setCachedValue()</a>.</p>
</div>
</div>
<a class="anchor" id="aa2eb4713aae1ff702316707578757b7d"></a><!-- doxytag: member="CVC3::TheoremValue::d_isSubst" ref="aa2eb4713aae1ff702316707578757b7d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1TheoremValue.html#aa2eb4713aae1ff702316707578757b7d">CVC3::TheoremValue::d_isSubst</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>whether this theorem was generated by substitution </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00092">92</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00146">isSubst()</a>, and <a class="el" href="theorem__value_8h_source.html#l00145">setSubst()</a>.</p>
</div>
</div>
<a class="anchor" id="aac23fbc1ab6d8e32c7dc13bb11c7884d"></a><!-- doxytag: member="CVC3::TheoremValue::d_isAssump" ref="aac23fbc1ab6d8e32c7dc13bb11c7884d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1TheoremValue.html#aac23fbc1ab6d8e32c7dc13bb11c7884d">CVC3::TheoremValue::d_isAssump</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00093">93</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00444">CVC3::RWTheoremValue::init()</a>, <a class="el" href="theorem__value_8h_source.html#l00315">isAssump()</a>, <a class="el" href="theorem__value_8h_source.html#l00397">CVC3::RegTheoremValue::~RegTheoremValue()</a>, and <a class="el" href="theorem__value_8h_source.html#l00516">CVC3::RWTheoremValue::~RWTheoremValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a74965c0ce02cfba99305eae7fa267ffe"></a><!-- doxytag: member="CVC3::TheoremValue::d_expand" ref="a74965c0ce02cfba99305eae7fa267ffe" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1TheoremValue.html#a74965c0ce02cfba99305eae7fa267ffe">CVC3::TheoremValue::d_expand</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>whether it should this be expanded in graph traversal </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00094">94</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00152">getExpandFlag()</a>, and <a class="el" href="theorem__value_8h_source.html#l00148">setExpandFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a376edd9ad7538621cc0fa2c07017c025"></a><!-- doxytag: member="CVC3::TheoremValue::d_clauselit" ref="a376edd9ad7538621cc0fa2c07017c025" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1TheoremValue.html#a376edd9ad7538621cc0fa2c07017c025">CVC3::TheoremValue::d_clauselit</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>whether it belongs to the conflict clause </p>
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00095">95</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
<p>Referenced by <a class="el" href="theorem__value_8h_source.html#l00160">getLitFlag()</a>, and <a class="el" href="theorem__value_8h_source.html#l00156">setLitFlag()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following file:<ul>
<li><a class="el" href="theorem__value_8h_source.html">theorem_value.h</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>
