<!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: Xchaff 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="#pub-static-methods">Static Public Member Functions</a> |
<a href="#pri-static-methods">Static Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> </div>
<div class="headertitle">
<div class="title">Xchaff Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="Xchaff" --><!-- doxytag: inherits="SatSolver" -->
<p><code>#include <<a class="el" href="xchaff_8h_source.html">xchaff.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for Xchaff:</div>
<div class="dyncontent">
<div class="center">
<img src="classXchaff.png" usemap="#Xchaff_map" alt=""/>
<map id="Xchaff_map" name="Xchaff_map">
<area href="classSatSolver.html" alt="SatSolver" shape="rect" coords="0,0,67,24"/>
</map>
</div></div>
<p><a href="classXchaff-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classXchaff.html#aa238850d5f8f2eb815548745d5b8304a">Xchaff</a> ()
<li><a class="el" href="classXchaff.html#adef92a80a3bbac1de8b94acb37cace6c">~Xchaff</a> ()
<li>int <a class="el" href="classXchaff.html#a271a1d5d92cf07c60d70a9939d623391">NumVariables</a> ()
<li><a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classXchaff.html#a510ddbd9f083c5372bdaf5f449f4846b">AddVariables</a> (int nvars)
<li><a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classXchaff.html#a41296b8c022c75dd7e2233631a5ac704">GetVar</a> (int varIndex)
<li>int <a class="el" href="classXchaff.html#a4f9ad9e1ff0a150b3f8fad414912cd9e">GetVarIndex</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> v)
<li><a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classXchaff.html#ac3891ccb7f41fb72e294da3899779c62">GetFirstVar</a> ()
<li><a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classXchaff.html#aff81fd8f5d3c694e8f5112077142ea03">GetNextVar</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> var)
<li>Lit <a class="el" href="classXchaff.html#a9e916fd4048dfdcfdec013481e970303">MakeLit</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> var, int phase)
<li><a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classXchaff.html#a40ebc0c7f213c049c561cf0f727dfab9">GetVarFromLit</a> (Lit lit)
<li>int <a class="el" href="classXchaff.html#ac6e0c04b5b1af99b742f444a32bdddf5">GetPhaseFromLit</a> (Lit lit)
<li>int <a class="el" href="classXchaff.html#a1a3fb172ed4b688d7938e160cc00716b">NumClauses</a> ()
<li><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="el" href="classXchaff.html#adee5769adfc8bc73e27117eacd1d5e06">AddClause</a> (std::vector< Lit > &lits)
<li><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="el" href="classXchaff.html#aa7755a77a17224ef7540ff9cf475ebe0">GetClause</a> (int clauseIndex)
<li><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="el" href="classXchaff.html#a4683a3d3e3c9ea39da714c76f0aa4471">GetFirstClause</a> ()
<li><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="el" href="classXchaff.html#af02ffc8cb39e8740a7536323ee937d76">GetNextClause</a> (<a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> clause)
<li>void <a class="el" href="classXchaff.html#ad55fdf1df93621b0f79859f9180eed8c">GetClauseLits</a> (<a class="el" href="unionSatSolver_1_1Clause.html">SatSolver::Clause</a> clause, std::vector< <a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> > *lits)
<li><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> <a class="el" href="classXchaff.html#af833605af7d820b9d7a350a77cd41ed1">Satisfiable</a> (bool allowNewClauses)
<li>int <a class="el" href="classXchaff.html#a00d874effad75d5544cdd9d257b2573d">GetVarAssignment</a> (<a class="el" href="unionSatSolver_1_1Var.html">Var</a> var)
<li><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> <a class="el" href="classXchaff.html#ab20bcd7cd57b138b62e63d0e1d9a425f">Continue</a> ()
<li>void <a class="el" href="classXchaff.html#a53ce24894150638b3285f7b12ebf23ba">Restart</a> ()
<li>void <a class="el" href="classXchaff.html#ae8d8fe530dede206922f26f52f1cafcf">Reset</a> ()
<li>void <a class="el" href="classXchaff.html#a9826417dcd2303591eaeb3259ac154f9">RegisterDLevelHook</a> (void(*f)(void *, int), void *cookie)
<li>void <a class="el" href="classXchaff.html#a029881b7aad15145d313fae454637a6a">RegisterDecisionHook</a> (Lit(*f)(void *, bool *), void *cookie)
<li>void <a class="el" href="classXchaff.html#a0a98f9f270df69b9f86d15258b915afb">RegisterAssignmentHook</a> (void(*f)(void *, <a class="el" href="unionSatSolver_1_1Var.html">Var</a>, int), void *cookie)
<li>void <a class="el" href="classXchaff.html#a2ffce1f21eb64712d4e26e1dbc4b0e36">RegisterDeductionHook</a> (void(*f)(void *), void *cookie)
<li>bool <a class="el" href="classXchaff.html#aae25937c3c0f355220a4533fb127edf7">SetBudget</a> (int budget)
<li>bool <a class="el" href="classXchaff.html#a58905ab92772d4603d41b8155a59f0c2">SetMemLimit</a> (int mem_limit)
<li>bool <a class="el" href="classXchaff.html#aa334fc9dd8673ff86d7214e439986e57">SetRandomness</a> (int n)
<li>bool <a class="el" href="classXchaff.html#a390d585a7258c0237ea17893587d1ee0">SetRandSeed</a> (int seed)
<li>bool <a class="el" href="classXchaff.html#a8a481eb175d81a80556e13ecff483da1">EnableClauseDeletion</a> ()
<li>bool <a class="el" href="classXchaff.html#ab763aebc2ca5e3b489aab695ed469213">DisableClauseDeletion</a> ()
<li>int <a class="el" href="classXchaff.html#a90a038ad50d710508f2f3c0a3f909528">GetBudgetUsed</a> ()
<li>int <a class="el" href="classXchaff.html#ad483bd394ba347d90afb2354a3579d5b">GetMemUsed</a> ()
<li>int <a class="el" href="classXchaff.html#a0ae00dfb15ac6f1f6947056c448cc4db">GetNumDecisions</a> ()
<li>int <a class="el" href="classXchaff.html#aafeebd0e319671ade2b15418a5491aa1">GetNumConflicts</a> ()
<li>int <a class="el" href="classXchaff.html#aa0c48459562f98b52b01999bb7c394ec">GetNumExtConflicts</a> ()
<li>float <a class="el" href="classXchaff.html#a554b43a08c1aadad56bcb16d7a5ae8f5">GetTotalTime</a> ()
<li>float <a class="el" href="classXchaff.html#a892c44f9b8bd6bb98a57c67f6e0261fa">GetSATTime</a> ()
<li>int <a class="el" href="classXchaff.html#aefa4cd2058553d7946cbebdb667e8670">GetNumLiterals</a> ()
<li>int <a class="el" href="classXchaff.html#a6f69523569c280d1486b7c6ddde2b112">GetNumDeletedClauses</a> ()
<li>int <a class="el" href="classXchaff.html#a0939c01d21987c020eb5fa783af11164">GetNumDeletedLiterals</a> ()
<li>int <a class="el" href="classXchaff.html#aec9cba92c3e56ed8aa68693c6083e54d">GetNumImplications</a> ()
<li>int <a class="el" href="classXchaff.html#a4ff03b5c032c7344058759ef1165ad9e">GetMaxDLevel</a> ()
</ul>
<h2><a name="pub-static-methods"></a>
Static Public Member Functions</h2>
<ul>
<li>static int <a class="el" href="classXchaff.html#ab42f8b43c2bc455a30955f4e8b8b4b9b">TranslateDecisionHook</a> (void *cookie, bool *done)
<li>static void <a class="el" href="classXchaff.html#a393a5a2f7d45b4ffc54c00a5afbefd28">TranslateAssignmentHook</a> (void *cookie, int var, int value)
</ul>
<h2><a name="pri-static-methods"></a>
Static Private Member Functions</h2>
<ul>
<li>static <a class="el" href="unionSatSolver_1_1Var.html">Var</a> <a class="el" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68">mkVar</a> (int id)
<li>static Lit <a class="el" href="classXchaff.html#a216cb72b0a5a4568ef9a0eb430b2d933">mkLit</a> (int id)
<li>static <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="el" href="classXchaff.html#a68161914638f53d93a26ff242e437472">mkClause</a> (int id)
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCSolver.html">CSolver</a> * <a class="el" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>
<li>Lit(* <a class="el" href="classXchaff.html#a745565adebc2ce37a9781e03860ba8ca">_decision_hook</a> )(void *, bool *)
<li>void(* <a class="el" href="classXchaff.html#a7680ebfc3431daea429904672209fdb8">_assignment_hook</a> )(void *, <a class="el" href="unionSatSolver_1_1Var.html">Var</a>, int)
<li>void * <a class="el" href="classXchaff.html#ac3a215c0cf6649a72471e5559e3e6f04">_decision_hook_cookie</a>
<li>void * <a class="el" href="classXchaff.html#aff3437eb408419a6c84e9ff923ef5444">_assignment_hook_cookie</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00016">16</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="aa238850d5f8f2eb815548745d5b8304a"></a><!-- doxytag: member="Xchaff::Xchaff" ref="aa238850d5f8f2eb815548745d5b8304a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Xchaff::Xchaff </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_8h_source.html#l00029">29</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>.</p>
</div>
</div>
<a class="anchor" id="adef92a80a3bbac1de8b94acb37cace6c"></a><!-- doxytag: member="Xchaff::~Xchaff" ref="adef92a80a3bbac1de8b94acb37cace6c" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Xchaff::~Xchaff </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_8h_source.html#l00030">30</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a7ffa41a1a67d90266b131230adebda68"></a><!-- doxytag: member="Xchaff::mkVar" ref="a7ffa41a1a67d90266b131230adebda68" args="(int id)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static <a class="el" href="unionSatSolver_1_1Var.html">Var</a> Xchaff::mkVar </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>id</em></td><td>)</td>
<td><code> [inline, static, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00024">24</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="sat__api_8h_source.html#l00052">SatSolver::Var::id</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00038">AddVariables()</a>, <a class="el" href="xchaff_8h_source.html#l00040">GetVar()</a>, <a class="el" href="xchaff_8h_source.html#l00051">GetVarFromLit()</a>, and <a class="el" href="xchaff_8h_source.html#l00094">TranslateAssignmentHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a216cb72b0a5a4568ef9a0eb430b2d933"></a><!-- doxytag: member="Xchaff::mkLit" ref="a216cb72b0a5a4568ef9a0eb430b2d933" args="(int id)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static Lit Xchaff::mkLit </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>id</em></td><td>)</td>
<td><code> [inline, static, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00025">25</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="sat__api_8h_source.html#l00060">SatSolver::Lit::id</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8cpp_source.html#l00035">GetClauseLits()</a>, and <a class="el" href="xchaff_8h_source.html#l00049">MakeLit()</a>.</p>
</div>
</div>
<a class="anchor" id="a68161914638f53d93a26ff242e437472"></a><!-- doxytag: member="Xchaff::mkClause" ref="a68161914638f53d93a26ff242e437472" args="(int id)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static <a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> Xchaff::mkClause </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>id</em></td><td>)</td>
<td><code> [inline, static, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00026">26</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="sat__api_8h_source.html#l00068">SatSolver::Clause::id</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00057">AddClause()</a>.</p>
</div>
</div>
<a class="anchor" id="a271a1d5d92cf07c60d70a9939d623391"></a><!-- doxytag: member="Xchaff::NumVariables" ref="a271a1d5d92cf07c60d70a9939d623391" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::NumVariables </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a75ac3919b9d2794bd2443e32bb1f29fd">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00036">36</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00210">CDatabase::num_variables()</a>.</p>
</div>
</div>
<a class="anchor" id="a510ddbd9f083c5372bdaf5f449f4846b"></a><!-- doxytag: member="Xchaff::AddVariables" ref="a510ddbd9f083c5372bdaf5f449f4846b" args="(int nvars)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> Xchaff::AddVariables </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>nvars</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#acf0e4f44556b7cfcea37100f92962fee">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00038">38</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00160">CSolver::add_variables()</a>, and <a class="el" href="xchaff_8h_source.html#l00024">mkVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a41296b8c022c75dd7e2233631a5ac704"></a><!-- doxytag: member="Xchaff::GetVar" ref="a41296b8c022c75dd7e2233631a5ac704" args="(int varIndex)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> Xchaff::GetVar </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>varIndex</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#aebeecffca634f23d8c9b941b44b4cfe7">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00040">40</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00024">mkVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a4f9ad9e1ff0a150b3f8fad414912cd9e"></a><!-- doxytag: member="Xchaff::GetVarIndex" ref="a4f9ad9e1ff0a150b3f8fad414912cd9e" args="(Var v)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetVarIndex </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td>
<td class="paramname"><em>v</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a78a8661d31ba8f3aca7e4c73a84f0bcf">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00042">42</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="sat__api_8h_source.html#l00052">SatSolver::Var::id</a>.</p>
</div>
</div>
<a class="anchor" id="ac3891ccb7f41fb72e294da3899779c62"></a><!-- doxytag: member="Xchaff::GetFirstVar" ref="ac3891ccb7f41fb72e294da3899779c62" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> Xchaff::GetFirstVar </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a6c62129375a3b6dda25ad2ba6c0a5696">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00044">44</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="sat__api_8h_source.html#l00052">SatSolver::Var::id</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00210">CDatabase::num_variables()</a>.</p>
</div>
</div>
<a class="anchor" id="aff81fd8f5d3c694e8f5112077142ea03"></a><!-- doxytag: member="Xchaff::GetNextVar" ref="aff81fd8f5d3c694e8f5112077142ea03" args="(Var var)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> Xchaff::GetNextVar </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a2a175341a5ca6b28add0a1cac3e9bc8a">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00046">46</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="sat__api_8h_source.html#l00052">SatSolver::Var::id</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00210">CDatabase::num_variables()</a>.</p>
</div>
</div>
<a class="anchor" id="a9e916fd4048dfdcfdec013481e970303"></a><!-- doxytag: member="Xchaff::MakeLit" ref="a9e916fd4048dfdcfdec013481e970303" args="(Var var, int phase)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Lit Xchaff::MakeLit </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> </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>phase</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a66bbef74a05f145e477adf37a1e1d116">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00049">49</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="sat__api_8h_source.html#l00052">SatSolver::Var::id</a>, and <a class="el" href="xchaff_8h_source.html#l00025">mkLit()</a>.</p>
</div>
</div>
<a class="anchor" id="a40ebc0c7f213c049c561cf0f727dfab9"></a><!-- doxytag: member="Xchaff::GetVarFromLit" ref="a40ebc0c7f213c049c561cf0f727dfab9" args="(Lit lit)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> Xchaff::GetVarFromLit </td>
<td>(</td>
<td class="paramtype">Lit </td>
<td class="paramname"><em>lit</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00051">51</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00024">mkVar()</a>.</p>
</div>
</div>
<a class="anchor" id="ac6e0c04b5b1af99b742f444a32bdddf5"></a><!-- doxytag: member="Xchaff::GetPhaseFromLit" ref="ac6e0c04b5b1af99b742f444a32bdddf5" args="(Lit lit)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetPhaseFromLit </td>
<td>(</td>
<td class="paramtype">Lit </td>
<td class="paramname"><em>lit</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00053">53</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
</div>
</div>
<a class="anchor" id="a1a3fb172ed4b688d7938e160cc00716b"></a><!-- doxytag: member="Xchaff::NumClauses" ref="a1a3fb172ed4b688d7938e160cc00716b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::NumClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#ad883af9527935afd6c8ad542ba119f4a">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00055">55</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00214">CDatabase::num_clauses()</a>.</p>
</div>
</div>
<a class="anchor" id="adee5769adfc8bc73e27117eacd1d5e06"></a><!-- doxytag: member="Xchaff::AddClause" ref="adee5769adfc8bc73e27117eacd1d5e06" args="(std::vector< Lit > &lits)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> Xchaff::AddClause </td>
<td>(</td>
<td class="paramtype">std::vector< Lit > & </td>
<td class="paramname"><em>lits</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00057">57</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, and <a class="el" href="xchaff_8h_source.html#l00026">mkClause()</a>.</p>
</div>
</div>
<a class="anchor" id="aa7755a77a17224ef7540ff9cf475ebe0"></a><!-- doxytag: member="Xchaff::GetClause" ref="aa7755a77a17224ef7540ff9cf475ebe0" args="(int clauseIndex)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="unionSatSolver_1_1Clause.html">SatSolver::Clause</a> Xchaff::GetClause </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>clauseIndex</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a3f5dcfdd713812059fdcba94bc6be3c1">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8cpp_source.html#l00020">20</a> of file <a class="el" href="xchaff_8cpp_source.html">xchaff.cpp</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">CDatabase::clause()</a>, <a class="el" href="sat__api_8h_source.html#l00068">SatSolver::Clause::id</a>, <a class="el" href="xchaff__base_8h_source.html#l00192">CClause::in_use()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00136">CDatabase::init_num_clauses()</a>.</p>
</div>
</div>
<a class="anchor" id="a4683a3d3e3c9ea39da714c76f0aa4471"></a><!-- doxytag: member="Xchaff::GetFirstClause" ref="a4683a3d3e3c9ea39da714c76f0aa4471" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> Xchaff::GetFirstClause </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a580f042cdf32047e73056dfd810226ad">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00060">60</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</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="sat__api_8h_source.html#l00068">SatSolver::Clause::id</a>, and <a class="el" href="xchaff__base_8h_source.html#l00192">CClause::in_use()</a>.</p>
</div>
</div>
<a class="anchor" id="af02ffc8cb39e8740a7536323ee937d76"></a><!-- doxytag: member="Xchaff::GetNextClause" ref="af02ffc8cb39e8740a7536323ee937d76" args="(Clause clause)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> Xchaff::GetNextClause </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Clause.html">Clause</a> </td>
<td class="paramname"><em>clause</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a61ca72083b23704e2007f0c4b7414ff1">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00065">65</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">CDatabase::clause()</a>, <a class="el" href="sat__api_8h_source.html#l00068">SatSolver::Clause::id</a>, and <a class="el" href="xchaff__base_8h_source.html#l00192">CClause::in_use()</a>.</p>
</div>
</div>
<a class="anchor" id="ad55fdf1df93621b0f79859f9180eed8c"></a><!-- doxytag: member="Xchaff::GetClauseLits" ref="ad55fdf1df93621b0f79859f9180eed8c" args="(SatSolver::Clause clause, std::vector< Lit > *lits)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Xchaff::GetClauseLits </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Clause.html">SatSolver::Clause</a> </td>
<td class="paramname"><em>clause</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="unionSatSolver_1_1Lit.html">Lit</a> > * </td>
<td class="paramname"><em>lits</em> </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_8cpp_source.html#l00035">35</a> of file <a class="el" href="xchaff_8cpp_source.html">xchaff.cpp</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00126">CDatabase::clause()</a>, <a class="el" href="sat__api_8h_source.html#l00068">SatSolver::Clause::id</a>, <a class="el" href="xchaff__base_8h_source.html#l00195">CClause::literal()</a>, <a class="el" href="xchaff_8h_source.html#l00025">mkLit()</a>, <a class="el" href="xchaff__base_8h_source.html#l00189">CClause::num_lits()</a>, and <a class="el" href="xchaff__base_8h_source.html#l00095">CLitPoolElement::s_var()</a>.</p>
</div>
</div>
<a class="anchor" id="af833605af7d820b9d7a350a77cd41ed1"></a><!-- doxytag: member="Xchaff::Satisfiable" ref="af833605af7d820b9d7a350a77cd41ed1" args="(bool allowNewClauses)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> Xchaff::Satisfiable </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>allowNewClauses</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a0dfc1321f3446be70349f35881144433">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8cpp_source.html#l00043">43</a> of file <a class="el" href="xchaff_8cpp_source.html">xchaff.cpp</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="sat__api_8h_source.html#l00030">SatSolver::BUDGET_EXCEEDED</a>, <a class="el" href="xchaff__solver_8h_source.html#l00057">MEM_OUT</a>, <a class="el" href="sat__api_8h_source.html#l00031">SatSolver::OUT_OF_MEMORY</a>, <a class="el" href="sat__api_8h_source.html#l00029">SatSolver::SATISFIABLE</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00804">CSolver::solve()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00056">TIME_OUT</a>, <a class="el" href="sat__api_8h_source.html#l00027">SatSolver::UNKNOWN</a>, and <a class="el" href="sat__api_8h_source.html#l00028">SatSolver::UNSATISFIABLE</a>.</p>
</div>
</div>
<a class="anchor" id="a00d874effad75d5544cdd9d257b2573d"></a><!-- doxytag: member="Xchaff::GetVarAssignment" ref="a00d874effad75d5544cdd9d257b2573d" args="(Var var)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetVarAssignment </td>
<td>(</td>
<td class="paramtype"><a class="el" href="unionSatSolver_1_1Var.html">Var</a> </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a111b3a56be2feaae62bc57483f0aa9bf">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00072">72</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="sat__api_8h_source.html#l00052">SatSolver::Var::id</a>, <a class="el" href="xchaff__base_8h_source.html#l00264">CVariable::value()</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00123">CDatabase::variable()</a>.</p>
</div>
</div>
<a class="anchor" id="ab20bcd7cd57b138b62e63d0e1d9a425f"></a><!-- doxytag: member="Xchaff::Continue" ref="ab20bcd7cd57b138b62e63d0e1d9a425f" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> Xchaff::Continue </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#ab4e73333fbc4b4372a18c66a40d4757f">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8cpp_source.html#l00057">57</a> of file <a class="el" href="xchaff_8cpp_source.html">xchaff.cpp</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="sat__api_8h_source.html#l00030">SatSolver::BUDGET_EXCEEDED</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00822">CSolver::continueCheck()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00057">MEM_OUT</a>, <a class="el" href="sat__api_8h_source.html#l00031">SatSolver::OUT_OF_MEMORY</a>, <a class="el" href="sat__api_8h_source.html#l00029">SatSolver::SATISFIABLE</a>, <a class="el" href="xchaff__solver_8h_source.html#l00056">TIME_OUT</a>, <a class="el" href="sat__api_8h_source.html#l00027">SatSolver::UNKNOWN</a>, and <a class="el" href="sat__api_8h_source.html#l00028">SatSolver::UNSATISFIABLE</a>.</p>
</div>
</div>
<a class="anchor" id="a53ce24894150638b3285f7b12ebf23ba"></a><!-- doxytag: member="Xchaff::Restart" ref="a53ce24894150638b3285f7b12ebf23ba" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Xchaff::Restart </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#aa05fce07f5c3363e2362a3b1de7795db">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00077">77</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
</div>
</div>
<a class="anchor" id="ae8d8fe530dede206922f26f52f1cafcf"></a><!-- doxytag: member="Xchaff::Reset" ref="ae8d8fe530dede206922f26f52f1cafcf" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Xchaff::Reset </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#ac64e81107b4b94fd1f6fb76b219a0517">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00078">78</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
</div>
</div>
<a class="anchor" id="a9826417dcd2303591eaeb3259ac154f9"></a><!-- doxytag: member="Xchaff::RegisterDLevelHook" ref="a9826417dcd2303591eaeb3259ac154f9" args="(void(*f)(void *, int), void *cookie)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Xchaff::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, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a2f5308d9fdff97f882186073f05d8874">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00080">80</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00264">CSolver::RegisterDLevelHook()</a>.</p>
</div>
</div>
<a class="anchor" id="ab42f8b43c2bc455a30955f4e8b8b4b9b"></a><!-- doxytag: member="Xchaff::TranslateDecisionHook" ref="ab42f8b43c2bc455a30955f4e8b8b4b9b" args="(void *cookie, bool *done)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static int Xchaff::TranslateDecisionHook </td>
<td>(</td>
<td class="paramtype">void * </td>
<td class="paramname"><em>cookie</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool * </td>
<td class="paramname"><em>done</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00083">83</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00019">_decision_hook</a>, <a class="el" href="xchaff_8h_source.html#l00021">_decision_hook_cookie</a>, and <a class="el" href="sat__api_8h_source.html#l00060">SatSolver::Lit::id</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00090">RegisterDecisionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a029881b7aad15145d313fae454637a6a"></a><!-- doxytag: member="Xchaff::RegisterDecisionHook" ref="a029881b7aad15145d313fae454637a6a" args="(Lit(*f)(void *, bool *), void *cookie)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Xchaff::RegisterDecisionHook </td>
<td>(</td>
<td class="paramtype">Lit(*)(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_8h_source.html#l00090">90</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00019">_decision_hook</a>, <a class="el" href="xchaff_8h_source.html#l00021">_decision_hook_cookie</a>, <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="xchaff__solver_8h_source.html#l00266">CSolver::RegisterDecisionHook()</a>, and <a class="el" href="xchaff_8h_source.html#l00083">TranslateDecisionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a393a5a2f7d45b4ffc54c00a5afbefd28"></a><!-- doxytag: member="Xchaff::TranslateAssignmentHook" ref="a393a5a2f7d45b4ffc54c00a5afbefd28" args="(void *cookie, int var, int value)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static void Xchaff::TranslateAssignmentHook </td>
<td>(</td>
<td class="paramtype">void * </td>
<td class="paramname"><em>cookie</em>, </td>
</tr>
<tr>
<td class="paramkey"></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></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00094">94</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00020">_assignment_hook</a>, <a class="el" href="xchaff_8h_source.html#l00022">_assignment_hook_cookie</a>, and <a class="el" href="xchaff_8h_source.html#l00024">mkVar()</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00100">RegisterAssignmentHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a0a98f9f270df69b9f86d15258b915afb"></a><!-- doxytag: member="Xchaff::RegisterAssignmentHook" ref="a0a98f9f270df69b9f86d15258b915afb" args="(void(*f)(void *, Var, int), void *cookie)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Xchaff::RegisterAssignmentHook </td>
<td>(</td>
<td class="paramtype">void(*)(void *, <a class="el" href="unionSatSolver_1_1Var.html">Var</a>, 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, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a658bb40c580f149024c59509e9e3acd0">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00100">100</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00020">_assignment_hook</a>, <a class="el" href="xchaff_8h_source.html#l00022">_assignment_hook_cookie</a>, <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, <a class="el" href="xchaff__solver_8h_source.html#l00268">CSolver::RegisterAssignmentHook()</a>, and <a class="el" href="xchaff_8h_source.html#l00094">TranslateAssignmentHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a2ffce1f21eb64712d4e26e1dbc4b0e36"></a><!-- doxytag: member="Xchaff::RegisterDeductionHook" ref="a2ffce1f21eb64712d4e26e1dbc4b0e36" args="(void(*f)(void *), void *cookie)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Xchaff::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, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="classSatSolver.html#a856cf7839d83dcc04ee421d2595fc671">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00103">103</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00270">CSolver::RegisterDeductionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="aae25937c3c0f355220a4533fb127edf7"></a><!-- doxytag: member="Xchaff::SetBudget" ref="aae25937c3c0f355220a4533fb127edf7" args="(int budget)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Xchaff::SetBudget </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>budget</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#ab6c0375792fa61834acc0e059b0f0215">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00105">105</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00228">CSolver::set_time_limit()</a>.</p>
</div>
</div>
<a class="anchor" id="a58905ab92772d4603d41b8155a59f0c2"></a><!-- doxytag: member="Xchaff::SetMemLimit" ref="a58905ab92772d4603d41b8155a59f0c2" args="(int mem_limit)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Xchaff::SetMemLimit </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>mem_limit</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#ae71ce584f847dd8f8cd79c15a1e18ac4">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00107">107</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00230">CSolver::set_mem_limit()</a>.</p>
</div>
</div>
<a class="anchor" id="aa334fc9dd8673ff86d7214e439986e57"></a><!-- doxytag: member="Xchaff::SetRandomness" ref="aa334fc9dd8673ff86d7214e439986e57" args="(int n)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Xchaff::SetRandomness </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>n</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#a2d799de14b8f73985474b6e6bb391799">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00109">109</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00253">CSolver::set_randomness()</a>.</p>
</div>
</div>
<a class="anchor" id="a390d585a7258c0237ea17893587d1ee0"></a><!-- doxytag: member="Xchaff::SetRandSeed" ref="a390d585a7258c0237ea17893587d1ee0" args="(int seed)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Xchaff::SetRandSeed </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>seed</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#a49baebbc72ee8480ce9b15931fd6a087">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00111">111</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00256">CSolver::set_random_seed()</a>.</p>
</div>
</div>
<a class="anchor" id="a8a481eb175d81a80556e13ecff483da1"></a><!-- doxytag: member="Xchaff::EnableClauseDeletion" ref="a8a481eb175d81a80556e13ecff483da1" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Xchaff::EnableClauseDeletion </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#aab2f83c7e7a2e0294904ff5c0fa3409d">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00113">113</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00237">CSolver::enable_cls_deletion()</a>.</p>
</div>
</div>
<a class="anchor" id="ab763aebc2ca5e3b489aab695ed469213"></a><!-- doxytag: member="Xchaff::DisableClauseDeletion" ref="ab763aebc2ca5e3b489aab695ed469213" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Xchaff::DisableClauseDeletion </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#ae4127dad23cea8d60a6eb2f5d0072554">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00115">115</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00237">CSolver::enable_cls_deletion()</a>.</p>
</div>
</div>
<a class="anchor" id="a90a038ad50d710508f2f3c0a3f909528"></a><!-- doxytag: member="Xchaff::GetBudgetUsed" ref="a90a038ad50d710508f2f3c0a3f909528" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetBudgetUsed </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#a9ab0d5988fd6b737626eddfdfb3086ca">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00117">117</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00310">CSolver::total_run_time()</a>.</p>
</div>
</div>
<a class="anchor" id="ad483bd394ba347d90afb2354a3579d5b"></a><!-- doxytag: member="Xchaff::GetMemUsed" ref="ad483bd394ba347d90afb2354a3579d5b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetMemUsed </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#a409a256b9b590f8881690422ac34f566">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00119">119</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00326">CSolver::estimate_mem_usage()</a>.</p>
</div>
</div>
<a class="anchor" id="a0ae00dfb15ac6f1f6947056c448cc4db"></a><!-- doxytag: member="Xchaff::GetNumDecisions" ref="a0ae00dfb15ac6f1f6947056c448cc4db" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetNumDecisions </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#a2a416ee5b49d9cf91a57c5b9e71388b8">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00121">121</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00275">CSolver::num_decisions()</a>.</p>
</div>
</div>
<a class="anchor" id="aafeebd0e319671ade2b15418a5491aa1"></a><!-- doxytag: member="Xchaff::GetNumConflicts" ref="aafeebd0e319671ade2b15418a5491aa1" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetNumConflicts </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#ab81836241806bc37ca6c5cfcd1a77df4">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00123">123</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
</div>
</div>
<a class="anchor" id="aa0c48459562f98b52b01999bb7c394ec"></a><!-- doxytag: member="Xchaff::GetNumExtConflicts" ref="aa0c48459562f98b52b01999bb7c394ec" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetNumExtConflicts </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#af11d56356aa9a578f0baaa4cbcdc0b97">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00125">125</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
</div>
</div>
<a class="anchor" id="a554b43a08c1aadad56bcb16d7a5ae8f5"></a><!-- doxytag: member="Xchaff::GetTotalTime" ref="a554b43a08c1aadad56bcb16d7a5ae8f5" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">float Xchaff::GetTotalTime </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#ab1d30058d42aecba7708cb9e29cbda67">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00127">127</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00310">CSolver::total_run_time()</a>.</p>
</div>
</div>
<a class="anchor" id="a892c44f9b8bd6bb98a57c67f6e0261fa"></a><!-- doxytag: member="Xchaff::GetSATTime" ref="a892c44f9b8bd6bb98a57c67f6e0261fa" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">float Xchaff::GetSATTime </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#a4af09fc1738959db1c0d197a4fbf8a6a">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00129">129</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
</div>
</div>
<a class="anchor" id="aefa4cd2058553d7946cbebdb667e8670"></a><!-- doxytag: member="Xchaff::GetNumLiterals" ref="aefa4cd2058553d7946cbebdb667e8670" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetNumLiterals </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#a6f617ce6eae22b959f135d347776cb27">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00131">131</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00217">CDatabase::num_literals()</a>.</p>
</div>
</div>
<a class="anchor" id="a6f69523569c280d1486b7c6ddde2b112"></a><!-- doxytag: member="Xchaff::GetNumDeletedClauses" ref="a6f69523569c280d1486b7c6ddde2b112" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetNumDeletedClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#a6499994eb391919ce6542412e3e43d01">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00133">133</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00140">CDatabase::num_deleted_clauses()</a>.</p>
</div>
</div>
<a class="anchor" id="a0939c01d21987c020eb5fa783af11164"></a><!-- doxytag: member="Xchaff::GetNumDeletedLiterals" ref="a0939c01d21987c020eb5fa783af11164" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetNumDeletedLiterals </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#ab81eb4127972de38906425ba4babfadc">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00135">135</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__dbase_8h_source.html#l00141">CDatabase::num_deleted_literals()</a>.</p>
</div>
</div>
<a class="anchor" id="aec9cba92c3e56ed8aa68693c6083e54d"></a><!-- doxytag: member="Xchaff::GetNumImplications" ref="aec9cba92c3e56ed8aa68693c6083e54d" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetNumImplications </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#a45923d3ff1c6145198098d7e689c23f0">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00137">137</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00280">CSolver::num_implications()</a>.</p>
</div>
</div>
<a class="anchor" id="a4ff03b5c032c7344058759ef1165ad9e"></a><!-- doxytag: member="Xchaff::GetMaxDLevel" ref="a4ff03b5c032c7344058759ef1165ad9e" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Xchaff::GetMaxDLevel </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented from <a class="el" href="classSatSolver.html#a74190d9fc4abdb54fc65c4efffdf75fc">SatSolver</a>.</p>
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00139">139</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>References <a class="el" href="xchaff_8h_source.html#l00017">_solver</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00279">CSolver::max_dlevel()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="ad12d883fd228bfbabd7cbe96e75fb9e1"></a><!-- doxytag: member="Xchaff::_solver" ref="ad12d883fd228bfbabd7cbe96e75fb9e1" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCSolver.html">CSolver</a>* <a class="el" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">Xchaff::_solver</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00017">17</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00057">AddClause()</a>, <a class="el" href="xchaff_8h_source.html#l00038">AddVariables()</a>, <a class="el" href="xchaff_8cpp_source.html#l00057">Continue()</a>, <a class="el" href="xchaff_8h_source.html#l00115">DisableClauseDeletion()</a>, <a class="el" href="xchaff_8h_source.html#l00113">EnableClauseDeletion()</a>, <a class="el" href="xchaff_8h_source.html#l00117">GetBudgetUsed()</a>, <a class="el" href="xchaff_8cpp_source.html#l00020">GetClause()</a>, <a class="el" href="xchaff_8cpp_source.html#l00035">GetClauseLits()</a>, <a class="el" href="xchaff_8h_source.html#l00060">GetFirstClause()</a>, <a class="el" href="xchaff_8h_source.html#l00044">GetFirstVar()</a>, <a class="el" href="xchaff_8h_source.html#l00139">GetMaxDLevel()</a>, <a class="el" href="xchaff_8h_source.html#l00119">GetMemUsed()</a>, <a class="el" href="xchaff_8h_source.html#l00065">GetNextClause()</a>, <a class="el" href="xchaff_8h_source.html#l00046">GetNextVar()</a>, <a class="el" href="xchaff_8h_source.html#l00121">GetNumDecisions()</a>, <a class="el" href="xchaff_8h_source.html#l00133">GetNumDeletedClauses()</a>, <a class="el" href="xchaff_8h_source.html#l00135">GetNumDeletedLiterals()</a>, <a class="el" href="xchaff_8h_source.html#l00137">GetNumImplications()</a>, <a class="el" href="xchaff_8h_source.html#l00131">GetNumLiterals()</a>, <a class="el" href="xchaff_8h_source.html#l00127">GetTotalTime()</a>, <a class="el" href="xchaff_8h_source.html#l00072">GetVarAssignment()</a>, <a class="el" href="xchaff_8h_source.html#l00055">NumClauses()</a>, <a class="el" href="xchaff_8h_source.html#l00036">NumVariables()</a>, <a class="el" href="xchaff_8h_source.html#l00100">RegisterAssignmentHook()</a>, <a class="el" href="xchaff_8h_source.html#l00090">RegisterDecisionHook()</a>, <a class="el" href="xchaff_8h_source.html#l00103">RegisterDeductionHook()</a>, <a class="el" href="xchaff_8h_source.html#l00080">RegisterDLevelHook()</a>, <a class="el" href="xchaff_8cpp_source.html#l00043">Satisfiable()</a>, <a class="el" href="xchaff_8h_source.html#l00105">SetBudget()</a>, <a class="el" href="xchaff_8h_source.html#l00107">SetMemLimit()</a>, <a class="el" href="xchaff_8h_source.html#l00109">SetRandomness()</a>, <a class="el" href="xchaff_8h_source.html#l00111">SetRandSeed()</a>, <a class="el" href="xchaff_8h_source.html#l00029">Xchaff()</a>, and <a class="el" href="xchaff_8h_source.html#l00030">~Xchaff()</a>.</p>
</div>
</div>
<a class="anchor" id="a745565adebc2ce37a9781e03860ba8ca"></a><!-- doxytag: member="Xchaff::_decision_hook" ref="a745565adebc2ce37a9781e03860ba8ca" args=")(void *, bool *)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Lit(* <a class="el" href="classXchaff.html#a745565adebc2ce37a9781e03860ba8ca">Xchaff::_decision_hook</a>)(void *, bool *)<code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00019">19</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00090">RegisterDecisionHook()</a>, and <a class="el" href="xchaff_8h_source.html#l00083">TranslateDecisionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="a7680ebfc3431daea429904672209fdb8"></a><!-- doxytag: member="Xchaff::_assignment_hook" ref="a7680ebfc3431daea429904672209fdb8" args=")(void *, Var, int)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void(* <a class="el" href="classXchaff.html#a7680ebfc3431daea429904672209fdb8">Xchaff::_assignment_hook</a>)(void *, <a class="el" href="unionSatSolver_1_1Var.html">Var</a>, int)<code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00020">20</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00100">RegisterAssignmentHook()</a>, and <a class="el" href="xchaff_8h_source.html#l00094">TranslateAssignmentHook()</a>.</p>
</div>
</div>
<a class="anchor" id="ac3a215c0cf6649a72471e5559e3e6f04"></a><!-- doxytag: member="Xchaff::_decision_hook_cookie" ref="ac3a215c0cf6649a72471e5559e3e6f04" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void* <a class="el" href="classXchaff.html#ac3a215c0cf6649a72471e5559e3e6f04">Xchaff::_decision_hook_cookie</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00021">21</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00090">RegisterDecisionHook()</a>, and <a class="el" href="xchaff_8h_source.html#l00083">TranslateDecisionHook()</a>.</p>
</div>
</div>
<a class="anchor" id="aff3437eb408419a6c84e9ff923ef5444"></a><!-- doxytag: member="Xchaff::_assignment_hook_cookie" ref="aff3437eb408419a6c84e9ff923ef5444" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void* <a class="el" href="classXchaff.html#aff3437eb408419a6c84e9ff923ef5444">Xchaff::_assignment_hook_cookie</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff_8h_source.html#l00022">22</a> of file <a class="el" href="xchaff_8h_source.html">xchaff.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff_8h_source.html#l00100">RegisterAssignmentHook()</a>, and <a class="el" href="xchaff_8h_source.html#l00094">TranslateAssignmentHook()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="xchaff_8h_source.html">xchaff.h</a></li>
<li><a class="el" href="xchaff_8cpp_source.html">xchaff.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>
