<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: CSolver Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pro-methods">Protected Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> </div>
<div class="headertitle">
<div class="title">CSolver Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CSolver" --><!-- doxytag: inherits="CDatabase" -->
<p><code>#include <<a class="el" href="xchaff__solver_8h_source.html">xchaff_solver.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CSolver:</div>
<div class="dyncontent">
<div class="center">
<img src="classCSolver.png" usemap="#CSolver_map" alt=""/>
<map id="CSolver_map" name="CSolver_map">
<area href="classCDatabase.html" alt="CDatabase" shape="rect" coords="0,0,74,24"/>
</map>
</div></div>
<p><a href="classCSolver-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCSolver.html#afa1c51e0570e7a835fae6ba187f9d09b">CSolver</a> ()
<li><a class="el" href="classCSolver.html#af3c9bd8a7dede30ca60e24bf30073206">~CSolver</a> ()
<li>void <a class="el" href="classCSolver.html#a19c6655c87bd6117db6510183dad2893">set_time_limit</a> (float t)
<li>void <a class="el" href="classCSolver.html#a069343e0391a7b95510634c9c96bb66f">set_mem_limit</a> (int s)
<li>void <a class="el" href="classCSolver.html#adc4bf726c678250a85fef5a600d5e1d7">set_decision_strategy</a> (int s)
<li>void <a class="el" href="classCSolver.html#a771e7780c8a112317bfd437599e2af22">set_preprocess_strategy</a> (int s)
<li>void <a class="el" href="classCSolver.html#ad61a4e50bc8640852b7cd9d2cbd423d0">enable_cls_deletion</a> (bool allow)
<li>void <a class="el" href="classCSolver.html#a31f9c112bb7ee8b3b334618d847d3d1f">set_cls_del_interval</a> (int n)
<li>void <a class="el" href="classCSolver.html#a72cf182c0c2c1dccb61c837765ea56f3">set_max_unrelevance</a> (int n)
<li>void <a class="el" href="classCSolver.html#a5778d83eeb8c5ad0d34120c3b472cde9">set_min_num_clause_lits_for_delete</a> (int n)
<li>void <a class="el" href="classCSolver.html#aa3bb06628177a7a003957e00f9584351">set_max_conflict_clause_length</a> (int l)
<li>void <a class="el" href="classCSolver.html#adcfb8dcb69c2221d25be0cd5ad6c43ff">set_allow_multiple_conflict</a> (bool b=false)
<li>void <a class="el" href="classCSolver.html#a9713537c85c12024d85d5b25ab2cb844">set_allow_multiple_conflict_clause</a> (bool b=false)
<li>void <a class="el" href="classCSolver.html#a17438ece1aeb9736e73bc25b96def58d">set_randomness</a> (int n)
<li>void <a class="el" href="classCSolver.html#a6765f3784e94ebde4c86447845e67c1d">set_random_seed</a> (int seed)
<li>void <a class="el" href="classCSolver.html#aa0f5bd7cea8ed3bc7254e29d744566fb">RegisterDLevelHook</a> (void(*f)(void *, int), void *cookie)
<li>void <a class="el" href="classCSolver.html#aac7bf85fb8516ff4b3478598306fcb2e">RegisterDecisionHook</a> (int(*f)(void *, bool *), void *cookie)
<li>void <a class="el" href="classCSolver.html#afcbec396917ed73948a67db3732054ae">RegisterAssignmentHook</a> (void(*f)(void *, int, int), void *cookie)
<li>void <a class="el" href="classCSolver.html#a5aeafd67c7a77683ae040c11fbf033b1">RegisterDeductionHook</a> (void(*f)(void *), void *cookie)
<li>int <a class="el" href="classCSolver.html#af7b4ed5bb5be8b7c56e4aa5f1913979b">outcome</a> ()
<li>int <a class="el" href="classCSolver.html#a1d592aab62ad4f2943e0687916a34397">num_decisions</a> ()
<li>int & <a class="el" href="classCSolver.html#a5b1c1a111284ece5745488b12baef8b2">num_free_variables</a> ()
<li>int <a class="el" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">max_dlevel</a> ()
<li>int <a class="el" href="classCSolver.html#ac1c4a48d4db9e61bc657a633b7230b88">num_implications</a> ()
<li>long <a class="el" href="classCSolver.html#ae8d515c8e764ad65b870d5703b51c847">total_bubble_move</a> (void)
<li>const char * <a class="el" href="classCSolver.html#a1153002750347545ac8b25d08ea96e39">version</a> (void)
<li>int <a class="el" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a> (void)
<li>int <a class="el" href="classCSolver.html#a4fc755c9adedc2769461bacfc8532f9e">current_world_time</a> (void)
<li>float <a class="el" href="classCSolver.html#a66d960cb2bd8f5642afe1bf581d64f97">elapsed_cpu_time</a> ()
<li>float <a class="el" href="classCSolver.html#afde50f1cee0bab34e2464b17693d59f7">total_run_time</a> ()
<li>float <a class="el" href="classCSolver.html#ace35bd2316cbf7b72d942c7a672374e3">cpu_run_time</a> ()
<li>float <a class="el" href="classCSolver.html#aa181acac744c04062df328ee5eac38f9">world_run_time</a> ()
<li>int <a class="el" href="classCSolver.html#a6a7cefe78a6f785c2c51950a74dde6d8">estimate_mem_usage</a> ()
<li>int <a class="el" href="classCSolver.html#af5b9bcac3d3bf0530bc36285ce8cc7f6">mem_usage</a> (void)
<li>int & <a class="el" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a> ()
<li>void <a class="el" href="classCSolver.html#ade3fe6d285fbae6d71d09051e0e4637b">add_hook</a> (<a class="el" href="xchaff__solver_8h.html#a4288f2865a52bcea1f6cd0afa93a7898">HookFunPtrT</a> fun, int interval)
<li>void <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)
<li>int <a class="el" href="classCSolver.html#a1b1f7e9d95712bd0852366c044a5829f">add_variables</a> (int new_vars)
<li><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> <a class="el" href="classCSolver.html#a5f90fcc1b1a7994a94fc8395d95cfb38">add_clause</a> (vector< long > &lits, bool addConflicts=true)
<li>void <a class="el" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">verify_integrity</a> (void)
<li>void <a class="el" href="classCSolver.html#a5b9ce0b016266150cad691e4bb475668">restart</a> (void)
<li>int <a class="el" href="classCSolver.html#a351fe372330bede0ada8c3723e844a8e">solve</a> (bool allowNewClauses)
<li>int <a class="el" href="classCSolver.html#a9119faa6145fead463e8b14ec2f7cf7b">continueCheck</a> ()
<li>void <a class="el" href="classCSolver.html#a60c64d82a19286ac5774adce294aa16a">dump_assignment_stack</a> (ostream &os=cout)
<li>void <a class="el" href="classCSolver.html#adf342158bf2d06241a075a8c22a1ee73">output_current_stats</a> (void)
<li>void <a class="el" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">dump</a> (ostream &os=cout)
</ul>
<h2><a name="pro-methods"></a>
Protected Member Functions</h2>
<ul>
<li>void <a class="el" href="classCSolver.html#af5c60a4d643467e199c00415fedc7e1d">real_solve</a> (void)
<li>int <a class="el" href="classCSolver.html#aef7418705a19f94876ab5c708e87e15c">preprocess</a> (bool allowNewClauses)
<li>int <a class="el" href="classCSolver.html#a769075f3a6ed6eab6e4ec9e93c964f89">deduce</a> (void)
<li>bool <a class="el" href="classCSolver.html#a752f7912bef54fb9f310cbeeabc34543">decide_next_branch</a> (void)
<li>int <a class="el" href="classCSolver.html#a2d476175cdda3b0028fb0efd754630d6">analyze_conflicts</a> (void)
<li>int <a class="el" href="classCSolver.html#a3bc2008b3318b4796cf2cd34fa446dee">conflict_analysis_grasp</a> (void)
<li>int <a class="el" href="classCSolver.html#a9329cbfb2ba31fe55352644822889242">conflict_analysis_zchaff</a> (void)
<li>void <a class="el" href="classCSolver.html#a48ffc1b95c078bcc0bb748f1068479fd">back_track</a> (int level)
<li>void <a class="el" href="classCSolver.html#a711b6b701409a5a5fa54dd54b609328b">init</a> (void)
<li>void <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)
<li>int <a class="el" href="classCSolver.html#a15a8ac75d8da0e7e47c0643870b3bcc9">find_max_clause_dlevel</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)
<li>void <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)
<li>void <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)
<li>void <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)
<li>void <a class="el" href="classCSolver.html#a78ae7136f91966fdc7a55af71060875c">unset_var_value</a> (int var)
<li>void <a class="el" href="classCSolver.html#a0ffdf7d6d085ca70b50391598bf4c543">run_periodic_functions</a> (void)
<li>void <a class="el" href="classCSolver.html#acc181946a5845c647818631415c22c22">update_var_stats</a> (void)
<li>bool <a class="el" href="classCSolver.html#af3b17269840c1a07e21303c1fca4e5a0">time_out</a> (void)
<li>void <a class="el" href="classCSolver.html#a09834f0e5025b7a748bc24bf113b0f9e">delete_unrelevant_clauses</a> (void)
</ul>
<h2><a name="pro-attribs"></a>
Protected Attributes</h2>
<ul>
<li>int <a class="el" href="classCSolver.html#a65a9481261bf9d9d90ff36de99992094">_dlevel</a>
<li>vector< vector< int > * > <a class="el" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>
<li>queue< pair< int, <a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> > > <a class="el" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>
<li><a class="el" href="structCSolverParameters.html">CSolverParameters</a> <a class="el" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>
<li><a class="el" href="structCSolverStats.html">CSolverStats</a> <a class="el" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>
<li>vector< pair< int, pair<br class="typebreak"/>
< <a class="el" href="xchaff__solver_8h.html#a4288f2865a52bcea1f6cd0afa93a7898">HookFunPtrT</a>, int > > > <a class="el" href="classCSolver.html#a49509a796f28911569176b2cc6d4a0a0">_hooks</a>
<li>int <a class="el" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">_max_score_pos</a>
<li>vector< int > <a class="el" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a> [2]
<li>vector< pair< int, int > > <a class="el" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>
<li>int <a class="el" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">_num_marked</a>
<li>vector< <a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> > <a class="el" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>
<li>vector< long > <a class="el" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>
<li>void(* <a class="el" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">_dlevel_hook</a> )(void *, int)
<li>int(* <a class="el" href="classCSolver.html#af74159b82e953b3b766001d27b8b7981">_decision_hook</a> )(void *, bool *)
<li>void(* <a class="el" href="classCSolver.html#a66cffc281bb01002d1b30e01f6e90a28">_assignment_hook</a> )(void *, int, int)
<li>void(* <a class="el" href="classCSolver.html#ac30b332eb58a51d87d9e1f80f62754f8">_deduction_hook</a> )(void *)
<li>void * <a class="el" href="classCSolver.html#ad1e4bd711ad507a40d36d5815bdaa69c">_dlevel_hook_cookie</a>
<li>void * <a class="el" href="classCSolver.html#a2a02aeed8e6eefe8b1d8a661c7e94c45">_decision_hook_cookie</a>
<li>void * <a class="el" href="classCSolver.html#a0de6dbd6e4d7f30c4ee841f15b8ae5e4">_assignment_hook_cookie</a>
<li>void * <a class="el" href="classCSolver.html#aa2c250ed33c494f50d06122943ae280d">_deduction_hook_cookie</a>
<li>vector< <a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> > <a class="el" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">_addedUnitClauses</a>
</ul>
<hr/><a name="details" id="details"></a><h2>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><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="afa1c51e0570e7a835fae6ba187f9d09b"></a><!-- doxytag: member="CSolver::CSolver" ref="afa1c51e0570e7a835fae6ba187f9d09b" args="()" -->
<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><!-- doxytag: member="CSolver::~CSolver" ref="af3c9bd8a7dede30ca60e24bf30073206" args="()" -->
<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>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="af5c60a4d643467e199c00415fedc7e1d"></a><!-- doxytag: member="CSolver::real_solve" ref="af5c60a4d643467e199c00415fedc7e1d" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::preprocess" ref="aef7418705a19f94876ab5c708e87e15c" args="(bool allowNewClauses)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::deduce" ref="a769075f3a6ed6eab6e4ec9e93c964f89" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::decide_next_branch" ref="a752f7912bef54fb9f310cbeeabc34543" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::analyze_conflicts" ref="a2d476175cdda3b0028fb0efd754630d6" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::conflict_analysis_grasp" ref="a3bc2008b3318b4796cf2cd34fa446dee" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="a9329cbfb2ba31fe55352644822889242"></a><!-- doxytag: member="CSolver::conflict_analysis_zchaff" ref="a9329cbfb2ba31fe55352644822889242" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::back_track" ref="a48ffc1b95c078bcc0bb748f1068479fd" args="(int level)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::init" ref="a711b6b701409a5a5fa54dd54b609328b" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classCDatabase.html#a8bac062c6bcaf5e92160fd0eff63bcd2">CDatabase</a>.</p>
<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__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><!-- doxytag: member="CSolver::mark_vars_at_level" ref="a525a84f821d273c9883a407c585b8b0d" args="(ClauseIdx cl, int var_idx, int dl)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::find_max_clause_dlevel" ref="a15a8ac75d8da0e7e47c0643870b3bcc9" args="(ClauseIdx cl)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::set_var_value" ref="ac06f1192d14de7730356cc102ebaee1b" args="(int var, int value, ClauseIdx ante, int dl)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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__solver_8h_source.html#l00337">dlevel()</a>, <a class="el" href="xchaff__base_8h_source.html#l00267">CVariable::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><!-- doxytag: member="CSolver::set_var_value_not_current_dl" ref="a4617b5f40d47a1ac33135a76669994a4" args="(int v, vector< CLitPoolElement * > &neg_ht_clauses)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::set_var_value_with_current_dl" ref="ac497f97142b2f82acf8f43ba191feb08" args="(int v, vector< CLitPoolElement * > &neg_ht_clauses)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::unset_var_value" ref="a78ae7136f91966fdc7a55af71060875c" args="(int var)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::run_periodic_functions" ref="a0ffdf7d6d085ca70b50391598bf4c543" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::update_var_stats" ref="acc181946a5845c647818631415c22c22" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::time_out" ref="af3b17269840c1a07e21303c1fca4e5a0" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::delete_unrelevant_clauses" ref="a09834f0e5025b7a748bc24bf113b0f9e" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [protected]</code></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><!-- doxytag: member="CSolver::set_time_limit" ref="a19c6655c87bd6117db6510183dad2893" args="(float t)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::set_mem_limit" ref="a069343e0391a7b95510634c9c96bb66f" args="(int s)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classCDatabase.html#adfda0cf04a767a89cc9ac7dbeb7a11ce">CDatabase</a>.</p>
<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>Referenced by <a class="el" href="xchaff_8h_source.html#l00107">Xchaff::SetMemLimit()</a>.</p>
</div>
</div>
<a class="anchor" id="adc4bf726c678250a85fef5a600d5e1d7"></a><!-- doxytag: member="CSolver::set_decision_strategy" ref="adc4bf726c678250a85fef5a600d5e1d7" args="(int s)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::set_preprocess_strategy" ref="a771e7780c8a112317bfd437599e2af22" args="(int s)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::enable_cls_deletion" ref="ad61a4e50bc8640852b7cd9d2cbd423d0" args="(bool allow)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::set_cls_del_interval" ref="a31f9c112bb7ee8b3b334618d847d3d1f" args="(int n)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::set_max_unrelevance" ref="a72cf182c0c2c1dccb61c837765ea56f3" args="(int n)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::set_min_num_clause_lits_for_delete" ref="a5778d83eeb8c5ad0d34120c3b472cde9" args="(int n)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::set_max_conflict_clause_length" ref="aa3bb06628177a7a003957e00f9584351" args="(int l)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::set_allow_multiple_conflict" ref="adcfb8dcb69c2221d25be0cd5ad6c43ff" args="(bool b=false)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::set_allow_multiple_conflict_clause" ref="a9713537c85c12024d85d5b25ab2cb844" args="(bool b=false)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::set_randomness" ref="a17438ece1aeb9736e73bc25b96def58d" args="(int n)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::set_random_seed" ref="a6765f3784e94ebde4c86447845e67c1d" args="(int seed)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::RegisterDLevelHook" ref="aa0f5bd7cea8ed3bc7254e29d744566fb" args="(void(*f)(void *, int), void *cookie)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::RegisterDecisionHook" ref="aac7bf85fb8516ff4b3478598306fcb2e" args="(int(*f)(void *, bool *), void *cookie)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::RegisterAssignmentHook" ref="afcbec396917ed73948a67db3732054ae" args="(void(*f)(void *, int, int), void *cookie)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::RegisterDeductionHook" ref="a5aeafd67c7a77683ae040c11fbf033b1" args="(void(*f)(void *), void *cookie)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::outcome" ref="af7b4ed5bb5be8b7c56e4aa5f1913979b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CSolver::outcome </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__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><!-- doxytag: member="CSolver::num_decisions" ref="a1d592aab62ad4f2943e0687916a34397" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CSolver::num_decisions </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__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><!-- doxytag: member="CSolver::num_free_variables" ref="a5b1c1a111284ece5745488b12baef8b2" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CSolver::num_free_variables </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__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><!-- doxytag: member="CSolver::max_dlevel" ref="a881e379b28047fde2157720bf4ee9fd0" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CSolver::max_dlevel </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__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><!-- doxytag: member="CSolver::num_implications" ref="ac1c4a48d4db9e61bc657a633b7230b88" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CSolver::num_implications </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__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><!-- doxytag: member="CSolver::total_bubble_move" ref="ae8d515c8e764ad65b870d5703b51c847" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::version" ref="a1153002750347545ac8b25d08ea96e39" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::current_cpu_time" ref="a7d23251aefbab59adac9658723ac60ad" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::current_world_time" ref="a4fc755c9adedc2769461bacfc8532f9e" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::elapsed_cpu_time" ref="a66d960cb2bd8f5642afe1bf581d64f97" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">float CSolver::elapsed_cpu_time </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__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><!-- doxytag: member="CSolver::total_run_time" ref="afde50f1cee0bab34e2464b17693d59f7" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">float CSolver::total_run_time </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__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><!-- doxytag: member="CSolver::cpu_run_time" ref="ace35bd2316cbf7b72d942c7a672374e3" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">float CSolver::cpu_run_time </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__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><!-- doxytag: member="CSolver::world_run_time" ref="aa181acac744c04062df328ee5eac38f9" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">float CSolver::world_run_time </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__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><!-- doxytag: member="CSolver::estimate_mem_usage" ref="a6a7cefe78a6f785c2c51950a74dde6d8" args="()" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classCDatabase.html#a358ccda3851e0469ef0f2a6f3cf55726">CDatabase</a>.</p>
<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>Referenced by <a class="el" href="xchaff_8h_source.html#l00119">Xchaff::GetMemUsed()</a>.</p>
</div>
</div>
<a class="anchor" id="af5b9bcac3d3bf0530bc36285ce8cc7f6"></a><!-- doxytag: member="CSolver::mem_usage" ref="af5b9bcac3d3bf0530bc36285ce8cc7f6" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classCDatabase.html#a1758bead04486434d17201a4bc9e6e40">CDatabase</a>.</p>
<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>, and <a class="el" href="xchaff__solver_8h_source.html#l00133">CSolverStats::max_dlevel</a>.</p>
</div>
</div>
<a class="anchor" id="ad51e4ee566b488f8d3610890f3fa1bb7"></a><!-- doxytag: member="CSolver::dlevel" ref="ad51e4ee566b488f8d3610890f3fa1bb7" args="()" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::add_hook" ref="ade3fe6d285fbae6d71d09051e0e4637b" args="(HookFunPtrT fun, int interval)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::queue_implication" ref="a21e170987f92adbe179f39ffe3c861be" args="(int lit, ClauseIdx ante_clause)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::add_variables" ref="a1b1f7e9d95712bd0852366c044a5829f" args="(int new_vars)" -->
<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><!-- doxytag: member="CSolver::add_clause" ref="a5f90fcc1b1a7994a94fc8395d95cfb38" args="(vector< long > &lits, bool addConflicts=true)" -->
<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><!-- doxytag: member="CSolver::verify_integrity" ref="ac14b7728d00ff497795bcedfd3f24faa" args="(void)" -->
<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><!-- doxytag: member="CSolver::restart" ref="a5b9ce0b016266150cad691e4bb475668" args="(void)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></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><!-- doxytag: member="CSolver::solve" ref="a351fe372330bede0ada8c3723e844a8e" args="(bool allowNewClauses)" -->
<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><!-- doxytag: member="CSolver::continueCheck" ref="a9119faa6145fead463e8b14ec2f7cf7b" args="()" -->
<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><!-- doxytag: member="CSolver::dump_assignment_stack" ref="a60c64d82a19286ac5774adce294aa16a" args="(ostream &os=cout)" -->
<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><!-- doxytag: member="CSolver::output_current_stats" ref="adf342158bf2d06241a075a8c22a1ee73" args="(void)" -->
<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><!-- doxytag: member="CSolver::dump" ref="a8804888a9795945f5b09c67c529b898d" args="(ostream &os=cout)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classCDatabase.html#a4ecc7a06a141221adf3aff50d3ac6cf6">CDatabase</a>.</p>
<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__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>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a65a9481261bf9d9d90ff36de99992094"></a><!-- doxytag: member="CSolver::_dlevel" ref="a65a9481261bf9d9d90ff36de99992094" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCSolver.html#a65a9481261bf9d9d90ff36de99992094">CSolver::_dlevel</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_assignment_stack" ref="a6a21ab9d2ab20a5c4f103cc1a337e35f" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<vector<int> *> <a class="el" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">CSolver::_assignment_stack</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_implication_queue" ref="aeab7cd8f6085990a2a1ed518c9d75c6e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">queue<pair<int,<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a>> > <a class="el" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">CSolver::_implication_queue</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_params" ref="a30e5a80e5be76e6be4398340f3925818" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="structCSolverParameters.html">CSolverParameters</a> <a class="el" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">CSolver::_params</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_stats" ref="a5f656ea799ff4b4304b9f4f71a4df315" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="structCSolverStats.html">CSolverStats</a> <a class="el" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">CSolver::_stats</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classCDatabase.html#abb17b94a5d63adc740acbe28adb537dd">CDatabase</a>.</p>
<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><!-- doxytag: member="CSolver::_hooks" ref="a49509a796f28911569176b2cc6d4a0a0" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<pair<int,pair< <a class="el" href="xchaff__solver_8h.html#a4288f2865a52bcea1f6cd0afa93a7898">HookFunPtrT</a>, int> > > <a class="el" href="classCSolver.html#a49509a796f28911569176b2cc6d4a0a0">CSolver::_hooks</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_max_score_pos" ref="ae7e25a4d85f75c17d55cf64e26056920" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">CSolver::_max_score_pos</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_last_var_lits_count" ref="aec6d0a9cf59ad2da0dad717bea16efcb" args="[2]" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<int> <a class="el" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">CSolver::_last_var_lits_count</a>[2]<code> [protected]</code></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><!-- doxytag: member="CSolver::_var_order" ref="a40c08e5478f016f460d6adec977c2446" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<pair<int,int> > <a class="el" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">CSolver::_var_order</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_num_marked" ref="a528d66d18534a7d6e73a2e7964103b1c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">CSolver::_num_marked</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_conflicts" ref="a6bba00c21025040cc46a0499eaea7f01" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a>> <a class="el" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">CSolver::_conflicts</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_conflict_lits" ref="ab162797183d22466c24feb117fefc7d6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<long> <a class="el" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">CSolver::_conflict_lits</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_dlevel_hook" ref="ad517659e82e1b42617886d2b6758acd3" args=")(void *, int)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void(* <a class="el" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">CSolver::_dlevel_hook</a>)(void *, int)<code> [protected]</code></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><!-- doxytag: member="CSolver::_decision_hook" ref="af74159b82e953b3b766001d27b8b7981" args=")(void *, bool *)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int(* <a class="el" href="classCSolver.html#af74159b82e953b3b766001d27b8b7981">CSolver::_decision_hook</a>)(void *, bool *)<code> [protected]</code></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><!-- doxytag: member="CSolver::_assignment_hook" ref="a66cffc281bb01002d1b30e01f6e90a28" args=")(void *, int, int)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void(* <a class="el" href="classCSolver.html#a66cffc281bb01002d1b30e01f6e90a28">CSolver::_assignment_hook</a>)(void *, int, int)<code> [protected]</code></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><!-- doxytag: member="CSolver::_deduction_hook" ref="ac30b332eb58a51d87d9e1f80f62754f8" args=")(void *)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void(* <a class="el" href="classCSolver.html#ac30b332eb58a51d87d9e1f80f62754f8">CSolver::_deduction_hook</a>)(void *)<code> [protected]</code></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><!-- doxytag: member="CSolver::_dlevel_hook_cookie" ref="ad1e4bd711ad507a40d36d5815bdaa69c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void* <a class="el" href="classCSolver.html#ad1e4bd711ad507a40d36d5815bdaa69c">CSolver::_dlevel_hook_cookie</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_decision_hook_cookie" ref="a2a02aeed8e6eefe8b1d8a661c7e94c45" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void* <a class="el" href="classCSolver.html#a2a02aeed8e6eefe8b1d8a661c7e94c45">CSolver::_decision_hook_cookie</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_assignment_hook_cookie" ref="a0de6dbd6e4d7f30c4ee841f15b8ae5e4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void* <a class="el" href="classCSolver.html#a0de6dbd6e4d7f30c4ee841f15b8ae5e4">CSolver::_assignment_hook_cookie</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_deduction_hook_cookie" ref="aa2c250ed33c494f50d06122943ae280d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void* <a class="el" href="classCSolver.html#aa2c250ed33c494f50d06122943ae280d">CSolver::_deduction_hook_cookie</a><code> [protected]</code></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><!-- doxytag: member="CSolver::_addedUnitClauses" ref="a6b12fb5fcb0e279221c4047b3a61d99e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a>> <a class="el" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">CSolver::_addedUnitClauses</a><code> [protected]</code></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>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
