<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: CVC3::Variable Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1Variable.html">Variable</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="#friends">Friends</a> </div>
<div class="headertitle">
<div class="title">CVC3::Variable Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::Variable" -->
<p><code>#include <<a class="el" href="variable_8h_source.html">variable.h</a>></code></p>
<p><a href="classCVC3_1_1Variable-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1Variable.html#a7659f63344c25dbc8209c4c531b2f0be">Variable</a> ()
<li><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)
<li><a class="el" href="classCVC3_1_1Variable.html#a76a03757802705d6496c35f296a935aa">Variable</a> (const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> &l)
<li><a class="el" href="classCVC3_1_1Variable.html#a21a9c85dd3b1320e8192fd581da15af4">~Variable</a> ()
<li><a class="el" href="classCVC3_1_1Variable.html">Variable</a> & <a class="el" href="classCVC3_1_1Variable.html#a551554c97de770f4160444c440342ac5">operator=</a> (const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> &l)
<li>bool <a class="el" href="classCVC3_1_1Variable.html#a35c435274fa96599d47f16239b843584">isNull</a> () const
<li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1Variable.html#af85a6bbfd1529fce66f70d0012556fdf">getExpr</a> () const
<li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1Variable.html#a6d8d3752f50dc4ce55d12e252398c837">getNegExpr</a> () const
<li>int <a class="el" href="classCVC3_1_1Variable.html#a36e8ce7a305e07e00adc90f6c22c4916">getValue</a> () const
<li>int <a class="el" href="classCVC3_1_1Variable.html#a6e50e61e2eaf7054bd1d84e4137ba270">getScope</a> () const
<li>const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="classCVC3_1_1Variable.html#a6cdc655ea6aaf36c8e8029af0dc41075">getTheorem</a> () const
<li>const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> & <a class="el" href="classCVC3_1_1Variable.html#a5bbd362f586ab0dbbc3432d140f77aab">getAntecedent</a> () const
<li>int <a class="el" href="classCVC3_1_1Variable.html#a681407094080368feea5c496ed3bdb69">getAntecedentIdx</a> () const
<li>const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="classCVC3_1_1Variable.html#a535715bc38709f902feb3f77aef4f89d">getAssumpThm</a> () const
<li>void <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)
<li>void <a class="el" href="classCVC3_1_1Variable.html#a860c092f668decb472202b137ca6e683">setValue</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<li>void <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)
<li>void <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)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1Variable.html#ad499afb9e33f92c2efd7cf92638e0396">deriveTheorem</a> () const
<li>unsigned & <a class="el" href="classCVC3_1_1Variable.html#ac78bae977cd6dead5e79debc77f52efc">count</a> (bool neg)
<li>unsigned & <a class="el" href="classCVC3_1_1Variable.html#acc8e18908c0b3c74811225c58f57c50d">countPrev</a> (bool neg)
<li>int & <a class="el" href="classCVC3_1_1Variable.html#aa4c74c18d5e3b6dff3a87dbb9600ea54">score</a> (bool neg)
<li>bool & <a class="el" href="classCVC3_1_1Variable.html#a0e4d827e11f6308f9c9bc957f0f7d2f7">added</a> (bool neg)
<li>unsigned <a class="el" href="classCVC3_1_1Variable.html#ac14d877633308fefc91fea8a07005fee">count</a> (bool neg) const
<li>unsigned <a class="el" href="classCVC3_1_1Variable.html#a987bd4125ec63afc7577b3dbf9cb7b76">countPrev</a> (bool neg) const
<li>int <a class="el" href="classCVC3_1_1Variable.html#a81e07d7b4272797fb31ed99ab88359ca">score</a> (bool neg) const
<li>bool <a class="el" href="classCVC3_1_1Variable.html#ab7d99f6dfbadfbbf71ee23a4fd49a5e0">added</a> (bool neg) const
<li>std::vector< std::pair< <a class="el" href="classCVC3_1_1Clause.html">Clause</a>, <br class="typebreak"/>
int > > & <a class="el" href="classCVC3_1_1Variable.html#a561c4d0ef9d246de12d5b22aef375315">wp</a> (bool neg) const
<li>std::string <a class="el" href="classCVC3_1_1Variable.html#a82f724d0ece90488867aa2de8cc43c32">toString</a> () const
</ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1Variable.html#a3511123177ecb1126031b1b88d37fd0a">deriveThmRec</a> (bool checkAssump) const
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1VariableValue.html">VariableValue</a> * <a class="el" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">d_val</a>
</ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>bool <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)
<li>std::ostream & <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)
</ul>
<hr/><a name="details" id="details"></a><h2>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><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a7659f63344c25dbc8209c4c531b2f0be"></a><!-- doxytag: member="CVC3::Variable::Variable" ref="a7659f63344c25dbc8209c4c531b2f0be" args="()" -->
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::Variable::Variable" ref="a32d191ff6db4d462c902f07fe4d5045b" args="(VariableManager *vm, const Expr &e)" -->
<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><!-- doxytag: member="CVC3::Variable::Variable" ref="a76a03757802705d6496c35f296a935aa" args="(const Variable &l)" -->
<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><!-- doxytag: member="CVC3::Variable::~Variable" ref="a21a9c85dd3b1320e8192fd581da15af4" args="()" -->
<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>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a3511123177ecb1126031b1b88d37fd0a"></a><!-- doxytag: member="CVC3::Variable::deriveThmRec" ref="a3511123177ecb1126031b1b88d37fd0a" args="(bool checkAssump) const " -->
<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::deriveThmRec </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>checkAssump</em></td><td>)</td>
<td> const<code> [private]</code></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="clause_8h_source.html#l00117">CVC3::Clause::getTheorem()</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="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="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, <a class="el" href="variable_8cpp_source.html#l00195">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><!-- doxytag: member="CVC3::Variable::operator=" ref="a551554c97de770f4160444c440342ac5" args="(const Variable &l)" -->
<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><!-- doxytag: member="CVC3::Variable::isNull" ref="a35c435274fa96599d47f16239b843584" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Variable::isNull </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="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><!-- doxytag: member="CVC3::Variable::getExpr" ref="af85a6bbfd1529fce66f70d0012556fdf" args="() const " -->
<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><!-- doxytag: member="CVC3::Variable::getNegExpr" ref="a6d8d3752f50dc4ce55d12e252398c837" args="() const " -->
<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><!-- doxytag: member="CVC3::Variable::getValue" ref="a36e8ce7a305e07e00adc90f6c22c4916" args="() const " -->
<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><!-- doxytag: member="CVC3::Variable::getScope" ref="a6e50e61e2eaf7054bd1d84e4137ba270" args="() const " -->
<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><!-- doxytag: member="CVC3::Variable::getTheorem" ref="a6cdc655ea6aaf36c8e8029af0dc41075" args="() const " -->
<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><!-- doxytag: member="CVC3::Variable::getAntecedent" ref="a5bbd362f586ab0dbbc3432d140f77aab" args="() const " -->
<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><!-- doxytag: member="CVC3::Variable::getAntecedentIdx" ref="a681407094080368feea5c496ed3bdb69" args="() const " -->
<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><!-- doxytag: member="CVC3::Variable::getAssumpThm" ref="a535715bc38709f902feb3f77aef4f89d" args="() const " -->
<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><!-- doxytag: member="CVC3::Variable::setValue" ref="ac1d2bf9a1a8eec600ffa18b679ef4d2c" args="(int val, const Clause &c, int idx)" -->
<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><!-- doxytag: member="CVC3::Variable::setValue" ref="a860c092f668decb472202b137ca6e683" args="(const Theorem &thm)" -->
<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><!-- doxytag: member="CVC3::Variable::setValue" ref="aeccc8931258bf6931c9a40a82e761144" args="(const Theorem &thm, int scope)" -->
<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><!-- doxytag: member="CVC3::Variable::setAssumpThm" ref="a688678fbc2dc4e25d9dbba2e4c7d72a5" args="(const Theorem &a, int scope)" -->
<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><!-- doxytag: member="CVC3::Variable::deriveTheorem" ref="ad499afb9e33f92c2efd7cf92638e0396" args="() const " -->
<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><!-- doxytag: member="CVC3::Variable::count" ref="ac78bae977cd6dead5e79debc77f52efc" args="(bool neg)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::Variable::countPrev" ref="acc8e18908c0b3c74811225c58f57c50d" args="(bool neg)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::Variable::score" ref="aa4c74c18d5e3b6dff3a87dbb9600ea54" args="(bool neg)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::Variable::added" ref="a0e4d827e11f6308f9c9bc957f0f7d2f7" args="(bool neg)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CVC3::Variable::count" ref="ac14d877633308fefc91fea8a07005fee" args="(bool neg) const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::Variable::countPrev" ref="a987bd4125ec63afc7577b3dbf9cb7b76" args="(bool neg) const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::Variable::score" ref="a81e07d7b4272797fb31ed99ab88359ca" args="(bool neg) const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::Variable::added" ref="ab7d99f6dfbadfbbf71ee23a4fd49a5e0" args="(bool neg) const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::Variable::wp" ref="a561c4d0ef9d246de12d5b22aef375315" args="(bool neg) const " -->
<div class="memitem">
<div class="memproto">
<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<code> [inline]</code></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><!-- doxytag: member="CVC3::Variable::toString" ref="a82f724d0ece90488867aa2de8cc43c32" args="() const " -->
<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>
<hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="a0f0f37a880864202b17cff52e9526026"></a><!-- doxytag: member="CVC3::Variable::operator==" ref="a0f0f37a880864202b17cff52e9526026" args="(const Variable &l1, const Variable &l2)" -->
<div class="memitem">
<div class="memproto">
<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><code> [friend]</code></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><!-- doxytag: member="CVC3::Variable::operator<<" ref="a998720ee70ba784d399ec3a97c8719b6" args="(std::ostream &os, const Variable &l)" -->
<div class="memitem">
<div class="memproto">
<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><code> [friend]</code></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>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="aac695e278985a090521f129729281189"></a><!-- doxytag: member="CVC3::Variable::d_val" ref="aac695e278985a090521f129729281189" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1VariableValue.html">VariableValue</a>* <a class="el" href="classCVC3_1_1Variable.html#aac695e278985a090521f129729281189">CVC3::Variable::d_val</a><code> [private]</code></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>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
