<!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: SAT::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="namespaceSAT.html">SAT</a> </li>
<li class="navelem"><a class="el" href="classSAT_1_1Clause.html">Clause</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-types">Public Types</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> </div>
<div class="headertitle">
<div class="title">SAT::Clause Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="SAT::Clause" -->
<p><code>#include <<a class="el" href="cnf_8h_source.html">cnf.h</a>></code></p>
<p><a href="classSAT_1_1Clause-members.html">List of all members.</a></p>
<h2><a name="pub-types"></a>
Public Types</h2>
<ul>
<li>typedef std::vector< <a class="el" href="classSAT_1_1Lit.html">Lit</a> ><br class="typebreak"/>
::<a class="el" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">const_iterator</a> <a class="el" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">const_iterator</a>
</ul>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classSAT_1_1Clause.html#a50d7f57e0458520fbd90ec157e14b1ab">Clause</a> ()
<li><a class="el" href="classSAT_1_1Clause.html#abce68afd36de5c1b77d2957671342efc">Clause</a> (const <a class="el" href="classSAT_1_1Clause.html">Clause</a> &clause)
<li><a class="el" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">const_iterator</a> <a class="el" href="classSAT_1_1Clause.html#a6d0f568c60e06a1c59c2bf37788ff778">begin</a> () const
<li><a class="el" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">const_iterator</a> <a class="el" href="classSAT_1_1Clause.html#a38094b009b923d08ca9b1a8f517b591e">end</a> () const
<li>void <a class="el" href="classSAT_1_1Clause.html#a7c3a264e08e022cd1b7526b62a55302d">clear</a> ()
<li>unsigned <a class="el" href="classSAT_1_1Clause.html#a3c64729606d93f16b66f58d62ef253d5">size</a> () const
<li>void <a class="el" href="classSAT_1_1Clause.html#a70345bd3ad10d629dde238b8868dcfd3">addLiteral</a> (<a class="el" href="classSAT_1_1Lit.html">Lit</a> l)
<li>unsigned <a class="el" href="classSAT_1_1Clause.html#a88bfd90868e75a24feffc7f428e30369">getMaxVar</a> () const
<li>bool <a class="el" href="classSAT_1_1Clause.html#aa3369b90f9db9e4653be5544117b4ba1">isSatisfied</a> () const
<li>bool <a class="el" href="classSAT_1_1Clause.html#abcf5873b0dcc37651c1af59c610a13a9">isUnit</a> () const
<li>bool <a class="el" href="classSAT_1_1Clause.html#a2b0467a4d28bbb34316aefd11113c273">isNull</a> () const
<li>void <a class="el" href="classSAT_1_1Clause.html#aab7aa74c7b44a33a190fb8f04bc6c6fe">setSatisfied</a> ()
<li>void <a class="el" href="classSAT_1_1Clause.html#a0f3cbc4ee36da4af89d7be70252222d9">setUnit</a> ()
<li>void <a class="el" href="classSAT_1_1Clause.html#ad906b9b541550cffbf95b6ed3c68e6d4">print</a> () const
<li>void <a class="el" href="classSAT_1_1Clause.html#a69be447d7ada144c2a905cf42f4a7a82">setClauseTheorem</a> (<a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> thm)
<li><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> <a class="el" href="classSAT_1_1Clause.html#aa4d692df8aaef4ea4c1c45af006c1301">getClauseTheorem</a> () const
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li>int <a class="el" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">d_satisfied</a>:1
<li>int <a class="el" href="classSAT_1_1Clause.html#a0f0c7bf5e7ed13659de7833887921c98">d_unit</a>:1
<li>std::vector< <a class="el" href="classSAT_1_1Lit.html">Lit</a> > <a class="el" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">d_lits</a>
<li><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> <a class="el" href="classSAT_1_1Clause.html#a1f48e48e24f17ae7131c2fe3a1879cd6">d_reason</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00078">78</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
</div><hr/><h2>Member Typedef Documentation</h2>
<a class="anchor" id="af739bca890fe8219a7ebda3beefb0474"></a><!-- doxytag: member="SAT::Clause::const_iterator" ref="af739bca890fe8219a7ebda3beefb0474" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::vector<<a class="el" href="classSAT_1_1Lit.html">Lit</a>>::<a class="el" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">const_iterator</a> <a class="el" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">SAT::Clause::const_iterator</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00090">90</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
</div>
</div>
<hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a50d7f57e0458520fbd90ec157e14b1ab"></a><!-- doxytag: member="SAT::Clause::Clause" ref="a50d7f57e0458520fbd90ec157e14b1ab" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SAT::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="cnf_8h_source.html#l00086">86</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
</div>
</div>
<a class="anchor" id="abce68afd36de5c1b77d2957671342efc"></a><!-- doxytag: member="SAT::Clause::Clause" ref="abce68afd36de5c1b77d2957671342efc" args="(const Clause &clause)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SAT::Clause::Clause </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>clause</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00088">88</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a6d0f568c60e06a1c59c2bf37788ff778"></a><!-- doxytag: member="SAT::Clause::begin" ref="a6d0f568c60e06a1c59c2bf37788ff778" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">const_iterator</a> SAT::Clause::begin </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="cnf_8h_source.html#l00093">93</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00081">d_lits</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00275">SAT::DPLLTBasic::addNewClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00121">MiniSat::cvcToMiniSat()</a>, and <a class="el" href="cnf_8cpp_source.html#l00117">SAT::CNF_Formula::operator+=()</a>.</p>
</div>
</div>
<a class="anchor" id="a38094b009b923d08ca9b1a8f517b591e"></a><!-- doxytag: member="SAT::Clause::end" ref="a38094b009b923d08ca9b1a8f517b591e" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1Clause.html#af739bca890fe8219a7ebda3beefb0474">const_iterator</a> SAT::Clause::end </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="cnf_8h_source.html#l00094">94</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00081">d_lits</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00275">SAT::DPLLTBasic::addNewClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00121">MiniSat::cvcToMiniSat()</a>, and <a class="el" href="cnf_8cpp_source.html#l00117">SAT::CNF_Formula::operator+=()</a>.</p>
</div>
</div>
<a class="anchor" id="a7c3a264e08e022cd1b7526b62a55302d"></a><!-- doxytag: member="SAT::Clause::clear" ref="a7c3a264e08e022cd1b7526b62a55302d" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SAT::Clause::clear </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="cnf_8h_source.html#l00096">96</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00081">d_lits</a>, <a class="el" href="cnf_8h_source.html#l00079">d_satisfied</a>, and <a class="el" href="cnf_8h_source.html#l00080">d_unit</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00289">SAT::DPLLTBasic::addNewClauses()</a>.</p>
</div>
</div>
<a class="anchor" id="a3c64729606d93f16b66f58d62ef253d5"></a><!-- doxytag: member="SAT::Clause::size" ref="a3c64729606d93f16b66f58d62ef253d5" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned SAT::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="cnf_8h_source.html#l00097">97</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00081">d_lits</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00275">SAT::DPLLTBasic::addNewClause()</a>.</p>
</div>
</div>
<a class="anchor" id="a70345bd3ad10d629dde238b8868dcfd3"></a><!-- doxytag: member="SAT::Clause::addLiteral" ref="a70345bd3ad10d629dde238b8868dcfd3" args="(Lit l)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SAT::Clause::addLiteral </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>l</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00098">98</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00081">d_lits</a>, and <a class="el" href="cnf_8h_source.html#l00079">d_satisfied</a>.</p>
<p>Referenced by <a class="el" href="cnf_8h_source.html#l00134">SAT::CNF_Formula::addLiteral()</a>.</p>
</div>
</div>
<a class="anchor" id="a88bfd90868e75a24feffc7f428e30369"></a><!-- doxytag: member="SAT::Clause::getMaxVar" ref="a88bfd90868e75a24feffc7f428e30369" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned SAT::Clause::getMaxVar </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="cnf_8cpp_source.html#l00030">30</a> of file <a class="el" href="cnf_8cpp_source.html">cnf.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="cvc__util_8h_source.html#l00056">CVC3::max()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00275">SAT::DPLLTBasic::addNewClause()</a>.</p>
</div>
</div>
<a class="anchor" id="aa3369b90f9db9e4653be5544117b4ba1"></a><!-- doxytag: member="SAT::Clause::isSatisfied" ref="aa3369b90f9db9e4653be5544117b4ba1" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SAT::Clause::isSatisfied </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="cnf_8h_source.html#l00100">100</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00079">d_satisfied</a>.</p>
</div>
</div>
<a class="anchor" id="abcf5873b0dcc37651c1af59c610a13a9"></a><!-- doxytag: member="SAT::Clause::isUnit" ref="abcf5873b0dcc37651c1af59c610a13a9" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SAT::Clause::isUnit </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="cnf_8h_source.html#l00101">101</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00080">d_unit</a>.</p>
<p>Referenced by <a class="el" href="cnf_8cpp_source.html#l00117">SAT::CNF_Formula::operator+=()</a>.</p>
</div>
</div>
<a class="anchor" id="a2b0467a4d28bbb34316aefd11113c273"></a><!-- doxytag: member="SAT::Clause::isNull" ref="a2b0467a4d28bbb34316aefd11113c273" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SAT::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="cnf_8h_source.html#l00102">102</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00081">d_lits</a>.</p>
</div>
</div>
<a class="anchor" id="aab7aa74c7b44a33a190fb8f04bc6c6fe"></a><!-- doxytag: member="SAT::Clause::setSatisfied" ref="aab7aa74c7b44a33a190fb8f04bc6c6fe" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SAT::Clause::setSatisfied </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="cnf_8h_source.html#l00103">103</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00079">d_satisfied</a>.</p>
</div>
</div>
<a class="anchor" id="a0f3cbc4ee36da4af89d7be70252222d9"></a><!-- doxytag: member="SAT::Clause::setUnit" ref="a0f3cbc4ee36da4af89d7be70252222d9" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SAT::Clause::setUnit </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="cnf_8h_source.html#l00104">104</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00080">d_unit</a>.</p>
</div>
</div>
<a class="anchor" id="ad906b9b541550cffbf95b6ed3c68e6d4"></a><!-- doxytag: member="SAT::Clause::print" ref="ad906b9b541550cffbf95b6ed3c68e6d4" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SAT::Clause::print </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="cnf_8cpp_source.html#l00042">42</a> of file <a class="el" href="cnf_8cpp_source.html">cnf.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>.</p>
<p>Referenced by <a class="el" href="cnf_8cpp_source.html#l00085">SAT::CNF_Formula::print()</a>.</p>
</div>
</div>
<a class="anchor" id="a69be447d7ada144c2a905cf42f4a7a82"></a><!-- doxytag: member="SAT::Clause::setClauseTheorem" ref="a69be447d7ada144c2a905cf42f4a7a82" args="(CVC3::Theorem thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SAT::Clause::setClauseTheorem </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::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="cnf_8h_source.html#l00106">106</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00082">d_reason</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00623">SAT::CNF_Manager::addAssumption()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00674">SAT::CNF_Manager::addLemma()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00593">SAT::CNF_Manager::convertLemma()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00510">SAT::CNF_Manager::translateExpr()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">SAT::CNF_Manager::translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="aa4d692df8aaef4ea4c1c45af006c1301"></a><!-- doxytag: member="SAT::Clause::getClauseTheorem" ref="aa4d692df8aaef4ea4c1c45af006c1301" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> SAT::Clause::getClauseTheorem </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="cnf_8h_source.html#l00108">108</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8h_source.html#l00082">d_reason</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00488">MiniSat::Solver::addClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00139">MiniSat::Solver::cvcToMiniSat()</a>, and <a class="el" href="cnf_8cpp_source.html#l00094">SAT::CNF_Formula::operator+=()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a82a2e007da132feab7b6a2322a669b22"></a><!-- doxytag: member="SAT::Clause::d_satisfied" ref="a82a2e007da132feab7b6a2322a669b22" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classSAT_1_1Clause.html#a82a2e007da132feab7b6a2322a669b22">SAT::Clause::d_satisfied</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00079">79</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>Referenced by <a class="el" href="cnf_8h_source.html#l00098">addLiteral()</a>, <a class="el" href="cnf_8h_source.html#l00096">clear()</a>, <a class="el" href="cnf_8h_source.html#l00100">isSatisfied()</a>, and <a class="el" href="cnf_8h_source.html#l00103">setSatisfied()</a>.</p>
</div>
</div>
<a class="anchor" id="a0f0c7bf5e7ed13659de7833887921c98"></a><!-- doxytag: member="SAT::Clause::d_unit" ref="a0f0c7bf5e7ed13659de7833887921c98" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classSAT_1_1Clause.html#a0f0c7bf5e7ed13659de7833887921c98">SAT::Clause::d_unit</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00080">80</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>Referenced by <a class="el" href="cnf_8h_source.html#l00096">clear()</a>, <a class="el" href="cnf_8h_source.html#l00101">isUnit()</a>, and <a class="el" href="cnf_8h_source.html#l00104">setUnit()</a>.</p>
</div>
</div>
<a class="anchor" id="ae5504b9674dbfbb7c579027805d7bb16"></a><!-- doxytag: member="SAT::Clause::d_lits" ref="ae5504b9674dbfbb7c579027805d7bb16" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classSAT_1_1Lit.html">Lit</a>> <a class="el" href="classSAT_1_1Clause.html#ae5504b9674dbfbb7c579027805d7bb16">SAT::Clause::d_lits</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00081">81</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>Referenced by <a class="el" href="cnf_8h_source.html#l00098">addLiteral()</a>, <a class="el" href="cnf_8h_source.html#l00093">begin()</a>, <a class="el" href="cnf_8h_source.html#l00096">clear()</a>, <a class="el" href="cnf_8h_source.html#l00094">end()</a>, <a class="el" href="cnf_8h_source.html#l00102">isNull()</a>, and <a class="el" href="cnf_8h_source.html#l00097">size()</a>.</p>
</div>
</div>
<a class="anchor" id="a1f48e48e24f17ae7131c2fe3a1879cd6"></a><!-- doxytag: member="SAT::Clause::d_reason" ref="a1f48e48e24f17ae7131c2fe3a1879cd6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> <a class="el" href="classSAT_1_1Clause.html#a1f48e48e24f17ae7131c2fe3a1879cd6">SAT::Clause::d_reason</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00082">82</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>Referenced by <a class="el" href="cnf_8h_source.html#l00108">getClauseTheorem()</a>, and <a class="el" href="cnf_8h_source.html#l00106">setClauseTheorem()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="cnf_8h_source.html">cnf.h</a></li>
<li><a class="el" href="cnf_8cpp_source.html">cnf.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>
