<!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.h Source File</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><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 class="header">
<div class="headertitle">
<div class="title">xchaff.h</div> </div>
</div>
<div class="contents">
<a href="xchaff_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00002"></a>00002 <span class="comment"></span><span class="comment">// //</span>
<a name="l00003"></a>00003 <span class="comment">// File: xchaff.h //</span>
<a name="l00004"></a>00004 <span class="comment">// Author: Clark Barrett //</span>
<a name="l00005"></a>00005 <span class="comment">// Created: Wed Oct 16 17:31:50 2002 //</span>
<a name="l00006"></a>00006 <span class="comment">// Description: Enhanced C++ API for Chaff //</span>
<a name="l00007"></a>00007 <span class="comment">// //</span><span class="comment"></span>
<a name="l00008"></a>00008 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00009"></a>00009 <span class="comment"></span>
<a name="l00010"></a>00010 <span class="preprocessor">#ifndef _XCHAFF_H_</span>
<a name="l00011"></a>00011 <span class="preprocessor"></span><span class="preprocessor">#define _XCHAFF_H_</span>
<a name="l00012"></a>00012 <span class="preprocessor"></span>
<a name="l00013"></a>00013 <span class="preprocessor">#include "<a class="code" href="sat__api_8h.html">sat_api.h</a>"</span>
<a name="l00014"></a>00014 <span class="preprocessor">#include "<a class="code" href="xchaff__solver_8h.html">xchaff_solver.h</a>"</span>
<a name="l00015"></a>00015
<a name="l00016"></a><a class="code" href="classXchaff.html">00016</a> <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> {
<a name="l00017"></a><a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">00017</a> <a class="code" href="classCSolver.html">CSolver</a> *<a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>;
<a name="l00018"></a>00018
<a name="l00019"></a><a class="code" href="classXchaff.html#a745565adebc2ce37a9781e03860ba8ca">00019</a> Lit (*<a class="code" href="classXchaff.html#a745565adebc2ce37a9781e03860ba8ca">_decision_hook</a>)(<span class="keywordtype">void</span> *, <span class="keywordtype">bool</span> *);
<a name="l00020"></a><a class="code" href="classXchaff.html#a7680ebfc3431daea429904672209fdb8">00020</a> 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);
<a name="l00021"></a><a class="code" href="classXchaff.html#ac3a215c0cf6649a72471e5559e3e6f04">00021</a> <span class="keywordtype">void</span> *<a class="code" href="classXchaff.html#ac3a215c0cf6649a72471e5559e3e6f04">_decision_hook_cookie</a>;
<a name="l00022"></a><a class="code" href="classXchaff.html#aff3437eb408419a6c84e9ff923ef5444">00022</a> <span class="keywordtype">void</span> *<a class="code" href="classXchaff.html#aff3437eb408419a6c84e9ff923ef5444">_assignment_hook_cookie</a>;
<a name="l00023"></a>00023
<a name="l00024"></a><a class="code" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68">00024</a> <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; }
<a name="l00025"></a><a class="code" href="classXchaff.html#a216cb72b0a5a4568ef9a0eb430b2d933">00025</a> <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; }
<a name="l00026"></a><a class="code" href="classXchaff.html#a68161914638f53d93a26ff242e437472">00026</a> <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; }
<a name="l00027"></a>00027
<a name="l00028"></a>00028 <span class="keyword">public</span>:
<a name="l00029"></a><a class="code" href="classXchaff.html#aa238850d5f8f2eb815548745d5b8304a">00029</a> <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>; }
<a name="l00030"></a><a class="code" href="classXchaff.html#adef92a80a3bbac1de8b94acb37cace6c">00030</a> <a class="code" href="classXchaff.html#adef92a80a3bbac1de8b94acb37cace6c">~Xchaff</a>() { <span class="keyword">delete</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>; }
<a name="l00031"></a>00031 <span class="comment"></span>
<a name="l00032"></a>00032 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00033"></a>00033 <span class="comment"></span> <span class="comment">// Implementation of SAT_API //</span><span class="comment"></span>
<a name="l00034"></a>00034 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00035"></a>00035 <span class="comment"></span>
<a name="l00036"></a><a class="code" href="classXchaff.html#a271a1d5d92cf07c60d70a9939d623391">00036</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a271a1d5d92cf07c60d70a9939d623391">NumVariables</a>()
<a name="l00037"></a>00037 { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#ac95e4d7648334447162c0fb4e3de28d7">num_variables</a>(); }
<a name="l00038"></a><a class="code" href="classXchaff.html#a510ddbd9f083c5372bdaf5f449f4846b">00038</a> <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)
<a name="l00039"></a>00039 { <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)); }
<a name="l00040"></a><a class="code" href="classXchaff.html#a41296b8c022c75dd7e2233631a5ac704">00040</a> <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)
<a name="l00041"></a>00041 { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68">mkVar</a>(varIndex); }
<a name="l00042"></a><a class="code" href="classXchaff.html#a4f9ad9e1ff0a150b3f8fad414912cd9e">00042</a> <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)
<a name="l00043"></a>00043 { <span class="keywordflow">return</span> v.<a class="code" href="unionSatSolver_1_1Var.html#a0dab20c0e01831dd8c30dd46fbeef533">id</a>; }
<a name="l00044"></a><a class="code" href="classXchaff.html#ac3891ccb7f41fb72e294da3899779c62">00044</a> <a class="code" href="unionSatSolver_1_1Var.html">Var</a> <a class="code" href="classXchaff.html#ac3891ccb7f41fb72e294da3899779c62">GetFirstVar</a>()
<a name="l00045"></a>00045 { <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; }
<a name="l00046"></a><a class="code" href="classXchaff.html#aff81fd8f5d3c694e8f5112077142ea03">00046</a> <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)
<a name="l00047"></a>00047 { <a class="code" href="unionSatSolver_1_1Var.html">Var</a> v;
<a name="l00048"></a>00048 <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; }
<a name="l00049"></a><a class="code" href="classXchaff.html#a9e916fd4048dfdcfdec013481e970303">00049</a> 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)
<a name="l00050"></a>00050 { <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); }
<a name="l00051"></a><a class="code" href="classXchaff.html#a40ebc0c7f213c049c561cf0f727dfab9">00051</a> <a class="code" href="unionSatSolver_1_1Var.html">Var</a> <a class="code" href="classXchaff.html#a40ebc0c7f213c049c561cf0f727dfab9">GetVarFromLit</a>(Lit lit)
<a name="l00052"></a>00052 { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68">mkVar</a>(lit.id >> 1); }
<a name="l00053"></a><a class="code" href="classXchaff.html#ac6e0c04b5b1af99b742f444a32bdddf5">00053</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#ac6e0c04b5b1af99b742f444a32bdddf5">GetPhaseFromLit</a>(Lit lit)
<a name="l00054"></a>00054 { <span class="keywordflow">return</span> lit.id & 1; }
<a name="l00055"></a><a class="code" href="classXchaff.html#a1a3fb172ed4b688d7938e160cc00716b">00055</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a1a3fb172ed4b688d7938e160cc00716b">NumClauses</a>()
<a name="l00056"></a>00056 { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#a1ea198396d083b323c22cd49cc2be36c">num_clauses</a>(); }
<a name="l00057"></a><a class="code" href="classXchaff.html#adee5769adfc8bc73e27117eacd1d5e06">00057</a> <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="code" href="classXchaff.html#adee5769adfc8bc73e27117eacd1d5e06">AddClause</a>(std::vector<Lit>& lits)
<a name="l00058"></a>00058 { <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)); }
<a name="l00059"></a>00059 Clause <a class="code" href="classXchaff.html#aa7755a77a17224ef7540ff9cf475ebe0">GetClause</a>(<span class="keywordtype">int</span> clauseIndex);
<a name="l00060"></a><a class="code" href="classXchaff.html#a4683a3d3e3c9ea39da714c76f0aa4471">00060</a> <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> <a class="code" href="classXchaff.html#a4683a3d3e3c9ea39da714c76f0aa4471">GetFirstClause</a>()
<a name="l00061"></a>00061 { <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> c;
<a name="l00062"></a>00062 <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)
<a name="l00063"></a>00063 <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>; }
<a name="l00064"></a>00064 <span class="keywordflow">return</span> c; }
<a name="l00065"></a><a class="code" href="classXchaff.html#af02ffc8cb39e8740a7536323ee937d76">00065</a> <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)
<a name="l00066"></a>00066 { <a class="code" href="unionSatSolver_1_1Clause.html">Clause</a> c;
<a name="l00067"></a>00067 <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)
<a name="l00068"></a>00068 <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>; }
<a name="l00069"></a>00069 <span class="keywordflow">return</span> c; }
<a name="l00070"></a>00070 <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);
<a name="l00071"></a>00071 <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);
<a name="l00072"></a><a class="code" href="classXchaff.html#a00d874effad75d5544cdd9d257b2573d">00072</a> <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)
<a name="l00073"></a>00073 { <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>(); }
<a name="l00074"></a>00074
<a name="l00075"></a>00075 <span class="comment">// Not implemented yet:</span>
<a name="l00076"></a>00076 <a class="code" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SatSolver::SATStatus</a> <a class="code" href="classXchaff.html#ab20bcd7cd57b138b62e63d0e1d9a425f">Continue</a>();
<a name="l00077"></a><a class="code" href="classXchaff.html#a53ce24894150638b3285f7b12ebf23ba">00077</a> <span class="keywordtype">void</span> <a class="code" href="classXchaff.html#a53ce24894150638b3285f7b12ebf23ba">Restart</a>() { assert(0); }
<a name="l00078"></a><a class="code" href="classXchaff.html#ae8d8fe530dede206922f26f52f1cafcf">00078</a> <span class="keywordtype">void</span> <a class="code" href="classXchaff.html#ae8d8fe530dede206922f26f52f1cafcf">Reset</a>() { assert(0); }
<a name="l00079"></a>00079
<a name="l00080"></a><a class="code" href="classXchaff.html#a9826417dcd2303591eaeb3259ac154f9">00080</a> <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)
<a name="l00081"></a>00081 { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#aa0f5bd7cea8ed3bc7254e29d744566fb">RegisterDLevelHook</a>(f, cookie); }
<a name="l00082"></a>00082
<a name="l00083"></a><a class="code" href="classXchaff.html#ab42f8b43c2bc455a30955f4e8b8b4b9b">00083</a> <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)
<a name="l00084"></a>00084 {
<a name="l00085"></a>00085 <a class="code" href="classXchaff.html">Xchaff</a> *b = (<a class="code" href="classXchaff.html">Xchaff</a>*)cookie;
<a name="l00086"></a>00086 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);
<a name="l00087"></a>00087 <span class="keywordflow">return</span> lit.<a class="code" href="unionSatSolver_1_1Lit.html#a96b4ad90adf8a2d6eee7af2c5b351481">id</a>;
<a name="l00088"></a>00088 }
<a name="l00089"></a>00089
<a name="l00090"></a><a class="code" href="classXchaff.html#a029881b7aad15145d313fae454637a6a">00090</a> <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)
<a name="l00091"></a>00091 { <a class="code" href="classXchaff.html#a745565adebc2ce37a9781e03860ba8ca">_decision_hook</a> = f; <a class="code" href="classXchaff.html#ac3a215c0cf6649a72471e5559e3e6f04">_decision_hook_cookie</a> = cookie;
<a name="l00092"></a>00092 <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>); }
<a name="l00093"></a>00093
<a name="l00094"></a><a class="code" href="classXchaff.html#a393a5a2f7d45b4ffc54c00a5afbefd28">00094</a> <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)
<a name="l00095"></a>00095 {
<a name="l00096"></a>00096 <a class="code" href="classXchaff.html">Xchaff</a> *b = (<a class="code" href="classXchaff.html">Xchaff</a>*)cookie;
<a name="l00097"></a>00097 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);
<a name="l00098"></a>00098 }
<a name="l00099"></a>00099
<a name="l00100"></a><a class="code" href="classXchaff.html#a0a98f9f270df69b9f86d15258b915afb">00100</a> <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)
<a name="l00101"></a>00101 { <a class="code" href="classXchaff.html#a7680ebfc3431daea429904672209fdb8">_assignment_hook</a> = f; <a class="code" href="classXchaff.html#aff3437eb408419a6c84e9ff923ef5444">_assignment_hook_cookie</a> = cookie;
<a name="l00102"></a>00102 <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>); }
<a name="l00103"></a><a class="code" href="classXchaff.html#a2ffce1f21eb64712d4e26e1dbc4b0e36">00103</a> <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)
<a name="l00104"></a>00104 { <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a5aeafd67c7a77683ae040c11fbf033b1">RegisterDeductionHook</a>(f, cookie); }
<a name="l00105"></a><a class="code" href="classXchaff.html#aae25937c3c0f355220a4533fb127edf7">00105</a> <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>
<a name="l00106"></a>00106 { <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>; }
<a name="l00107"></a><a class="code" href="classXchaff.html#a58905ab92772d4603d41b8155a59f0c2">00107</a> <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#a58905ab92772d4603d41b8155a59f0c2">SetMemLimit</a>(<span class="keywordtype">int</span> mem_limit)
<a name="l00108"></a>00108 { <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>; }
<a name="l00109"></a><a class="code" href="classXchaff.html#aa334fc9dd8673ff86d7214e439986e57">00109</a> <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#aa334fc9dd8673ff86d7214e439986e57">SetRandomness</a>(<span class="keywordtype">int</span> n)
<a name="l00110"></a>00110 { <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>; }
<a name="l00111"></a><a class="code" href="classXchaff.html#a390d585a7258c0237ea17893587d1ee0">00111</a> <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#a390d585a7258c0237ea17893587d1ee0">SetRandSeed</a>(<span class="keywordtype">int</span> seed)
<a name="l00112"></a>00112 { <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>; }
<a name="l00113"></a><a class="code" href="classXchaff.html#a8a481eb175d81a80556e13ecff483da1">00113</a> <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#a8a481eb175d81a80556e13ecff483da1">EnableClauseDeletion</a>()
<a name="l00114"></a>00114 { <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>; }
<a name="l00115"></a><a class="code" href="classXchaff.html#ab763aebc2ca5e3b489aab695ed469213">00115</a> <span class="keywordtype">bool</span> <a class="code" href="classXchaff.html#ab763aebc2ca5e3b489aab695ed469213">DisableClauseDeletion</a>()
<a name="l00116"></a>00116 { <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>; }
<a name="l00117"></a><a class="code" href="classXchaff.html#a90a038ad50d710508f2f3c0a3f909528">00117</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a90a038ad50d710508f2f3c0a3f909528">GetBudgetUsed</a>()
<a name="l00118"></a>00118 { <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>()); }
<a name="l00119"></a><a class="code" href="classXchaff.html#ad483bd394ba347d90afb2354a3579d5b">00119</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#ad483bd394ba347d90afb2354a3579d5b">GetMemUsed</a>()
<a name="l00120"></a>00120 { <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>(); }
<a name="l00121"></a><a class="code" href="classXchaff.html#a0ae00dfb15ac6f1f6947056c448cc4db">00121</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a0ae00dfb15ac6f1f6947056c448cc4db">GetNumDecisions</a>()
<a name="l00122"></a>00122 { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a1d592aab62ad4f2943e0687916a34397">num_decisions</a>(); }
<a name="l00123"></a><a class="code" href="classXchaff.html#aafeebd0e319671ade2b15418a5491aa1">00123</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#aafeebd0e319671ade2b15418a5491aa1">GetNumConflicts</a>()
<a name="l00124"></a>00124 { <span class="keywordflow">return</span> -1; }
<a name="l00125"></a><a class="code" href="classXchaff.html#aa0c48459562f98b52b01999bb7c394ec">00125</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#aa0c48459562f98b52b01999bb7c394ec">GetNumExtConflicts</a>()
<a name="l00126"></a>00126 { <span class="keywordflow">return</span> -1; }
<a name="l00127"></a><a class="code" href="classXchaff.html#a554b43a08c1aadad56bcb16d7a5ae8f5">00127</a> <span class="keywordtype">float</span> <a class="code" href="classXchaff.html#a554b43a08c1aadad56bcb16d7a5ae8f5">GetTotalTime</a>()
<a name="l00128"></a>00128 { <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>(); }
<a name="l00129"></a><a class="code" href="classXchaff.html#a892c44f9b8bd6bb98a57c67f6e0261fa">00129</a> <span class="keywordtype">float</span> <a class="code" href="classXchaff.html#a892c44f9b8bd6bb98a57c67f6e0261fa">GetSATTime</a>()
<a name="l00130"></a>00130 { <span class="keywordflow">return</span> -1; }
<a name="l00131"></a><a class="code" href="classXchaff.html#aefa4cd2058553d7946cbebdb667e8670">00131</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#aefa4cd2058553d7946cbebdb667e8670">GetNumLiterals</a>()
<a name="l00132"></a>00132 { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCDatabase.html#a93f69dacd75d1cf2d4a006b961f3b7b6">num_literals</a>(); }
<a name="l00133"></a><a class="code" href="classXchaff.html#a6f69523569c280d1486b7c6ddde2b112">00133</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a6f69523569c280d1486b7c6ddde2b112">GetNumDeletedClauses</a>()
<a name="l00134"></a>00134 { <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>(); }
<a name="l00135"></a><a class="code" href="classXchaff.html#a0939c01d21987c020eb5fa783af11164">00135</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a0939c01d21987c020eb5fa783af11164">GetNumDeletedLiterals</a>()
<a name="l00136"></a>00136 { <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>(); }
<a name="l00137"></a><a class="code" href="classXchaff.html#aec9cba92c3e56ed8aa68693c6083e54d">00137</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#aec9cba92c3e56ed8aa68693c6083e54d">GetNumImplications</a>()
<a name="l00138"></a>00138 { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#ac1c4a48d4db9e61bc657a633b7230b88">num_implications</a>(); }
<a name="l00139"></a><a class="code" href="classXchaff.html#a4ff03b5c032c7344058759ef1165ad9e">00139</a> <span class="keywordtype">int</span> <a class="code" href="classXchaff.html#a4ff03b5c032c7344058759ef1165ad9e">GetMaxDLevel</a>()
<a name="l00140"></a>00140 { <span class="keywordflow">return</span> <a class="code" href="classXchaff.html#ad12d883fd228bfbabd7cbe96e75fb9e1">_solver</a>-><a class="code" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">max_dlevel</a>(); }
<a name="l00141"></a>00141 };
<a name="l00142"></a>00142
<a name="l00143"></a>00143 <span class="preprocessor">#endif</span>
<a name="l00144"></a>00144 <span class="preprocessor"></span>
<a name="l00145"></a>00145
<a name="l00146"></a>00146
<a name="l00147"></a>00147
<a name="l00148"></a>00148
<a name="l00149"></a>00149
<a name="l00150"></a>00150
</pre></div></div>
</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>
