<!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::CNF_Formula_Impl 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_1CNF__Formula__Impl.html">CNF_Formula_Impl</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> </div>
<div class="headertitle">
<div class="title">SAT::CNF_Formula_Impl Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="SAT::CNF_Formula_Impl" --><!-- doxytag: inherits="SAT::CNF_Formula" -->
<p><code>#include <<a class="el" href="cnf_8h_source.html">cnf.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for SAT::CNF_Formula_Impl:</div>
<div class="dyncontent">
<div class="center">
<img src="classSAT_1_1CNF__Formula__Impl.png" usemap="#SAT::CNF_Formula_Impl_map" alt=""/>
<map id="SAT::CNF_Formula_Impl_map" name="SAT::CNF_Formula_Impl_map">
<area href="classSAT_1_1CNF__Formula.html" alt="SAT::CNF_Formula" shape="rect" coords="0,0,150,24"/>
</map>
</div></div>
<p><a href="classSAT_1_1CNF__Formula__Impl-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a4d1ed697fe1e2c50a6442304480b496b">CNF_Formula_Impl</a> ()
<li><a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a39b98ba60bf53df6247643de77706ac2">CNF_Formula_Impl</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> &cnf)
<li><a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a41f7fb3a1ae1922889e0745f91f56a93">~CNF_Formula_Impl</a> ()
<li>bool <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a22f2d325345957ac96478fd4aa87fd9c">empty</a> () const
<li>const <a class="el" href="classSAT_1_1Clause.html">Clause</a> & <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#ade695e467e158eb2550683c14f19be34">operator[]</a> (int i) const
<li><a class="el" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a> <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a688bb703f9faac959eed7e9587c13658">begin</a> () const
<li><a class="el" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a> <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a91087be2e218a74f381ed2b77e4c79dd">end</a> () const
<li>unsigned <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#acf6148ff29fbfa341e58c134dc77fda0">numVars</a> () const
<li>unsigned <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a136ece8939e5be6f5218705694fa7f14">numClauses</a> () const
<li>void <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#accfd5e8d24cbb46cef5c4025a92c40eb">deleteLast</a> ()
<li>void <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#adffd09ad005d74fdad1be0fc80727767">newClause</a> ()
<li>void <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#ab72a764586f913bc1aa45e0334a75140">registerUnit</a> ()
<li>void <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#ad4e85285d108ed917b748e09c356aa7d">simplify</a> ()
<li>void <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a6bc99606944e873ded2b37c954b18170">reset</a> ()
</ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li>void <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a096fb99ab48eb623116c288bc43d7877">setNumVars</a> (unsigned numVars)
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< int, bool > <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a572e3d2d4333290f5632902ce701d1a5">d_lits</a>
<li>std::deque< <a class="el" href="classSAT_1_1Clause.html">Clause</a> > <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">d_formula</a>
<li>unsigned <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a64d083ac6c0bbd52edaca213dcf84b0a">d_numVars</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#l00145">145</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a4d1ed697fe1e2c50a6442304480b496b"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::CNF_Formula_Impl" ref="a4d1ed697fe1e2c50a6442304480b496b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SAT::CNF_Formula_Impl::CNF_Formula_Impl </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#l00152">152</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
</div>
</div>
<a class="anchor" id="a39b98ba60bf53df6247643de77706ac2"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::CNF_Formula_Impl" ref="a39b98ba60bf53df6247643de77706ac2" args="(const CNF_Formula &cnf)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SAT::CNF_Formula_Impl::CNF_Formula_Impl </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</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#l00153">153</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
<p>References <a class="el" href="cnf_8cpp_source.html#l00060">SAT::CNF_Formula::copy()</a>.</p>
</div>
</div>
<a class="anchor" id="a41f7fb3a1ae1922889e0745f91f56a93"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::~CNF_Formula_Impl" ref="a41f7fb3a1ae1922889e0745f91f56a93" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SAT::CNF_Formula_Impl::~CNF_Formula_Impl </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#l00154">154</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="a096fb99ab48eb623116c288bc43d7877"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::setNumVars" ref="a096fb99ab48eb623116c288bc43d7877" args="(unsigned numVars)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SAT::CNF_Formula_Impl::setNumVars </td>
<td>(</td>
<td class="paramtype">unsigned </td>
<td class="paramname"><em>numVars</em></td><td>)</td>
<td><code> [inline, private, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1CNF__Formula.html#a2a648614c90bccd3fe0a884749349ef1">SAT::CNF_Formula</a>.</p>
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00150">150</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#l00148">d_numVars</a>, and <a class="el" href="cnf_8h_source.html#l00160">numVars()</a>.</p>
</div>
</div>
<a class="anchor" id="a22f2d325345957ac96478fd4aa87fd9c"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::empty" ref="a22f2d325345957ac96478fd4aa87fd9c" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SAT::CNF_Formula_Impl::empty </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1CNF__Formula.html#a15e2d3d65a38c23558a0ae8cf35f1938">SAT::CNF_Formula</a>.</p>
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00156">156</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#l00147">d_formula</a>.</p>
</div>
</div>
<a class="anchor" id="ade695e467e158eb2550683c14f19be34"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::operator[]" ref="ade695e467e158eb2550683c14f19be34" args="(int i) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classSAT_1_1Clause.html">Clause</a>& SAT::CNF_Formula_Impl::operator[] </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td> const<code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1CNF__Formula.html#a46737d000053162c46af92bf15766642">SAT::CNF_Formula</a>.</p>
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00157">157</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#l00147">d_formula</a>.</p>
</div>
</div>
<a class="anchor" id="a688bb703f9faac959eed7e9587c13658"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::begin" ref="a688bb703f9faac959eed7e9587c13658" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a> SAT::CNF_Formula_Impl::begin </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1CNF__Formula.html#a69dfc94796b23b6913c44a4d6d60f0d8">SAT::CNF_Formula</a>.</p>
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00158">158</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#l00147">d_formula</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00289">SAT::DPLLTBasic::addNewClauses()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00147">SAT::DPLLTBasic::generate_CDB()</a>.</p>
</div>
</div>
<a class="anchor" id="a91087be2e218a74f381ed2b77e4c79dd"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::end" ref="a91087be2e218a74f381ed2b77e4c79dd" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">const_iterator</a> SAT::CNF_Formula_Impl::end </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1CNF__Formula.html#a6631cf3c5a6938f655360f7f63522b79">SAT::CNF_Formula</a>.</p>
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00159">159</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#l00147">d_formula</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00289">SAT::DPLLTBasic::addNewClauses()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00147">SAT::DPLLTBasic::generate_CDB()</a>.</p>
</div>
</div>
<a class="anchor" id="acf6148ff29fbfa341e58c134dc77fda0"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::numVars" ref="acf6148ff29fbfa341e58c134dc77fda0" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned SAT::CNF_Formula_Impl::numVars </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1CNF__Formula.html#acbdfb5348367dd76a65661dd1ea3599f">SAT::CNF_Formula</a>.</p>
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00160">160</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#l00148">d_numVars</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00289">SAT::DPLLTBasic::addNewClauses()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00147">SAT::DPLLTBasic::generate_CDB()</a>, and <a class="el" href="cnf_8h_source.html#l00150">setNumVars()</a>.</p>
</div>
</div>
<a class="anchor" id="a136ece8939e5be6f5218705694fa7f14"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::numClauses" ref="a136ece8939e5be6f5218705694fa7f14" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned SAT::CNF_Formula_Impl::numClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1CNF__Formula.html#a78d99de58d45109256158d55e65bb96f">SAT::CNF_Formula</a>.</p>
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00161">161</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#l00147">d_formula</a>.</p>
</div>
</div>
<a class="anchor" id="accfd5e8d24cbb46cef5c4025a92c40eb"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::deleteLast" ref="accfd5e8d24cbb46cef5c4025a92c40eb" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SAT::CNF_Formula_Impl::deleteLast </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#l00162">162</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#l00147">d_formula</a>, and <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l01042">CVC3::SearchSat::newUserAssumptionIntHelper()</a>.</p>
</div>
</div>
<a class="anchor" id="adffd09ad005d74fdad1be0fc80727767"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::newClause" ref="adffd09ad005d74fdad1be0fc80727767" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CNF_Formula_Impl::newClause </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1CNF__Formula.html#ab9f3ffd03469b827138a14392960ba30">SAT::CNF_Formula</a>.</p>
<p>Definition at line <a class="el" href="cnf_8cpp_source.html#l00137">137</a> of file <a class="el" href="cnf_8cpp_source.html">cnf.cpp</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00396">SAT::DPLLTBasic::checkSat()</a>.</p>
</div>
</div>
<a class="anchor" id="ab72a764586f913bc1aa45e0334a75140"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::registerUnit" ref="ab72a764586f913bc1aa45e0334a75140" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CNF_Formula_Impl::registerUnit </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSAT_1_1CNF__Formula.html#a3b0eb426b9713bbc92041f046dd83ab5">SAT::CNF_Formula</a>.</p>
<p>Definition at line <a class="el" href="cnf_8cpp_source.html#l00144">144</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="cnf_8h_source.html#l00069">SAT::Lit::getID()</a>.</p>
</div>
</div>
<a class="anchor" id="ad4e85285d108ed917b748e09c356aa7d"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::simplify" ref="ad4e85285d108ed917b748e09c356aa7d" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CNF_Formula_Impl::simplify </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="cnf_8cpp_source.html#l00153">153</a> of file <a class="el" href="cnf_8cpp_source.html">cnf.cpp</a>.</p>
<p>References <a class="el" href="hash__map_8h_source.html#l00257">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end()</a>, and <a class="el" href="hash__map_8h_source.html#l00171">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__basic_8cpp_source.html#l00289">SAT::DPLLTBasic::addNewClauses()</a>, and <a class="el" href="dpllt__basic_8cpp_source.html#l00147">SAT::DPLLTBasic::generate_CDB()</a>.</p>
</div>
</div>
<a class="anchor" id="a6bc99606944e873ded2b37c954b18170"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::reset" ref="a6bc99606944e873ded2b37c954b18170" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CNF_Formula_Impl::reset </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="cnf_8cpp_source.html#l00174">174</a> of file <a class="el" href="cnf_8cpp_source.html">cnf.cpp</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02510">MiniSat::Solver::push()</a>, <a class="el" href="dpllt__basic_8cpp_source.html#l00117">SATDeductionHook()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">MiniSat::Solver::search()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a572e3d2d4333290f5632902ce701d1a5"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::d_lits" ref="a572e3d2d4333290f5632902ce701d1a5" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><int, bool> <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a572e3d2d4333290f5632902ce701d1a5">SAT::CNF_Formula_Impl::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#l00146">146</a> of file <a class="el" href="cnf_8h_source.html">cnf.h</a>.</p>
</div>
</div>
<a class="anchor" id="ac96490e959862063b370e79085e4ab67"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::d_formula" ref="ac96490e959862063b370e79085e4ab67" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::deque<<a class="el" href="classSAT_1_1Clause.html">Clause</a>> <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#ac96490e959862063b370e79085e4ab67">SAT::CNF_Formula_Impl::d_formula</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00147">147</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#l00158">begin()</a>, <a class="el" href="cnf_8h_source.html#l00162">deleteLast()</a>, <a class="el" href="cnf_8h_source.html#l00156">empty()</a>, <a class="el" href="cnf_8h_source.html#l00159">end()</a>, <a class="el" href="cnf_8h_source.html#l00161">numClauses()</a>, and <a class="el" href="cnf_8h_source.html#l00157">operator[]()</a>.</p>
</div>
</div>
<a class="anchor" id="a64d083ac6c0bbd52edaca213dcf84b0a"></a><!-- doxytag: member="SAT::CNF_Formula_Impl::d_numVars" ref="a64d083ac6c0bbd52edaca213dcf84b0a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a64d083ac6c0bbd52edaca213dcf84b0a">SAT::CNF_Formula_Impl::d_numVars</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="cnf_8h_source.html#l00148">148</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#l00160">numVars()</a>, and <a class="el" href="cnf_8h_source.html#l00150">setNumVars()</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>
