<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: xchaff.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_a36840dfa927f36fc689e54a034a1fa1.html">sat</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">xchaff.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="xchaff_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="comment">///////////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="comment"></span><span class="comment">// //</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="comment">// File: xchaff.h //</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment">// Author: Clark Barrett //</span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment">// Created: Wed Oct 16 17:31:50 2002 //</span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment">// Description: Enhanced C++ API for Chaff //</span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment">// //</span><span class="comment"></span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment">///////////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment"></span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="preprocessor">#ifndef _XCHAFF_H_</span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span> <span class="preprocessor"></span><span class="preprocessor">#define _XCHAFF_H_</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="preprocessor">#include "<a class="code" href="sat__api_8h.html">sat_api.h</a>"</span></div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="preprocessor">#include "<a class="code" href="xchaff__solver_8h.html">xchaff_solver.h</a>"</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span> </div>
<div class="line"><a name="l00016"></a><span class="lineno"><a class="code" href="classXchaff.html"> 16</a></span> <span class="keyword">class </span><a class="code" href="classXchaff.html">Xchaff</a> :<span class="keyword">public</span> <a class="code" href="classSatSolver.html">SatSolver</a> {</div>
<div class="line"><a name="l00017"></a><span class="lineno"><a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1"> 17</a></span>  <a class="code" href="classCSolver.html">CSolver</a> *<a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>;</div>
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span> </div>
<div class="line"><a name="l00019"></a><span class="lineno"><a class="code" href="classXchaff.html#a745565adebc2ce37a9781e03860ba8ca"> 19</a></span>  Lit (*<a class="code" href="classXchaff.html#a745565adebc2ce37a9781e03860ba8ca">_decision_hook</a>)(<span class="keywordtype">void</span> *, <span class="keywordtype">bool</span> *);</div>
<div class="line"><a name="l00020"></a><span class="lineno"><a class="code" href="classXchaff.html#a7680ebfc3431daea429904672209fdb8"> 20</a></span>  void (*<a class="code" href="classXchaff.html#a7680ebfc3431daea429904672209fdb8">_assignment_hook</a>)(<span class="keywordtype">void</span> *, <a class="code" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a>, int);</div>
<div class="line"><a name="l00021"></a><span class="lineno"><a class="code" href="classXchaff.html#ac3a215c0cf6649a72471e5559e3e6f04"> 21</a></span>  <span class="keywordtype">void</span> *<a class="code" href="classXchaff.html#ac3a215c0cf6649a72471e5559e3e6f04">_decision_hook_cookie</a>;</div>
<div class="line"><a name="l00022"></a><span class="lineno"><a class="code" href="classXchaff.html#aff3437eb408419a6c84e9ff923ef5444"> 22</a></span>  <span class="keywordtype">void</span> *<a class="code" href="classXchaff.html#aff3437eb408419a6c84e9ff923ef5444">_assignment_hook_cookie</a>;</div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span> </div>
<div class="line"><a name="l00024"></a><span class="lineno"><a class="code" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68"> 24</a></span>  <span class="keyword">static</span> <a class="code" href="unionSatSolver_1_1Var.html">Var</a> <a class="code" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68">mkVar</a>(<span class="keywordtype">int</span> <span class="keywordtype">id</span>) { <a class="code" href="unionSatSolver_1_1Var.html">Var</a> v; v.<a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a> = id; <span class="keywordflow">return</span> v; }</div>
<div class="line"><a name="l00025"></a><span class="lineno"><a class="code" href="classXchaff.html#a216cb72b0a5a4568ef9a0eb430b2d933"> 25</a></span>  <span class="keyword">static</span> Lit <a class="code" href="classXchaff.html#a216cb72b0a5a4568ef9a0eb430b2d933">mkLit</a>(<span class="keywordtype">int</span> <span class="keywordtype">id</span>) { Lit l; l.<a class="code" href="unionSatSolver_1_1Lit.html#a96b4ad90adf8a2d6eee7af2c5b351481">id</a> = id; <span class="keywordflow">return</span> l; }</div>
<div class="line"><a name="l00026"></a><span class="lineno"><a class="code" href="classXchaff.html#a68161914638f53d93a26ff242e437472"> 26</a></span>  <span class="keyword">static</span> <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="code" href="classXchaff.html#a68161914638f53d93a26ff242e437472">mkClause</a>(<span class="keywordtype">int</span> <span class="keywordtype">id</span>) { <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> c; c.<a class="code" href="unionSatSolver_1_1Clause.html#a525bdedc03ca4e24251a3b715fc35da8">id</a> = id; <span class="keywordflow">return</span> c; }</div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> </div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00029"></a><span class="lineno"><a class="code" href="classXchaff.html#aa238850d5f8f2eb815548745d5b8304a"> 29</a></span>  <a class="code" href="classXchaff.html#aa238850d5f8f2eb815548745d5b8304a">Xchaff</a>() { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a> = <span class="keyword">new</span> <a class="code" href="classCSolver.html">CSolver</a>; }</div>
<div class="line"><a name="l00030"></a><span class="lineno"><a class="code" href="classXchaff.html#adef92a80a3bbac1de8b94acb37cace6c"> 30</a></span>  <a class="code" href="classXchaff.html#adef92a80a3bbac1de8b94acb37cace6c">~Xchaff</a>() { <span class="keyword">delete</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>; }</div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span> <span class="comment"></span></div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span> <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> <span class="comment"></span> <span class="comment">// Implementation of SAT_API //</span><span class="comment"></span></div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span> <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span> <span class="comment"></span></div>
<div class="line"><a name="l00036"></a><span class="lineno"><a class="code" href="classXchaff.html#a271a1d5d92cf07c60d70a9939d623391"> 36</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a271a1d5d92cf07c60d70a9939d623391">NumVariables</a>()</div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#ac95e4d7648334447162c0fb4e3de28d7">num_variables</a>(); }</div>
<div class="line"><a name="l00038"></a><span class="lineno"><a class="code" href="classXchaff.html#a510ddbd9f083c5372bdaf5f449f4846b"> 38</a></span>  <a class="code" href="unionSatSolver_1_1Var.html">Var</a> <a class="code" href="classXchaff.html#a510ddbd9f083c5372bdaf5f449f4846b">AddVariables</a>(<span class="keywordtype">int</span> nvars)</div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68">mkVar</a>(<a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a1b1f7e9d95712bd0852366c044a5829f">add_variables</a>(nvars)); }</div>
<div class="line"><a name="l00040"></a><span class="lineno"><a class="code" href="classXchaff.html#a41296b8c022c75dd7e2233631a5ac704"> 40</a></span>  <a class="code" href="unionSatSolver_1_1Var.html">Var</a> <a class="code" href="classXchaff.html#a41296b8c022c75dd7e2233631a5ac704">GetVar</a>(<span class="keywordtype">int</span> varIndex)</div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68">mkVar</a>(varIndex); }</div>
<div class="line"><a name="l00042"></a><span class="lineno"><a class="code" href="classXchaff.html#a4f9ad9e1ff0a150b3f8fad414912cd9e"> 42</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a4f9ad9e1ff0a150b3f8fad414912cd9e">GetVarIndex</a>(<a class="code" href="unionSatSolver_1_1Var.html">Var</a> v)</div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span>  { <span class="keywordflow">return</span> v.<a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a>; }</div>
<div class="line"><a name="l00044"></a><span class="lineno"><a class="code" href="classXchaff.html#ac3891ccb7f41fb72e294da3899779c62"> 44</a></span>  <a class="code" href="unionSatSolver_1_1Var.html">Var</a> <a class="code" href="classXchaff.html#ac3891ccb7f41fb72e294da3899779c62">GetFirstVar</a>()</div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span>  { <a class="code" href="unionSatSolver_1_1Var.html">Var</a> v; <span class="keywordflow">if</span> (<a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#ac95e4d7648334447162c0fb4e3de28d7">num_variables</a>() != 0) v.<a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a> = 1; <span class="keywordflow">return</span> v; }</div>
<div class="line"><a name="l00046"></a><span class="lineno"><a class="code" href="classXchaff.html#aff81fd8f5d3c694e8f5112077142ea03"> 46</a></span>  <a class="code" href="unionSatSolver_1_1Var.html">Var</a> <a class="code" href="classXchaff.html#aff81fd8f5d3c694e8f5112077142ea03">GetNextVar</a>(<a class="code" href="unionSatSolver_1_1Var.html">Var</a> var)</div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span>  { <a class="code" href="unionSatSolver_1_1Var.html">Var</a> v;</div>
<div class="line"><a name="l00048"></a><span class="lineno"> 48</span>  <span class="keywordflow">if</span> (var.<a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a> != <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#ac95e4d7648334447162c0fb4e3de28d7">num_variables</a>()) v.<a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a> = var.<a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a>+1; <span class="keywordflow">return</span> v; }</div>
<div class="line"><a name="l00049"></a><span class="lineno"><a class="code" href="classXchaff.html#a9e916fd4048dfdcfdec013481e970303"> 49</a></span>  Lit <a class="code" href="classXchaff.html#a9e916fd4048dfdcfdec013481e970303">MakeLit</a>(<a class="code" href="unionSatSolver_1_1Var.html">Var</a> var, <span class="keywordtype">int</span> phase)</div>
<div class="line"><a name="l00050"></a><span class="lineno"> 50</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#a216cb72b0a5a4568ef9a0eb430b2d933">mkLit</a>((var.<a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a> << 1)+phase); }</div>
<div class="line"><a name="l00051"></a><span class="lineno"><a class="code" href="classXchaff.html#a40ebc0c7f213c049c561cf0f727dfab9"> 51</a></span>  <a class="code" href="unionSatSolver_1_1Var.html">Var</a> <a class="code" href="classXchaff.html#a40ebc0c7f213c049c561cf0f727dfab9">GetVarFromLit</a>(Lit lit)</div>
<div class="line"><a name="l00052"></a><span class="lineno"> 52</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68">mkVar</a>(lit.id >> 1); }</div>
<div class="line"><a name="l00053"></a><span class="lineno"><a class="code" href="classXchaff.html#ac6e0c04b5b1af99b742f444a32bdddf5"> 53</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#ac6e0c04b5b1af99b742f444a32bdddf5">GetPhaseFromLit</a>(Lit lit)</div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span>  { <span class="keywordflow">return</span> lit.id & 1; }</div>
<div class="line"><a name="l00055"></a><span class="lineno"><a class="code" href="classXchaff.html#a1a3fb172ed4b688d7938e160cc00716b"> 55</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a1a3fb172ed4b688d7938e160cc00716b">NumClauses</a>()</div>
<div class="line"><a name="l00056"></a><span class="lineno"> 56</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#a1ea198396d083b323c22cd49cc2be36c">num_clauses</a>(); }</div>
<div class="line"><a name="l00057"></a><span class="lineno"><a class="code" href="classXchaff.html#adee5769adfc8bc73e27117eacd1d5e06"> 57</a></span>  <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="code" href="classXchaff.html#adee5769adfc8bc73e27117eacd1d5e06">AddClause</a>(std::vector<Lit>& lits)</div>
<div class="line"><a name="l00058"></a><span class="lineno"> 58</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#a68161914638f53d93a26ff242e437472">mkClause</a>(<a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a5f90fcc1b1a7994a94fc8395d95cfb38">add_clause</a>((std::vector<long>&)lits)); }</div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span>  Clause <a class="code" href="classXchaff.html#aa7755a77a17224ef7540ff9cf475ebe0">GetClause</a>(<span class="keywordtype">int</span> clauseIndex);</div>
<div class="line"><a name="l00060"></a><span class="lineno"><a class="code" href="classXchaff.html#a4683a3d3e3c9ea39da714c76f0aa4471"> 60</a></span>  <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="code" href="classXchaff.html#a4683a3d3e3c9ea39da714c76f0aa4471">GetFirstClause</a>()</div>
<div class="line"><a name="l00061"></a><span class="lineno"> 61</span>  { <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> c;</div>
<div class="line"><a name="l00062"></a><span class="lineno"> 62</span>  <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i=0; i< <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#a0c2329a20ee0a2672475933c3edd888e">clauses</a>().size(); ++i)</div>
<div class="line"><a name="l00063"></a><span class="lineno"> 63</span>  <span class="keywordflow">if</span> ( <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(i).<a class="code" href="classCClause.html#accc3ecb433cd7ba00affc3180b0911d4">in_use</a>()) { c.<a class="code" href="unionSatSolver_1_1Clause.html#a525bdedc03ca4e24251a3b715fc35da8">id</a> = i; <span class="keywordflow">break</span>; }</div>
<div class="line"><a name="l00064"></a><span class="lineno"> 64</span>  <span class="keywordflow">return</span> c; }</div>
<div class="line"><a name="l00065"></a><span class="lineno"><a class="code" href="classXchaff.html#af02ffc8cb39e8740a7536323ee937d76"> 65</a></span>  <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="code" href="classXchaff.html#af02ffc8cb39e8740a7536323ee937d76">GetNextClause</a>(<a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> clause)</div>
<div class="line"><a name="l00066"></a><span class="lineno"> 66</span>  { <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> c;</div>
<div class="line"><a name="l00067"></a><span class="lineno"> 67</span>  <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i= clause.<a class="code" href="unionSatSolver_1_1Clause.html#a525bdedc03ca4e24251a3b715fc35da8">id</a> + 1; i< _solver->clauses().size(); ++i)</div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span>  <span class="keywordflow">if</span> ( <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(i).<a class="code" href="classCClause.html#accc3ecb433cd7ba00affc3180b0911d4">in_use</a>()) { c.<a class="code" href="unionSatSolver_1_1Clause.html#a525bdedc03ca4e24251a3b715fc35da8">id</a> = i; <span class="keywordflow">break</span>; }</div>
<div class="line"><a name="l00069"></a><span class="lineno"> 69</span>  <span class="keywordflow">return</span> c; }</div>
<div class="line"><a name="l00070"></a><span class="lineno"> 70</span>  <span class="keywordtype">void</span> <a class="code" href="classXchaff.html#ad55fdf1df93621b0f79859f9180eed8c">GetClauseLits</a>(<a class="code" href="unionSatSolver_1_1Clause.html">SatSolver::Clause</a> clause, std::vector<Lit>* lits);</div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span>  <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> <a class="code" href="classXchaff.html#af833605af7d820b9d7a350a77cd41ed1">Satisfiable</a>(<span class="keywordtype">bool</span> allowNewClauses);</div>
<div class="line"><a name="l00072"></a><span class="lineno"><a class="code" href="classXchaff.html#a00d874effad75d5544cdd9d257b2573d"> 72</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a00d874effad75d5544cdd9d257b2573d">GetVarAssignment</a>(<a class="code" href="unionSatSolver_1_1Var.html">Var</a> var)</div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(var.<a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a>).<a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>(); }</div>
<div class="line"><a name="l00074"></a><span class="lineno"> 74</span> </div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span>  <span class="comment">// Not implemented yet:</span></div>
<div class="line"><a name="l00076"></a><span class="lineno"> 76</span>  <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> <a class="code" href="classXchaff.html#ab20bcd7cd57b138b62e63d0e1d9a425f">Continue</a>();</div>
<div class="line"><a name="l00077"></a><span class="lineno"><a class="code" href="classXchaff.html#a53ce24894150638b3285f7b12ebf23ba"> 77</a></span>  <span class="keywordtype">void</span> <a class="code" href="classXchaff.html#a53ce24894150638b3285f7b12ebf23ba">Restart</a>() { assert(0); }</div>
<div class="line"><a name="l00078"></a><span class="lineno"><a class="code" href="classXchaff.html#ae8d8fe530dede206922f26f52f1cafcf"> 78</a></span>  <span class="keywordtype">void</span> <a class="code" href="classXchaff.html#ae8d8fe530dede206922f26f52f1cafcf">Reset</a>() { assert(0); }</div>
<div class="line"><a name="l00079"></a><span class="lineno"> 79</span> </div>
<div class="line"><a name="l00080"></a><span class="lineno"><a class="code" href="classXchaff.html#a9826417dcd2303591eaeb3259ac154f9"> 80</a></span>  <span class="keywordtype">void</span> <a class="code" href="classXchaff.html#a9826417dcd2303591eaeb3259ac154f9">RegisterDLevelHook</a>(<span class="keywordtype">void</span> (*f)(<span class="keywordtype">void</span> *, <span class="keywordtype">int</span>), <span class="keywordtype">void</span> *cookie)</div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span>  { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#aa0f5bd7cea8ed3bc7254e29d744566fb">RegisterDLevelHook</a>(f, cookie); }</div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span> </div>
<div class="line"><a name="l00083"></a><span class="lineno"><a class="code" href="classXchaff.html#ab42f8b43c2bc455a30955f4e8b8b4b9b"> 83</a></span>  <span class="keyword">static</span> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#ab42f8b43c2bc455a30955f4e8b8b4b9b">TranslateDecisionHook</a>(<span class="keywordtype">void</span> *cookie, <span class="keywordtype">bool</span> *done)</div>
<div class="line"><a name="l00084"></a><span class="lineno"> 84</span>  {</div>
<div class="line"><a name="l00085"></a><span class="lineno"> 85</span>  <a class="code" href="classXchaff.html">Xchaff</a> *b = (<a class="code" href="classXchaff.html">Xchaff</a>*)cookie;</div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span>  Lit lit = b-><a class="code" href="classXchaff.html#a745565adebc2ce37a9781e03860ba8ca">_decision_hook</a>(b-><a class="code" href="classXchaff.html#ac3a215c0cf6649a72471e5559e3e6f04">_decision_hook_cookie</a>, done);</div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span>  <span class="keywordflow">return</span> lit.<a class="code" href="unionSatSolver_1_1Lit.html#a96b4ad90adf8a2d6eee7af2c5b351481">id</a>;</div>
<div class="line"><a name="l00088"></a><span class="lineno"> 88</span>  }</div>
<div class="line"><a name="l00089"></a><span class="lineno"> 89</span> </div>
<div class="line"><a name="l00090"></a><span class="lineno"><a class="code" href="classXchaff.html#a029881b7aad15145d313fae454637a6a"> 90</a></span>  <span class="keywordtype">void</span> <a class="code" href="classXchaff.html#a029881b7aad15145d313fae454637a6a">RegisterDecisionHook</a>(Lit (*f)(<span class="keywordtype">void</span> *, <span class="keywordtype">bool</span> *), <span class="keywordtype">void</span> *cookie)</div>
<div class="line"><a name="l00091"></a><span class="lineno"> 91</span>  { <a class="code" href="classXchaff.html#a745565adebc2ce37a9781e03860ba8ca">_decision_hook</a> = f; <a class="code" href="classXchaff.html#ac3a215c0cf6649a72471e5559e3e6f04">_decision_hook_cookie</a> = cookie;</div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span>  <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#aac7bf85fb8516ff4b3478598306fcb2e">RegisterDecisionHook</a>(<a class="code" href="classXchaff.html#ab42f8b43c2bc455a30955f4e8b8b4b9b">TranslateDecisionHook</a>, <span class="keyword">this</span>); }</div>
<div class="line"><a name="l00093"></a><span class="lineno"> 93</span> </div>
<div class="line"><a name="l00094"></a><span class="lineno"><a class="code" href="classXchaff.html#a393a5a2f7d45b4ffc54c00a5afbefd28"> 94</a></span>  <span class="keyword">static</span> <span class="keywordtype">void</span> <a class="code" href="classXchaff.html#a393a5a2f7d45b4ffc54c00a5afbefd28">TranslateAssignmentHook</a>(<span class="keywordtype">void</span> *cookie, <span class="keywordtype">int</span> var, <span class="keywordtype">int</span> value)</div>
<div class="line"><a name="l00095"></a><span class="lineno"> 95</span>  {</div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span>  <a class="code" href="classXchaff.html">Xchaff</a> *b = (<a class="code" href="classXchaff.html">Xchaff</a>*)cookie;</div>
<div class="line"><a name="l00097"></a><span class="lineno"> 97</span>  b-><a class="code" href="classXchaff.html#a7680ebfc3431daea429904672209fdb8">_assignment_hook</a>(b-><a class="code" href="classXchaff.html#aff3437eb408419a6c84e9ff923ef5444">_assignment_hook_cookie</a>, <a class="code" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68">mkVar</a>(var), value);</div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span>  }</div>
<div class="line"><a name="l00099"></a><span class="lineno"> 99</span> </div>
<div class="line"><a name="l00100"></a><span class="lineno"><a class="code" href="classXchaff.html#a0a98f9f270df69b9f86d15258b915afb"> 100</a></span>  <span class="keywordtype">void</span> <a class="code" href="classXchaff.html#a0a98f9f270df69b9f86d15258b915afb">RegisterAssignmentHook</a>(<span class="keywordtype">void</span> (*f)(<span class="keywordtype">void</span> *, <a class="code" href="unionSatSolver_1_1Var.html">Var</a>, <span class="keywordtype">int</span>), <span class="keywordtype">void</span> *cookie)</div>
<div class="line"><a name="l00101"></a><span class="lineno"> 101</span>  { <a class="code" href="classXchaff.html#a7680ebfc3431daea429904672209fdb8">_assignment_hook</a> = f; <a class="code" href="classXchaff.html#aff3437eb408419a6c84e9ff923ef5444">_assignment_hook_cookie</a> = cookie;</div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span>  <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#afcbec396917ed73948a67db3732054ae">RegisterAssignmentHook</a>(<a class="code" href="classXchaff.html#a393a5a2f7d45b4ffc54c00a5afbefd28">TranslateAssignmentHook</a>, <span class="keyword">this</span>); }</div>
<div class="line"><a name="l00103"></a><span class="lineno"><a class="code" href="classXchaff.html#a2ffce1f21eb64712d4e26e1dbc4b0e36"> 103</a></span>  <span class="keywordtype">void</span> <a class="code" href="classXchaff.html#a2ffce1f21eb64712d4e26e1dbc4b0e36">RegisterDeductionHook</a>(<span class="keywordtype">void</span> (*f)(<span class="keywordtype">void</span> *), <span class="keywordtype">void</span> *cookie)</div>
<div class="line"><a name="l00104"></a><span class="lineno"> 104</span>  { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a5aeafd67c7a77683ae040c11fbf033b1">RegisterDeductionHook</a>(f, cookie); }</div>
<div class="line"><a name="l00105"></a><span class="lineno"><a class="code" href="classXchaff.html#aae25937c3c0f355220a4533fb127edf7"> 105</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#aae25937c3c0f355220a4533fb127edf7">SetBudget</a>(<span class="keywordtype">int</span> budget) <span class="comment">// budget is time in seconds</span></div>
<div class="line"><a name="l00106"></a><span class="lineno"> 106</span>  { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a19c6655c87bd6117db6510183dad2893">set_time_limit</a>(<span class="keywordtype">float</span>(budget)); <span class="keywordflow">return</span> <span class="keyword">true</span>; }</div>
<div class="line"><a name="l00107"></a><span class="lineno"><a class="code" href="classXchaff.html#a58905ab92772d4603d41b8155a59f0c2"> 107</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#a58905ab92772d4603d41b8155a59f0c2">SetMemLimit</a>(<span class="keywordtype">int</span> mem_limit)</div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span>  { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a069343e0391a7b95510634c9c96bb66f">set_mem_limit</a>(mem_limit); <span class="keywordflow">return</span> <span class="keyword">true</span>; }</div>
<div class="line"><a name="l00109"></a><span class="lineno"><a class="code" href="classXchaff.html#aa334fc9dd8673ff86d7214e439986e57"> 109</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#aa334fc9dd8673ff86d7214e439986e57">SetRandomness</a>(<span class="keywordtype">int</span> n)</div>
<div class="line"><a name="l00110"></a><span class="lineno"> 110</span>  { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a17438ece1aeb9736e73bc25b96def58d">set_randomness</a>(n); <span class="keywordflow">return</span> <span class="keyword">true</span>; }</div>
<div class="line"><a name="l00111"></a><span class="lineno"><a class="code" href="classXchaff.html#a390d585a7258c0237ea17893587d1ee0"> 111</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#a390d585a7258c0237ea17893587d1ee0">SetRandSeed</a>(<span class="keywordtype">int</span> seed)</div>
<div class="line"><a name="l00112"></a><span class="lineno"> 112</span>  { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a6765f3784e94ebde4c86447845e67c1d">set_random_seed</a>(seed); <span class="keywordflow">return</span> <span class="keyword">true</span>; }</div>
<div class="line"><a name="l00113"></a><span class="lineno"><a class="code" href="classXchaff.html#a8a481eb175d81a80556e13ecff483da1"> 113</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#a8a481eb175d81a80556e13ecff483da1">EnableClauseDeletion</a>()</div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span>  { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#ad61a4e50bc8640852b7cd9d2cbd423d0">enable_cls_deletion</a>(<span class="keyword">true</span>); <span class="keywordflow">return</span> <span class="keyword">true</span>; }</div>
<div class="line"><a name="l00115"></a><span class="lineno"><a class="code" href="classXchaff.html#ab763aebc2ca5e3b489aab695ed469213"> 115</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#ab763aebc2ca5e3b489aab695ed469213">DisableClauseDeletion</a>()</div>
<div class="line"><a name="l00116"></a><span class="lineno"> 116</span>  { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#ad61a4e50bc8640852b7cd9d2cbd423d0">enable_cls_deletion</a>(<span class="keyword">false</span>); <span class="keywordflow">return</span> <span class="keyword">true</span>; }</div>
<div class="line"><a name="l00117"></a><span class="lineno"><a class="code" href="classXchaff.html#a90a038ad50d710508f2f3c0a3f909528"> 117</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a90a038ad50d710508f2f3c0a3f909528">GetBudgetUsed</a>()</div>
<div class="line"><a name="l00118"></a><span class="lineno"> 118</span>  { <span class="keywordflow">return</span> int(<a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#afde50f1cee0bab34e2464b17693d59f7">total_run_time</a>()); }</div>
<div class="line"><a name="l00119"></a><span class="lineno"><a class="code" href="classXchaff.html#ad483bd394ba347d90afb2354a3579d5b"> 119</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#ad483bd394ba347d90afb2354a3579d5b">GetMemUsed</a>()</div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a6a7cefe78a6f785c2c51950a74dde6d8">estimate_mem_usage</a>(); }</div>
<div class="line"><a name="l00121"></a><span class="lineno"><a class="code" href="classXchaff.html#a0ae00dfb15ac6f1f6947056c448cc4db"> 121</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a0ae00dfb15ac6f1f6947056c448cc4db">GetNumDecisions</a>()</div>
<div class="line"><a name="l00122"></a><span class="lineno"> 122</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a1d592aab62ad4f2943e0687916a34397">num_decisions</a>(); }</div>
<div class="line"><a name="l00123"></a><span class="lineno"><a class="code" href="classXchaff.html#aafeebd0e319671ade2b15418a5491aa1"> 123</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#aafeebd0e319671ade2b15418a5491aa1">GetNumConflicts</a>()</div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span>  { <span class="keywordflow">return</span> -1; }</div>
<div class="line"><a name="l00125"></a><span class="lineno"><a class="code" href="classXchaff.html#aa0c48459562f98b52b01999bb7c394ec"> 125</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#aa0c48459562f98b52b01999bb7c394ec">GetNumExtConflicts</a>()</div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span>  { <span class="keywordflow">return</span> -1; }</div>
<div class="line"><a name="l00127"></a><span class="lineno"><a class="code" href="classXchaff.html#a554b43a08c1aadad56bcb16d7a5ae8f5"> 127</a></span>  <span class="keywordtype">float</span> <a class="code" href="classXchaff.html#a554b43a08c1aadad56bcb16d7a5ae8f5">GetTotalTime</a>()</div>
<div class="line"><a name="l00128"></a><span class="lineno"> 128</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#afde50f1cee0bab34e2464b17693d59f7">total_run_time</a>(); }</div>
<div class="line"><a name="l00129"></a><span class="lineno"><a class="code" href="classXchaff.html#a892c44f9b8bd6bb98a57c67f6e0261fa"> 129</a></span>  <span class="keywordtype">float</span> <a class="code" href="classXchaff.html#a892c44f9b8bd6bb98a57c67f6e0261fa">GetSATTime</a>()</div>
<div class="line"><a name="l00130"></a><span class="lineno"> 130</span>  { <span class="keywordflow">return</span> -1; }</div>
<div class="line"><a name="l00131"></a><span class="lineno"><a class="code" href="classXchaff.html#aefa4cd2058553d7946cbebdb667e8670"> 131</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#aefa4cd2058553d7946cbebdb667e8670">GetNumLiterals</a>()</div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#a93f69dacd75d1cf2d4a006b961f3b7b6">num_literals</a>(); }</div>
<div class="line"><a name="l00133"></a><span class="lineno"><a class="code" href="classXchaff.html#a6f69523569c280d1486b7c6ddde2b112"> 133</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a6f69523569c280d1486b7c6ddde2b112">GetNumDeletedClauses</a>()</div>
<div class="line"><a name="l00134"></a><span class="lineno"> 134</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#ad386f2990781ab78ebbe6eb83b7c365e">num_deleted_clauses</a>(); }</div>
<div class="line"><a name="l00135"></a><span class="lineno"><a class="code" href="classXchaff.html#a0939c01d21987c020eb5fa783af11164"> 135</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a0939c01d21987c020eb5fa783af11164">GetNumDeletedLiterals</a>()</div>
<div class="line"><a name="l00136"></a><span class="lineno"> 136</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#a3e0c56c9059f90ce0b3ba0f94e2aeed2">num_deleted_literals</a>(); }</div>
<div class="line"><a name="l00137"></a><span class="lineno"><a class="code" href="classXchaff.html#aec9cba92c3e56ed8aa68693c6083e54d"> 137</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#aec9cba92c3e56ed8aa68693c6083e54d">GetNumImplications</a>()</div>
<div class="line"><a name="l00138"></a><span class="lineno"> 138</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#ac1c4a48d4db9e61bc657a633b7230b88">num_implications</a>(); }</div>
<div class="line"><a name="l00139"></a><span class="lineno"><a class="code" href="classXchaff.html#a4ff03b5c032c7344058759ef1165ad9e"> 139</a></span>  <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a4ff03b5c032c7344058759ef1165ad9e">GetMaxDLevel</a>()</div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span>  { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">max_dlevel</a>(); }</div>
<div class="line"><a name="l00141"></a><span class="lineno"> 141</span> };</div>
<div class="line"><a name="l00142"></a><span class="lineno"> 142</span> </div>
<div class="line"><a name="l00143"></a><span class="lineno"> 143</span> <span class="preprocessor">#endif</span></div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00145"></a><span class="lineno"> 145</span> </div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span> </div>
<div class="line"><a name="l00147"></a><span class="lineno"> 147</span> </div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span> </div>
<div class="line"><a name="l00149"></a><span class="lineno"> 149</span> </div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span> </div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:16 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
