<!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::Variable 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_1Variable.html">Variable</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="#friends">Friends</a> |
<a href="classCVC3_1_1Variable-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::Variable Class Reference</div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="variable_8h_source.html">variable.h</a>></code></p>
<div class="dynheader">
Collaboration diagram for CVC3::Variable:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1Variable__coll__graph.gif" border="0" usemap="#CVC3_1_1Variable_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1Variable_coll__map" id="CVC3_1_1Variable_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:a7659f63344c25dbc8209c4c531b2f0be"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a7659f63344c25dbc8209c4c531b2f0be">Variable</a> ()</td></tr>
<tr class="separator:a7659f63344c25dbc8209c4c531b2f0be"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a32d191ff6db4d462c902f07fe4d5045b"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a32d191ff6db4d462c902f07fe4d5045b">Variable</a> (<a class="el" href="classCVC3_1_1VariableManager.html">VariableManager</a> *vm, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a32d191ff6db4d462c902f07fe4d5045b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a76a03757802705d6496c35f296a935aa"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a76a03757802705d6496c35f296a935aa">Variable</a> (const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> &l)</td></tr>
<tr class="separator:a76a03757802705d6496c35f296a935aa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a21a9c85dd3b1320e8192fd581da15af4"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a21a9c85dd3b1320e8192fd581da15af4">~Variable</a> ()</td></tr>
<tr class="separator:a21a9c85dd3b1320e8192fd581da15af4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a551554c97de770f4160444c440342ac5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Variable.html">Variable</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a551554c97de770f4160444c440342ac5">operator=</a> (const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> &l)</td></tr>
<tr class="separator:a551554c97de770f4160444c440342ac5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a35c435274fa96599d47f16239b843584"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a> () const </td></tr>
<tr class="separator:a35c435274fa96599d47f16239b843584"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af85a6bbfd1529fce66f70d0012556fdf"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#af85a6bbfd1529fce66f70d0012556fdf">getExpr</a> () const </td></tr>
<tr class="separator:af85a6bbfd1529fce66f70d0012556fdf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6d8d3752f50dc4ce55d12e252398c837"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a6d8d3752f50dc4ce55d12e252398c837">getNegExpr</a> () const </td></tr>
<tr class="separator:a6d8d3752f50dc4ce55d12e252398c837"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a36e8ce7a305e07e00adc90f6c22c4916"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a36e8ce7a305e07e00adc90f6c22c4916">getValue</a> () const </td></tr>
<tr class="separator:a36e8ce7a305e07e00adc90f6c22c4916"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6e50e61e2eaf7054bd1d84e4137ba270"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a6e50e61e2eaf7054bd1d84e4137ba270">getScope</a> () const </td></tr>
<tr class="separator:a6e50e61e2eaf7054bd1d84e4137ba270"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6cdc655ea6aaf36c8e8029af0dc41075"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a6cdc655ea6aaf36c8e8029af0dc41075">getTheorem</a> () const </td></tr>
<tr class="separator:a6cdc655ea6aaf36c8e8029af0dc41075"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5bbd362f586ab0dbbc3432d140f77aab"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a5bbd362f586ab0dbbc3432d140f77aab">getAntecedent</a> () const </td></tr>
<tr class="separator:a5bbd362f586ab0dbbc3432d140f77aab"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a681407094080368feea5c496ed3bdb69"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a681407094080368feea5c496ed3bdb69">getAntecedentIdx</a> () const </td></tr>
<tr class="separator:a681407094080368feea5c496ed3bdb69"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a535715bc38709f902feb3f77aef4f89d"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a535715bc38709f902feb3f77aef4f89d">getAssumpThm</a> () const </td></tr>
<tr class="separator:a535715bc38709f902feb3f77aef4f89d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac1d2bf9a1a8eec600ffa18b679ef4d2c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#ac1d2bf9a1a8eec600ffa18b679ef4d2c">setValue</a> (int val, const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> &c, int idx)</td></tr>
<tr class="separator:ac1d2bf9a1a8eec600ffa18b679ef4d2c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a860c092f668decb472202b137ca6e683"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a860c092f668decb472202b137ca6e683">setValue</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)</td></tr>
<tr class="separator:a860c092f668decb472202b137ca6e683"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aeccc8931258bf6931c9a40a82e761144"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#aeccc8931258bf6931c9a40a82e761144">setValue</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm, int scope)</td></tr>
<tr class="separator:aeccc8931258bf6931c9a40a82e761144"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a688678fbc2dc4e25d9dbba2e4c7d72a5"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a688678fbc2dc4e25d9dbba2e4c7d72a5">setAssumpThm</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a, int scope)</td></tr>
<tr class="separator:a688678fbc2dc4e25d9dbba2e4c7d72a5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad499afb9e33f92c2efd7cf92638e0396"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#ad499afb9e33f92c2efd7cf92638e0396">deriveTheorem</a> () const </td></tr>
<tr class="separator:ad499afb9e33f92c2efd7cf92638e0396"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac78bae977cd6dead5e79debc77f52efc"><td class="memItemLeft" align="right" valign="top">unsigned & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#ac78bae977cd6dead5e79debc77f52efc">count</a> (bool neg)</td></tr>
<tr class="separator:ac78bae977cd6dead5e79debc77f52efc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acc8e18908c0b3c74811225c58f57c50d"><td class="memItemLeft" align="right" valign="top">unsigned & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#acc8e18908c0b3c74811225c58f57c50d">countPrev</a> (bool neg)</td></tr>
<tr class="separator:acc8e18908c0b3c74811225c58f57c50d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa4c74c18d5e3b6dff3a87dbb9600ea54"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#aa4c74c18d5e3b6dff3a87dbb9600ea54">score</a> (bool neg)</td></tr>
<tr class="separator:aa4c74c18d5e3b6dff3a87dbb9600ea54"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0e4d827e11f6308f9c9bc957f0f7d2f7"><td class="memItemLeft" align="right" valign="top">bool & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a0e4d827e11f6308f9c9bc957f0f7d2f7">added</a> (bool neg)</td></tr>
<tr class="separator:a0e4d827e11f6308f9c9bc957f0f7d2f7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac14d877633308fefc91fea8a07005fee"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#ac14d877633308fefc91fea8a07005fee">count</a> (bool neg) const </td></tr>
<tr class="separator:ac14d877633308fefc91fea8a07005fee"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a987bd4125ec63afc7577b3dbf9cb7b76"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a987bd4125ec63afc7577b3dbf9cb7b76">countPrev</a> (bool neg) const </td></tr>
<tr class="separator:a987bd4125ec63afc7577b3dbf9cb7b76"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a81e07d7b4272797fb31ed99ab88359ca"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a81e07d7b4272797fb31ed99ab88359ca">score</a> (bool neg) const </td></tr>
<tr class="separator:a81e07d7b4272797fb31ed99ab88359ca"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab7d99f6dfbadfbbf71ee23a4fd49a5e0"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#ab7d99f6dfbadfbbf71ee23a4fd49a5e0">added</a> (bool neg) const </td></tr>
<tr class="separator:ab7d99f6dfbadfbbf71ee23a4fd49a5e0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a561c4d0ef9d246de12d5b22aef375315"><td class="memItemLeft" align="right" valign="top">std::vector< std::pair< <a class="el" href="classCVC3_1_1Clause.html">Clause</a>, <br class="typebreak"/>
int > > & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a561c4d0ef9d246de12d5b22aef375315">wp</a> (bool neg) const </td></tr>
<tr class="separator:a561c4d0ef9d246de12d5b22aef375315"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a82f724d0ece90488867aa2de8cc43c32"><td class="memItemLeft" align="right" valign="top">std::string </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a82f724d0ece90488867aa2de8cc43c32">toString</a> () const </td></tr>
<tr class="separator:a82f724d0ece90488867aa2de8cc43c32"><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:a3511123177ecb1126031b1b88d37fd0a"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a3511123177ecb1126031b1b88d37fd0a">deriveThmRec</a> (bool checkAssump) const </td></tr>
<tr class="separator:a3511123177ecb1126031b1b88d37fd0a"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-attribs"></a>
Private Attributes</h2></td></tr>
<tr class="memitem:aac695e278985a090521f129729281189"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1VariableValue.html">VariableValue</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a></td></tr>
<tr class="separator:aac695e278985a090521f129729281189"><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:a0f0f37a880864202b17cff52e9526026"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a0f0f37a880864202b17cff52e9526026">operator==</a> (const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> &l1, const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> &l2)</td></tr>
<tr class="separator:a0f0f37a880864202b17cff52e9526026"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a998720ee70ba784d399ec3a97c8719b6"><td class="memItemLeft" align="right" valign="top">std::ostream & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Variable.html#a998720ee70ba784d399ec3a97c8719b6">operator<<</a> (std::ostream &os, const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> &l)</td></tr>
<tr class="separator:a998720ee70ba784d399ec3a97c8719b6"><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="variable_8h_source.html#l00039">39</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a7659f63344c25dbc8209c4c531b2f0be"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::Variable::Variable </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00046">46</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
</div>
</div>
<a class="anchor" id="a32d191ff6db4d462c902f07fe4d5045b"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Variable::Variable </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1VariableManager.html">VariableManager</a> * </td>
<td class="paramname"><em>vm</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>e</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00037">37</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00211">CVC3::VariableValue::d_refcount</a>, and <a class="el" href="variable_8h_source.html#l00041">d_val</a>.</p>
</div>
</div>
<a class="anchor" id="a76a03757802705d6496c35f296a935aa"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Variable::Variable </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> & </td>
<td class="paramname"><em>l</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00043">43</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00211">CVC3::VariableValue::d_refcount</a>, <a class="el" href="variable_8h_source.html#l00041">d_val</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="a21a9c85dd3b1320e8192fd581da15af4"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Variable::~Variable </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00048">48</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00211">CVC3::VariableValue::d_refcount</a>, <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00210">CVC3::VariableValue::d_vm</a>, <a class="el" href="variable_8cpp_source.html#l00400">CVC3::VariableManager::gc()</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="a3511123177ecb1126031b1b88d37fd0a"></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_1Theorem.html">Theorem</a> CVC3::Variable::deriveThmRec </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>checkAssump</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00162">162</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="group__SE__Rules.html#ga9c74425b4471d411f58f16781951c441">CVC3::SearchEngineRules::conflictRule()</a>, <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00210">CVC3::VariableValue::d_vm</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="variable_8cpp_source.html#l00103">getAntecedent()</a>, <a class="el" href="variable_8cpp_source.html#l00110">getAntecedentIdx()</a>, <a class="el" href="variable_8cpp_source.html#l00116">getAssumpThm()</a>, <a class="el" href="variable_8cpp_source.html#l00068">getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="clause_8h_source.html#l00138">CVC3::Clause::getLiterals()</a>, <a class="el" href="variable_8h_source.html#l00414">CVC3::VariableManager::getRules()</a>, <a class="el" href="variable_8cpp_source.html#l00090">getScope()</a>, <a class="el" href="variable_8cpp_source.html#l00096">getTheorem()</a>, <a class="el" href="clause_8h_source.html#l00117">CVC3::Clause::getTheorem()</a>, <a class="el" href="variable_8cpp_source.html#l00083">getValue()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="variable_8h_source.html#l00057">isNull()</a>, <a class="el" href="variable_8cpp_source.html#l00242">CVC3::VariableValue::setValue()</a>, <a class="el" href="variable_8cpp_source.html#l00195">toString()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="group__SE__Rules.html#gae7221bb8b77313a9b53a4beca9cc0aa0">CVC3::SearchEngineRules::unitProp()</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00156">deriveTheorem()</a>.</p>
</div>
</div>
<a class="anchor" id="a551554c97de770f4160444c440342ac5"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Variable.html">Variable</a> & CVC3::Variable::operator= </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> & </td>
<td class="paramname"><em>l</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00057">57</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00211">CVC3::VariableValue::d_refcount</a>, <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00210">CVC3::VariableValue::d_vm</a>, <a class="el" href="variable_8cpp_source.html#l00400">CVC3::VariableManager::gc()</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="a35c435274fa96599d47f16239b843584"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Variable::isNull </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="variable_8h_source.html#l00057">57</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>, <a class="el" href="variable_8cpp_source.html#l00103">getAntecedent()</a>, <a class="el" href="variable_8cpp_source.html#l00110">getAntecedentIdx()</a>, <a class="el" href="variable_8cpp_source.html#l00116">getAssumpThm()</a>, <a class="el" href="variable_8cpp_source.html#l00068">getExpr()</a>, <a class="el" href="variable_8cpp_source.html#l00075">getNegExpr()</a>, <a class="el" href="variable_8cpp_source.html#l00090">getScope()</a>, <a class="el" href="variable_8cpp_source.html#l00096">getTheorem()</a>, <a class="el" href="variable_8cpp_source.html#l00083">getValue()</a>, <a class="el" href="variable_8h_source.html#l00138">CVC3::Literal::isNull()</a>, <a class="el" href="variable_8cpp_source.html#l00057">operator=()</a>, <a class="el" href="variable_8cpp_source.html#l00146">setAssumpThm()</a>, <a class="el" href="variable_8cpp_source.html#l00126">setValue()</a>, <a class="el" href="variable_8cpp_source.html#l00043">Variable()</a>, and <a class="el" href="variable_8cpp_source.html#l00048">~Variable()</a>.</p>
</div>
</div>
<a class="anchor" id="af85a6bbfd1529fce66f70d0012556fdf"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & CVC3::Variable::getExpr </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00068">68</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00255">CVC3::VariableValue::getExpr()</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>, <a class="el" href="variable_8h_source.html#l00140">CVC3::Literal::getExpr()</a>, and <a class="el" href="clause_8cpp_source.html#l00157">CVC3::printLit()</a>.</p>
</div>
</div>
<a class="anchor" id="a6d8d3752f50dc4ce55d12e252398c837"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & CVC3::Variable::getNegExpr </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00075">75</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00257">CVC3::VariableValue::getNegExpr()</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00140">CVC3::Literal::getExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a36e8ce7a305e07e00adc90f6c22c4916"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Variable::getValue </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00083">83</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00265">CVC3::VariableValue::getValue()</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>, and <a class="el" href="variable_8h_source.html#l00144">CVC3::Literal::getValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a6e50e61e2eaf7054bd1d84e4137ba270"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Variable::getScope </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00090">90</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00270">CVC3::VariableValue::getScope()</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>, and <a class="el" href="variable_8h_source.html#l00148">CVC3::Literal::getScope()</a>.</p>
</div>
</div>
<a class="anchor" id="a6cdc655ea6aaf36c8e8029af0dc41075"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & CVC3::Variable::getTheorem </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00096">96</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00275">CVC3::VariableValue::getTheorem()</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>, and <a class="el" href="variable_8h_source.html#l00159">CVC3::Literal::getTheorem()</a>.</p>
</div>
</div>
<a class="anchor" id="a5bbd362f586ab0dbbc3432d140f77aab"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> & CVC3::Variable::getAntecedent </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00103">103</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00281">CVC3::VariableValue::getAntecedent()</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a681407094080368feea5c496ed3bdb69"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Variable::getAntecedentIdx </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00110">110</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00287">CVC3::VariableValue::getAntecedentIdx()</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a535715bc38709f902feb3f77aef4f89d"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & CVC3::Variable::getAssumpThm </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00116">116</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="variable_8h_source.html#l00292">CVC3::VariableValue::getAssumpThm()</a>, and <a class="el" href="variable_8h_source.html#l00057">isNull()</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>.</p>
</div>
</div>
<a class="anchor" id="ac1d2bf9a1a8eec600ffa18b679ef4d2c"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Variable::setValue </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>val</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>c</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>idx</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00126">126</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="variable_8h_source.html#l00057">isNull()</a>, and <a class="el" href="variable_8cpp_source.html#l00242">CVC3::VariableValue::setValue()</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00153">CVC3::Literal::setValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a860c092f668decb472202b137ca6e683"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Variable::setValue </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00134">134</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8cpp_source.html#l00486">CVC3::Theorem::getScope()</a>, <a class="el" href="variable_8h_source.html#l00057">isNull()</a>, and <a class="el" href="variable_8cpp_source.html#l00242">CVC3::VariableValue::setValue()</a>.</p>
</div>
</div>
<a class="anchor" id="aeccc8931258bf6931c9a40a82e761144"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Variable::setValue </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>scope</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00140">140</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="variable_8h_source.html#l00057">isNull()</a>, and <a class="el" href="variable_8cpp_source.html#l00242">CVC3::VariableValue::setValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a688678fbc2dc4e25d9dbba2e4c7d72a5"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Variable::setAssumpThm </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>a</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>scope</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00146">146</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="variable_8h_source.html#l00057">isNull()</a>, and <a class="el" href="variable_8cpp_source.html#l00328">CVC3::VariableValue::setAssumpThm()</a>.</p>
</div>
</div>
<a class="anchor" id="ad499afb9e33f92c2efd7cf92638e0396"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::Variable::deriveTheorem </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00156">156</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>References <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00164">CVC3::Literal::deriveTheorem()</a>.</p>
</div>
</div>
<a class="anchor" id="ac78bae977cd6dead5e79debc77f52efc"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned & CVC3::Variable::count </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>neg</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00342">342</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00308">CVC3::VariableValue::count()</a>, and <a class="el" href="variable_8h_source.html#l00041">d_val</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00166">CVC3::Literal::count()</a>.</p>
</div>
</div>
<a class="anchor" id="acc8e18908c0b3c74811225c58f57c50d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned & CVC3::Variable::countPrev </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>neg</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00343">343</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00312">CVC3::VariableValue::countPrev()</a>, and <a class="el" href="variable_8h_source.html#l00041">d_val</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00167">CVC3::Literal::countPrev()</a>.</p>
</div>
</div>
<a class="anchor" id="aa4c74c18d5e3b6dff3a87dbb9600ea54"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int & CVC3::Variable::score </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>neg</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00345">345</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, and <a class="el" href="variable_8h_source.html#l00316">CVC3::VariableValue::score()</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00168">CVC3::Literal::score()</a>.</p>
</div>
</div>
<a class="anchor" id="a0e4d827e11f6308f9c9bc957f0f7d2f7"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool & CVC3::Variable::added </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>neg</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00346">346</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00320">CVC3::VariableValue::added()</a>, and <a class="el" href="variable_8h_source.html#l00041">d_val</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00169">CVC3::Literal::added()</a>.</p>
</div>
</div>
<a class="anchor" id="ac14d877633308fefc91fea8a07005fee"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::Variable::count </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>neg</em></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="variable_8h_source.html#l00348">348</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00308">CVC3::VariableValue::count()</a>, and <a class="el" href="variable_8h_source.html#l00041">d_val</a>.</p>
</div>
</div>
<a class="anchor" id="a987bd4125ec63afc7577b3dbf9cb7b76"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::Variable::countPrev </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>neg</em></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="variable_8h_source.html#l00349">349</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00312">CVC3::VariableValue::countPrev()</a>, and <a class="el" href="variable_8h_source.html#l00041">d_val</a>.</p>
</div>
</div>
<a class="anchor" id="a81e07d7b4272797fb31ed99ab88359ca"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::Variable::score </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>neg</em></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="variable_8h_source.html#l00351">351</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00041">d_val</a>, and <a class="el" href="variable_8h_source.html#l00316">CVC3::VariableValue::score()</a>.</p>
</div>
</div>
<a class="anchor" id="ab7d99f6dfbadfbbf71ee23a4fd49a5e0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Variable::added </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>neg</em></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="variable_8h_source.html#l00352">352</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00320">CVC3::VariableValue::added()</a>, and <a class="el" href="variable_8h_source.html#l00041">d_val</a>.</p>
</div>
</div>
<a class="anchor" id="a561c4d0ef9d246de12d5b22aef375315"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector< std::pair< <a class="el" href="classCVC3_1_1Clause.html">Clause</a>, int > > & CVC3::Variable::wp </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>neg</em></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="variable_8h_source.html#l00354">354</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00232">CVC3::VariableValue::d_negwp</a>, <a class="el" href="variable_8h_source.html#l00041">d_val</a>, and <a class="el" href="variable_8h_source.html#l00231">CVC3::VariableValue::d_wp</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00176">CVC3::Literal::wp()</a>.</p>
</div>
</div>
<a class="anchor" id="a82f724d0ece90488867aa2de8cc43c32"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">string CVC3::Variable::toString </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00195">195</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>.</p>
</div>
</div>
<h2 class="groupheader">Friends And Related Function Documentation</h2>
<a class="anchor" id="a0f0f37a880864202b17cff52e9526026"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool operator== </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> & </td>
<td class="paramname"><em>l1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> & </td>
<td class="paramname"><em>l2</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">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00112">112</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
</div>
</div>
<a class="anchor" id="a998720ee70ba784d399ec3a97c8719b6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::ostream& operator<< </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> & </td>
<td class="paramname"><em>l</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">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8cpp_source.html#l00202">202</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="aac695e278985a090521f129729281189"></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_1VariableValue.html">VariableValue</a>* CVC3::Variable::d_val</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00041">41</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00346">added()</a>, <a class="el" href="variable_8h_source.html#l00342">count()</a>, <a class="el" href="variable_8h_source.html#l00343">countPrev()</a>, <a class="el" href="variable_8cpp_source.html#l00162">deriveThmRec()</a>, <a class="el" href="variable_8cpp_source.html#l00103">getAntecedent()</a>, <a class="el" href="variable_8cpp_source.html#l00110">getAntecedentIdx()</a>, <a class="el" href="variable_8cpp_source.html#l00116">getAssumpThm()</a>, <a class="el" href="variable_8cpp_source.html#l00068">getExpr()</a>, <a class="el" href="variable_8cpp_source.html#l00075">getNegExpr()</a>, <a class="el" href="variable_8cpp_source.html#l00090">getScope()</a>, <a class="el" href="variable_8cpp_source.html#l00096">getTheorem()</a>, <a class="el" href="variable_8cpp_source.html#l00083">getValue()</a>, <a class="el" href="variable_8h_source.html#l00057">isNull()</a>, <a class="el" href="variable_8cpp_source.html#l00202">CVC3::operator<<()</a>, <a class="el" href="variable_8cpp_source.html#l00057">operator=()</a>, <a class="el" href="variable_8h_source.html#l00345">score()</a>, <a class="el" href="variable_8cpp_source.html#l00146">setAssumpThm()</a>, <a class="el" href="variable_8cpp_source.html#l00126">setValue()</a>, <a class="el" href="variable_8cpp_source.html#l00037">Variable()</a>, <a class="el" href="variable_8h_source.html#l00354">wp()</a>, and <a class="el" href="variable_8cpp_source.html#l00048">~Variable()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="variable_8h_source.html">variable.h</a></li>
<li><a class="el" href="variable_8cpp_source.html">variable.cpp</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>
