<!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"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: CDatabase Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<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="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> |
<a href="classCDatabase-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CDatabase Class Reference</div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="xchaff__dbase_8h_source.html">xchaff_dbase.h</a>></code></p>
<p>Inherited by <a class="el" href="classCSolver.html">CSolver</a>.</p>
<div class="dynheader">
Collaboration diagram for CDatabase:</div>
<div class="dyncontent">
<div class="center"><img src="classCDatabase__coll__graph.gif" border="0" usemap="#CDatabase_coll__map" alt="Collaboration graph"/></div>
<map name="CDatabase_coll__map" id="CDatabase_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:a3959a40851f6fcb985542d1d43ff75dc"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a3959a40851f6fcb985542d1d43ff75dc">CDatabase</a> ()</td></tr>
<tr class="separator:a3959a40851f6fcb985542d1d43ff75dc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9a3adb67c04d4f1432556aab4149841e"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a9a3adb67c04d4f1432556aab4149841e">~CDatabase</a> ()</td></tr>
<tr class="separator:a9a3adb67c04d4f1432556aab4149841e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8bac062c6bcaf5e92160fd0eff63bcd2"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a8bac062c6bcaf5e92160fd0eff63bcd2">init</a> (void)</td></tr>
<tr class="separator:a8bac062c6bcaf5e92160fd0eff63bcd2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af4388cf12d2984898332c519b220d67b"><td class="memItemLeft" align="right" valign="top">vector< <a class="el" href="classCVariable.html">CVariable</a> > & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a> (void)</td></tr>
<tr class="separator:af4388cf12d2984898332c519b220d67b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0c2329a20ee0a2672475933c3edd888e"><td class="memItemLeft" align="right" valign="top">vector< <a class="el" href="classCClause.html">CClause</a> > & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a0c2329a20ee0a2672475933c3edd888e">clauses</a> (void)</td></tr>
<tr class="separator:a0c2329a20ee0a2672475933c3edd888e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af421024d0ade14743332069684aba162"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVariable.html">CVariable</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a> (int idx)</td></tr>
<tr class="separator:af421024d0ade14743332069684aba162"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5af3586dfcd579ab14d37c6b6cf75e18"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCClause.html">CClause</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> idx)</td></tr>
<tr class="separator:a5af3586dfcd579ab14d37c6b6cf75e18"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:addf48e1802591c3d505308224d7ceb31"><td class="memItemLeft" align="right" valign="top"><a class="el" href="structCDatabaseStats.html">CDatabaseStats</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#addf48e1802591c3d505308224d7ceb31">stats</a> (void)</td></tr>
<tr class="separator:addf48e1802591c3d505308224d7ceb31"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adfda0cf04a767a89cc9ac7dbeb7a11ce"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#adfda0cf04a767a89cc9ac7dbeb7a11ce">set_mem_limit</a> (int n)</td></tr>
<tr class="separator:adfda0cf04a767a89cc9ac7dbeb7a11ce"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a25c0a024183a09bf973942b1e4865501"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a25c0a024183a09bf973942b1e4865501">init_num_clauses</a> ()</td></tr>
<tr class="separator:a25c0a024183a09bf973942b1e4865501"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac4f22334ba90a99dc686757f484a9651"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#ac4f22334ba90a99dc686757f484a9651">init_num_literals</a> ()</td></tr>
<tr class="separator:ac4f22334ba90a99dc686757f484a9651"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7c466015881107beb66f443839fd75e9"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a7c466015881107beb66f443839fd75e9">num_added_clauses</a> ()</td></tr>
<tr class="separator:a7c466015881107beb66f443839fd75e9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a098b913b13aaab438a5f73a4cef09370"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a098b913b13aaab438a5f73a4cef09370">num_added_literals</a> ()</td></tr>
<tr class="separator:a098b913b13aaab438a5f73a4cef09370"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad386f2990781ab78ebbe6eb83b7c365e"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#ad386f2990781ab78ebbe6eb83b7c365e">num_deleted_clauses</a> ()</td></tr>
<tr class="separator:ad386f2990781ab78ebbe6eb83b7c365e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3e0c56c9059f90ce0b3ba0f94e2aeed2"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a3e0c56c9059f90ce0b3ba0f94e2aeed2">num_deleted_literals</a> ()</td></tr>
<tr class="separator:a3e0c56c9059f90ce0b3ba0f94e2aeed2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2e6aeb6e495ae18667311b79982a5e6d"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a2e6aeb6e495ae18667311b79982a5e6d">lit_pool_begin</a> (void)</td></tr>
<tr class="separator:a2e6aeb6e495ae18667311b79982a5e6d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3217dc6be8cff75fd418fbd4ff2e5763"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a3217dc6be8cff75fd418fbd4ff2e5763">lit_pool_end</a> (void)</td></tr>
<tr class="separator:a3217dc6be8cff75fd418fbd4ff2e5763"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7fa3358fa63aa02cae8055c0dfe832b7"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a7fa3358fa63aa02cae8055c0dfe832b7">lit_pool_push_back</a> (int value)</td></tr>
<tr class="separator:a7fa3358fa63aa02cae8055c0dfe832b7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab6e49a71237bf7a6f060f79675bb39e7"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#ab6e49a71237bf7a6f060f79675bb39e7">lit_pool_size</a> (void)</td></tr>
<tr class="separator:ab6e49a71237bf7a6f060f79675bb39e7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac66c5172be66fa260f8f6d5fd41ca295"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#ac66c5172be66fa260f8f6d5fd41ca295">lit_pool_free_space</a> (void)</td></tr>
<tr class="separator:ac66c5172be66fa260f8f6d5fd41ca295"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a338b044147d1e34dfbed7cc8663725ae"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a338b044147d1e34dfbed7cc8663725ae">lit_pool</a> (int i)</td></tr>
<tr class="separator:a338b044147d1e34dfbed7cc8663725ae"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0a1c2417b7ef79f11d50add3d49625f7"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a0a1c2417b7ef79f11d50add3d49625f7">output_lit_pool_state</a> (void)</td></tr>
<tr class="separator:a0a1c2417b7ef79f11d50add3d49625f7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae121408a92221766e9139e7cf40ab7de"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#ae121408a92221766e9139e7cf40ab7de">enlarge_lit_pool</a> (void)</td></tr>
<tr class="separator:ae121408a92221766e9139e7cf40ab7de"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a81a2e3d63658a6aa21bda0b8660ee15f"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a81a2e3d63658a6aa21bda0b8660ee15f">compact_lit_pool</a> (void)</td></tr>
<tr class="separator:a81a2e3d63658a6aa21bda0b8660ee15f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a358ccda3851e0469ef0f2a6f3cf55726"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a358ccda3851e0469ef0f2a6f3cf55726">estimate_mem_usage</a> (void)</td></tr>
<tr class="separator:a358ccda3851e0469ef0f2a6f3cf55726"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1758bead04486434d17201a4bc9e6e40"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a1758bead04486434d17201a4bc9e6e40">mem_usage</a> (void)</td></tr>
<tr class="separator:a1758bead04486434d17201a4bc9e6e40"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae153743ecd52bb30bb757ad8d49c74e9"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#ae153743ecd52bb30bb757ad8d49c74e9">set_variable_number</a> (int n)</td></tr>
<tr class="separator:ae153743ecd52bb30bb757ad8d49c74e9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a84d9594576e3c2c13bde2f9d6a98a583"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a84d9594576e3c2c13bde2f9d6a98a583">add_variable</a> (void)</td></tr>
<tr class="separator:a84d9594576e3c2c13bde2f9d6a98a583"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac95e4d7648334447162c0fb4e3de28d7"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#ac95e4d7648334447162c0fb4e3de28d7">num_variables</a> (void)</td></tr>
<tr class="separator:ac95e4d7648334447162c0fb4e3de28d7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1ea198396d083b323c22cd49cc2be36c"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a1ea198396d083b323c22cd49cc2be36c">num_clauses</a> (void)</td></tr>
<tr class="separator:a1ea198396d083b323c22cd49cc2be36c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a93f69dacd75d1cf2d4a006b961f3b7b6"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a93f69dacd75d1cf2d4a006b961f3b7b6">num_literals</a> (void)</td></tr>
<tr class="separator:a93f69dacd75d1cf2d4a006b961f3b7b6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6529c55a489afcd88e37370d6a61ae96"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a6529c55a489afcd88e37370d6a61ae96">mark_clause_deleted</a> (<a class="el" href="classCClause.html">CClause</a> &cl)</td></tr>
<tr class="separator:a6529c55a489afcd88e37370d6a61ae96"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8fa67bd6b830c6853b01ed51b5fd183c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a8fa67bd6b830c6853b01ed51b5fd183c">mark_var_in_new_cl</a> (int v_idx, int phase)</td></tr>
<tr class="separator:a8fa67bd6b830c6853b01ed51b5fd183c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab0c8f1826cf8c92fc01943ab62d223df"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a> (<a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> l)</td></tr>
<tr class="separator:ab0c8f1826cf8c92fc01943ab62d223df"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3e469952453c4b10f1040e9a19375f77"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">find_unit_literal</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)</td></tr>
<tr class="separator:a3e469952453c4b10f1040e9a19375f77"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aeb01a55c31dfd135d9f19b561829e88d"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#aeb01a55c31dfd135d9f19b561829e88d">is_conflict</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)</td></tr>
<tr class="separator:aeb01a55c31dfd135d9f19b561829e88d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a85e3fc325b5e311c4081e5ac05e4ac5c"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a85e3fc325b5e311c4081e5ac05e4ac5c">is_satisfied</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)</td></tr>
<tr class="separator:a85e3fc325b5e311c4081e5ac05e4ac5c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a074d5b5a1fa285b8ae0e3c516a06a508"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:a074d5b5a1fa285b8ae0e3c516a06a508"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4ecc7a06a141221adf3aff50d3ac6cf6"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a4ecc7a06a141221adf3aff50d3ac6cf6">dump</a> (ostream &os=cout)</td></tr>
<tr class="separator:a4ecc7a06a141221adf3aff50d3ac6cf6"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pro-attribs"></a>
Protected Attributes</h2></td></tr>
<tr class="memitem:abb17b94a5d63adc740acbe28adb537dd"><td class="memItemLeft" align="right" valign="top"><a class="el" href="structCDatabaseStats.html">CDatabaseStats</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#abb17b94a5d63adc740acbe28adb537dd">_stats</a></td></tr>
<tr class="separator:abb17b94a5d63adc740acbe28adb537dd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9a30273cdd0b1f4814f470950cd90a77"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a9a30273cdd0b1f4814f470950cd90a77">_lit_pool_start</a></td></tr>
<tr class="separator:a9a30273cdd0b1f4814f470950cd90a77"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a970c8066adfcb3875af1f78f1c4029ff"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a970c8066adfcb3875af1f78f1c4029ff">_lit_pool_finish</a></td></tr>
<tr class="separator:a970c8066adfcb3875af1f78f1c4029ff"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3a4e4403ef1f9cb15c219bfe52b1d935"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a3a4e4403ef1f9cb15c219bfe52b1d935">_lit_pool_end_storage</a></td></tr>
<tr class="separator:a3a4e4403ef1f9cb15c219bfe52b1d935"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0bc13af9359ede872eefe8e1f44b3069"><td class="memItemLeft" align="right" valign="top">vector< <a class="el" href="classCVariable.html">CVariable</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a0bc13af9359ede872eefe8e1f44b3069">_variables</a></td></tr>
<tr class="separator:a0bc13af9359ede872eefe8e1f44b3069"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6adefe9983a5487fca8fc26cf8d9573f"><td class="memItemLeft" align="right" valign="top">vector< <a class="el" href="classCClause.html">CClause</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a6adefe9983a5487fca8fc26cf8d9573f">_clauses</a></td></tr>
<tr class="separator:a6adefe9983a5487fca8fc26cf8d9573f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae238340b46c3fc75854c4c244ae96d28"><td class="memItemLeft" align="right" valign="top">queue< <a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#ae238340b46c3fc75854c4c244ae96d28">_unused_clause_idx_queue</a></td></tr>
<tr class="separator:ae238340b46c3fc75854c4c244ae96d28"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa53ab545bfb59adcee894879520ee612"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#aa53ab545bfb59adcee894879520ee612">_num_var_in_new_cl</a></td></tr>
<tr class="separator:aa53ab545bfb59adcee894879520ee612"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5f8cf11f16f22e1ffd47a8d0146a584f"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCDatabase.html#a5f8cf11f16f22e1ffd47a8d0146a584f">_mem_limit</a></td></tr>
<tr class="separator:a5f8cf11f16f22e1ffd47a8d0146a584f"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">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><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a3959a40851f6fcb985542d1d43ff75dc"></a>
<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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CDatabase::~CDatabase </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="a8bac062c6bcaf5e92160fd0eff63bcd2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<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>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00142">CSolver::init()</a>.</p>
</div>
</div>
<a class="anchor" id="af4388cf12d2984898332c519b220d67b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<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>
<p>Referenced by <a class="el" href="xchaff__solver_8h_source.html#l00230">CSolver::set_mem_limit()</a>.</p>
</div>
</div>
<a class="anchor" id="a25c0a024183a09bf973942b1e4865501"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::init_num_clauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::init_num_literals </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::num_added_clauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::num_added_literals </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::num_deleted_clauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int& CDatabase::num_deleted_literals </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<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>
<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>
<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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<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>, and <a class="el" href="xchaff__solver_8h_source.html#l00326">CSolver::estimate_mem_usage()</a>.</p>
</div>
</div>
<a class="anchor" id="a1758bead04486434d17201a4bc9e6e40"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<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>
<p>Referenced by <a class="el" href="xchaff__solver_8h_source.html#l00329">CSolver::mem_usage()</a>.</p>
</div>
</div>
<a class="anchor" id="ae153743ecd52bb30bb757ad8d49c74e9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<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>
<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>
<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>
<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>
<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>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>
<p>Referenced by <a class="el" href="xchaff__solver_8h_source.html#l00381">CSolver::dump()</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="abb17b94a5d63adc740acbe28adb537dd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="structCDatabaseStats.html">CDatabaseStats</a> CDatabase::_stats</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a>* CDatabase::_lit_pool_start</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a>* CDatabase::_lit_pool_finish</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCLitPoolElement.html">CLitPoolElement</a>* CDatabase::_lit_pool_end_storage</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="classCVariable.html">CVariable</a>> CDatabase::_variables</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="classCClause.html">CClause</a>> CDatabase::_clauses</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">queue<<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a>> CDatabase::_unused_clause_idx_queue</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CDatabase::_num_var_in_new_cl</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CDatabase::_mem_limit</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:16 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
