<!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::Literal 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_1Literal.html">Literal</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="#friends">Friends</a> </div>
<div class="headertitle">
<div class="title">CVC3::Literal Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::Literal" -->
<p><code>#include <<a class="el" href="variable_8h_source.html">variable.h</a>></code></p>
<p><a href="classCVC3_1_1Literal-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_1Literal.html#a1066f94f42e8277ca8aa33e2bebfc1fb">Literal</a> (const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> &v, bool positive=true)
<li><a class="el" href="classCVC3_1_1Literal.html#aa24c193b2ed3df0b23278a81703a496a">Literal</a> ()
<li><a class="el" href="classCVC3_1_1Literal.html#a3146ac3b39f4045619d16e346dba973a">Literal</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">Variable</a> & <a class="el" href="classCVC3_1_1Literal.html#af43cfe38032a00cc8e8e60b0389eeb3e">getVar</a> ()
<li>const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> & <a class="el" href="classCVC3_1_1Literal.html#a2f2c48302fa499905d1eb690331f66de">getVar</a> () const
<li>bool <a class="el" href="classCVC3_1_1Literal.html#aefb2cb8f18bdc70d3130ee7d8dca614c">isPositive</a> () const
<li>bool <a class="el" href="classCVC3_1_1Literal.html#aad653dd8534feb823b9d30f060b4e181">isNegative</a> () const
<li>bool <a class="el" href="classCVC3_1_1Literal.html#aa63f859d19f8c132864d41bb1805c4c0">isNull</a> () const
<li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1Literal.html#a4a2e0a421bfcb590c3a7964d2583a94c">getExpr</a> () const
<li>int <a class="el" href="classCVC3_1_1Literal.html#a48feb6e7cf83b3a59b94ca0e75627d0f">getValue</a> () const
<li>int <a class="el" href="classCVC3_1_1Literal.html#a2abe99239ecdf75235e242282cd672f2">getScope</a> () const
<li>void <a class="el" href="classCVC3_1_1Literal.html#ad731e76b4037cb3e5d797543596514a1">setValue</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<li>void <a class="el" href="classCVC3_1_1Literal.html#afd1c69616427acb7bac118dfa627b611">setValue</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm, int scope)
<li>const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="classCVC3_1_1Literal.html#a9d607c46f54954c7c1371cb8452f8e6f">getTheorem</a> () const
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1Literal.html#a9d040e10a412d4a86642a9b2776dd258">deriveTheorem</a> () const
<li>unsigned & <a class="el" href="classCVC3_1_1Literal.html#a4823b2e9ec3a6a13a28c209d22269564">count</a> ()
<li>unsigned & <a class="el" href="classCVC3_1_1Literal.html#ab2a9170779ff251399c8d197c5c5c8ce">countPrev</a> ()
<li>int & <a class="el" href="classCVC3_1_1Literal.html#a436c5126780bd81c31bc01a868b5b857">score</a> ()
<li>bool & <a class="el" href="classCVC3_1_1Literal.html#a49129c1ccac9ad6380af512daae84b34">added</a> ()
<li>unsigned <a class="el" href="classCVC3_1_1Literal.html#a8a8aaec71bc7d9603b83dec2d4b3feeb">count</a> () const
<li>unsigned <a class="el" href="classCVC3_1_1Literal.html#a673002c88b2767a90c4112c946119080">countPrev</a> () const
<li>int <a class="el" href="classCVC3_1_1Literal.html#af7709a0b26086c61e516460b41c032d2">score</a> () const
<li>bool <a class="el" href="classCVC3_1_1Literal.html#a4db8e1bbf73145f6453a04cec746c67d">added</a> () 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_1Literal.html#a93986b2c3cd2889cbbf35fca5d216251">wp</a> () const
<li>std::string <a class="el" href="classCVC3_1_1Literal.html#aff53e6b3e4da8c649816441046983a30">toString</a> () const
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1Variable.html">Variable</a> <a class="el" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">d_var</a>
<li>bool <a class="el" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">d_negative</a>
</ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>std::ostream & <a class="el" href="classCVC3_1_1Literal.html#a8b8d2fbbe7ee1896d8be5be1c4974580">operator<<</a> (std::ostream &os, const <a class="el" href="classCVC3_1_1Literal.html">Literal</a> &l)
<li>bool <a class="el" href="classCVC3_1_1Literal.html#af8bdb08600f29ef91133ad24bf850c49">operator==</a> (const <a class="el" href="classCVC3_1_1Literal.html">Literal</a> &l1, const <a class="el" href="classCVC3_1_1Literal.html">Literal</a> &l2)
</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#l00120">120</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="a1066f94f42e8277ca8aa33e2bebfc1fb"></a><!-- doxytag: member="CVC3::Literal::Literal" ref="a1066f94f42e8277ca8aa33e2bebfc1fb" args="(const Variable &v, bool positive=true)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Literal::Literal </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Variable.html">Variable</a> & </td>
<td class="paramname"><em>v</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>positive</em> = <code>true</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00126">126</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
</div>
</div>
<a class="anchor" id="aa24c193b2ed3df0b23278a81703a496a"></a><!-- doxytag: member="CVC3::Literal::Literal" ref="aa24c193b2ed3df0b23278a81703a496a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Literal::Literal </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#l00129">129</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
</div>
</div>
<a class="anchor" id="a3146ac3b39f4045619d16e346dba973a"></a><!-- doxytag: member="CVC3::Literal::Literal" ref="a3146ac3b39f4045619d16e346dba973a" args="(VariableManager *vm, const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Literal::Literal </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><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00132">132</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="af43cfe38032a00cc8e8e60b0389eeb3e"></a><!-- doxytag: member="CVC3::Literal::getVar" ref="af43cfe38032a00cc8e8e60b0389eeb3e" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Variable.html">Variable</a>& CVC3::Literal::getVar </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#l00134">134</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#l00122">d_var</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00148">getScope()</a>, <a class="el" href="variable_8h_source.html#l00192">CVC3::operator!()</a>, <a class="el" href="variable_8cpp_source.html#l00217">CVC3::operator<<()</a>, and <a class="el" href="clause_8cpp_source.html#l00157">CVC3::printLit()</a>.</p>
</div>
</div>
<a class="anchor" id="a2f2c48302fa499905d1eb690331f66de"></a><!-- doxytag: member="CVC3::Literal::getVar" ref="a2f2c48302fa499905d1eb690331f66de" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Variable.html">Variable</a>& CVC3::Literal::getVar </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#l00135">135</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#l00122">d_var</a>.</p>
</div>
</div>
<a class="anchor" id="aefb2cb8f18bdc70d3130ee7d8dca614c"></a><!-- doxytag: member="CVC3::Literal::isPositive" ref="aefb2cb8f18bdc70d3130ee7d8dca614c" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Literal::isPositive </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#l00136">136</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#l00123">d_negative</a>.</p>
</div>
</div>
<a class="anchor" id="aad653dd8534feb823b9d30f060b4e181"></a><!-- doxytag: member="CVC3::Literal::isNegative" ref="aad653dd8534feb823b9d30f060b4e181" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Literal::isNegative </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#l00137">137</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#l00123">d_negative</a>.</p>
<p>Referenced by <a class="el" href="variable_8h_source.html#l00192">CVC3::operator!()</a>, <a class="el" href="variable_8cpp_source.html#l00217">CVC3::operator<<()</a>, <a class="el" href="clause_8cpp_source.html#l00157">CVC3::printLit()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>.</p>
</div>
</div>
<a class="anchor" id="aa63f859d19f8c132864d41bb1805c4c0"></a><!-- doxytag: member="CVC3::Literal::isNull" ref="aa63f859d19f8c132864d41bb1805c4c0" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Literal::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#l00138">138</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#l00122">d_var</a>, and <a class="el" href="variable_8h_source.html#l00057">CVC3::Variable::isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="a4a2e0a421bfcb590c3a7964d2583a94c"></a><!-- doxytag: member="CVC3::Literal::getExpr" ref="a4a2e0a421bfcb590c3a7964d2583a94c" 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::Literal::getExpr </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#l00140">140</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#l00123">d_negative</a>, <a class="el" href="variable_8h_source.html#l00122">d_var</a>, <a class="el" href="variable_8cpp_source.html#l00068">CVC3::Variable::getExpr()</a>, and <a class="el" href="variable_8cpp_source.html#l00075">CVC3::Variable::getNegExpr()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>, <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00412">CVC3::SearchEngineFast::updateLitCounts()</a>.</p>
</div>
</div>
<a class="anchor" id="a48feb6e7cf83b3a59b94ca0e75627d0f"></a><!-- doxytag: member="CVC3::Literal::getValue" ref="a48feb6e7cf83b3a59b94ca0e75627d0f" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Literal::getValue </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#l00144">144</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#l00123">d_negative</a>, <a class="el" href="variable_8h_source.html#l00122">d_var</a>, and <a class="el" href="variable_8cpp_source.html#l00083">CVC3::Variable::getValue()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, <a class="el" href="clause_8cpp_source.html#l00157">CVC3::printLit()</a>, <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>, <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>, <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="a2abe99239ecdf75235e242282cd672f2"></a><!-- doxytag: member="CVC3::Literal::getScope" ref="a2abe99239ecdf75235e242282cd672f2" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Literal::getScope </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#l00148">148</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
<p>References <a class="el" href="variable_8cpp_source.html#l00090">CVC3::Variable::getScope()</a>, and <a class="el" href="variable_8h_source.html#l00134">getVar()</a>.</p>
<p>Referenced by <a class="el" href="clause_8cpp_source.html#l00157">CVC3::printLit()</a>, <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="ad731e76b4037cb3e5d797543596514a1"></a><!-- doxytag: member="CVC3::Literal::setValue" ref="ad731e76b4037cb3e5d797543596514a1" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Literal::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><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00153">153</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#l00122">d_var</a>, <a class="el" href="theorem_8cpp_source.html#l00486">CVC3::Theorem::getScope()</a>, and <a class="el" href="variable_8cpp_source.html#l00126">CVC3::Variable::setValue()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>.</p>
</div>
</div>
<a class="anchor" id="afd1c69616427acb7bac118dfa627b611"></a><!-- doxytag: member="CVC3::Literal::setValue" ref="afd1c69616427acb7bac118dfa627b611" args="(const Theorem &thm, int scope)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Literal::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><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00156">156</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#l00122">d_var</a>, and <a class="el" href="variable_8cpp_source.html#l00126">CVC3::Variable::setValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a9d607c46f54954c7c1371cb8452f8e6f"></a><!-- doxytag: member="CVC3::Literal::getTheorem" ref="a9d607c46f54954c7c1371cb8452f8e6f" 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::Literal::getTheorem </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#l00159">159</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#l00122">d_var</a>, and <a class="el" href="variable_8cpp_source.html#l00096">CVC3::Variable::getTheorem()</a>.</p>
<p>Referenced by <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="a9d040e10a412d4a86642a9b2776dd258"></a><!-- doxytag: member="CVC3::Literal::deriveTheorem" ref="a9d040e10a412d4a86642a9b2776dd258" 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::Literal::deriveTheorem </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#l00164">164</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#l00122">d_var</a>, and <a class="el" href="variable_8cpp_source.html#l00156">CVC3::Variable::deriveTheorem()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>.</p>
</div>
</div>
<a class="anchor" id="a4823b2e9ec3a6a13a28c209d22269564"></a><!-- doxytag: member="CVC3::Literal::count" ref="a4823b2e9ec3a6a13a28c209d22269564" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned& CVC3::Literal::count </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#l00166">166</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#l00342">CVC3::Variable::count()</a>, <a class="el" href="variable_8h_source.html#l00123">d_negative</a>, and <a class="el" href="variable_8h_source.html#l00122">d_var</a>.</p>
<p>Referenced by <a class="el" href="clause_8cpp_source.html#l00035">CVC3::ClauseValue::ClauseValue()</a>, <a class="el" href="variable_8cpp_source.html#l00217">CVC3::operator<<()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00089">CVC3::SearchImplBase::Splitter::operator=()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00075">CVC3::SearchImplBase::Splitter::Splitter()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00345">CVC3::SearchEngineFast::updateLitScores()</a>.</p>
</div>
</div>
<a class="anchor" id="ab2a9170779ff251399c8d197c5c5c8ce"></a><!-- doxytag: member="CVC3::Literal::countPrev" ref="ab2a9170779ff251399c8d197c5c5c8ce" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned& CVC3::Literal::countPrev </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#l00167">167</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#l00343">CVC3::Variable::countPrev()</a>, <a class="el" href="variable_8h_source.html#l00123">d_negative</a>, and <a class="el" href="variable_8h_source.html#l00122">d_var</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00345">CVC3::SearchEngineFast::updateLitScores()</a>.</p>
</div>
</div>
<a class="anchor" id="a436c5126780bd81c31bc01a868b5b857"></a><!-- doxytag: member="CVC3::Literal::score" ref="a436c5126780bd81c31bc01a868b5b857" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CVC3::Literal::score </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#l00168">168</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#l00123">d_negative</a>, <a class="el" href="variable_8h_source.html#l00122">d_var</a>, and <a class="el" href="variable_8h_source.html#l00345">CVC3::Variable::score()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00323">compareLits()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, <a class="el" href="variable_8cpp_source.html#l00217">CVC3::operator<<()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00345">CVC3::SearchEngineFast::updateLitScores()</a>.</p>
</div>
</div>
<a class="anchor" id="a49129c1ccac9ad6380af512daae84b34"></a><!-- doxytag: member="CVC3::Literal::added" ref="a49129c1ccac9ad6380af512daae84b34" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool& CVC3::Literal::added </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#l00169">169</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#l00346">CVC3::Variable::added()</a>, <a class="el" href="variable_8h_source.html#l00123">d_negative</a>, and <a class="el" href="variable_8h_source.html#l00122">d_var</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00412">CVC3::SearchEngineFast::updateLitCounts()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00345">CVC3::SearchEngineFast::updateLitScores()</a>.</p>
</div>
</div>
<a class="anchor" id="a8a8aaec71bc7d9603b83dec2d4b3feeb"></a><!-- doxytag: member="CVC3::Literal::count" ref="a8a8aaec71bc7d9603b83dec2d4b3feeb" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::Literal::count </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#l00171">171</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#l00342">CVC3::Variable::count()</a>, <a class="el" href="variable_8h_source.html#l00123">d_negative</a>, and <a class="el" href="variable_8h_source.html#l00122">d_var</a>.</p>
</div>
</div>
<a class="anchor" id="a673002c88b2767a90c4112c946119080"></a><!-- doxytag: member="CVC3::Literal::countPrev" ref="a673002c88b2767a90c4112c946119080" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::Literal::countPrev </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#l00172">172</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#l00343">CVC3::Variable::countPrev()</a>, <a class="el" href="variable_8h_source.html#l00123">d_negative</a>, and <a class="el" href="variable_8h_source.html#l00122">d_var</a>.</p>
</div>
</div>
<a class="anchor" id="af7709a0b26086c61e516460b41c032d2"></a><!-- doxytag: member="CVC3::Literal::score" ref="af7709a0b26086c61e516460b41c032d2" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Literal::score </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#l00173">173</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#l00123">d_negative</a>, <a class="el" href="variable_8h_source.html#l00122">d_var</a>, and <a class="el" href="variable_8h_source.html#l00345">CVC3::Variable::score()</a>.</p>
</div>
</div>
<a class="anchor" id="a4db8e1bbf73145f6453a04cec746c67d"></a><!-- doxytag: member="CVC3::Literal::added" ref="a4db8e1bbf73145f6453a04cec746c67d" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Literal::added </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#l00174">174</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#l00346">CVC3::Variable::added()</a>, <a class="el" href="variable_8h_source.html#l00123">d_negative</a>, and <a class="el" href="variable_8h_source.html#l00122">d_var</a>.</p>
</div>
</div>
<a class="anchor" id="a93986b2c3cd2889cbbf35fca5d216251"></a><!-- doxytag: member="CVC3::Literal::wp" ref="a93986b2c3cd2889cbbf35fca5d216251" args="() 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::Literal::wp </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#l00176">176</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#l00123">d_negative</a>, <a class="el" href="variable_8h_source.html#l00122">d_var</a>, and <a class="el" href="variable_8h_source.html#l00354">CVC3::Variable::wp()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00136">CVC3::SearchEngineFast::wp()</a>.</p>
</div>
</div>
<a class="anchor" id="aff53e6b3e4da8c649816441046983a30"></a><!-- doxytag: member="CVC3::Literal::toString" ref="aff53e6b3e4da8c649816441046983a30" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">string CVC3::Literal::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#l00211">211</a> of file <a class="el" href="variable_8cpp_source.html">variable.cpp</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00345">CVC3::SearchEngineFast::updateLitScores()</a>.</p>
</div>
</div>
<hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="a8b8d2fbbe7ee1896d8be5be1c4974580"></a><!-- doxytag: member="CVC3::Literal::operator<<" ref="a8b8d2fbbe7ee1896d8be5be1c4974580" args="(std::ostream &os, const Literal &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_1Literal.html">Literal</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">
</div>
</div>
<a class="anchor" id="af8bdb08600f29ef91133ad24bf850c49"></a><!-- doxytag: member="CVC3::Literal::operator==" ref="af8bdb08600f29ef91133ad24bf850c49" args="(const Literal &l1, const Literal &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_1Literal.html">Literal</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_1Literal.html">Literal</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#l00182">182</a> of file <a class="el" href="variable_8h_source.html">variable.h</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a9ade1c15df2b3f10d263c4f01d6ea8d5"></a><!-- doxytag: member="CVC3::Literal::d_var" ref="a9ade1c15df2b3f10d263c4f01d6ea8d5" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Variable.html">Variable</a> <a class="el" href="classCVC3_1_1Literal.html#a9ade1c15df2b3f10d263c4f01d6ea8d5">CVC3::Literal::d_var</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00122">122</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#l00169">added()</a>, <a class="el" href="variable_8h_source.html#l00166">count()</a>, <a class="el" href="variable_8h_source.html#l00167">countPrev()</a>, <a class="el" href="variable_8h_source.html#l00164">deriveTheorem()</a>, <a class="el" href="variable_8h_source.html#l00140">getExpr()</a>, <a class="el" href="variable_8h_source.html#l00159">getTheorem()</a>, <a class="el" href="variable_8h_source.html#l00144">getValue()</a>, <a class="el" href="variable_8h_source.html#l00134">getVar()</a>, <a class="el" href="variable_8h_source.html#l00138">isNull()</a>, <a class="el" href="variable_8h_source.html#l00168">score()</a>, <a class="el" href="variable_8h_source.html#l00153">setValue()</a>, and <a class="el" href="variable_8h_source.html#l00176">wp()</a>.</p>
</div>
</div>
<a class="anchor" id="a674fd67861c9bca1aef2179728745f36"></a><!-- doxytag: member="CVC3::Literal::d_negative" ref="a674fd67861c9bca1aef2179728745f36" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Literal.html#a674fd67861c9bca1aef2179728745f36">CVC3::Literal::d_negative</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="variable_8h_source.html#l00123">123</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#l00169">added()</a>, <a class="el" href="variable_8h_source.html#l00166">count()</a>, <a class="el" href="variable_8h_source.html#l00167">countPrev()</a>, <a class="el" href="variable_8h_source.html#l00140">getExpr()</a>, <a class="el" href="variable_8h_source.html#l00144">getValue()</a>, <a class="el" href="variable_8h_source.html#l00137">isNegative()</a>, <a class="el" href="variable_8h_source.html#l00136">isPositive()</a>, <a class="el" href="variable_8h_source.html#l00168">score()</a>, and <a class="el" href="variable_8h_source.html#l00176">wp()</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>
