<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: CVC3::TheoremValue Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a></li><li class="navelem"><a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a></li> </ul>
</div>
</div><!-- top -->
<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> |
<a href="classCVC3_1_1TheoremValue-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::TheoremValue Class Reference<span class="mlabels"><span class="mlabel">abstract</span></span></div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>></code></p>
<p>Inherited by <a class="el" href="classCVC3_1_1RegTheoremValue.html">CVC3::RegTheoremValue</a>, and <a class="el" href="classCVC3_1_1RWTheoremValue.html">CVC3::RWTheoremValue</a>.</p>
<div class="dynheader">
Collaboration diagram for CVC3::TheoremValue:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1TheoremValue__coll__graph.gif" border="0" usemap="#CVC3_1_1TheoremValue_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1TheoremValue_coll__map" id="CVC3_1_1TheoremValue_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:a9b8baaeba9459d6b036086f9d0d67a1b"><td class="memItemLeft" align="right" valign="top">virtual </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a9b8baaeba9459d6b036086f9d0d67a1b">~TheoremValue</a> ()</td></tr>
<tr class="separator:a9b8baaeba9459d6b036086f9d0d67a1b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6862e6f9c77deced7b0ae841c01af3a8"><td class="memItemLeft" align="right" valign="top">std::string </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a6862e6f9c77deced7b0ae841c01af3a8">toString</a> () const </td></tr>
<tr class="separator:a6862e6f9c77deced7b0ae841c01af3a8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af8bf999e469afe124c04bfbbb6aba1e2"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1MemoryManager.html">MemoryManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#af8bf999e469afe124c04bfbbb6aba1e2">getMM</a> ()=0</td></tr>
<tr class="separator:af8bf999e469afe124c04bfbbb6aba1e2"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pro-attribs"></a>
Protected Attributes</h2></td></tr>
<tr class="memitem:af0167eefead6921ed3919808bc0f9845"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#af0167eefead6921ed3919808bc0f9845">d_tm</a></td></tr>
<tr class="memdesc:af0167eefead6921ed3919808bc0f9845"><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> Manager. <a href="#af0167eefead6921ed3919808bc0f9845"></a><br/></td></tr>
<tr class="separator:af0167eefead6921ed3919808bc0f9845"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a702623ca8da01e55a811e573a82fd0e4"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a702623ca8da01e55a811e573a82fd0e4">d_thm</a></td></tr>
<tr class="memdesc:a702623ca8da01e55a811e573a82fd0e4"><td class="mdescLeft"> </td><td class="mdescRight">The expression representing a theorem. <a href="#a702623ca8da01e55a811e573a82fd0e4"></a><br/></td></tr>
<tr class="separator:a702623ca8da01e55a811e573a82fd0e4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5cf31c613884270c10170d87ff58817b"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Proof.html">Proof</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a5cf31c613884270c10170d87ff58817b">d_proof</a></td></tr>
<tr class="memdesc:a5cf31c613884270c10170d87ff58817b"><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classCVC3_1_1Proof.html">Proof</a> of the theorem. <a href="#a5cf31c613884270c10170d87ff58817b"></a><br/></td></tr>
<tr class="separator:a5cf31c613884270c10170d87ff58817b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a138c67c7a778d8e0d525a658439f105c"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a138c67c7a778d8e0d525a658439f105c">d_refcount</a></td></tr>
<tr class="memdesc:a138c67c7a778d8e0d525a658439f105c"><td class="mdescLeft"> </td><td class="mdescRight">How many pointers to this theorem value. <a href="#a138c67c7a778d8e0d525a658439f105c"></a><br/></td></tr>
<tr class="separator:a138c67c7a778d8e0d525a658439f105c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a44a5fb4e3e9d28ee1d32c2fa61e05d15"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a44a5fb4e3e9d28ee1d32c2fa61e05d15">d_scopeLevel</a></td></tr>
<tr class="memdesc:a44a5fb4e3e9d28ee1d32c2fa61e05d15"><td class="mdescLeft"> </td><td class="mdescRight">Largest scope level of the assumptions. <a href="#a44a5fb4e3e9d28ee1d32c2fa61e05d15"></a><br/></td></tr>
<tr class="separator:a44a5fb4e3e9d28ee1d32c2fa61e05d15"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a819e06a02c53175bf33d4d475bd15d09"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a819e06a02c53175bf33d4d475bd15d09">d_quantLevel</a></td></tr>
<tr class="memdesc:a819e06a02c53175bf33d4d475bd15d09"><td class="mdescLeft"> </td><td class="mdescRight">Quantification level of this theorem. <a href="#a819e06a02c53175bf33d4d475bd15d09"></a><br/></td></tr>
<tr class="separator:a819e06a02c53175bf33d4d475bd15d09"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1cec81e358483c5459d125eed27c5edf"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a1cec81e358483c5459d125eed27c5edf">d_flag</a></td></tr>
<tr class="memdesc:a1cec81e358483c5459d125eed27c5edf"><td class="mdescLeft"> </td><td class="mdescRight">debug quantlevel, this one is from proof, not from assumption list <a href="#a1cec81e358483c5459d125eed27c5edf"></a><br/></td></tr>
<tr class="separator:a1cec81e358483c5459d125eed27c5edf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae5df8e7dcf6660844d291e512b66516d"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#ae5df8e7dcf6660844d291e512b66516d">d_cachedValue</a>: 28</td></tr>
<tr class="memdesc:ae5df8e7dcf6660844d291e512b66516d"><td class="mdescLeft"> </td><td class="mdescRight">Temporary cache used during traversals. <a href="#ae5df8e7dcf6660844d291e512b66516d"></a><br/></td></tr>
<tr class="separator:ae5df8e7dcf6660844d291e512b66516d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa2eb4713aae1ff702316707578757b7d"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#aa2eb4713aae1ff702316707578757b7d">d_isSubst</a>: 1</td></tr>
<tr class="memdesc:aa2eb4713aae1ff702316707578757b7d"><td class="mdescLeft"> </td><td class="mdescRight">whether this theorem was generated by substitution <a href="#aa2eb4713aae1ff702316707578757b7d"></a><br/></td></tr>
<tr class="separator:aa2eb4713aae1ff702316707578757b7d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aac23fbc1ab6d8e32c7dc13bb11c7884d"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#aac23fbc1ab6d8e32c7dc13bb11c7884d">d_isAssump</a>: 1</td></tr>
<tr class="separator:aac23fbc1ab6d8e32c7dc13bb11c7884d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a74965c0ce02cfba99305eae7fa267ffe"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a74965c0ce02cfba99305eae7fa267ffe">d_expand</a>: 1</td></tr>
<tr class="memdesc:a74965c0ce02cfba99305eae7fa267ffe"><td class="mdescLeft"> </td><td class="mdescRight">whether it should this be expanded in graph traversal <a href="#a74965c0ce02cfba99305eae7fa267ffe"></a><br/></td></tr>
<tr class="separator:a74965c0ce02cfba99305eae7fa267ffe"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a376edd9ad7538621cc0fa2c07017c025"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a376edd9ad7538621cc0fa2c07017c025">d_clauselit</a>: 1</td></tr>
<tr class="memdesc:a376edd9ad7538621cc0fa2c07017c025"><td class="mdescLeft"> </td><td class="mdescRight">whether it belongs to the conflict clause <a href="#a376edd9ad7538621cc0fa2c07017c025"></a><br/></td></tr>
<tr class="separator:a376edd9ad7538621cc0fa2c07017c025"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-methods"></a>
Private Member Functions</h2></td></tr>
<tr class="memitem:a159a1ef9a2ff876cf9d31704ed23f816"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><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 <a class="el" href="classCVC3_1_1TheoremValue.html#aaaabd2fab47103f9a4574c380c790a11">isAssump</a>)</td></tr>
<tr class="separator:a159a1ef9a2ff876cf9d31704ed23f816"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ada947e18738c40ed80eb8b2e4fff499b"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#ada947e18738c40ed80eb8b2e4fff499b">TheoremValue</a> (const <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> &t)</td></tr>
<tr class="separator:ada947e18738c40ed80eb8b2e4fff499b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a217ca4cd1244901bded79a8a8be2692a"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a217ca4cd1244901bded79a8a8be2692a">operator=</a> (const <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> &t)</td></tr>
<tr class="separator:a217ca4cd1244901bded79a8a8be2692a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1b91df4037f8888079646e7aefe174a2"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a1b91df4037f8888079646e7aefe174a2">isFlagged</a> () const </td></tr>
<tr class="separator:a1b91df4037f8888079646e7aefe174a2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ace65848828d3d96490a45a52ff7f8f73"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#ace65848828d3d96490a45a52ff7f8f73">clearAllFlags</a> ()</td></tr>
<tr class="separator:ace65848828d3d96490a45a52ff7f8f73"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aee29e499025f39a5b04b610dee9dae0c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#aee29e499025f39a5b04b610dee9dae0c">setFlag</a> ()</td></tr>
<tr class="separator:aee29e499025f39a5b04b610dee9dae0c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9d2d00b50cf9eb8f5378cb8d289a412c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a9d2d00b50cf9eb8f5378cb8d289a412c">setCachedValue</a> (int value)</td></tr>
<tr class="separator:a9d2d00b50cf9eb8f5378cb8d289a412c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a223a1c591286bee75524a573bc87518e"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a223a1c591286bee75524a573bc87518e">getCachedValue</a> () const </td></tr>
<tr class="separator:a223a1c591286bee75524a573bc87518e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a31762e3d339154a150064b0e91c6497d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a31762e3d339154a150064b0e91c6497d">setSubst</a> ()</td></tr>
<tr class="separator:a31762e3d339154a150064b0e91c6497d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7bc742af6a03964e8c4d9fc876426e5e"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a7bc742af6a03964e8c4d9fc876426e5e">isSubst</a> ()</td></tr>
<tr class="separator:a7bc742af6a03964e8c4d9fc876426e5e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a67f5136c43e385f2398841f8ad94d18a"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a67f5136c43e385f2398841f8ad94d18a">setExpandFlag</a> (bool val)</td></tr>
<tr class="separator:a67f5136c43e385f2398841f8ad94d18a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae88fe39382cb64565b4a30a0ad170797"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#ae88fe39382cb64565b4a30a0ad170797">getExpandFlag</a> ()</td></tr>
<tr class="separator:ae88fe39382cb64565b4a30a0ad170797"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae9091cd1e351cd1e00f9f57e286e1414"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#ae9091cd1e351cd1e00f9f57e286e1414">setLitFlag</a> (bool val)</td></tr>
<tr class="separator:ae9091cd1e351cd1e00f9f57e286e1414"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a74e6ab319ca0b6945ae472ba30698aae"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a74e6ab319ca0b6945ae472ba30698aae">getLitFlag</a> ()</td></tr>
<tr class="separator:a74e6ab319ca0b6945ae472ba30698aae"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9c11008cb459d81b618c10913057435c"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a9c11008cb459d81b618c10913057435c">getScope</a> ()</td></tr>
<tr class="separator:a9c11008cb459d81b618c10913057435c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5548a7ad205c1fee8fa49309d865cf44"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a5548a7ad205c1fee8fa49309d865cf44">getQuantLevel</a> ()</td></tr>
<tr class="separator:a5548a7ad205c1fee8fa49309d865cf44"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae091d4527d043cdf0bd83ba56ab98ca3"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#ae091d4527d043cdf0bd83ba56ab98ca3">getQuantLevelDebug</a> ()</td></tr>
<tr class="separator:ae091d4527d043cdf0bd83ba56ab98ca3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4a305d7049aab9528a6205250303c574"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a4a305d7049aab9528a6205250303c574">setQuantLevel</a> (unsigned level)</td></tr>
<tr class="separator:a4a305d7049aab9528a6205250303c574"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa437b081740be2d064d8d71e1db90d04"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#aa437b081740be2d064d8d71e1db90d04">recQuantLevel</a> (<a class="el" href="classCVC3_1_1Expr.html">Expr</a> proof)</td></tr>
<tr class="separator:aa437b081740be2d064d8d71e1db90d04"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8f33f1f21c512afeed47e16346dd168c"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a8f33f1f21c512afeed47e16346dd168c">findQuantLevelDebug</a> ()</td></tr>
<tr class="separator:a8f33f1f21c512afeed47e16346dd168c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a123ac5cf8dde8d8ba3ca7d47a7d9bfde"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a123ac5cf8dde8d8ba3ca7d47a7d9bfde">isRewrite</a> () const </td></tr>
<tr class="separator:a123ac5cf8dde8d8ba3ca7d47a7d9bfde"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ada6a2145dda62e6d3bd6781c7ef96141"><td class="memItemLeft" align="right" valign="top">virtual const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#ada6a2145dda62e6d3bd6781c7ef96141">getExpr</a> () const </td></tr>
<tr class="separator:ada6a2145dda62e6d3bd6781c7ef96141"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a183c518edb1e346997882c5cce931fa3"><td class="memItemLeft" align="right" valign="top">virtual const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a183c518edb1e346997882c5cce931fa3">getLHS</a> () const </td></tr>
<tr class="separator:a183c518edb1e346997882c5cce931fa3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae28c3198351296f187065e78bba73a1f"><td class="memItemLeft" align="right" valign="top">virtual const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#ae28c3198351296f187065e78bba73a1f">getRHS</a> () const </td></tr>
<tr class="separator:ae28c3198351296f187065e78bba73a1f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a375f504a8a9844005b2eb8e055483829"><td class="memItemLeft" align="right" valign="top">virtual const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a375f504a8a9844005b2eb8e055483829">getAssumptionsRef</a> () const =0</td></tr>
<tr class="separator:a375f504a8a9844005b2eb8e055483829"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aaaabd2fab47103f9a4574c380c790a11"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#aaaabd2fab47103f9a4574c380c790a11">isAssump</a> () const </td></tr>
<tr class="separator:aaaabd2fab47103f9a4574c380c790a11"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af7120729a27c693ca032d176cf33e595"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Proof.html">Proof</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#af7120729a27c693ca032d176cf33e595">getProof</a> ()</td></tr>
<tr class="separator:af7120729a27c693ca032d176cf33e595"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="friends"></a>
Friends</h2></td></tr>
<tr class="memitem:a51f48d7e14c97707595cfe5f8f6df209"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a51f48d7e14c97707595cfe5f8f6df209">Theorem</a></td></tr>
<tr class="separator:a51f48d7e14c97707595cfe5f8f6df209"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2fc7fcb35dcb6d97f101ffb632ac1dcd"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#a2fc7fcb35dcb6d97f101ffb632ac1dcd">RegTheoremValue</a></td></tr>
<tr class="separator:a2fc7fcb35dcb6d97f101ffb632ac1dcd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:add1e5fec863ffafbd22cac7aa0d1b689"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1TheoremValue.html#add1e5fec863ffafbd22cac7aa0d1b689">RWTheoremValue</a></td></tr>
<tr class="separator:add1e5fec863ffafbd22cac7aa0d1b689"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="theorem__value_8h_source.html#l00056">56</a> of file <a class="el" href="theorem__value_8h_source.html">theorem_value.h</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a159a1ef9a2ff876cf9d31704ed23f816"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::TheoremValue::~TheoremValue </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </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>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="a217ca4cd1244901bded79a8a8be2692a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::isFlagged </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremValue::clearAllFlags </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremValue::setFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::TheoremValue::getCachedValue </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoremValue::setSubst </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::isSubst </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::getExpandFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::getLitFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::TheoremValue::getScope </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremValue::getQuantLevel </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremValue::getQuantLevelDebug </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremValue::findQuantLevelDebug </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual bool CVC3::TheoremValue::isRewrite </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span><span class="mlabel">virtual</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span><span class="mlabel">virtual</span></span> </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="vcl_8cpp_source.html#l00311">CVC3::VCL::deriveClosure()</a>, <a class="el" href="vcl_8cpp_source.html#l00381">CVC3::VCL::getAssumptions()</a>, <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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span><span class="mlabel">virtual</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span><span class="mlabel">virtual</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1RWTheoremValue.html#a90d334b1d81a6ecaed725b689920733c">CVC3::RWTheoremValue</a>, and <a class="el" href="classCVC3_1_1RegTheoremValue.html#a695377925f8cc4f3607f304bec4cc325">CVC3::RegTheoremValue</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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::isAssump </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Proof.html">Proof</a>& CVC3::TheoremValue::getProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">private</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::TheoremValue::toString </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="theorem__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="assumptions_8cpp_source.html#l00250">CVC3::Assumptions::toString()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1RWTheoremValue.html#a4593444ed15ecbd4b1be7b44e5b5bc48">CVC3::RWTheoremValue</a>, and <a class="el" href="classCVC3_1_1RegTheoremValue.html#a7ee05bf85a8647cfaf296a2d76091bc0">CVC3::RegTheoremValue</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>
<h2 class="groupheader">Friends And Related Function Documentation</h2>
<a class="anchor" id="a51f48d7e14c97707595cfe5f8f6df209"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1RegTheoremValue.html">RegTheoremValue</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1RWTheoremValue.html">RWTheoremValue</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </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>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="af0167eefead6921ed3919808bc0f9845"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* CVC3::TheoremValue::d_tm</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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#l00408">CVC3::RegTheoremValue::getMM()</a>, <a class="el" href="theorem__value_8h_source.html#l00532">CVC3::RWTheoremValue::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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> CVC3::TheoremValue::d_thm</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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#l00297">getExpr()</a>, <a class="el" href="theorem__value_8h_source.html#l00500">CVC3::RWTheoremValue::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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Proof.html">Proof</a> CVC3::TheoremValue::d_proof</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremValue::d_refcount</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::TheoremValue::d_scopeLevel</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremValue::d_quantLevel</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::TheoremValue::d_flag</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::TheoremValue::d_cachedValue</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::d_isSubst</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::d_isAssump</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::d_expand</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoremValue::d_clauselit</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:19 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
