<!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: CDatabase 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>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> </div>
<div class="headertitle">
<div class="title">CDatabase Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CDatabase" -->
<p><code>#include <<a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CDatabase:</div>
<div class="dyncontent">
<div class="center">
<img src="classCDatabase.png" usemap="#CDatabase_map" alt=""/>
<map id="CDatabase_map" name="CDatabase_map">
<area href="classCSolver.html" alt="CSolver" shape="rect" coords="0,56,74,80"/>
</map>
</div></div>
<p><a href="classCDatabase-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCDatabase.html#a3959a40851f6fcb985542d1d43ff75dc">CDatabase</a> ()
<li><a class="el" href="classCDatabase.html#a9a3adb67c04d4f1432556aab4149841e">~CDatabase</a> ()
<li>void <a class="el" href="classCDatabase.html#a8bac062c6bcaf5e92160fd0eff63bcd2">init</a> (void)
<li>vector< <a class="el" href="classCVariable.html">CVariable</a> > & <a class="el" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a> (void)
<li>vector< <a class="el" href="classCClause.html">CClause</a> > & <a class="el" href="classCDatabase.html#a0c2329a20ee0a2672475933c3edd888e">clauses</a> (void)
<li><a class="el" href="classCVariable.html">CVariable</a> & <a class="el" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a> (int idx)
<li><a class="el" href="classCClause.html">CClause</a> & <a class="el" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> idx)
<li><a class="el" href="structCDatabaseStats.html">CDatabaseStats</a> & <a class="el" href="classCDatabase.html#addf48e1802591c3d505308224d7ceb31">stats</a> (void)
<li>void <a class="el" href="classCDatabase.html#adfda0cf04a767a89cc9ac7dbeb7a11ce">set_mem_limit</a> (int n)
<li>int & <a class="el" href="classCDatabase.html#a25c0a024183a09bf973942b1e4865501">init_num_clauses</a> ()
<li>int & <a class="el" href="classCDatabase.html#ac4f22334ba90a99dc686757f484a9651">init_num_literals</a> ()
<li>int & <a class="el" href="classCDatabase.html#a7c466015881107beb66f443839fd75e9">num_added_clauses</a> ()
<li>int & <a class="el" href="classCDatabase.html#a098b913b13aaab438a5f73a4cef09370">num_added_literals</a> ()
<li>int & <a class="el" href="classCDatabase.html#ad386f2990781ab78ebbe6eb83b7c365e">num_deleted_clauses</a> ()
<li>int & <a class="el" href="classCDatabase.html#a3e0c56c9059f90ce0b3ba0f94e2aeed2">num_deleted_literals</a> ()
<li><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * <a class="el" href="classCDatabase.html#a2e6aeb6e495ae18667311b79982a5e6d">lit_pool_begin</a> (void)
<li><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * <a class="el" href="classCDatabase.html#a3217dc6be8cff75fd418fbd4ff2e5763">lit_pool_end</a> (void)
<li>void <a class="el" href="classCDatabase.html#a7fa3358fa63aa02cae8055c0dfe832b7">lit_pool_push_back</a> (int value)
<li>int <a class="el" href="classCDatabase.html#ab6e49a71237bf7a6f060f79675bb39e7">lit_pool_size</a> (void)
<li>int <a class="el" href="classCDatabase.html#ac66c5172be66fa260f8f6d5fd41ca295">lit_pool_free_space</a> (void)
<li><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> & <a class="el" href="classCDatabase.html#a338b044147d1e34dfbed7cc8663725ae">lit_pool</a> (int i)
<li>void <a class="el" href="classCDatabase.html#a0a1c2417b7ef79f11d50add3d49625f7">output_lit_pool_state</a> (void)
<li>bool <a class="el" href="classCDatabase.html#ae121408a92221766e9139e7cf40ab7de">enlarge_lit_pool</a> (void)
<li>void <a class="el" href="classCDatabase.html#a81a2e3d63658a6aa21bda0b8660ee15f">compact_lit_pool</a> (void)
<li>int <a class="el" href="classCDatabase.html#a358ccda3851e0469ef0f2a6f3cf55726">estimate_mem_usage</a> (void)
<li>int <a class="el" href="classCDatabase.html#a1758bead04486434d17201a4bc9e6e40">mem_usage</a> (void)
<li>void <a class="el" href="classCDatabase.html#ae153743ecd52bb30bb757ad8d49c74e9">set_variable_number</a> (int n)
<li>int <a class="el" href="classCDatabase.html#a84d9594576e3c2c13bde2f9d6a98a583">add_variable</a> (void)
<li>int <a class="el" href="classCDatabase.html#ac95e4d7648334447162c0fb4e3de28d7">num_variables</a> (void)
<li>int <a class="el" href="classCDatabase.html#a1ea198396d083b323c22cd49cc2be36c">num_clauses</a> (void)
<li>int <a class="el" href="classCDatabase.html#a93f69dacd75d1cf2d4a006b961f3b7b6">num_literals</a> (void)
<li>void <a class="el" href="classCDatabase.html#a6529c55a489afcd88e37370d6a61ae96">mark_clause_deleted</a> (<a class="el" href="classCClause.html">CClause</a> &cl)
<li>void <a class="el" href="classCDatabase.html#a8fa67bd6b830c6853b01ed51b5fd183c">mark_var_in_new_cl</a> (int v_idx, int phase)
<li>int <a class="el" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a> (<a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> l)
<li>int <a class="el" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">find_unit_literal</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)
<li>bool <a class="el" href="classCDatabase.html#aeb01a55c31dfd135d9f19b561829e88d">is_conflict</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)
<li>bool <a class="el" href="classCDatabase.html#a85e3fc325b5e311c4081e5ac05e4ac5c">is_satisfied</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)
<li>void <a class="el" href="classCDatabase.html#a074d5b5a1fa285b8ae0e3c516a06a508">detail_dump_cl</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl_idx, ostream &os=cout)
<li>void <a class="el" href="classCDatabase.html#a4ecc7a06a141221adf3aff50d3ac6cf6">dump</a> (ostream &os=cout)
</ul>
<h2><a name="pro-attribs"></a>
Protected Attributes</h2>
<ul>
<li><a class="el" href="structCDatabaseStats.html">CDatabaseStats</a> <a class="el" href="classCDatabase.html#abb17b94a5d63adc740acbe28adb537dd">_stats</a>
<li><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * <a class="el" href="classCDatabase.html#a9a30273cdd0b1f4814f470950cd90a77">_lit_pool_start</a>
<li><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * <a class="el" href="classCDatabase.html#a970c8066adfcb3875af1f78f1c4029ff">_lit_pool_finish</a>
<li><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * <a class="el" href="classCDatabase.html#a3a4e4403ef1f9cb15c219bfe52b1d935">_lit_pool_end_storage</a>
<li>vector< <a class="el" href="classCVariable.html">CVariable</a> > <a class="el" href="classCDatabase.html#a0bc13af9359ede872eefe8e1f44b3069">_variables</a>
<li>vector< <a class="el" href="classCClause.html">CClause</a> > <a class="el" href="classCDatabase.html#a6adefe9983a5487fca8fc26cf8d9573f">_clauses</a>
<li>queue< <a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> > <a class="el" href="classCDatabase.html#ae238340b46c3fc75854c4c244ae96d28">_unused_clause_idx_queue</a>
<li>int <a class="el" href="classCDatabase.html#aa53ab545bfb59adcee894879520ee612">_num_var_in_new_cl</a>
<li>int <a class="el" href="classCDatabase.html#a5f8cf11f16f22e1ffd47a8d0146a584f">_mem_limit</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock"><p>Class**********************************************************************</p>
<p>Synopsis [Definition of clause database ]</p>
<p>Description [Clause Database is the place where the information of the <a class="el" href="namespaceSAT.html">SAT</a> problem are stored. it is a parent class of <a class="el" href="classCSolver.html">CSolver</a> ]</p>
<p>SeeAlso [<a class="el" href="classCSolver.html">CSolver</a>] </p>
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00090">90</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a3959a40851f6fcb985542d1d43ff75dc"></a><!-- doxytag: member="CDatabase::CDatabase" ref="a3959a40851f6fcb985542d1d43ff75dc" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDatabase::CDatabase </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="xchaff__dbase_8cpp_source.html#l00041">41</a> of file <a class="el" href="xchaff__dbase_8cpp_source.html">xchaff_dbase.cpp</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00098">_lit_pool_end_storage</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00097">_lit_pool_finish</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00096">_lit_pool_start</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00105">_mem_limit</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00072">CDatabaseStats::init_num_clauses</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00073">CDatabaseStats::init_num_literals</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00150">lit_pool_push_back()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00071">CDatabaseStats::mem_used_up</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00070">CDatabaseStats::mem_used_up_counts</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00074">CDatabaseStats::num_added_clauses</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00075">CDatabaseStats::num_added_literals</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00076">CDatabaseStats::num_deleted_clauses</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00077">CDatabaseStats::num_deleted_literals</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00045">STARTUP_LIT_POOL_SIZE</a>.</p>
</div>
</div>
<a class="anchor" id="a9a3adb67c04d4f1432556aab4149841e"></a><!-- doxytag: member="CDatabase::~CDatabase" ref="a9a3adb67c04d4f1432556aab4149841e" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDatabase::~CDatabase </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="xchaff__dbase_8h_source.html#l00109">109</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00096">_lit_pool_start</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a8bac062c6bcaf5e92160fd0eff63bcd2"></a><!-- doxytag: member="CDatabase::init" ref="a8bac062c6bcaf5e92160fd0eff63bcd2" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CDatabase::init </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCSolver.html#a711b6b701409a5a5fa54dd54b609328b">CSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00112">112</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00136">init_num_clauses()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00137">init_num_literals()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00214">num_clauses()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00217">num_literals()</a>.</p>
</div>
</div>
<a class="anchor" id="af4388cf12d2984898332c519b220d67b"></a><!-- doxytag: member="CDatabase::variables" ref="af4388cf12d2984898332c519b220d67b" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="classCVariable.html">CVariable</a>>& CDatabase::variables </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00117">117</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00100">_variables</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00206">add_variable()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00160">CSolver::add_variables()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">compact_lit_pool()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00916">CSolver::conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">CSolver::decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">CSolver::deduce()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00513">CSolver::delete_unrelevant_clauses()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00172">estimate_mem_usage()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00142">CSolver::init()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00188">mem_usage()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00210">num_variables()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">CSolver::preprocess()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00358">CSolver::restart()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00203">set_variable_number()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00601">CSolver::update_var_stats()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00101">CSolver::~CSolver()</a>.</p>
</div>
</div>
<a class="anchor" id="a0c2329a20ee0a2672475933c3edd888e"></a><!-- doxytag: member="CDatabase::clauses" ref="a0c2329a20ee0a2672475933c3edd888e" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="classCClause.html">CClause</a>>& CDatabase::clauses </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00120">120</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00101">_clauses</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00513">CSolver::delete_unrelevant_clauses()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00172">estimate_mem_usage()</a>, <a class="el" href="xchaff_8h_source.html#l00060">Xchaff::GetFirstClause()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00188">mem_usage()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00706">CSolver::preprocess()</a>.</p>
</div>
</div>
<a class="anchor" id="af421024d0ade14743332069684aba162"></a><!-- doxytag: member="CDatabase::variable" ref="af421024d0ade14743332069684aba162" args="(int idx)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVariable.html">CVariable</a>& CDatabase::variable </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>idx</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00123">123</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00100">_variables</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">compact_lit_pool()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00916">CSolver::conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00176">detail_dump_cl()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00197">dump()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00463">CSolver::dump_assignment_stack()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff_8h_source.html#l00072">Xchaff::GetVarAssignment()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00239">literal_value()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00221">mark_clause_deleted()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00231">mark_var_in_new_cl()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00890">CSolver::mark_vars_at_level()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00188">mem_usage()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">CSolver::preprocess()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00358">CSolver::restart()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00368">CSolver::set_var_value_not_current_dl()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00321">CSolver::set_var_value_with_current_dl()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00433">CSolver::unset_var_value()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00601">CSolver::update_var_stats()</a>.</p>
</div>
</div>
<a class="anchor" id="a5af3586dfcd579ab14d37c6b6cf75e18"></a><!-- doxytag: member="CDatabase::clause" ref="a5af3586dfcd579ab14d37c6b6cf75e18" args="(ClauseIdx idx)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCClause.html">CClause</a>& CDatabase::clause </td>
<td>(</td>
<td class="paramtype"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td>
<td class="paramname"><em>idx</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00126">126</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00101">_clauses</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">compact_lit_pool()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00916">CSolver::conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00176">detail_dump_cl()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00447">CSolver::find_max_clause_dlevel()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00497">find_unit_literal()</a>, <a class="el" href="xchaff_8cpp_source.html#l00020">Xchaff::GetClause()</a>, <a class="el" href="xchaff_8cpp_source.html#l00035">Xchaff::GetClauseLits()</a>, <a class="el" href="xchaff_8h_source.html#l00060">Xchaff::GetFirstClause()</a>, <a class="el" href="xchaff_8h_source.html#l00065">Xchaff::GetNextClause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00479">is_conflict()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00488">is_satisfied()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00890">CSolver::mark_vars_at_level()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00706">CSolver::preprocess()</a>.</p>
</div>
</div>
<a class="anchor" id="addf48e1802591c3d505308224d7ceb31"></a><!-- doxytag: member="CDatabase::stats" ref="addf48e1802591c3d505308224d7ceb31" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="structCDatabaseStats.html">CDatabaseStats</a>& CDatabase::stats </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00129">129</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>.</p>
</div>
</div>
<a class="anchor" id="adfda0cf04a767a89cc9ac7dbeb7a11ce"></a><!-- doxytag: member="CDatabase::set_mem_limit" ref="adfda0cf04a767a89cc9ac7dbeb7a11ce" args="(int n)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CDatabase::set_mem_limit </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>n</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCSolver.html#a069343e0391a7b95510634c9c96bb66f">CSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00132">132</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00105">_mem_limit</a>.</p>
</div>
</div>
<a class="anchor" id="a25c0a024183a09bf973942b1e4865501"></a><!-- doxytag: member="CDatabase::init_num_clauses" ref="a25c0a024183a09bf973942b1e4865501" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::init_num_clauses </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="xchaff__dbase_8h_source.html#l00136">136</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00072">CDatabaseStats::init_num_clauses</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00513">CSolver::delete_unrelevant_clauses()</a>, <a class="el" href="xchaff_8cpp_source.html#l00020">Xchaff::GetClause()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00112">init()</a>.</p>
</div>
</div>
<a class="anchor" id="ac4f22334ba90a99dc686757f484a9651"></a><!-- doxytag: member="CDatabase::init_num_literals" ref="ac4f22334ba90a99dc686757f484a9651" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::init_num_literals </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="xchaff__dbase_8h_source.html#l00137">137</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00073">CDatabaseStats::init_num_literals</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8h_source.html#l00112">init()</a>.</p>
</div>
</div>
<a class="anchor" id="a7c466015881107beb66f443839fd75e9"></a><!-- doxytag: member="CDatabase::num_added_clauses" ref="a7c466015881107beb66f443839fd75e9" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::num_added_clauses </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="xchaff__dbase_8h_source.html#l00138">138</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00074">CDatabaseStats::num_added_clauses</a>.</p>
</div>
</div>
<a class="anchor" id="a098b913b13aaab438a5f73a4cef09370"></a><!-- doxytag: member="CDatabase::num_added_literals" ref="a098b913b13aaab438a5f73a4cef09370" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::num_added_literals </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="xchaff__dbase_8h_source.html#l00139">139</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00075">CDatabaseStats::num_added_literals</a>.</p>
</div>
</div>
<a class="anchor" id="ad386f2990781ab78ebbe6eb83b7c365e"></a><!-- doxytag: member="CDatabase::num_deleted_clauses" ref="ad386f2990781ab78ebbe6eb83b7c365e" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::num_deleted_clauses </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="xchaff__dbase_8h_source.html#l00140">140</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00076">CDatabaseStats::num_deleted_clauses</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00513">CSolver::delete_unrelevant_clauses()</a>, and <a class="el" href="xchaff_8h_source.html#l00133">Xchaff::GetNumDeletedClauses()</a>.</p>
</div>
</div>
<a class="anchor" id="a3e0c56c9059f90ce0b3ba0f94e2aeed2"></a><!-- doxytag: member="CDatabase::num_deleted_literals" ref="a3e0c56c9059f90ce0b3ba0f94e2aeed2" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::num_deleted_literals </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="xchaff__dbase_8h_source.html#l00141">141</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00077">CDatabaseStats::num_deleted_literals</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00513">CSolver::delete_unrelevant_clauses()</a>, and <a class="el" href="xchaff_8h_source.html#l00135">Xchaff::GetNumDeletedLiterals()</a>.</p>
</div>
</div>
<a class="anchor" id="a2e6aeb6e495ae18667311b79982a5e6d"></a><!-- doxytag: member="CDatabase::lit_pool_begin" ref="a2e6aeb6e495ae18667311b79982a5e6d" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a>* CDatabase::lit_pool_begin </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00144">144</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00096">_lit_pool_start</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">compact_lit_pool()</a>.</p>
</div>
</div>
<a class="anchor" id="a3217dc6be8cff75fd418fbd4ff2e5763"></a><!-- doxytag: member="CDatabase::lit_pool_end" ref="a3217dc6be8cff75fd418fbd4ff2e5763" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a>* CDatabase::lit_pool_end </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00147">147</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00097">_lit_pool_finish</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>.</p>
</div>
</div>
<a class="anchor" id="a7fa3358fa63aa02cae8055c0dfe832b7"></a><!-- doxytag: member="CDatabase::lit_pool_push_back" ref="a7fa3358fa63aa02cae8055c0dfe832b7" args="(int value)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CDatabase::lit_pool_push_back </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>value</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00150">150</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00098">_lit_pool_end_storage</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00097">_lit_pool_finish</a>, and <a class="el" href="xchaff__base_8h_source.html#l00092">CLitPoolElement::val()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, and <a class="el" href="xchaff__dbase_8cpp_source.html#l00041">CDatabase()</a>.</p>
</div>
</div>
<a class="anchor" id="ab6e49a71237bf7a6f060f79675bb39e7"></a><!-- doxytag: member="CDatabase::lit_pool_size" ref="ab6e49a71237bf7a6f060f79675bb39e7" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CDatabase::lit_pool_size </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00155">155</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00097">_lit_pool_finish</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00096">_lit_pool_start</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">compact_lit_pool()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00172">estimate_mem_usage()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00188">mem_usage()</a>, and <a class="el" href="xchaff__dbase_8cpp_source.html#l00167">output_lit_pool_state()</a>.</p>
</div>
</div>
<a class="anchor" id="ac66c5172be66fa260f8f6d5fd41ca295"></a><!-- doxytag: member="CDatabase::lit_pool_free_space" ref="ac66c5172be66fa260f8f6d5fd41ca295" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CDatabase::lit_pool_free_space </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00158">158</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00098">_lit_pool_end_storage</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00097">_lit_pool_finish</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00172">estimate_mem_usage()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00188">mem_usage()</a>, and <a class="el" href="xchaff__dbase_8cpp_source.html#l00167">output_lit_pool_state()</a>.</p>
</div>
</div>
<a class="anchor" id="a338b044147d1e34dfbed7cc8663725ae"></a><!-- doxytag: member="CDatabase::lit_pool" ref="a338b044147d1e34dfbed7cc8663725ae" args="(int i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a>& CDatabase::lit_pool </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00161">161</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00096">_lit_pool_start</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">compact_lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00172">estimate_mem_usage()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00188">mem_usage()</a>.</p>
</div>
</div>
<a class="anchor" id="a0a1c2417b7ef79f11d50add3d49625f7"></a><!-- doxytag: member="CDatabase::output_lit_pool_state" ref="a0a1c2417b7ef79f11d50add3d49625f7" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CDatabase::output_lit_pool_state </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8cpp_source.html#l00167">167</a> of file <a class="el" href="xchaff__dbase_8cpp_source.html">xchaff_dbase.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00158">lit_pool_free_space()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00155">lit_pool_size()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00214">num_clauses()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00217">num_literals()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">compact_lit_pool()</a>, and <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>.</p>
</div>
</div>
<a class="anchor" id="ae121408a92221766e9139e7cf40ab7de"></a><!-- doxytag: member="CDatabase::enlarge_lit_pool" ref="ae121408a92221766e9139e7cf40ab7de" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CDatabase::enlarge_lit_pool </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">100</a> of file <a class="el" href="xchaff__dbase_8cpp_source.html">xchaff_dbase.cpp</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00098">_lit_pool_end_storage</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00097">_lit_pool_finish</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00096">_lit_pool_start</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00105">_mem_limit</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">clause()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00120">clauses()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">compact_lit_pool()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00172">estimate_mem_usage()</a>, <a class="el" href="xchaff__base_8h_source.html#l00186">CClause::first_lit()</a>, <a class="el" href="xchaff__base_8h_source.html#l00297">CVariable::ht_ptr()</a>, <a class="el" href="xchaff__base_8h_source.html#l00192">CClause::in_use()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00155">lit_pool_size()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00071">CDatabaseStats::mem_used_up</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00214">num_clauses()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00217">num_literals()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00167">output_lit_pool_state()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00123">variable()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>.</p>
</div>
</div>
<a class="anchor" id="a81a2e3d63658a6aa21bda0b8660ee15f"></a><!-- doxytag: member="CDatabase::compact_lit_pool" ref="a81a2e3d63658a6aa21bda0b8660ee15f" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CDatabase::compact_lit_pool </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">62</a> of file <a class="el" href="xchaff__dbase_8cpp_source.html">xchaff_dbase.cpp</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00097">_lit_pool_finish</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">clause()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__base_8h_source.html#l00186">CClause::first_lit()</a>, <a class="el" href="xchaff__base_8h_source.html#l00297">CVariable::ht_ptr()</a>, <a class="el" href="xchaff__base_8h_source.html#l00114">CLitPoolElement::is_ht()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00161">lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00144">lit_pool_begin()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00155">lit_pool_size()</a>, <a class="el" href="xchaff__base_8h_source.html#l00189">CClause::num_lits()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00167">output_lit_pool_state()</a>, <a class="el" href="xchaff__base_8h_source.html#l00092">CLitPoolElement::val()</a>, <a class="el" href="xchaff__base_8h_source.html#l00098">CLitPoolElement::var_index()</a>, <a class="el" href="xchaff__base_8h_source.html#l00101">CLitPoolElement::var_sign()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00123">variable()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>.</p>
</div>
</div>
<a class="anchor" id="a358ccda3851e0469ef0f2a6f3cf55726"></a><!-- doxytag: member="CDatabase::estimate_mem_usage" ref="a358ccda3851e0469ef0f2a6f3cf55726" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CDatabase::estimate_mem_usage </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCSolver.html#a6a7cefe78a6f785c2c51950a74dde6d8">CSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00172">172</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00102">_unused_clause_idx_queue</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00120">clauses()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00161">lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00158">lit_pool_free_space()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00155">lit_pool_size()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>.</p>
</div>
</div>
<a class="anchor" id="a1758bead04486434d17201a4bc9e6e40"></a><!-- doxytag: member="CDatabase::mem_usage" ref="a1758bead04486434d17201a4bc9e6e40" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CDatabase::mem_usage </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCSolver.html#af5b9bcac3d3bf0530bc36285ce8cc7f6">CSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00188">188</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00102">_unused_clause_idx_queue</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00120">clauses()</a>, <a class="el" href="xchaff__base_8h_source.html#l00297">CVariable::ht_ptr()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00161">lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00158">lit_pool_free_space()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00155">lit_pool_size()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00123">variable()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">variables()</a>.</p>
</div>
</div>
<a class="anchor" id="ae153743ecd52bb30bb757ad8d49c74e9"></a><!-- doxytag: member="CDatabase::set_variable_number" ref="ae153743ecd52bb30bb757ad8d49c74e9" args="(int n)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CDatabase::set_variable_number </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>n</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00203">203</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00117">variables()</a>.</p>
</div>
</div>
<a class="anchor" id="a84d9594576e3c2c13bde2f9d6a98a583"></a><!-- doxytag: member="CDatabase::add_variable" ref="a84d9594576e3c2c13bde2f9d6a98a583" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CDatabase::add_variable </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00206">206</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00117">variables()</a>.</p>
</div>
</div>
<a class="anchor" id="ac95e4d7648334447162c0fb4e3de28d7"></a><!-- doxytag: member="CDatabase::num_variables" ref="ac95e4d7648334447162c0fb4e3de28d7" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CDatabase::num_variables </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00210">210</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00117">variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00044">Xchaff::GetFirstVar()</a>, <a class="el" href="xchaff_8h_source.html#l00046">Xchaff::GetNextVar()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00142">CSolver::init()</a>, and <a class="el" href="xchaff_8h_source.html#l00036">Xchaff::NumVariables()</a>.</p>
</div>
</div>
<a class="anchor" id="a1ea198396d083b323c22cd49cc2be36c"></a><!-- doxytag: member="CDatabase::num_clauses" ref="a1ea198396d083b323c22cd49cc2be36c" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CDatabase::num_clauses </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00214">214</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00101">_clauses</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00102">_unused_clause_idx_queue</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00112">init()</a>, <a class="el" href="xchaff_8h_source.html#l00055">Xchaff::NumClauses()</a>, and <a class="el" href="xchaff__dbase_8cpp_source.html#l00167">output_lit_pool_state()</a>.</p>
</div>
</div>
<a class="anchor" id="a93f69dacd75d1cf2d4a006b961f3b7b6"></a><!-- doxytag: member="CDatabase::num_literals" ref="a93f69dacd75d1cf2d4a006b961f3b7b6" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CDatabase::num_literals </td>
<td>(</td>
<td class="paramtype">void </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="xchaff__dbase_8h_source.html#l00217">217</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00075">CDatabaseStats::num_added_literals</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00077">CDatabaseStats::num_deleted_literals</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff_8h_source.html#l00131">Xchaff::GetNumLiterals()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00112">init()</a>, and <a class="el" href="xchaff__dbase_8cpp_source.html#l00167">output_lit_pool_state()</a>.</p>
</div>
</div>
<a class="anchor" id="a6529c55a489afcd88e37370d6a61ae96"></a><!-- doxytag: member="CDatabase::mark_clause_deleted" ref="a6529c55a489afcd88e37370d6a61ae96" args="(CClause &cl)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CDatabase::mark_clause_deleted </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCClause.html">CClause</a> & </td>
<td class="paramname"><em>cl</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00221">221</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00093">_stats</a>, <a class="el" href="xchaff__base_8h_source.html#l00192">CClause::in_use()</a>, <a class="el" href="xchaff__base_8h_source.html#l00195">CClause::literal()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00076">CDatabaseStats::num_deleted_clauses</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00077">CDatabaseStats::num_deleted_literals</a>, <a class="el" href="xchaff__base_8h_source.html#l00189">CClause::num_lits()</a>, <a class="el" href="xchaff__base_8h_source.html#l00092">CLitPoolElement::val()</a>, <a class="el" href="xchaff__base_8h_source.html#l00098">CLitPoolElement::var_index()</a>, <a class="el" href="xchaff__base_8h_source.html#l00101">CLitPoolElement::var_sign()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">variable()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00513">CSolver::delete_unrelevant_clauses()</a>.</p>
</div>
</div>
<a class="anchor" id="a8fa67bd6b830c6853b01ed51b5fd183c"></a><!-- doxytag: member="CDatabase::mark_var_in_new_cl" ref="a8fa67bd6b830c6853b01ed51b5fd183c" args="(int v_idx, int phase)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CDatabase::mark_var_in_new_cl </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>v_idx</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>phase</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="xchaff__dbase_8h_source.html#l00231">231</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00104">_num_var_in_new_cl</a>, <a class="el" href="xchaff__base_8h_source.html#l00273">CVariable::set_in_new_cl()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">variable()</a>.</p>
</div>
</div>
<a class="anchor" id="ab0c8f1826cf8c92fc01943ab62d223df"></a><!-- doxytag: member="CDatabase::literal_value" ref="ab0c8f1826cf8c92fc01943ab62d223df" args="(CLitPoolElement l)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CDatabase::literal_value </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</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="xchaff__dbase_8h_source.html#l00239">239</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>References <a class="el" href="xchaff__base_8h_source.html#l00098">CLitPoolElement::var_index()</a>, <a class="el" href="xchaff__base_8h_source.html#l00101">CLitPoolElement::var_sign()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">variable()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00513">CSolver::delete_unrelevant_clauses()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00176">detail_dump_cl()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00479">is_conflict()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00488">is_satisfied()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00368">CSolver::set_var_value_not_current_dl()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00321">CSolver::set_var_value_with_current_dl()</a>.</p>
</div>
</div>
<a class="anchor" id="a3e469952453c4b10f1040e9a19375f77"></a><!-- doxytag: member="CDatabase::find_unit_literal" ref="a3e469952453c4b10f1040e9a19375f77" args="(ClauseIdx cl)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CDatabase::find_unit_literal </td>
<td>(</td>
<td class="paramtype"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td>
<td class="paramname"><em>cl</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00497">497</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00100">_variables</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">clause()</a>, <a class="el" href="xchaff__base_8h_source.html#l00183">CClause::literals()</a>, <a class="el" href="xchaff__base_8h_source.html#l00095">CLitPoolElement::s_var()</a>, and <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00916">CSolver::conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">CSolver::preprocess()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00763">CSolver::real_solve()</a>.</p>
</div>
</div>
<a class="anchor" id="aeb01a55c31dfd135d9f19b561829e88d"></a><!-- doxytag: member="CDatabase::is_conflict" ref="aeb01a55c31dfd135d9f19b561829e88d" args="(ClauseIdx cl)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CDatabase::is_conflict </td>
<td>(</td>
<td class="paramtype"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td>
<td class="paramname"><em>cl</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00479">479</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00126">clause()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00239">literal_value()</a>, and <a class="el" href="xchaff__base_8h_source.html#l00183">CClause::literals()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00916">CSolver::conflict_analysis_zchaff()</a>.</p>
</div>
</div>
<a class="anchor" id="a85e3fc325b5e311c4081e5ac05e4ac5c"></a><!-- doxytag: member="CDatabase::is_satisfied" ref="a85e3fc325b5e311c4081e5ac05e4ac5c" args="(ClauseIdx cl)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CDatabase::is_satisfied </td>
<td>(</td>
<td class="paramtype"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td>
<td class="paramname"><em>cl</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00488">488</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00126">clause()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00239">literal_value()</a>, and <a class="el" href="xchaff__base_8h_source.html#l00183">CClause::literals()</a>.</p>
</div>
</div>
<a class="anchor" id="a074d5b5a1fa285b8ae0e3c516a06a508"></a><!-- doxytag: member="CDatabase::detail_dump_cl" ref="a074d5b5a1fa285b8ae0e3c516a06a508" args="(ClauseIdx cl_idx, ostream &os=cout)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CDatabase::detail_dump_cl </td>
<td>(</td>
<td class="paramtype"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td>
<td class="paramname"><em>cl_idx</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">ostream & </td>
<td class="paramname"><em>os</em> = <code>cout</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8cpp_source.html#l00176">176</a> of file <a class="el" href="xchaff__dbase_8cpp_source.html">xchaff_dbase.cpp</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00126">clause()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__base_8h_source.html#l00192">CClause::in_use()</a>, <a class="el" href="xchaff__base_8h_source.html#l00195">CClause::literal()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00239">literal_value()</a>, <a class="el" href="xchaff__base_8h_source.html#l00183">CClause::literals()</a>, <a class="el" href="xchaff__base_8h_source.html#l00189">CClause::num_lits()</a>, <a class="el" href="xchaff__base_8h_source.html#l00098">CLitPoolElement::var_index()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">variable()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00197">dump()</a>.</p>
</div>
</div>
<a class="anchor" id="a4ecc7a06a141221adf3aff50d3ac6cf6"></a><!-- doxytag: member="CDatabase::dump" ref="a4ecc7a06a141221adf3aff50d3ac6cf6" args="(ostream &os=cout)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CDatabase::dump </td>
<td>(</td>
<td class="paramtype">ostream & </td>
<td class="paramname"><em>os</em> = <code>cout</code></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">CSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff__dbase_8cpp_source.html#l00197">197</a> of file <a class="el" href="xchaff__dbase_8cpp_source.html">xchaff_dbase.cpp</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00101">_clauses</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00100">_variables</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00176">detail_dump_cl()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">variable()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="abb17b94a5d63adc740acbe28adb537dd"></a><!-- doxytag: member="CDatabase::_stats" ref="abb17b94a5d63adc740acbe28adb537dd" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="structCDatabaseStats.html">CDatabaseStats</a> <a class="el" href="classCDatabase.html#abb17b94a5d63adc740acbe28adb537dd">CDatabase::_stats</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">CSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00093">93</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00041">CDatabase()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00513">CSolver::delete_unrelevant_clauses()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00136">init_num_clauses()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00137">init_num_literals()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00221">mark_clause_deleted()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00138">num_added_clauses()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00139">num_added_literals()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00140">num_deleted_clauses()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00141">num_deleted_literals()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00217">num_literals()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00129">stats()</a>.</p>
</div>
</div>
<a class="anchor" id="a9a30273cdd0b1f4814f470950cd90a77"></a><!-- doxytag: member="CDatabase::_lit_pool_start" ref="a9a30273cdd0b1f4814f470950cd90a77" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a>* <a class="el" href="classCDatabase.html#a9a30273cdd0b1f4814f470950cd90a77">CDatabase::_lit_pool_start</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00096">96</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00041">CDatabase()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00161">lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00144">lit_pool_begin()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00155">lit_pool_size()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00109">~CDatabase()</a>.</p>
</div>
</div>
<a class="anchor" id="a970c8066adfcb3875af1f78f1c4029ff"></a><!-- doxytag: member="CDatabase::_lit_pool_finish" ref="a970c8066adfcb3875af1f78f1c4029ff" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a>* <a class="el" href="classCDatabase.html#a970c8066adfcb3875af1f78f1c4029ff">CDatabase::_lit_pool_finish</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00097">97</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00041">CDatabase()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">compact_lit_pool()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00147">lit_pool_end()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00158">lit_pool_free_space()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00150">lit_pool_push_back()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00155">lit_pool_size()</a>.</p>
</div>
</div>
<a class="anchor" id="a3a4e4403ef1f9cb15c219bfe52b1d935"></a><!-- doxytag: member="CDatabase::_lit_pool_end_storage" ref="a3a4e4403ef1f9cb15c219bfe52b1d935" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a>* <a class="el" href="classCDatabase.html#a3a4e4403ef1f9cb15c219bfe52b1d935">CDatabase::_lit_pool_end_storage</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00098">98</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00041">CDatabase()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00158">lit_pool_free_space()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00150">lit_pool_push_back()</a>.</p>
</div>
</div>
<a class="anchor" id="a0bc13af9359ede872eefe8e1f44b3069"></a><!-- doxytag: member="CDatabase::_variables" ref="a0bc13af9359ede872eefe8e1f44b3069" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="classCVariable.html">CVariable</a>> <a class="el" href="classCDatabase.html#a0bc13af9359ede872eefe8e1f44b3069">CDatabase::_variables</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00100">100</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00197">dump()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00447">CSolver::find_max_clause_dlevel()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00497">find_unit_literal()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00296">CSolver::set_var_value()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00123">variable()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">variables()</a>.</p>
</div>
</div>
<a class="anchor" id="a6adefe9983a5487fca8fc26cf8d9573f"></a><!-- doxytag: member="CDatabase::_clauses" ref="a6adefe9983a5487fca8fc26cf8d9573f" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="classCClause.html">CClause</a>> <a class="el" href="classCDatabase.html#a6adefe9983a5487fca8fc26cf8d9573f">CDatabase::_clauses</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00101">101</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">clause()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00120">clauses()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00197">dump()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00214">num_clauses()</a>.</p>
</div>
</div>
<a class="anchor" id="ae238340b46c3fc75854c4c244ae96d28"></a><!-- doxytag: member="CDatabase::_unused_clause_idx_queue" ref="ae238340b46c3fc75854c4c244ae96d28" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">queue<<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a>> <a class="el" href="classCDatabase.html#ae238340b46c3fc75854c4c244ae96d28">CDatabase::_unused_clause_idx_queue</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00102">102</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00513">CSolver::delete_unrelevant_clauses()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00172">estimate_mem_usage()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00188">mem_usage()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00214">num_clauses()</a>.</p>
</div>
</div>
<a class="anchor" id="aa53ab545bfb59adcee894879520ee612"></a><!-- doxytag: member="CDatabase::_num_var_in_new_cl" ref="aa53ab545bfb59adcee894879520ee612" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCDatabase.html#aa53ab545bfb59adcee894879520ee612">CDatabase::_num_var_in_new_cl</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00104">104</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8h_source.html#l00231">mark_var_in_new_cl()</a>.</p>
</div>
</div>
<a class="anchor" id="a5f8cf11f16f22e1ffd47a8d0146a584f"></a><!-- doxytag: member="CDatabase::_mem_limit" ref="a5f8cf11f16f22e1ffd47a8d0146a584f" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCDatabase.html#a5f8cf11f16f22e1ffd47a8d0146a584f">CDatabase::_mem_limit</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__dbase_8h_source.html#l00105">105</a> of file <a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__dbase_8cpp_source.html#l00041">CDatabase()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">enlarge_lit_pool()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00132">set_mem_limit()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a></li>
<li><a class="el" href="xchaff__dbase_8cpp_source.html">xchaff_dbase.cpp</a></li>
<li><a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.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>
