<!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::Clause 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_1Clause.html">Clause</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::Clause Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::Clause" -->
<p>A class representing a CNF clause (a smart pointer)
<a href="classCVC3_1_1Clause.html#details">More...</a></p>
<p><code>#include <<a class="el" href="clause_8h_source.html">clause.h</a>></code></p>
<p><a href="classCVC3_1_1Clause-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_1Clause.html#acae4255e91f5c855b4371fcb393b2554">Clause</a> ()
<li><a class="el" href="classCVC3_1_1Clause.html#a3b97c11fb450efb6e88d68ecc69f3205">Clause</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core, <a class="el" href="classCVC3_1_1VariableManager.html">VariableManager</a> *vm, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &clause, int scope, const std::string &file="", int line=0)
<li><a class="el" href="classCVC3_1_1Clause.html#af68486a625e745a9136a22f3e763da10">Clause</a> (const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> &c)
<li><a class="el" href="classCVC3_1_1Clause.html#aacf7ed78bdf948f49fc3eec100b1213b">~Clause</a> ()
<li><a class="el" href="classCVC3_1_1Clause.html">Clause</a> & <a class="el" href="classCVC3_1_1Clause.html#aeba63913bd39d5a49979459c4a6b5b52">operator=</a> (const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> &c)
<li>bool <a class="el" href="classCVC3_1_1Clause.html#a60c298aa79d5cec791f8eeef2086e92f">isNull</a> () const
<li>size_t <a class="el" href="classCVC3_1_1Clause.html#a7cfde40c65fc8eb4f733094fad07dfa1">size</a> () const
<li>const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="classCVC3_1_1Clause.html#aa933cec7528780d7971be0c10b76dc02">getTheorem</a> () const
<li>int <a class="el" href="classCVC3_1_1Clause.html#af505679fdb9d5b220115747cb4548612">getScope</a> () const
<li>const <a class="el" href="classCVC3_1_1Literal.html">Literal</a> & <a class="el" href="classCVC3_1_1Clause.html#a80356479c3ca0ca5340c7746980d033e">getLiteral</a> (size_t i) const
<li>const <a class="el" href="classCVC3_1_1Literal.html">Literal</a> & <a class="el" href="classCVC3_1_1Clause.html#a8d8f9619cf3a6b0b8bc656e6f4e6dc1a">operator[]</a> (size_t i) const
<li>const std::vector< <a class="el" href="classCVC3_1_1Literal.html">Literal</a> > & <a class="el" href="classCVC3_1_1Clause.html#afbdcb9cd34cb4ff3e14f2e5aace81d7e">getLiterals</a> () const
<li>size_t <a class="el" href="classCVC3_1_1Clause.html#ad399ff73eb62edf9cc4d1135e91afdcb">wp</a> (int i) const
<li>const <a class="el" href="classCVC3_1_1Literal.html">Literal</a> & <a class="el" href="classCVC3_1_1Clause.html#a4a2b1e46395f03fe87a6a5b7558292f0">watched</a> (int i) const
<li>size_t <a class="el" href="classCVC3_1_1Clause.html#a8d651070ee46e190670b2e37d655fcf9">wp</a> (int i, size_t l) const
<li>int <a class="el" href="classCVC3_1_1Clause.html#a4c9a2e81c05572893ba1a3b09526d172">dir</a> (int i) const
<li>int <a class="el" href="classCVC3_1_1Clause.html#a6940a2041da94ff0697f8d26c277cdab">dir</a> (int i, int d) const
<li>bool <a class="el" href="classCVC3_1_1Clause.html#a1e5660eadbc4e0c0ad18c6a9aae45d39">sat</a> () const
<dl class="el"><dd class="mdescRight">Check if the clause marked as <a class="el" href="namespaceSAT.html">SAT</a>. <a href="#a1e5660eadbc4e0c0ad18c6a9aae45d39"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1Clause.html#a80b8c7c207788b8b340d312cbcc61a37">sat</a> (bool ignored) const
<dl class="el"><dd class="mdescRight">Precise version of <a class="el" href="classCVC3_1_1Clause.html#a1e5660eadbc4e0c0ad18c6a9aae45d39" title="Check if the clause marked as SAT.">sat()</a>: check all the literals and cache the result. <a href="#a80b8c7c207788b8b340d312cbcc61a37"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1Clause.html#ae266a9c156142d2f9f53ec741d7304df">markSat</a> () const
<li>bool <a class="el" href="classCVC3_1_1Clause.html#a420281d9272ac052c75859be690bfd4d">deleted</a> () const
<li>void <a class="el" href="classCVC3_1_1Clause.html#a47d7c887d12dce3ad803bd7e9fbdefe8">markDeleted</a> () const
<li>size_t <a class="el" href="classCVC3_1_1Clause.html#a3b3fad14d36eec81247fb512acc73b41">id</a> () const
<li>bool <a class="el" href="classCVC3_1_1Clause.html#a942fff24fc6b33e44b06a41aa223294c">operator==</a> (const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> &c) const
<li>int <a class="el" href="classCVC3_1_1Clause.html#a4be95d5cff0e0ffb20f01f8c2036caa3">owners</a> () const
<dl class="el"><dd class="mdescRight">Tell how many owners this clause has (for debugging) <a href="#a4be95d5cff0e0ffb20f01f8c2036caa3"></a><br/></dl><li>std::string <a class="el" href="classCVC3_1_1Clause.html#a97eeb3430667cd3c05a3c977d7285102">toString</a> () const
</ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li>int & <a class="el" href="classCVC3_1_1Clause.html#a81569af778b6560a6a05e97c26ec9bcc">countOwner</a> ()
<dl class="el"><dd class="mdescRight">Export owner refcounting to <a class="el" href="classCVC3_1_1ClauseOwner.html" title="Same as class Clause, but when destroyed, marks the clause as deleted.">ClauseOwner</a>. <a href="#a81569af778b6560a6a05e97c26ec9bcc"></a><br/></dl></ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1ClauseValue.html">ClauseValue</a> * <a class="el" href="classCVC3_1_1Clause.html#a5455f3993d1b7d6c9e8f3731a7d260cc">d_clause</a>
<dl class="el"><dd class="mdescRight">The only value member. <a href="#a5455f3993d1b7d6c9e8f3731a7d260cc"></a><br/></dl></ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1Clause.html#a9ec1b299748dd15af6ebcb9b1f1f6a23">ClauseOwner</a>
<li>std::ostream & <a class="el" href="classCVC3_1_1Clause.html#ac9926dca26ee870cb35ae18cfd4f40d4">operator<<</a> (std::ostream &os, const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> &c)
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock"><p>A class representing a CNF clause (a smart pointer) </p>
<p>Definition at line <a class="el" href="clause_8h_source.html#l00083">83</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="acae4255e91f5c855b4371fcb393b2554"></a><!-- doxytag: member="CVC3::Clause::Clause" ref="acae4255e91f5c855b4371fcb393b2554" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Clause::Clause </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="clause_8h_source.html#l00094">94</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
</div>
</div>
<a class="anchor" id="a3b97c11fb450efb6e88d68ecc69f3205"></a><!-- doxytag: member="CVC3::Clause::Clause" ref="a3b97c11fb450efb6e88d68ecc69f3205" args="(TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope, const std::string &file="", int line=0)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Clause::Clause </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * </td>
<td class="paramname"><em>core</em>, </td>
</tr>
<tr>
<td class="paramkey"></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_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>clause</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 class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>file</em> = <code>""</code>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>line</em> = <code>0</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="clause_8h_source.html#l00096">96</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00046">CVC3::ClauseValue::d_refcount</a>, and <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>.</p>
</div>
</div>
<a class="anchor" id="af68486a625e745a9136a22f3e763da10"></a><!-- doxytag: member="CVC3::Clause::Clause" ref="af68486a625e745a9136a22f3e763da10" args="(const Clause &c)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Clause::Clause </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><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8h_source.html#l00103">103</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, and <a class="el" href="clause_8h_source.html#l00046">CVC3::ClauseValue::d_refcount</a>.</p>
</div>
</div>
<a class="anchor" id="aacf7ed78bdf948f49fc3eec100b1213b"></a><!-- doxytag: member="CVC3::Clause::~Clause" ref="aacf7ed78bdf948f49fc3eec100b1213b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Clause::~Clause </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="clause_8cpp_source.html#l00085">85</a> of file <a class="el" href="clause_8cpp_source.html">clause.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, and <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a81569af778b6560a6a05e97c26ec9bcc"></a><!-- doxytag: member="CVC3::Clause::countOwner" ref="a81569af778b6560a6a05e97c26ec9bcc" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CVC3::Clause::countOwner </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Export owner refcounting to <a class="el" href="classCVC3_1_1ClauseOwner.html" title="Same as class Clause, but when destroyed, marks the clause as deleted.">ClauseOwner</a>. </p>
<p>Definition at line <a class="el" href="clause_8h_source.html#l00089">89</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00048">CVC3::ClauseValue::d_refcountOwner</a>, and <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
</div>
</div>
<a class="anchor" id="aeba63913bd39d5a49979459c4a6b5b52"></a><!-- doxytag: member="CVC3::Clause::operator=" ref="aeba63913bd39d5a49979459c4a6b5b52" args="(const Clause &c)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Clause.html">Clause</a> & CVC3::Clause::operator= </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><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8cpp_source.html#l00115">115</a> of file <a class="el" href="clause_8cpp_source.html">clause.cpp</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00046">CVC3::ClauseValue::d_refcount</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>.</p>
</div>
</div>
<a class="anchor" id="a60c298aa79d5cec791f8eeef2086e92f"></a><!-- doxytag: member="CVC3::Clause::isNull" ref="a60c298aa79d5cec791f8eeef2086e92f" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Clause::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="clause_8h_source.html#l00111">111</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="clause_8h_source.html#l00212">deleted()</a>, <a class="el" href="clause_8h_source.html#l00168">dir()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="clause_8h_source.html#l00127">getLiteral()</a>, <a class="el" href="clause_8h_source.html#l00138">getLiterals()</a>, <a class="el" href="clause_8h_source.html#l00122">getScope()</a>, <a class="el" href="clause_8h_source.html#l00117">getTheorem()</a>, <a class="el" href="clause_8h_source.html#l00207">markSat()</a>, <a class="el" href="clause_8cpp_source.html#l00135">CVC3::operator<<()</a>, <a class="el" href="clause_8h_source.html#l00187">sat()</a>, and <a class="el" href="clause_8h_source.html#l00143">wp()</a>.</p>
</div>
</div>
<a class="anchor" id="a7cfde40c65fc8eb4f733094fad07dfa1"></a><!-- doxytag: member="CVC3::Clause::size" ref="a7cfde40c65fc8eb4f733094fad07dfa1" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">size_t CVC3::Clause::size </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="clause_8h_source.html#l00113">113</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, and <a class="el" href="clause_8h_source.html#l00055">CVC3::ClauseValue::d_literals</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01069">CVC3::SearchEngineFast::addNewClause()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</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="clause_8h_source.html#l00127">getLiteral()</a>, <a class="el" href="clause_8cpp_source.html#l00135">CVC3::operator<<()</a>, <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>, <a class="el" href="variable_8cpp_source.html#l00242">CVC3::VariableValue::setValue()</a>, <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>, <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>, <a class="el" href="search__fast_8cpp_source.html#l00412">CVC3::SearchEngineFast::updateLitCounts()</a>, and <a class="el" href="clause_8h_source.html#l00153">wp()</a>.</p>
</div>
</div>
<a class="anchor" id="aa933cec7528780d7971be0c10b76dc02"></a><!-- doxytag: member="CVC3::Clause::getTheorem" ref="aa933cec7528780d7971be0c10b76dc02" 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::Clause::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="clause_8h_source.html#l00117">117</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00050">CVC3::ClauseValue::d_thm</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="clause_8h_source.html#l00111">isNull()</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">CVC3::Variable::deriveThmRec()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="clause_8cpp_source.html#l00135">CVC3::operator<<()</a>, <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>.</p>
</div>
</div>
<a class="anchor" id="af505679fdb9d5b220115747cb4548612"></a><!-- doxytag: member="CVC3::Clause::getScope" ref="af505679fdb9d5b220115747cb4548612" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Clause::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="clause_8h_source.html#l00122">122</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00052">CVC3::ClauseValue::d_scope</a>, and <a class="el" href="clause_8h_source.html#l00111">isNull()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, and <a class="el" href="variable_8cpp_source.html#l00242">CVC3::VariableValue::setValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a80356479c3ca0ca5340c7746980d033e"></a><!-- doxytag: member="CVC3::Clause::getLiteral" ref="a80356479c3ca0ca5340c7746980d033e" args="(size_t i) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Literal.html">Literal</a>& CVC3::Clause::getLiteral </td>
<td>(</td>
<td class="paramtype">size_t </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8h_source.html#l00127">127</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00055">CVC3::ClauseValue::d_literals</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="clause_8h_source.html#l00111">isNull()</a>, and <a class="el" href="clause_8h_source.html#l00113">size()</a>.</p>
<p>Referenced by <a class="el" href="clause_8h_source.html#l00135">operator[]()</a>, and <a class="el" href="clause_8h_source.html#l00151">watched()</a>.</p>
</div>
</div>
<a class="anchor" id="a8d8f9619cf3a6b0b8bc656e6f4e6dc1a"></a><!-- doxytag: member="CVC3::Clause::operator[]" ref="a8d8f9619cf3a6b0b8bc656e6f4e6dc1a" args="(size_t i) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Literal.html">Literal</a>& CVC3::Clause::operator[] </td>
<td>(</td>
<td class="paramtype">size_t </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8h_source.html#l00135">135</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00127">getLiteral()</a>.</p>
</div>
</div>
<a class="anchor" id="afbdcb9cd34cb4ff3e14f2e5aace81d7e"></a><!-- doxytag: member="CVC3::Clause::getLiterals" ref="afbdcb9cd34cb4ff3e14f2e5aace81d7e" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::vector<<a class="el" href="classCVC3_1_1Literal.html">Literal</a>>& CVC3::Clause::getLiterals </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="clause_8h_source.html#l00138">138</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00055">CVC3::ClauseValue::d_literals</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="clause_8h_source.html#l00111">isNull()</a>.</p>
<p>Referenced by <a class="el" href="variable_8cpp_source.html#l00162">CVC3::Variable::deriveThmRec()</a>, and <a class="el" href="clause_8cpp_source.html#l00164">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="ad399ff73eb62edf9cc4d1135e91afdcb"></a><!-- doxytag: member="CVC3::Clause::wp" ref="ad399ff73eb62edf9cc4d1135e91afdcb" args="(int i) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">size_t CVC3::Clause::wp </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8h_source.html#l00143">143</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00061">CVC3::ClauseValue::d_wp</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, and <a class="el" href="clause_8h_source.html#l00111">isNull()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01069">CVC3::SearchEngineFast::addNewClause()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="clause_8cpp_source.html#l00135">CVC3::operator<<()</a>, <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>, and <a class="el" href="clause_8h_source.html#l00151">watched()</a>.</p>
</div>
</div>
<a class="anchor" id="a4a2b1e46395f03fe87a6a5b7558292f0"></a><!-- doxytag: member="CVC3::Clause::watched" ref="a4a2b1e46395f03fe87a6a5b7558292f0" args="(int i) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Literal.html">Literal</a>& CVC3::Clause::watched </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8h_source.html#l00151">151</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00127">getLiteral()</a>, and <a class="el" href="clause_8h_source.html#l00143">wp()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01069">CVC3::SearchEngineFast::addNewClause()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="a8d651070ee46e190670b2e37d655fcf9"></a><!-- doxytag: member="CVC3::Clause::wp" ref="a8d651070ee46e190670b2e37d655fcf9" args="(int i, size_t l) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">size_t CVC3::Clause::wp </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">size_t </td>
<td class="paramname"><em>l</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8h_source.html#l00153">153</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00061">CVC3::ClauseValue::d_wp</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="clause_8h_source.html#l00111">isNull()</a>, <a class="el" href="clause_8h_source.html#l00113">size()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
</div>
</div>
<a class="anchor" id="a4c9a2e81c05572893ba1a3b09526d172"></a><!-- doxytag: member="CVC3::Clause::dir" ref="a4c9a2e81c05572893ba1a3b09526d172" args="(int i) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Clause::dir </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8h_source.html#l00168">168</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00065">CVC3::ClauseValue::d_dir</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, and <a class="el" href="clause_8h_source.html#l00111">isNull()</a>.</p>
<p>Referenced by <a class="el" href="clause_8cpp_source.html#l00135">CVC3::operator<<()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="a6940a2041da94ff0697f8d26c277cdab"></a><!-- doxytag: member="CVC3::Clause::dir" ref="a6940a2041da94ff0697f8d26c277cdab" args="(int i, int d) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Clause::dir </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>d</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8h_source.html#l00176">176</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00065">CVC3::ClauseValue::d_dir</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, and <a class="el" href="clause_8h_source.html#l00111">isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="a1e5660eadbc4e0c0ad18c6a9aae45d39"></a><!-- doxytag: member="CVC3::Clause::sat" ref="a1e5660eadbc4e0c0ad18c6a9aae45d39" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Clause::sat </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if the clause marked as <a class="el" href="namespaceSAT.html">SAT</a>. </p>
<p>Definition at line <a class="el" href="clause_8h_source.html#l00187">187</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00067">CVC3::ClauseValue::d_sat</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="clause_8h_source.html#l00111">isNull()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, and <a class="el" href="clause_8cpp_source.html#l00135">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a80b8c7c207788b8b340d312cbcc61a37"></a><!-- doxytag: member="CVC3::Clause::sat" ref="a80b8c7c207788b8b340d312cbcc61a37" args="(bool ignored) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Clause::sat </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>ignored</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Precise version of <a class="el" href="classCVC3_1_1Clause.html#a1e5660eadbc4e0c0ad18c6a9aae45d39" title="Check if the clause marked as SAT.">sat()</a>: check all the literals and cache the result. </p>
<p>Definition at line <a class="el" href="clause_8h_source.html#l00192">192</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00055">CVC3::ClauseValue::d_literals</a>, <a class="el" href="clause_8h_source.html#l00067">CVC3::ClauseValue::d_sat</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="clause_8h_source.html#l00111">isNull()</a>, and <a class="el" href="clause_8h_source.html#l00207">markSat()</a>.</p>
</div>
</div>
<a class="anchor" id="ae266a9c156142d2f9f53ec741d7304df"></a><!-- doxytag: member="CVC3::Clause::markSat" ref="ae266a9c156142d2f9f53ec741d7304df" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Clause::markSat </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="clause_8h_source.html#l00207">207</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00067">CVC3::ClauseValue::d_sat</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="clause_8h_source.html#l00111">isNull()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>, and <a class="el" href="clause_8h_source.html#l00192">sat()</a>.</p>
</div>
</div>
<a class="anchor" id="a420281d9272ac052c75859be690bfd4d"></a><!-- doxytag: member="CVC3::Clause::deleted" ref="a420281d9272ac052c75859be690bfd4d" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Clause::deleted </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="clause_8h_source.html#l00212">212</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, <a class="el" href="clause_8h_source.html#l00069">CVC3::ClauseValue::d_deleted</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="clause_8h_source.html#l00111">isNull()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, and <a class="el" href="clause_8cpp_source.html#l00135">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a47d7c887d12dce3ad803bd7e9fbdefe8"></a><!-- doxytag: member="CVC3::Clause::markDeleted" ref="a47d7c887d12dce3ad803bd7e9fbdefe8" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Clause::markDeleted </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="clause_8cpp_source.html#l00096">96</a> of file <a class="el" href="clause_8cpp_source.html">clause.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
</div>
</div>
<a class="anchor" id="a3b3fad14d36eec81247fb512acc73b41"></a><!-- doxytag: member="CVC3::Clause::id" ref="a3b3fad14d36eec81247fb512acc73b41" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">size_t CVC3::Clause::id </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="clause_8h_source.html#l00219">219</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>.</p>
<p>Referenced by <a class="el" href="clause_8cpp_source.html#l00135">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a942fff24fc6b33e44b06a41aa223294c"></a><!-- doxytag: member="CVC3::Clause::operator==" ref="a942fff24fc6b33e44b06a41aa223294c" args="(const Clause &c) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Clause::operator== </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><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8h_source.html#l00222">222</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>.</p>
</div>
</div>
<a class="anchor" id="a4be95d5cff0e0ffb20f01f8c2036caa3"></a><!-- doxytag: member="CVC3::Clause::owners" ref="a4be95d5cff0e0ffb20f01f8c2036caa3" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Clause::owners </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Tell how many owners this clause has (for debugging) </p>
<p>Definition at line <a class="el" href="clause_8h_source.html#l00225">225</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>References <a class="el" href="clause_8h_source.html#l00087">d_clause</a>, and <a class="el" href="clause_8h_source.html#l00048">CVC3::ClauseValue::d_refcountOwner</a>.</p>
<p>Referenced by <a class="el" href="clause_8cpp_source.html#l00164">CVC3::operator<<()</a>.</p>
</div>
</div>
<a class="anchor" id="a97eeb3430667cd3c05a3c977d7285102"></a><!-- doxytag: member="CVC3::Clause::toString" ref="a97eeb3430667cd3c05a3c977d7285102" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">string CVC3::Clause::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="clause_8cpp_source.html#l00129">129</a> of file <a class="el" href="clause_8cpp_source.html">clause.cpp</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>, <a class="el" href="variable_8cpp_source.html#l00242">CVC3::VariableValue::setValue()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>.</p>
</div>
</div>
<hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="a9ec1b299748dd15af6ebcb9b1f1f6a23"></a><!-- doxytag: member="CVC3::Clause::ClauseOwner" ref="a9ec1b299748dd15af6ebcb9b1f1f6a23" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ClauseOwner.html">ClauseOwner</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="clause_8h_source.html#l00085">85</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
</div>
</div>
<a class="anchor" id="ac9926dca26ee870cb35ae18cfd4f40d4"></a><!-- doxytag: member="CVC3::Clause::operator<<" ref="ac9926dca26ee870cb35ae18cfd4f40d4" args="(std::ostream &os, const Clause &c)" -->
<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_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>c</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="clause_8cpp_source.html#l00135">135</a> of file <a class="el" href="clause_8cpp_source.html">clause.cpp</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a5455f3993d1b7d6c9e8f3731a7d260cc"></a><!-- doxytag: member="CVC3::Clause::d_clause" ref="a5455f3993d1b7d6c9e8f3731a7d260cc" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ClauseValue.html">ClauseValue</a>* <a class="el" href="classCVC3_1_1Clause.html#a5455f3993d1b7d6c9e8f3731a7d260cc">CVC3::Clause::d_clause</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The only value member. </p>
<p>Definition at line <a class="el" href="clause_8h_source.html#l00087">87</a> of file <a class="el" href="clause_8h_source.html">clause.h</a>.</p>
<p>Referenced by <a class="el" href="clause_8h_source.html#l00096">Clause()</a>, <a class="el" href="clause_8h_source.html#l00248">CVC3::ClauseOwner::ClauseOwner()</a>, <a class="el" href="clause_8h_source.html#l00089">countOwner()</a>, <a class="el" href="clause_8h_source.html#l00212">deleted()</a>, <a class="el" href="clause_8h_source.html#l00168">dir()</a>, <a class="el" href="clause_8h_source.html#l00127">getLiteral()</a>, <a class="el" href="clause_8h_source.html#l00138">getLiterals()</a>, <a class="el" href="clause_8h_source.html#l00122">getScope()</a>, <a class="el" href="clause_8h_source.html#l00117">getTheorem()</a>, <a class="el" href="clause_8h_source.html#l00219">id()</a>, <a class="el" href="clause_8h_source.html#l00111">isNull()</a>, <a class="el" href="clause_8h_source.html#l00207">markSat()</a>, <a class="el" href="clause_8h_source.html#l00276">CVC3::ClauseOwner::operator Clause &()</a>, <a class="el" href="clause_8h_source.html#l00278">CVC3::ClauseOwner::operator const Clause &()</a>, <a class="el" href="clause_8h_source.html#l00259">CVC3::ClauseOwner::operator=()</a>, <a class="el" href="clause_8cpp_source.html#l00115">operator=()</a>, <a class="el" href="clause_8h_source.html#l00222">operator==()</a>, <a class="el" href="clause_8h_source.html#l00225">owners()</a>, <a class="el" href="clause_8h_source.html#l00187">sat()</a>, <a class="el" href="clause_8h_source.html#l00113">size()</a>, <a class="el" href="clause_8h_source.html#l00143">wp()</a>, and <a class="el" href="clause_8h_source.html#l00269">CVC3::ClauseOwner::~ClauseOwner()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="clause_8h_source.html">clause.h</a></li>
<li><a class="el" href="clause_8cpp_source.html">clause.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>
