<!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: Member List</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="headertitle">
<div class="title">CSolver Member List</div> </div>
</div>
<div class="contents">
This is the complete list of members for <a class="el" href="classCSolver.html">CSolver</a>, including all inherited members.<table>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">_addedUnitClauses</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a66cffc281bb01002d1b30e01f6e90a28">_assignment_hook</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a0de6dbd6e4d7f30c4ee841f15b8ae5e4">_assignment_hook_cookie</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a6adefe9983a5487fca8fc26cf8d9573f">_clauses</a></td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#af74159b82e953b3b766001d27b8b7981">_decision_hook</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a2a02aeed8e6eefe8b1d8a661c7e94c45">_decision_hook_cookie</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ac30b332eb58a51d87d9e1f80f62754f8">_deduction_hook</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#aa2c250ed33c494f50d06122943ae280d">_deduction_hook_cookie</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a65a9481261bf9d9d90ff36de99992094">_dlevel</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">_dlevel_hook</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ad1e4bd711ad507a40d36d5815bdaa69c">_dlevel_hook_cookie</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a49509a796f28911569176b2cc6d4a0a0">_hooks</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a3a4e4403ef1f9cb15c219bfe52b1d935">_lit_pool_end_storage</a></td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a970c8066adfcb3875af1f78f1c4029ff">_lit_pool_finish</a></td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a9a30273cdd0b1f4814f470950cd90a77">_lit_pool_start</a></td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">_max_score_pos</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a5f8cf11f16f22e1ffd47a8d0146a584f">_mem_limit</a></td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">_num_marked</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#aa53ab545bfb59adcee894879520ee612">_num_var_in_new_cl</a></td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#ae238340b46c3fc75854c4c244ae96d28">_unused_clause_idx_queue</a></td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a></td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a0bc13af9359ede872eefe8e1f44b3069">_variables</a></td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a5f90fcc1b1a7994a94fc8395d95cfb38">add_clause</a>(vector< long > &lits, bool addConflicts=true)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ade3fe6d285fbae6d71d09051e0e4637b">add_hook</a>(HookFunPtrT fun, int interval)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a84d9594576e3c2c13bde2f9d6a98a583">add_variable</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a1b1f7e9d95712bd0852366c044a5829f">add_variables</a>(int new_vars)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a2d476175cdda3b0028fb0efd754630d6">analyze_conflicts</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a48ffc1b95c078bcc0bb748f1068479fd">back_track</a>(int level)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a3959a40851f6fcb985542d1d43ff75dc">CDatabase</a>()</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(ClauseIdx idx)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a0c2329a20ee0a2672475933c3edd888e">clauses</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a81a2e3d63658a6aa21bda0b8660ee15f">compact_lit_pool</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a3bc2008b3318b4796cf2cd34fa446dee">conflict_analysis_grasp</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a9329cbfb2ba31fe55352644822889242">conflict_analysis_zchaff</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a9119faa6145fead463e8b14ec2f7cf7b">continueCheck</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ace35bd2316cbf7b72d942c7a672374e3">cpu_run_time</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#afa1c51e0570e7a835fae6ba187f9d09b">CSolver</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a4fc755c9adedc2769461bacfc8532f9e">current_world_time</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a752f7912bef54fb9f310cbeeabc34543">decide_next_branch</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a769075f3a6ed6eab6e4ec9e93c964f89">deduce</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a09834f0e5025b7a748bc24bf113b0f9e">delete_unrelevant_clauses</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a074d5b5a1fa285b8ae0e3c516a06a508">detail_dump_cl</a>(ClauseIdx cl_idx, ostream &os=cout)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">dump</a>(ostream &os=cout)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a60c64d82a19286ac5774adce294aa16a">dump_assignment_stack</a>(ostream &os=cout)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a66d960cb2bd8f5642afe1bf581d64f97">elapsed_cpu_time</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ad61a4e50bc8640852b7cd9d2cbd423d0">enable_cls_deletion</a>(bool allow)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#ae121408a92221766e9139e7cf40ab7de">enlarge_lit_pool</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a6a7cefe78a6f785c2c51950a74dde6d8">estimate_mem_usage</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a15a8ac75d8da0e7e47c0643870b3bcc9">find_max_clause_dlevel</a>(ClauseIdx cl)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">find_unit_literal</a>(ClauseIdx cl)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a711b6b701409a5a5fa54dd54b609328b">init</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a25c0a024183a09bf973942b1e4865501">init_num_clauses</a>()</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#ac4f22334ba90a99dc686757f484a9651">init_num_literals</a>()</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#aeb01a55c31dfd135d9f19b561829e88d">is_conflict</a>(ClauseIdx cl)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a85e3fc325b5e311c4081e5ac05e4ac5c">is_satisfied</a>(ClauseIdx cl)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a338b044147d1e34dfbed7cc8663725ae">lit_pool</a>(int i)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a2e6aeb6e495ae18667311b79982a5e6d">lit_pool_begin</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a3217dc6be8cff75fd418fbd4ff2e5763">lit_pool_end</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#ac66c5172be66fa260f8f6d5fd41ca295">lit_pool_free_space</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a7fa3358fa63aa02cae8055c0dfe832b7">lit_pool_push_back</a>(int value)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#ab6e49a71237bf7a6f060f79675bb39e7">lit_pool_size</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a>(CLitPoolElement l)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a6529c55a489afcd88e37370d6a61ae96">mark_clause_deleted</a>(CClause &cl)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a8fa67bd6b830c6853b01ed51b5fd183c">mark_var_in_new_cl</a>(int v_idx, int phase)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a525a84f821d273c9883a407c585b8b0d">mark_vars_at_level</a>(ClauseIdx cl, int var_idx, int dl)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">max_dlevel</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#af5b9bcac3d3bf0530bc36285ce8cc7f6">mem_usage</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a7c466015881107beb66f443839fd75e9">num_added_clauses</a>()</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a098b913b13aaab438a5f73a4cef09370">num_added_literals</a>()</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a1ea198396d083b323c22cd49cc2be36c">num_clauses</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a1d592aab62ad4f2943e0687916a34397">num_decisions</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#ad386f2990781ab78ebbe6eb83b7c365e">num_deleted_clauses</a>()</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a3e0c56c9059f90ce0b3ba0f94e2aeed2">num_deleted_literals</a>()</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a5b1c1a111284ece5745488b12baef8b2">num_free_variables</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ac1c4a48d4db9e61bc657a633b7230b88">num_implications</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a93f69dacd75d1cf2d4a006b961f3b7b6">num_literals</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#ac95e4d7648334447162c0fb4e3de28d7">num_variables</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#af7b4ed5bb5be8b7c56e4aa5f1913979b">outcome</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#adf342158bf2d06241a075a8c22a1ee73">output_current_stats</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a0a1c2417b7ef79f11d50add3d49625f7">output_lit_pool_state</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#aef7418705a19f94876ab5c708e87e15c">preprocess</a>(bool allowNewClauses)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a>(int lit, ClauseIdx ante_clause)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#af5c60a4d643467e199c00415fedc7e1d">real_solve</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#afcbec396917ed73948a67db3732054ae">RegisterAssignmentHook</a>(void(*f)(void *, int, int), void *cookie)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#aac7bf85fb8516ff4b3478598306fcb2e">RegisterDecisionHook</a>(int(*f)(void *, bool *), void *cookie)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a5aeafd67c7a77683ae040c11fbf033b1">RegisterDeductionHook</a>(void(*f)(void *), void *cookie)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#aa0f5bd7cea8ed3bc7254e29d744566fb">RegisterDLevelHook</a>(void(*f)(void *, int), void *cookie)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a5b9ce0b016266150cad691e4bb475668">restart</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a0ffdf7d6d085ca70b50391598bf4c543">run_periodic_functions</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#adcfb8dcb69c2221d25be0cd5ad6c43ff">set_allow_multiple_conflict</a>(bool b=false)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a9713537c85c12024d85d5b25ab2cb844">set_allow_multiple_conflict_clause</a>(bool b=false)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a31f9c112bb7ee8b3b334618d847d3d1f">set_cls_del_interval</a>(int n)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#adc4bf726c678250a85fef5a600d5e1d7">set_decision_strategy</a>(int s)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#aa3bb06628177a7a003957e00f9584351">set_max_conflict_clause_length</a>(int l)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a72cf182c0c2c1dccb61c837765ea56f3">set_max_unrelevance</a>(int n)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a069343e0391a7b95510634c9c96bb66f">set_mem_limit</a>(int s)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a5778d83eeb8c5ad0d34120c3b472cde9">set_min_num_clause_lits_for_delete</a>(int n)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a771e7780c8a112317bfd437599e2af22">set_preprocess_strategy</a>(int s)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a6765f3784e94ebde4c86447845e67c1d">set_random_seed</a>(int seed)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a17438ece1aeb9736e73bc25b96def58d">set_randomness</a>(int n)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a19c6655c87bd6117db6510183dad2893">set_time_limit</a>(float t)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ac06f1192d14de7730356cc102ebaee1b">set_var_value</a>(int var, int value, ClauseIdx ante, int dl)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a4617b5f40d47a1ac33135a76669994a4">set_var_value_not_current_dl</a>(int v, vector< CLitPoolElement * > &neg_ht_clauses)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ac497f97142b2f82acf8f43ba191feb08">set_var_value_with_current_dl</a>(int v, vector< CLitPoolElement * > &neg_ht_clauses)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#ae153743ecd52bb30bb757ad8d49c74e9">set_variable_number</a>(int n)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a351fe372330bede0ada8c3723e844a8e">solve</a>(bool allowNewClauses)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#addf48e1802591c3d505308224d7ceb31">stats</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#af3b17269840c1a07e21303c1fca4e5a0">time_out</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ae8d515c8e764ad65b870d5703b51c847">total_bubble_move</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#afde50f1cee0bab34e2464b17693d59f7">total_run_time</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a78ae7136f91966fdc7a55af71060875c">unset_var_value</a>(int var)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#acc181946a5845c647818631415c22c22">update_var_stats</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [protected]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(int idx)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>(void)</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">verify_integrity</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#a1153002750347545ac8b25d08ea96e39">version</a>(void)</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#aa181acac744c04062df328ee5eac38f9">world_run_time</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCDatabase.html#a9a3adb67c04d4f1432556aab4149841e">~CDatabase</a>()</td><td><a class="el" href="classCDatabase.html">CDatabase</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCSolver.html#af3c9bd8a7dede30ca60e24bf30073206">~CSolver</a>()</td><td><a class="el" href="classCSolver.html">CSolver</a></td><td></td></tr>
</table></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>
