<!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: CSolver 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-methods">Protected Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> |
<a href="classCSolver-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CSolver Class Reference</div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>></code></p>
<p>Inherits <a class="el" href="classCDatabase.html">CDatabase</a>.</p>
<div class="dynheader">
Collaboration diagram for CSolver:</div>
<div class="dyncontent">
<div class="center"><img src="classCSolver__coll__graph.gif" border="0" usemap="#CSolver_coll__map" alt="Collaboration graph"/></div>
<map name="CSolver_coll__map" id="CSolver_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:afa1c51e0570e7a835fae6ba187f9d09b"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#afa1c51e0570e7a835fae6ba187f9d09b">CSolver</a> ()</td></tr>
<tr class="separator:afa1c51e0570e7a835fae6ba187f9d09b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af3c9bd8a7dede30ca60e24bf30073206"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#af3c9bd8a7dede30ca60e24bf30073206">~CSolver</a> ()</td></tr>
<tr class="separator:af3c9bd8a7dede30ca60e24bf30073206"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a19c6655c87bd6117db6510183dad2893"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a19c6655c87bd6117db6510183dad2893">set_time_limit</a> (float t)</td></tr>
<tr class="separator:a19c6655c87bd6117db6510183dad2893"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a069343e0391a7b95510634c9c96bb66f"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a069343e0391a7b95510634c9c96bb66f">set_mem_limit</a> (int s)</td></tr>
<tr class="separator:a069343e0391a7b95510634c9c96bb66f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adc4bf726c678250a85fef5a600d5e1d7"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#adc4bf726c678250a85fef5a600d5e1d7">set_decision_strategy</a> (int s)</td></tr>
<tr class="separator:adc4bf726c678250a85fef5a600d5e1d7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a771e7780c8a112317bfd437599e2af22"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a771e7780c8a112317bfd437599e2af22">set_preprocess_strategy</a> (int s)</td></tr>
<tr class="separator:a771e7780c8a112317bfd437599e2af22"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad61a4e50bc8640852b7cd9d2cbd423d0"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ad61a4e50bc8640852b7cd9d2cbd423d0">enable_cls_deletion</a> (bool allow)</td></tr>
<tr class="separator:ad61a4e50bc8640852b7cd9d2cbd423d0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a31f9c112bb7ee8b3b334618d847d3d1f"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a31f9c112bb7ee8b3b334618d847d3d1f">set_cls_del_interval</a> (int n)</td></tr>
<tr class="separator:a31f9c112bb7ee8b3b334618d847d3d1f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a72cf182c0c2c1dccb61c837765ea56f3"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a72cf182c0c2c1dccb61c837765ea56f3">set_max_unrelevance</a> (int n)</td></tr>
<tr class="separator:a72cf182c0c2c1dccb61c837765ea56f3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5778d83eeb8c5ad0d34120c3b472cde9"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a5778d83eeb8c5ad0d34120c3b472cde9">set_min_num_clause_lits_for_delete</a> (int n)</td></tr>
<tr class="separator:a5778d83eeb8c5ad0d34120c3b472cde9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa3bb06628177a7a003957e00f9584351"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#aa3bb06628177a7a003957e00f9584351">set_max_conflict_clause_length</a> (int l)</td></tr>
<tr class="separator:aa3bb06628177a7a003957e00f9584351"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adcfb8dcb69c2221d25be0cd5ad6c43ff"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#adcfb8dcb69c2221d25be0cd5ad6c43ff">set_allow_multiple_conflict</a> (bool b=false)</td></tr>
<tr class="separator:adcfb8dcb69c2221d25be0cd5ad6c43ff"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9713537c85c12024d85d5b25ab2cb844"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a9713537c85c12024d85d5b25ab2cb844">set_allow_multiple_conflict_clause</a> (bool b=false)</td></tr>
<tr class="separator:a9713537c85c12024d85d5b25ab2cb844"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a17438ece1aeb9736e73bc25b96def58d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a17438ece1aeb9736e73bc25b96def58d">set_randomness</a> (int n)</td></tr>
<tr class="separator:a17438ece1aeb9736e73bc25b96def58d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6765f3784e94ebde4c86447845e67c1d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a6765f3784e94ebde4c86447845e67c1d">set_random_seed</a> (int seed)</td></tr>
<tr class="separator:a6765f3784e94ebde4c86447845e67c1d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa0f5bd7cea8ed3bc7254e29d744566fb"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#aa0f5bd7cea8ed3bc7254e29d744566fb">RegisterDLevelHook</a> (void(*f)(void *, int), void *cookie)</td></tr>
<tr class="separator:aa0f5bd7cea8ed3bc7254e29d744566fb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aac7bf85fb8516ff4b3478598306fcb2e"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#aac7bf85fb8516ff4b3478598306fcb2e">RegisterDecisionHook</a> (int(*f)(void *, bool *), void *cookie)</td></tr>
<tr class="separator:aac7bf85fb8516ff4b3478598306fcb2e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afcbec396917ed73948a67db3732054ae"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#afcbec396917ed73948a67db3732054ae">RegisterAssignmentHook</a> (void(*f)(void *, int, int), void *cookie)</td></tr>
<tr class="separator:afcbec396917ed73948a67db3732054ae"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5aeafd67c7a77683ae040c11fbf033b1"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a5aeafd67c7a77683ae040c11fbf033b1">RegisterDeductionHook</a> (void(*f)(void *), void *cookie)</td></tr>
<tr class="separator:a5aeafd67c7a77683ae040c11fbf033b1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af7b4ed5bb5be8b7c56e4aa5f1913979b"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#af7b4ed5bb5be8b7c56e4aa5f1913979b">outcome</a> ()</td></tr>
<tr class="separator:af7b4ed5bb5be8b7c56e4aa5f1913979b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1d592aab62ad4f2943e0687916a34397"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a1d592aab62ad4f2943e0687916a34397">num_decisions</a> ()</td></tr>
<tr class="separator:a1d592aab62ad4f2943e0687916a34397"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5b1c1a111284ece5745488b12baef8b2"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a5b1c1a111284ece5745488b12baef8b2">num_free_variables</a> ()</td></tr>
<tr class="separator:a5b1c1a111284ece5745488b12baef8b2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a881e379b28047fde2157720bf4ee9fd0"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">max_dlevel</a> ()</td></tr>
<tr class="separator:a881e379b28047fde2157720bf4ee9fd0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac1c4a48d4db9e61bc657a633b7230b88"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ac1c4a48d4db9e61bc657a633b7230b88">num_implications</a> ()</td></tr>
<tr class="separator:ac1c4a48d4db9e61bc657a633b7230b88"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae8d515c8e764ad65b870d5703b51c847"><td class="memItemLeft" align="right" valign="top">long </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ae8d515c8e764ad65b870d5703b51c847">total_bubble_move</a> (void)</td></tr>
<tr class="separator:ae8d515c8e764ad65b870d5703b51c847"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1153002750347545ac8b25d08ea96e39"><td class="memItemLeft" align="right" valign="top">const char * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a1153002750347545ac8b25d08ea96e39">version</a> (void)</td></tr>
<tr class="separator:a1153002750347545ac8b25d08ea96e39"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7d23251aefbab59adac9658723ac60ad"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a> (void)</td></tr>
<tr class="separator:a7d23251aefbab59adac9658723ac60ad"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4fc755c9adedc2769461bacfc8532f9e"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a4fc755c9adedc2769461bacfc8532f9e">current_world_time</a> (void)</td></tr>
<tr class="separator:a4fc755c9adedc2769461bacfc8532f9e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a66d960cb2bd8f5642afe1bf581d64f97"><td class="memItemLeft" align="right" valign="top">float </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a66d960cb2bd8f5642afe1bf581d64f97">elapsed_cpu_time</a> ()</td></tr>
<tr class="separator:a66d960cb2bd8f5642afe1bf581d64f97"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afde50f1cee0bab34e2464b17693d59f7"><td class="memItemLeft" align="right" valign="top">float </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#afde50f1cee0bab34e2464b17693d59f7">total_run_time</a> ()</td></tr>
<tr class="separator:afde50f1cee0bab34e2464b17693d59f7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ace35bd2316cbf7b72d942c7a672374e3"><td class="memItemLeft" align="right" valign="top">float </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ace35bd2316cbf7b72d942c7a672374e3">cpu_run_time</a> ()</td></tr>
<tr class="separator:ace35bd2316cbf7b72d942c7a672374e3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa181acac744c04062df328ee5eac38f9"><td class="memItemLeft" align="right" valign="top">float </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#aa181acac744c04062df328ee5eac38f9">world_run_time</a> ()</td></tr>
<tr class="separator:aa181acac744c04062df328ee5eac38f9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6a7cefe78a6f785c2c51950a74dde6d8"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a6a7cefe78a6f785c2c51950a74dde6d8">estimate_mem_usage</a> ()</td></tr>
<tr class="separator:a6a7cefe78a6f785c2c51950a74dde6d8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af5b9bcac3d3bf0530bc36285ce8cc7f6"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#af5b9bcac3d3bf0530bc36285ce8cc7f6">mem_usage</a> (void)</td></tr>
<tr class="separator:af5b9bcac3d3bf0530bc36285ce8cc7f6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad51e4ee566b488f8d3610890f3fa1bb7"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a> ()</td></tr>
<tr class="separator:ad51e4ee566b488f8d3610890f3fa1bb7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ade3fe6d285fbae6d71d09051e0e4637b"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ade3fe6d285fbae6d71d09051e0e4637b">add_hook</a> (<a class="el" href="xchaff__solver_8h.html#a4288f2865a52bcea1f6cd0afa93a7898">HookFunPtrT</a> fun, int interval)</td></tr>
<tr class="separator:ade3fe6d285fbae6d71d09051e0e4637b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a21e170987f92adbe179f39ffe3c861be"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a> (int lit, <a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> ante_clause)</td></tr>
<tr class="separator:a21e170987f92adbe179f39ffe3c861be"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1b1f7e9d95712bd0852366c044a5829f"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a1b1f7e9d95712bd0852366c044a5829f">add_variables</a> (int new_vars)</td></tr>
<tr class="separator:a1b1f7e9d95712bd0852366c044a5829f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5f90fcc1b1a7994a94fc8395d95cfb38"><td class="memItemLeft" align="right" valign="top"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a5f90fcc1b1a7994a94fc8395d95cfb38">add_clause</a> (vector< long > &lits, bool addConflicts=true)</td></tr>
<tr class="separator:a5f90fcc1b1a7994a94fc8395d95cfb38"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac14b7728d00ff497795bcedfd3f24faa"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">verify_integrity</a> (void)</td></tr>
<tr class="separator:ac14b7728d00ff497795bcedfd3f24faa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5b9ce0b016266150cad691e4bb475668"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a5b9ce0b016266150cad691e4bb475668">restart</a> (void)</td></tr>
<tr class="separator:a5b9ce0b016266150cad691e4bb475668"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a351fe372330bede0ada8c3723e844a8e"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a351fe372330bede0ada8c3723e844a8e">solve</a> (bool allowNewClauses)</td></tr>
<tr class="separator:a351fe372330bede0ada8c3723e844a8e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9119faa6145fead463e8b14ec2f7cf7b"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a9119faa6145fead463e8b14ec2f7cf7b">continueCheck</a> ()</td></tr>
<tr class="separator:a9119faa6145fead463e8b14ec2f7cf7b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a60c64d82a19286ac5774adce294aa16a"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a60c64d82a19286ac5774adce294aa16a">dump_assignment_stack</a> (ostream &os=cout)</td></tr>
<tr class="separator:a60c64d82a19286ac5774adce294aa16a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adf342158bf2d06241a075a8c22a1ee73"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#adf342158bf2d06241a075a8c22a1ee73">output_current_stats</a> (void)</td></tr>
<tr class="separator:adf342158bf2d06241a075a8c22a1ee73"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8804888a9795945f5b09c67c529b898d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">dump</a> (ostream &os=cout)</td></tr>
<tr class="separator:a8804888a9795945f5b09c67c529b898d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="inherit_header pub_methods_classCDatabase"><td colspan="2" onclick="javascript:toggleInherit('pub_methods_classCDatabase')"><img src="closed.png" alt="-"/> Public Member Functions inherited from <a class="el" href="classCDatabase.html">CDatabase</a></td></tr>
<tr class="memitem:a3959a40851f6fcb985542d1d43ff75dc inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9a3adb67c04d4f1432556aab4149841e inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8bac062c6bcaf5e92160fd0eff63bcd2 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af4388cf12d2984898332c519b220d67b inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0c2329a20ee0a2672475933c3edd888e inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af421024d0ade14743332069684aba162 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5af3586dfcd579ab14d37c6b6cf75e18 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:addf48e1802591c3d505308224d7ceb31 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adfda0cf04a767a89cc9ac7dbeb7a11ce inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a25c0a024183a09bf973942b1e4865501 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac4f22334ba90a99dc686757f484a9651 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7c466015881107beb66f443839fd75e9 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a098b913b13aaab438a5f73a4cef09370 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad386f2990781ab78ebbe6eb83b7c365e inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3e0c56c9059f90ce0b3ba0f94e2aeed2 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2e6aeb6e495ae18667311b79982a5e6d inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3217dc6be8cff75fd418fbd4ff2e5763 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7fa3358fa63aa02cae8055c0dfe832b7 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab6e49a71237bf7a6f060f79675bb39e7 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac66c5172be66fa260f8f6d5fd41ca295 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a338b044147d1e34dfbed7cc8663725ae inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0a1c2417b7ef79f11d50add3d49625f7 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae121408a92221766e9139e7cf40ab7de inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a81a2e3d63658a6aa21bda0b8660ee15f inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a358ccda3851e0469ef0f2a6f3cf55726 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1758bead04486434d17201a4bc9e6e40 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae153743ecd52bb30bb757ad8d49c74e9 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a84d9594576e3c2c13bde2f9d6a98a583 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac95e4d7648334447162c0fb4e3de28d7 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1ea198396d083b323c22cd49cc2be36c inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a93f69dacd75d1cf2d4a006b961f3b7b6 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6529c55a489afcd88e37370d6a61ae96 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8fa67bd6b830c6853b01ed51b5fd183c inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab0c8f1826cf8c92fc01943ab62d223df inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3e469952453c4b10f1040e9a19375f77 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aeb01a55c31dfd135d9f19b561829e88d inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a85e3fc325b5e311c4081e5ac05e4ac5c inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a074d5b5a1fa285b8ae0e3c516a06a508 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4ecc7a06a141221adf3aff50d3ac6cf6 inherit pub_methods_classCDatabase"><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 inherit pub_methods_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pro-methods"></a>
Protected Member Functions</h2></td></tr>
<tr class="memitem:af5c60a4d643467e199c00415fedc7e1d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#af5c60a4d643467e199c00415fedc7e1d">real_solve</a> (void)</td></tr>
<tr class="separator:af5c60a4d643467e199c00415fedc7e1d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aef7418705a19f94876ab5c708e87e15c"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#aef7418705a19f94876ab5c708e87e15c">preprocess</a> (bool allowNewClauses)</td></tr>
<tr class="separator:aef7418705a19f94876ab5c708e87e15c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a769075f3a6ed6eab6e4ec9e93c964f89"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a769075f3a6ed6eab6e4ec9e93c964f89">deduce</a> (void)</td></tr>
<tr class="separator:a769075f3a6ed6eab6e4ec9e93c964f89"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a752f7912bef54fb9f310cbeeabc34543"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a752f7912bef54fb9f310cbeeabc34543">decide_next_branch</a> (void)</td></tr>
<tr class="separator:a752f7912bef54fb9f310cbeeabc34543"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2d476175cdda3b0028fb0efd754630d6"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a2d476175cdda3b0028fb0efd754630d6">analyze_conflicts</a> (void)</td></tr>
<tr class="separator:a2d476175cdda3b0028fb0efd754630d6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3bc2008b3318b4796cf2cd34fa446dee"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a3bc2008b3318b4796cf2cd34fa446dee">conflict_analysis_grasp</a> (void)</td></tr>
<tr class="separator:a3bc2008b3318b4796cf2cd34fa446dee"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9329cbfb2ba31fe55352644822889242"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a9329cbfb2ba31fe55352644822889242">conflict_analysis_zchaff</a> (void)</td></tr>
<tr class="separator:a9329cbfb2ba31fe55352644822889242"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a48ffc1b95c078bcc0bb748f1068479fd"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a48ffc1b95c078bcc0bb748f1068479fd">back_track</a> (int level)</td></tr>
<tr class="separator:a48ffc1b95c078bcc0bb748f1068479fd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a711b6b701409a5a5fa54dd54b609328b"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a711b6b701409a5a5fa54dd54b609328b">init</a> (void)</td></tr>
<tr class="separator:a711b6b701409a5a5fa54dd54b609328b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a525a84f821d273c9883a407c585b8b0d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a525a84f821d273c9883a407c585b8b0d">mark_vars_at_level</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl, int var_idx, int dl)</td></tr>
<tr class="separator:a525a84f821d273c9883a407c585b8b0d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a15a8ac75d8da0e7e47c0643870b3bcc9"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a15a8ac75d8da0e7e47c0643870b3bcc9">find_max_clause_dlevel</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)</td></tr>
<tr class="separator:a15a8ac75d8da0e7e47c0643870b3bcc9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac06f1192d14de7730356cc102ebaee1b"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ac06f1192d14de7730356cc102ebaee1b">set_var_value</a> (int var, int value, <a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> ante, int dl)</td></tr>
<tr class="separator:ac06f1192d14de7730356cc102ebaee1b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4617b5f40d47a1ac33135a76669994a4"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a4617b5f40d47a1ac33135a76669994a4">set_var_value_not_current_dl</a> (int v, vector< <a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * > &neg_ht_clauses)</td></tr>
<tr class="separator:a4617b5f40d47a1ac33135a76669994a4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac497f97142b2f82acf8f43ba191feb08"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ac497f97142b2f82acf8f43ba191feb08">set_var_value_with_current_dl</a> (int v, vector< <a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * > &neg_ht_clauses)</td></tr>
<tr class="separator:ac497f97142b2f82acf8f43ba191feb08"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a78ae7136f91966fdc7a55af71060875c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a78ae7136f91966fdc7a55af71060875c">unset_var_value</a> (int var)</td></tr>
<tr class="separator:a78ae7136f91966fdc7a55af71060875c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0ffdf7d6d085ca70b50391598bf4c543"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a0ffdf7d6d085ca70b50391598bf4c543">run_periodic_functions</a> (void)</td></tr>
<tr class="separator:a0ffdf7d6d085ca70b50391598bf4c543"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acc181946a5845c647818631415c22c22"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#acc181946a5845c647818631415c22c22">update_var_stats</a> (void)</td></tr>
<tr class="separator:acc181946a5845c647818631415c22c22"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af3b17269840c1a07e21303c1fca4e5a0"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#af3b17269840c1a07e21303c1fca4e5a0">time_out</a> (void)</td></tr>
<tr class="separator:af3b17269840c1a07e21303c1fca4e5a0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a09834f0e5025b7a748bc24bf113b0f9e"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a09834f0e5025b7a748bc24bf113b0f9e">delete_unrelevant_clauses</a> (void)</td></tr>
<tr class="separator:a09834f0e5025b7a748bc24bf113b0f9e"><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:a65a9481261bf9d9d90ff36de99992094"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a65a9481261bf9d9d90ff36de99992094">_dlevel</a></td></tr>
<tr class="separator:a65a9481261bf9d9d90ff36de99992094"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6a21ab9d2ab20a5c4f103cc1a337e35f"><td class="memItemLeft" align="right" valign="top">vector< vector< int > * > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a></td></tr>
<tr class="separator:a6a21ab9d2ab20a5c4f103cc1a337e35f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aeab7cd8f6085990a2a1ed518c9d75c6e"><td class="memItemLeft" align="right" valign="top">queue< pair< int, <a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> > > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a></td></tr>
<tr class="separator:aeab7cd8f6085990a2a1ed518c9d75c6e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a30e5a80e5be76e6be4398340f3925818"><td class="memItemLeft" align="right" valign="top"><a class="el" href="structCSolverParameters.html">CSolverParameters</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a></td></tr>
<tr class="separator:a30e5a80e5be76e6be4398340f3925818"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5f656ea799ff4b4304b9f4f71a4df315"><td class="memItemLeft" align="right" valign="top"><a class="el" href="structCSolverStats.html">CSolverStats</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a></td></tr>
<tr class="separator:a5f656ea799ff4b4304b9f4f71a4df315"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a49509a796f28911569176b2cc6d4a0a0"><td class="memItemLeft" align="right" valign="top">vector< pair< int, pair<br class="typebreak"/>
< <a class="el" href="xchaff__solver_8h.html#a4288f2865a52bcea1f6cd0afa93a7898">HookFunPtrT</a>, int > > > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a49509a796f28911569176b2cc6d4a0a0">_hooks</a></td></tr>
<tr class="separator:a49509a796f28911569176b2cc6d4a0a0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae7e25a4d85f75c17d55cf64e26056920"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">_max_score_pos</a></td></tr>
<tr class="separator:ae7e25a4d85f75c17d55cf64e26056920"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aec6d0a9cf59ad2da0dad717bea16efcb"><td class="memItemLeft" align="right" valign="top">vector< int > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a> [2]</td></tr>
<tr class="separator:aec6d0a9cf59ad2da0dad717bea16efcb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a40c08e5478f016f460d6adec977c2446"><td class="memItemLeft" align="right" valign="top">vector< pair< int, int > > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a></td></tr>
<tr class="separator:a40c08e5478f016f460d6adec977c2446"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a528d66d18534a7d6e73a2e7964103b1c"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">_num_marked</a></td></tr>
<tr class="separator:a528d66d18534a7d6e73a2e7964103b1c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6bba00c21025040cc46a0499eaea7f01"><td class="memItemLeft" align="right" valign="top">vector< <a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a></td></tr>
<tr class="separator:a6bba00c21025040cc46a0499eaea7f01"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab162797183d22466c24feb117fefc7d6"><td class="memItemLeft" align="right" valign="top">vector< long > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a></td></tr>
<tr class="separator:ab162797183d22466c24feb117fefc7d6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad517659e82e1b42617886d2b6758acd3"><td class="memItemLeft" align="right" valign="top">void(* </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">_dlevel_hook</a> )(void *, int)</td></tr>
<tr class="separator:ad517659e82e1b42617886d2b6758acd3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af74159b82e953b3b766001d27b8b7981"><td class="memItemLeft" align="right" valign="top">int(* </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#af74159b82e953b3b766001d27b8b7981">_decision_hook</a> )(void *, bool *)</td></tr>
<tr class="separator:af74159b82e953b3b766001d27b8b7981"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a66cffc281bb01002d1b30e01f6e90a28"><td class="memItemLeft" align="right" valign="top">void(* </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a66cffc281bb01002d1b30e01f6e90a28">_assignment_hook</a> )(void *, int, int)</td></tr>
<tr class="separator:a66cffc281bb01002d1b30e01f6e90a28"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac30b332eb58a51d87d9e1f80f62754f8"><td class="memItemLeft" align="right" valign="top">void(* </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ac30b332eb58a51d87d9e1f80f62754f8">_deduction_hook</a> )(void *)</td></tr>
<tr class="separator:ac30b332eb58a51d87d9e1f80f62754f8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad1e4bd711ad507a40d36d5815bdaa69c"><td class="memItemLeft" align="right" valign="top">void * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#ad1e4bd711ad507a40d36d5815bdaa69c">_dlevel_hook_cookie</a></td></tr>
<tr class="separator:ad1e4bd711ad507a40d36d5815bdaa69c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2a02aeed8e6eefe8b1d8a661c7e94c45"><td class="memItemLeft" align="right" valign="top">void * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a2a02aeed8e6eefe8b1d8a661c7e94c45">_decision_hook_cookie</a></td></tr>
<tr class="separator:a2a02aeed8e6eefe8b1d8a661c7e94c45"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0de6dbd6e4d7f30c4ee841f15b8ae5e4"><td class="memItemLeft" align="right" valign="top">void * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a0de6dbd6e4d7f30c4ee841f15b8ae5e4">_assignment_hook_cookie</a></td></tr>
<tr class="separator:a0de6dbd6e4d7f30c4ee841f15b8ae5e4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa2c250ed33c494f50d06122943ae280d"><td class="memItemLeft" align="right" valign="top">void * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#aa2c250ed33c494f50d06122943ae280d">_deduction_hook_cookie</a></td></tr>
<tr class="separator:aa2c250ed33c494f50d06122943ae280d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6b12fb5fcb0e279221c4047b3a61d99e"><td class="memItemLeft" align="right" valign="top">vector< <a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">_addedUnitClauses</a></td></tr>
<tr class="separator:a6b12fb5fcb0e279221c4047b3a61d99e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="inherit_header pro_attribs_classCDatabase"><td colspan="2" onclick="javascript:toggleInherit('pro_attribs_classCDatabase')"><img src="closed.png" alt="-"/> Protected Attributes inherited from <a class="el" href="classCDatabase.html">CDatabase</a></td></tr>
<tr class="memitem:abb17b94a5d63adc740acbe28adb537dd inherit pro_attribs_classCDatabase"><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 inherit pro_attribs_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9a30273cdd0b1f4814f470950cd90a77 inherit pro_attribs_classCDatabase"><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 inherit pro_attribs_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a970c8066adfcb3875af1f78f1c4029ff inherit pro_attribs_classCDatabase"><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 inherit pro_attribs_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3a4e4403ef1f9cb15c219bfe52b1d935 inherit pro_attribs_classCDatabase"><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 inherit pro_attribs_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0bc13af9359ede872eefe8e1f44b3069 inherit pro_attribs_classCDatabase"><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 inherit pro_attribs_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6adefe9983a5487fca8fc26cf8d9573f inherit pro_attribs_classCDatabase"><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 inherit pro_attribs_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae238340b46c3fc75854c4c244ae96d28 inherit pro_attribs_classCDatabase"><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 inherit pro_attribs_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa53ab545bfb59adcee894879520ee612 inherit pro_attribs_classCDatabase"><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 inherit pro_attribs_classCDatabase"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5f8cf11f16f22e1ffd47a8d0146a584f inherit pro_attribs_classCDatabase"><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 inherit pro_attribs_classCDatabase"><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 [Sat Solver]</p>
<p>Description [This class contains the process and datastructrues to solve the Sat problem.]</p>
<p>SeeAlso [] </p>
<p>Definition at line <a class="el" href="xchaff__solver_8h_source.html#l00148">148</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="afa1c51e0570e7a835fae6ba187f9d09b"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CSolver::CSolver </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__solver_8cpp_source.html#l00043">43</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00172">_assignment_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00171">_decision_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00173">_deduction_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00151">_dlevel</a>, <a class="el" href="xchaff__solver_8h_source.html#l00170">_dlevel_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00165">_num_marked</a>, <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00083">CSolverParameters::allow_clause_deletion</a>, <a class="el" href="xchaff__solver_8h_source.html#l00105">CSolverParameters::allow_multiple_conflict</a>, <a class="el" href="xchaff__solver_8h_source.html#l00106">CSolverParameters::allow_multiple_conflict_clause</a>, <a class="el" href="xchaff__solver_8h_source.html#l00093">CSolverParameters::allow_restart</a>, <a class="el" href="xchaff__solver_8h_source.html#l00103">CSolverParameters::back_track_complete</a>, <a class="el" href="xchaff__solver_8h_source.html#l00101">CSolverParameters::base_randomness</a>, <a class="el" href="xchaff__solver_8h_source.html#l00088">CSolverParameters::bubble_init_step</a>, <a class="el" href="xchaff__solver_8h_source.html#l00084">CSolverParameters::clause_deletion_interval</a>, <a class="el" href="xchaff__solver_8h_source.html#l00080">CSolverParameters::decision_strategy</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00125">CSolverStats::finish_cpu_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00127">CSolverStats::finish_world_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00121">CSolverStats::is_mem_out</a>, <a class="el" href="xchaff__solver_8h_source.html#l00118">CSolverStats::is_solver_started</a>, <a class="el" href="xchaff__solver_8h_source.html#l00124">CSolverStats::last_cpu_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00087">CSolverParameters::max_conflict_clause_length</a>, <a class="el" href="xchaff__solver_8h_source.html#l00133">CSolverStats::max_dlevel</a>, <a class="el" href="xchaff__solver_8h_source.html#l00085">CSolverParameters::max_unrelevance</a>, <a class="el" href="xchaff__solver_8h_source.html#l00086">CSolverParameters::min_num_clause_lits_for_delete</a>, <a class="el" href="xchaff__solver_8h_source.html#l00097">CSolverParameters::next_restart_backtrack</a>, <a class="el" href="xchaff__solver_8h_source.html#l00094">CSolverParameters::next_restart_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00132">CSolverStats::num_backtracks</a>, <a class="el" href="xchaff__solver_8h_source.html#l00131">CSolverStats::num_decisions</a>, <a class="el" href="xchaff__solver_8h_source.html#l00134">CSolverStats::num_implications</a>, <a class="el" href="xchaff__solver_8h_source.html#l00119">CSolverStats::outcome</a>, <a class="el" href="xchaff__solver_8h_source.html#l00081">CSolverParameters::preprocess_strategy</a>, <a class="el" href="xchaff__solver_8h_source.html#l00091">CSolverParameters::randomness</a>, <a class="el" href="xchaff__solver_8h_source.html#l00098">CSolverParameters::restart_backtrack_incr</a>, <a class="el" href="xchaff__solver_8h_source.html#l00099">CSolverParameters::restart_backtrack_incr_incr</a>, <a class="el" href="xchaff__solver_8h_source.html#l00100">CSolverParameters::restart_randomness</a>, <a class="el" href="xchaff__solver_8h_source.html#l00096">CSolverParameters::restart_time_incr_incr</a>, <a class="el" href="xchaff__solver_8h_source.html#l00095">CSolverParameters::restart_time_increment</a>, <a class="el" href="xchaff__solver_8h_source.html#l00123">CSolverStats::start_cpu_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00126">CSolverStats::start_world_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00078">CSolverParameters::time_limit</a>, <a class="el" href="xchaff__solver_8h_source.html#l00129">CSolverStats::total_bubble_move</a>, <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00090">CSolverParameters::verbosity</a>.</p>
</div>
</div>
<a class="anchor" id="af3c9bd8a7dede30ca60e24bf30073206"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CSolver::~CSolver </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__solver_8cpp_source.html#l00101">101</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00152">_assignment_stack</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00118">CSolverStats::is_solver_started</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="af5c60a4d643467e199c00415fedc7e1d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::real_solve </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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00763">763</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00180">_addedUnitClauses</a>, <a class="el" href="xchaff__solver_8h_source.html#l00166">_conflicts</a>, <a class="el" href="xchaff__solver_8h_source.html#l00153">_implication_queue</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00912">analyze_conflicts()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00063">CONFLICT</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00497">CDatabase::find_unit_literal()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00121">CSolverStats::is_mem_out</a>, <a class="el" href="xchaff__solver_8h_source.html#l00057">MEM_OUT</a>, <a class="el" href="xchaff__solver_8h_source.html#l00119">CSolverStats::outcome</a>, <a class="el" href="xchaff__solver_8h_source.html#l00345">queue_implication()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00109">run_periodic_functions()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00055">SATISFIABLE</a>, <a class="el" href="xchaff__solver_8h_source.html#l00056">TIME_OUT</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00587">time_out()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00054">UNSATISFIABLE</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00822">continueCheck()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00804">solve()</a>.</p>
</div>
</div>
<a class="anchor" id="aef7418705a19f94876ab5c708e87e15c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::preprocess </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>allowNewClauses</em></td><td>)</td>
<td></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__solver_8cpp_source.html#l00706">706</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">CDatabase::clause()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00120">CDatabase::clauses()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00063">CONFLICT</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, <a class="el" href="xchaff__base_8h_source.html#l00267">CVariable::dlevel()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00497">CDatabase::find_unit_literal()</a>, <a class="el" href="xchaff__base_8h_source.html#l00276">CVariable::lits_count()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00064">NO_CONFLICT</a>, <a class="el" href="xchaff__base_8h_source.html#l00051">NULL_CLAUSE</a>, <a class="el" href="xchaff__solver_8h_source.html#l00276">num_free_variables()</a>, <a class="el" href="xchaff__base_8h_source.html#l00189">CClause::num_lits()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00345">queue_implication()</a>, <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>, <a class="el" href="xchaff__base_8h_source.html#l00264">CVariable::value()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00123">CDatabase::variable()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00090">CSolverParameters::verbosity</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00804">solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a769075f3a6ed6eab6e4ec9e93c964f89"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::deduce </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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00852">852</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00152">_assignment_stack</a>, <a class="el" href="xchaff__solver_8h_source.html#l00166">_conflicts</a>, <a class="el" href="xchaff__solver_8h_source.html#l00173">_deduction_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00177">_deduction_hook_cookie</a>, <a class="el" href="xchaff__solver_8h_source.html#l00153">_implication_queue</a>, <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, <a class="el" href="xchaff__solver_8h_source.html#l00103">CSolverParameters::back_track_complete</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, <a class="el" href="xchaff__solver_8h_source.html#l00063">CONFLICT</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00447">find_max_clause_dlevel()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00064">NO_CONFLICT</a>, <a class="el" href="xchaff__solver_8h_source.html#l00358">restart()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00296">set_var_value()</a>, <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>, <a class="el" href="xchaff__base_8h_source.html#l00264">CVariable::value()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00886">verify_integrity()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00706">preprocess()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a752f7912bef54fb9f310cbeeabc34543"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CSolver::decide_next_branch </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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00617">617</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00166">_conflicts</a>, <a class="el" href="xchaff__solver_8h_source.html#l00171">_decision_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00175">_decision_hook_cookie</a>, <a class="el" href="xchaff__solver_8h_source.html#l00170">_dlevel_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00174">_dlevel_hook_cookie</a>, <a class="el" href="xchaff__solver_8h_source.html#l00153">_implication_queue</a>, <a class="el" href="xchaff__solver_8h_source.html#l00160">_max_score_pos</a>, <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00162">_var_order</a>, <a class="el" href="xchaff__solver_8h_source.html#l00101">CSolverParameters::base_randomness</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00133">CSolverStats::max_dlevel</a>, <a class="el" href="xchaff__base_8h_source.html#l00051">NULL_CLAUSE</a>, <a class="el" href="xchaff__solver_8h_source.html#l00131">CSolverStats::num_decisions</a>, <a class="el" href="xchaff__solver_8h_source.html#l00276">num_free_variables()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00345">queue_implication()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00091">CSolverParameters::randomness</a>, <a class="el" href="xchaff__base_8h_source.html#l00249">CVariable::score()</a>, <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>, <a class="el" href="xchaff__base_8h_source.html#l00264">CVariable::value()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a2d476175cdda3b0028fb0efd754630d6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::analyze_conflicts </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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00912">912</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a3bc2008b3318b4796cf2cd34fa446dee"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::conflict_analysis_grasp </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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
</div>
</div>
<a class="anchor" id="a9329cbfb2ba31fe55352644822889242"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::conflict_analysis_zchaff </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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00916">916</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00152">_assignment_stack</a>, <a class="el" href="xchaff__solver_8h_source.html#l00167">_conflict_lits</a>, <a class="el" href="xchaff__solver_8h_source.html#l00166">_conflicts</a>, <a class="el" href="xchaff__solver_8h_source.html#l00153">_implication_queue</a>, <a class="el" href="xchaff__solver_8h_source.html#l00165">_num_marked</a>, <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00179">add_clause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00103">CSolverParameters::back_track_complete</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">CDatabase::clause()</a>, <a class="el" href="xchaff__base_8h_source.html#l00286">CVariable::clear_marked()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00463">dump_assignment_stack()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00447">find_max_clause_dlevel()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00497">CDatabase::find_unit_literal()</a>, <a class="el" href="xchaff__base_8h_source.html#l00270">CVariable::in_new_cl()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00479">CDatabase::is_conflict()</a>, <a class="el" href="xchaff__base_8h_source.html#l00280">CVariable::is_marked()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00121">CSolverStats::is_mem_out</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00890">mark_vars_at_level()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00279">max_dlevel()</a>, <a class="el" href="xchaff__base_8h_source.html#l00051">NULL_CLAUSE</a>, <a class="el" href="xchaff__solver_8h_source.html#l00345">queue_implication()</a>, <a class="el" href="xchaff__base_8h_source.html#l00273">CVariable::set_in_new_cl()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00123">CDatabase::variable()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00912">analyze_conflicts()</a>.</p>
</div>
</div>
<a class="anchor" id="a48ffc1b95c078bcc0bb748f1068479fd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::back_track </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>level</em></td><td>)</td>
<td></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__solver_8cpp_source.html#l00830">830</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00152">_assignment_stack</a>, <a class="el" href="xchaff__solver_8h_source.html#l00170">_dlevel_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00174">_dlevel_hook_cookie</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, <a class="el" href="xchaff__utils_8h_source.html#l00043">CHECK_FULL</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00381">dump()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00132">CSolverStats::num_backtracks</a>, <a class="el" href="xchaff__solver_8h_source.html#l00276">num_free_variables()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00433">unset_var_value()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00886">verify_integrity()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00358">restart()</a>.</p>
</div>
</div>
<a class="anchor" id="a711b6b701409a5a5fa54dd54b609328b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00142">142</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00152">_assignment_stack</a>, <a class="el" href="xchaff__solver_8h_source.html#l00161">_last_var_lits_count</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00162">_var_order</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, <a class="el" href="xchaff__solver_8h_source.html#l00287">current_cpu_time()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00296">current_world_time()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00381">dump()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00112">CDatabase::init()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00118">CSolverStats::is_solver_started</a>, <a class="el" href="xchaff__solver_8h_source.html#l00135">CSolverStats::num_free_variables</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00210">CDatabase::num_variables()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00123">CSolverStats::start_cpu_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00126">CSolverStats::start_world_time</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00804">solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a525a84f821d273c9883a407c585b8b0d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::mark_vars_at_level </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>var_idx</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>dl</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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00890">890</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00167">_conflict_lits</a>, <a class="el" href="xchaff__solver_8h_source.html#l00165">_num_marked</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">CDatabase::clause()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="xchaff__base_8h_source.html#l00273">CVariable::set_in_new_cl()</a>, <a class="el" href="xchaff__base_8h_source.html#l00283">CVariable::set_marked()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">CDatabase::variable()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>.</p>
</div>
</div>
<a class="anchor" id="a15a8ac75d8da0e7e47c0643870b3bcc9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::find_max_clause_dlevel </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>
</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__solver_8cpp_source.html#l00447">447</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">CDatabase::_variables</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">CDatabase::clause()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="xchaff__base_8h_source.html#l00052">FLIPPED</a>, <a class="el" href="xchaff__base_8h_source.html#l00183">CClause::literals()</a>, <a class="el" href="xchaff__base_8h_source.html#l00051">NULL_CLAUSE</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#l00916">conflict_analysis_zchaff()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>.</p>
</div>
</div>
<a class="anchor" id="ac06f1192d14de7730356cc102ebaee1b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_var_value </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>var</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>value</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td>
<td class="paramname"><em>ante</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>dl</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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00296">296</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00172">_assignment_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00176">_assignment_hook_cookie</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00100">CDatabase::_variables</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, <a class="el" href="xchaff__utils_8h_source.html#l00043">CHECK_FULL</a>, <a class="el" href="xchaff__base_8h_source.html#l00267">CVariable::dlevel()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00381">dump()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__base_8h_source.html#l00297">CVariable::ht_ptr()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00276">num_free_variables()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00134">CSolverStats::num_implications</a>, <a class="el" href="xchaff__base_8h_source.html#l00293">CVariable::set_antecedence()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00368">set_var_value_not_current_dl()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00321">set_var_value_with_current_dl()</a>, <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>, <a class="el" href="xchaff__base_8h_source.html#l00264">CVariable::value()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00886">verify_integrity()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>.</p>
</div>
</div>
<a class="anchor" id="a4617b5f40d47a1ac33135a76669994a4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_var_value_not_current_dl </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>v</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">vector< <a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * > & </td>
<td class="paramname"><em>neg_ht_clauses</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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00368">368</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00166">_conflicts</a>, <a class="el" href="xchaff__base_8h_source.html#l00111">CLitPoolElement::direction()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="xchaff__base_8h_source.html#l00297">CVariable::ht_ptr()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00239">CDatabase::literal_value()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00345">queue_implication()</a>, <a class="el" href="xchaff__base_8h_source.html#l00095">CLitPoolElement::s_var()</a>, <a class="el" href="xchaff__base_8h_source.html#l00117">CLitPoolElement::unset_ht()</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>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">CDatabase::variable()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00296">set_var_value()</a>.</p>
</div>
</div>
<a class="anchor" id="ac497f97142b2f82acf8f43ba191feb08"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_var_value_with_current_dl </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>v</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">vector< <a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * > & </td>
<td class="paramname"><em>neg_ht_clauses</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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00321">321</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00166">_conflicts</a>, <a class="el" href="xchaff__base_8h_source.html#l00111">CLitPoolElement::direction()</a>, <a class="el" href="xchaff__base_8h_source.html#l00297">CVariable::ht_ptr()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00239">CDatabase::literal_value()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00345">queue_implication()</a>, <a class="el" href="xchaff__base_8h_source.html#l00095">CLitPoolElement::s_var()</a>, <a class="el" href="xchaff__base_8h_source.html#l00117">CLitPoolElement::unset_ht()</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>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">CDatabase::variable()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00296">set_var_value()</a>.</p>
</div>
</div>
<a class="anchor" id="a78ae7136f91966fdc7a55af71060875c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::unset_var_value </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td></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__solver_8cpp_source.html#l00433">433</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00172">_assignment_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00176">_assignment_hook_cookie</a>, <a class="el" href="xchaff__solver_8h_source.html#l00160">_max_score_pos</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__base_8h_source.html#l00051">NULL_CLAUSE</a>, <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">CDatabase::variable()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>.</p>
</div>
</div>
<a class="anchor" id="a0ffdf7d6d085ca70b50391598bf4c543"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::run_periodic_functions </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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00109">109</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00157">_hooks</a>, <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00083">CSolverParameters::allow_clause_deletion</a>, <a class="el" href="xchaff__solver_8h_source.html#l00093">CSolverParameters::allow_restart</a>, <a class="el" href="xchaff__solver_8h_source.html#l00084">CSolverParameters::clause_deletion_interval</a>, <a class="el" href="xchaff__solver_8h_source.html#l00287">current_cpu_time()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00513">delete_unrelevant_clauses()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00097">CSolverParameters::next_restart_backtrack</a>, <a class="el" href="xchaff__solver_8h_source.html#l00094">CSolverParameters::next_restart_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00132">CSolverStats::num_backtracks</a>, <a class="el" href="xchaff__solver_8h_source.html#l00131">CSolverStats::num_decisions</a>, <a class="el" href="xchaff__solver_8h_source.html#l00091">CSolverParameters::randomness</a>, <a class="el" href="xchaff__solver_8h_source.html#l00358">restart()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00098">CSolverParameters::restart_backtrack_incr</a>, <a class="el" href="xchaff__solver_8h_source.html#l00099">CSolverParameters::restart_backtrack_incr_incr</a>, <a class="el" href="xchaff__solver_8h_source.html#l00100">CSolverParameters::restart_randomness</a>, <a class="el" href="xchaff__solver_8h_source.html#l00096">CSolverParameters::restart_time_incr_incr</a>, <a class="el" href="xchaff__solver_8h_source.html#l00095">CSolverParameters::restart_time_increment</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00601">update_var_stats()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00090">CSolverParameters::verbosity</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>.</p>
</div>
</div>
<a class="anchor" id="acc181946a5845c647818631415c22c22"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::update_var_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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00601">601</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00161">_last_var_lits_count</a>, <a class="el" href="xchaff__solver_8h_source.html#l00160">_max_score_pos</a>, <a class="el" href="xchaff__solver_8h_source.html#l00162">_var_order</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00594">compare_var_stat()</a>, <a class="el" href="xchaff__base_8h_source.html#l00276">CVariable::lits_count()</a>, <a class="el" href="xchaff__base_8h_source.html#l00249">CVariable::score()</a>, <a class="el" href="xchaff__base_8h_source.html#l00251">CVariable::var_score_pos()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00123">CDatabase::variable()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8h_source.html#l00358">restart()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00109">run_periodic_functions()</a>.</p>
</div>
</div>
<a class="anchor" id="af3b17269840c1a07e21303c1fca4e5a0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CSolver::time_out </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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00587">587</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00287">current_cpu_time()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00123">CSolverStats::start_cpu_time</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00078">CSolverParameters::time_limit</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a09834f0e5025b7a748bc24bf113b0f9e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::delete_unrelevant_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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__solver_8cpp_source.html#l00513">513</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00093">CDatabase::_stats</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00102">CDatabase::_unused_clause_idx_queue</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, <a class="el" href="xchaff__utils_8h_source.html#l00043">CHECK_FULL</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00120">CDatabase::clauses()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00381">dump()</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__dbase_8h_source.html#l00136">CDatabase::init_num_clauses()</a>, <a class="el" href="xchaff__base_8h_source.html#l00195">CClause::literal()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00239">CDatabase::literal_value()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00221">CDatabase::mark_clause_deleted()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00087">CSolverParameters::max_conflict_clause_length</a>, <a class="el" href="xchaff__solver_8h_source.html#l00085">CSolverParameters::max_unrelevance</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00071">CDatabaseStats::mem_used_up</a>, <a class="el" href="xchaff__solver_8h_source.html#l00086">CSolverParameters::min_num_clause_lits_for_delete</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00140">CDatabase::num_deleted_clauses()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00141">CDatabase::num_deleted_literals()</a>, <a class="el" href="xchaff__base_8h_source.html#l00189">CClause::num_lits()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00109">run_periodic_functions()</a>.</p>
</div>
</div>
<a class="anchor" id="a19c6655c87bd6117db6510183dad2893"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_time_limit </td>
<td>(</td>
<td class="paramtype">float </td>
<td class="paramname"><em>t</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__solver_8h_source.html#l00228">228</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00078">CSolverParameters::time_limit</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00105">Xchaff::SetBudget()</a>.</p>
</div>
</div>
<a class="anchor" id="a069343e0391a7b95510634c9c96bb66f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_mem_limit </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>s</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__solver_8h_source.html#l00230">230</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00132">CDatabase::set_mem_limit()</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00107">Xchaff::SetMemLimit()</a>.</p>
</div>
</div>
<a class="anchor" id="adc4bf726c678250a85fef5a600d5e1d7"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_decision_strategy </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>s</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__solver_8h_source.html#l00233">233</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00080">CSolverParameters::decision_strategy</a>.</p>
</div>
</div>
<a class="anchor" id="a771e7780c8a112317bfd437599e2af22"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_preprocess_strategy </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>s</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__solver_8h_source.html#l00235">235</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00081">CSolverParameters::preprocess_strategy</a>.</p>
</div>
</div>
<a class="anchor" id="ad61a4e50bc8640852b7cd9d2cbd423d0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::enable_cls_deletion </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>allow</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__solver_8h_source.html#l00237">237</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00083">CSolverParameters::allow_clause_deletion</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00115">Xchaff::DisableClauseDeletion()</a>, and <a class="el" href="xchaff_8h_source.html#l00113">Xchaff::EnableClauseDeletion()</a>.</p>
</div>
</div>
<a class="anchor" id="a31f9c112bb7ee8b3b334618d847d3d1f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_cls_del_interval </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__solver_8h_source.html#l00239">239</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00084">CSolverParameters::clause_deletion_interval</a>.</p>
</div>
</div>
<a class="anchor" id="a72cf182c0c2c1dccb61c837765ea56f3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_max_unrelevance </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__solver_8h_source.html#l00241">241</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00085">CSolverParameters::max_unrelevance</a>.</p>
</div>
</div>
<a class="anchor" id="a5778d83eeb8c5ad0d34120c3b472cde9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_min_num_clause_lits_for_delete </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__solver_8h_source.html#l00243">243</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00086">CSolverParameters::min_num_clause_lits_for_delete</a>.</p>
</div>
</div>
<a class="anchor" id="aa3bb06628177a7a003957e00f9584351"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_max_conflict_clause_length </td>
<td>(</td>
<td class="paramtype">int </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__solver_8h_source.html#l00245">245</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00087">CSolverParameters::max_conflict_clause_length</a>.</p>
</div>
</div>
<a class="anchor" id="adcfb8dcb69c2221d25be0cd5ad6c43ff"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_allow_multiple_conflict </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>b</em> = <code>false</code></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__solver_8h_source.html#l00247">247</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00105">CSolverParameters::allow_multiple_conflict</a>.</p>
</div>
</div>
<a class="anchor" id="a9713537c85c12024d85d5b25ab2cb844"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_allow_multiple_conflict_clause </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>b</em> = <code>false</code></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__solver_8h_source.html#l00250">250</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00106">CSolverParameters::allow_multiple_conflict_clause</a>.</p>
</div>
</div>
<a class="anchor" id="a17438ece1aeb9736e73bc25b96def58d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_randomness </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__solver_8h_source.html#l00253">253</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00101">CSolverParameters::base_randomness</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00109">Xchaff::SetRandomness()</a>.</p>
</div>
</div>
<a class="anchor" id="a6765f3784e94ebde4c86447845e67c1d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::set_random_seed </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>seed</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__solver_8h_source.html#l00256">256</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00296">current_world_time()</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00111">Xchaff::SetRandSeed()</a>.</p>
</div>
</div>
<a class="anchor" id="aa0f5bd7cea8ed3bc7254e29d744566fb"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::RegisterDLevelHook </td>
<td>(</td>
<td class="paramtype">void(*)(void *, int) </td>
<td class="paramname"><em>f</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">void * </td>
<td class="paramname"><em>cookie</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__solver_8h_source.html#l00264">264</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00170">_dlevel_hook</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00174">_dlevel_hook_cookie</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00080">Xchaff::RegisterDLevelHook()</a>.</p>
</div>
</div>
<a class="anchor" id="aac7bf85fb8516ff4b3478598306fcb2e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::RegisterDecisionHook </td>
<td>(</td>
<td class="paramtype">int(*)(void *, bool *) </td>
<td class="paramname"><em>f</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">void * </td>
<td class="paramname"><em>cookie</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__solver_8h_source.html#l00266">266</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00171">_decision_hook</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00175">_decision_hook_cookie</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00090">Xchaff::RegisterDecisionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="afcbec396917ed73948a67db3732054ae"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::RegisterAssignmentHook </td>
<td>(</td>
<td class="paramtype">void(*)(void *, int, int) </td>
<td class="paramname"><em>f</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">void * </td>
<td class="paramname"><em>cookie</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__solver_8h_source.html#l00268">268</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00172">_assignment_hook</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00176">_assignment_hook_cookie</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00100">Xchaff::RegisterAssignmentHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a5aeafd67c7a77683ae040c11fbf033b1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::RegisterDeductionHook </td>
<td>(</td>
<td class="paramtype">void(*)(void *) </td>
<td class="paramname"><em>f</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">void * </td>
<td class="paramname"><em>cookie</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__solver_8h_source.html#l00270">270</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00173">_deduction_hook</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00177">_deduction_hook_cookie</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00103">Xchaff::RegisterDeductionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="af7b4ed5bb5be8b7c56e4aa5f1913979b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::outcome </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__solver_8h_source.html#l00274">274</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00119">CSolverStats::outcome</a>.</p>
</div>
</div>
<a class="anchor" id="a1d592aab62ad4f2943e0687916a34397"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::num_decisions </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__solver_8h_source.html#l00275">275</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00131">CSolverStats::num_decisions</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00121">Xchaff::GetNumDecisions()</a>.</p>
</div>
</div>
<a class="anchor" id="a5b1c1a111284ece5745488b12baef8b2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int& CSolver::num_free_variables </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__solver_8h_source.html#l00276">276</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00135">CSolverStats::num_free_variables</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">preprocess()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00296">set_var_value()</a>.</p>
</div>
</div>
<a class="anchor" id="a881e379b28047fde2157720bf4ee9fd0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::max_dlevel </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__solver_8h_source.html#l00279">279</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00133">CSolverStats::max_dlevel</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, and <a class="el" href="xchaff_8h_source.html#l00139">Xchaff::GetMaxDLevel()</a>.</p>
</div>
</div>
<a class="anchor" id="ac1c4a48d4db9e61bc657a633b7230b88"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::num_implications </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__solver_8h_source.html#l00280">280</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00134">CSolverStats::num_implications</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00137">Xchaff::GetNumImplications()</a>.</p>
</div>
</div>
<a class="anchor" id="ae8d515c8e764ad65b870d5703b51c847"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">long CSolver::total_bubble_move </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__solver_8h_source.html#l00281">281</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00129">CSolverStats::total_bubble_move</a>.</p>
</div>
</div>
<a class="anchor" id="a1153002750347545ac8b25d08ea96e39"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const char* CSolver::version </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__solver_8h_source.html#l00283">283</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
</div>
</div>
<a class="anchor" id="a7d23251aefbab59adac9658723ac60ad"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::current_cpu_time </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__solver_8h_source.html#l00287">287</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00822">continueCheck()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00303">elapsed_cpu_time()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00142">init()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00109">run_periodic_functions()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00804">solve()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00587">time_out()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00310">total_run_time()</a>.</p>
</div>
</div>
<a class="anchor" id="a4fc755c9adedc2769461bacfc8532f9e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::current_world_time </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__solver_8h_source.html#l00296">296</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00822">continueCheck()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00142">init()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00256">set_random_seed()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00804">solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a66d960cb2bd8f5642afe1bf581d64f97"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">float CSolver::elapsed_cpu_time </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__solver_8h_source.html#l00303">303</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00287">current_cpu_time()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00124">CSolverStats::last_cpu_time</a>.</p>
</div>
</div>
<a class="anchor" id="afde50f1cee0bab34e2464b17693d59f7"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">float CSolver::total_run_time </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__solver_8h_source.html#l00310">310</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00287">current_cpu_time()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00118">CSolverStats::is_solver_started</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00123">CSolverStats::start_cpu_time</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00117">Xchaff::GetBudgetUsed()</a>, and <a class="el" href="xchaff_8h_source.html#l00127">Xchaff::GetTotalTime()</a>.</p>
</div>
</div>
<a class="anchor" id="ace35bd2316cbf7b72d942c7a672374e3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">float CSolver::cpu_run_time </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__solver_8h_source.html#l00316">316</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00125">CSolverStats::finish_cpu_time</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00123">CSolverStats::start_cpu_time</a>.</p>
</div>
</div>
<a class="anchor" id="aa181acac744c04062df328ee5eac38f9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">float CSolver::world_run_time </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__solver_8h_source.html#l00321">321</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00127">CSolverStats::finish_world_time</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00126">CSolverStats::start_world_time</a>.</p>
</div>
</div>
<a class="anchor" id="a6a7cefe78a6f785c2c51950a74dde6d8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::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__solver_8h_source.html#l00326">326</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8h_source.html#l00172">CDatabase::estimate_mem_usage()</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00119">Xchaff::GetMemUsed()</a>.</p>
</div>
</div>
<a class="anchor" id="af5b9bcac3d3bf0530bc36285ce8cc7f6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::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__solver_8h_source.html#l00329">329</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00152">_assignment_stack</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00133">CSolverStats::max_dlevel</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00188">CDatabase::mem_usage()</a>.</p>
</div>
</div>
<a class="anchor" id="ad51e4ee566b488f8d3610890f3fa1bb7"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int& CSolver::dlevel </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__solver_8h_source.html#l00337">337</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00151">_dlevel</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">add_clause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00043">CSolver()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00463">dump_assignment_stack()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00447">find_max_clause_dlevel()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00890">mark_vars_at_level()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00358">restart()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00296">set_var_value()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00368">set_var_value_not_current_dl()</a>.</p>
</div>
</div>
<a class="anchor" id="ade3fe6d285fbae6d71d09051e0e4637b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::add_hook </td>
<td>(</td>
<td class="paramtype"><a class="el" href="xchaff__solver_8h.html#a4288f2865a52bcea1f6cd0afa93a7898">HookFunPtrT</a> </td>
<td class="paramname"><em>fun</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>interval</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__solver_8h_source.html#l00340">340</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00157">_hooks</a>.</p>
</div>
</div>
<a class="anchor" id="a21e170987f92adbe179f39ffe3c861be"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::queue_implication </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>lit</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td>
<td class="paramname"><em>ante_clause</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__solver_8h_source.html#l00345">345</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00153">_implication_queue</a>, <a class="el" href="xchaff__utils_8h_source.html#l00042">CHECK</a>, and <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">add_clause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">preprocess()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00368">set_var_value_not_current_dl()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00321">set_var_value_with_current_dl()</a>.</p>
</div>
</div>
<a class="anchor" id="a1b1f7e9d95712bd0852366c044a5829f"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CSolver::add_variables </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>new_vars</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#l00160">160</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00152">_assignment_stack</a>, <a class="el" href="xchaff__solver_8h_source.html#l00161">_last_var_lits_count</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00162">_var_order</a>, <a class="el" href="xchaff__solver_8h_source.html#l00118">CSolverStats::is_solver_started</a>, <a class="el" href="xchaff__solver_8h_source.html#l00135">CSolverStats::num_free_variables</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00038">Xchaff::AddVariables()</a>.</p>
</div>
</div>
<a class="anchor" id="a5f90fcc1b1a7994a94fc8395d95cfb38"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> CSolver::add_clause </td>
<td>(</td>
<td class="paramtype">vector< long > & </td>
<td class="paramname"><em>lits</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>addConflicts</em> = <code>true</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__solver_8cpp_source.html#l00179">179</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00180">_addedUnitClauses</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00101">CDatabase::_clauses</a>, <a class="el" href="xchaff__solver_8h_source.html#l00166">_conflicts</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00093">CDatabase::_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00102">CDatabase::_unused_clause_idx_queue</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">CDatabase::clause()</a>, <a class="el" href="xchaff__base_8h_source.html#l00267">CVariable::dlevel()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">CDatabase::enlarge_lit_pool()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00497">CDatabase::find_unit_literal()</a>, <a class="el" href="xchaff__base_8h_source.html#l00297">CVariable::ht_ptr()</a>, <a class="el" href="xchaff__base_8h_source.html#l00177">CClause::init()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00479">CDatabase::is_conflict()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00118">CSolverStats::is_solver_started</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00147">CDatabase::lit_pool_end()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00158">CDatabase::lit_pool_free_space()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00150">CDatabase::lit_pool_push_back()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00239">CDatabase::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#l00276">CVariable::lits_count()</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__base_8h_source.html#l00189">CClause::num_lits()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00345">queue_implication()</a>, <a class="el" href="xchaff__base_8h_source.html#l00120">CLitPoolElement::set_ht()</a>, <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</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">CDatabase::variable()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00057">Xchaff::AddClause()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>.</p>
</div>
</div>
<a class="anchor" id="ac14b7728d00ff497795bcedfd3f24faa"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CSolver::verify_integrity </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__solver_8cpp_source.html#l00886">886</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00296">set_var_value()</a>.</p>
</div>
</div>
<a class="anchor" id="a5b9ce0b016266150cad691e4bb475668"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::restart </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__solver_8h_source.html#l00358">358</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00161">_last_var_lits_count</a>, <a class="el" href="xchaff__solver_8h_source.html#l00154">_params</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__base_8h_source.html#l00249">CVariable::score()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00601">update_var_stats()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00123">CDatabase::variable()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00117">CDatabase::variables()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00090">CSolverParameters::verbosity</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00109">run_periodic_functions()</a>.</p>
</div>
</div>
<a class="anchor" id="a351fe372330bede0ada8c3723e844a8e"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CSolver::solve </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>allowNewClauses</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#l00804">804</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00170">_dlevel_hook</a>, <a class="el" href="xchaff__solver_8h_source.html#l00174">_dlevel_hook_cookie</a>, <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00063">CONFLICT</a>, <a class="el" href="xchaff__solver_8h_source.html#l00287">current_cpu_time()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00296">current_world_time()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00125">CSolverStats::finish_cpu_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00127">CSolverStats::finish_world_time</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00142">init()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00119">CSolverStats::outcome</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">preprocess()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00054">UNSATISFIABLE</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8cpp_source.html#l00043">Xchaff::Satisfiable()</a>.</p>
</div>
</div>
<a class="anchor" id="a9119faa6145fead463e8b14ec2f7cf7b"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CSolver::continueCheck </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__solver_8cpp_source.html#l00822">822</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00155">_stats</a>, <a class="el" href="xchaff__solver_8h_source.html#l00287">current_cpu_time()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00296">current_world_time()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00125">CSolverStats::finish_cpu_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00127">CSolverStats::finish_world_time</a>, <a class="el" href="xchaff__solver_8h_source.html#l00119">CSolverStats::outcome</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8cpp_source.html#l00057">Xchaff::Continue()</a>.</p>
</div>
</div>
<a class="anchor" id="a60c64d82a19286ac5774adce294aa16a"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CSolver::dump_assignment_stack </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__solver_8cpp_source.html#l00463">463</a> of file <a class="el" href="xchaff__solver_8cpp_source.html">xchaff_solver.cpp</a>.</p>
<p>References <a class="el" href="xchaff__solver_8h_source.html#l00152">_assignment_stack</a>, <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="xchaff__base_8h_source.html#l00052">FLIPPED</a>, <a class="el" href="xchaff__base_8h_source.html#l00290">CVariable::get_antecedence()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">CDatabase::variable()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00381">dump()</a>.</p>
</div>
</div>
<a class="anchor" id="adf342158bf2d06241a075a8c22a1ee73"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CSolver::output_current_stats </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
</div>
</div>
<a class="anchor" id="a8804888a9795945f5b09c67c529b898d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CSolver::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>
</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__solver_8h_source.html#l00381">381</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>References <a class="el" href="xchaff__dbase_8cpp_source.html#l00197">CDatabase::dump()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00463">dump_assignment_stack()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00513">delete_unrelevant_clauses()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00142">init()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00296">set_var_value()</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="a65a9481261bf9d9d90ff36de99992094"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::_dlevel</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__solver_8h_source.html#l00151">151</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00043">CSolver()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00337">dlevel()</a>.</p>
</div>
</div>
<a class="anchor" id="a6a21ab9d2ab20a5c4f103cc1a337e35f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">vector<vector<int> *> CSolver::_assignment_stack</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__solver_8h_source.html#l00152">152</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00160">add_variables()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00463">dump_assignment_stack()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00142">init()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00329">mem_usage()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00101">~CSolver()</a>.</p>
</div>
</div>
<a class="anchor" id="aeab7cd8f6085990a2a1ed518c9d75c6e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">queue<pair<int,<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a>> > CSolver::_implication_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__solver_8h_source.html#l00153">153</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00345">queue_implication()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a30e5a80e5be76e6be4398340f3925818"></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="structCSolverParameters.html">CSolverParameters</a> CSolver::_params</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__solver_8h_source.html#l00154">154</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00043">CSolver()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00513">delete_unrelevant_clauses()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00237">enable_cls_deletion()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">preprocess()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00358">restart()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00109">run_periodic_functions()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00247">set_allow_multiple_conflict()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00250">set_allow_multiple_conflict_clause()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00239">set_cls_del_interval()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00233">set_decision_strategy()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00245">set_max_conflict_clause_length()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00241">set_max_unrelevance()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00243">set_min_num_clause_lits_for_delete()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00235">set_preprocess_strategy()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00253">set_randomness()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00228">set_time_limit()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00587">time_out()</a>.</p>
</div>
</div>
<a class="anchor" id="a5f656ea799ff4b4304b9f4f71a4df315"></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="structCSolverStats.html">CSolverStats</a> CSolver::_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__solver_8h_source.html#l00155">155</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">add_clause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00160">add_variables()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00822">continueCheck()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00316">cpu_run_time()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00043">CSolver()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00303">elapsed_cpu_time()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00142">init()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00279">max_dlevel()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00329">mem_usage()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00275">num_decisions()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00276">num_free_variables()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00280">num_implications()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00274">outcome()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00109">run_periodic_functions()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00296">set_var_value()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00804">solve()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00587">time_out()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00281">total_bubble_move()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00310">total_run_time()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00321">world_run_time()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00101">~CSolver()</a>.</p>
</div>
</div>
<a class="anchor" id="a49509a796f28911569176b2cc6d4a0a0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">vector<pair<int,pair< <a class="el" href="xchaff__solver_8h.html#a4288f2865a52bcea1f6cd0afa93a7898">HookFunPtrT</a>, int> > > CSolver::_hooks</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__solver_8h_source.html#l00157">157</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8h_source.html#l00340">add_hook()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00109">run_periodic_functions()</a>.</p>
</div>
</div>
<a class="anchor" id="ae7e25a4d85f75c17d55cf64e26056920"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::_max_score_pos</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__solver_8h_source.html#l00160">160</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00433">unset_var_value()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00601">update_var_stats()</a>.</p>
</div>
</div>
<a class="anchor" id="aec6d0a9cf59ad2da0dad717bea16efcb"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">vector<int> CSolver::_last_var_lits_count[2]</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__solver_8h_source.html#l00161">161</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00160">add_variables()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00142">init()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00358">restart()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00601">update_var_stats()</a>.</p>
</div>
</div>
<a class="anchor" id="a40c08e5478f016f460d6adec977c2446"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">vector<pair<int,int> > CSolver::_var_order</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__solver_8h_source.html#l00162">162</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00160">add_variables()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00142">init()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00601">update_var_stats()</a>.</p>
</div>
</div>
<a class="anchor" id="a528d66d18534a7d6e73a2e7964103b1c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CSolver::_num_marked</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__solver_8h_source.html#l00165">165</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00043">CSolver()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00890">mark_vars_at_level()</a>.</p>
</div>
</div>
<a class="anchor" id="a6bba00c21025040cc46a0499eaea7f01"></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="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a>> CSolver::_conflicts</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__solver_8h_source.html#l00166">166</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">add_clause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00368">set_var_value_not_current_dl()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00321">set_var_value_with_current_dl()</a>.</p>
</div>
</div>
<a class="anchor" id="ab162797183d22466c24feb117fefc7d6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">vector<long> CSolver::_conflict_lits</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__solver_8h_source.html#l00167">167</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">conflict_analysis_zchaff()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00890">mark_vars_at_level()</a>.</p>
</div>
</div>
<a class="anchor" id="ad517659e82e1b42617886d2b6758acd3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void(* CSolver::_dlevel_hook)(void *, int)</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__solver_8h_source.html#l00170">170</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00043">CSolver()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00264">RegisterDLevelHook()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00804">solve()</a>.</p>
</div>
</div>
<a class="anchor" id="af74159b82e953b3b766001d27b8b7981"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int(* CSolver::_decision_hook)(void *, bool *)</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__solver_8h_source.html#l00171">171</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00043">CSolver()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00266">RegisterDecisionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a66cffc281bb01002d1b30e01f6e90a28"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void(* CSolver::_assignment_hook)(void *, int, int)</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__solver_8h_source.html#l00172">172</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00043">CSolver()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00268">RegisterAssignmentHook()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00296">set_var_value()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00433">unset_var_value()</a>.</p>
</div>
</div>
<a class="anchor" id="ac30b332eb58a51d87d9e1f80f62754f8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void(* CSolver::_deduction_hook)(void *)</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__solver_8h_source.html#l00173">173</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00043">CSolver()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00270">RegisterDeductionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="ad1e4bd711ad507a40d36d5815bdaa69c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void* CSolver::_dlevel_hook_cookie</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__solver_8h_source.html#l00174">174</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00830">back_track()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00264">RegisterDLevelHook()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00804">solve()</a>.</p>
</div>
</div>
<a class="anchor" id="a2a02aeed8e6eefe8b1d8a661c7e94c45"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void* CSolver::_decision_hook_cookie</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__solver_8h_source.html#l00175">175</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00617">decide_next_branch()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00266">RegisterDecisionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a0de6dbd6e4d7f30c4ee841f15b8ae5e4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void* CSolver::_assignment_hook_cookie</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__solver_8h_source.html#l00176">176</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8h_source.html#l00268">RegisterAssignmentHook()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00296">set_var_value()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00433">unset_var_value()</a>.</p>
</div>
</div>
<a class="anchor" id="aa2c250ed33c494f50d06122943ae280d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void* CSolver::_deduction_hook_cookie</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__solver_8h_source.html#l00177">177</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00852">deduce()</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00270">RegisterDeductionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a6b12fb5fcb0e279221c4047b3a61d99e"></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="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a>> CSolver::_addedUnitClauses</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__solver_8h_source.html#l00180">180</a> of file <a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">add_clause()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00763">real_solve()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</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>
