<!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: CVariable Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> |
<a href="#friends">Friends</a> </div>
<div class="headertitle">
<div class="title">CVariable Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVariable" -->
<p><code>#include <<a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>></code></p>
<p><a href="classCVariable-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li>int & <a class="el" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a> (int i)
<li>int <a class="el" href="classCVariable.html#a519b8d883ea489998f7cabd31fae1ddb">score</a> (void)
<li>int & <a class="el" href="classCVariable.html#a5d0f657e55242e1324c345bb8f6c9877">var_score_pos</a> (void)
<li><a class="el" href="classCVariable.html#ac4db0d1a0f6c5a42a2a746dff0013019">CVariable</a> (void)
<li>short & <a class="el" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a> (void)
<li>short & <a class="el" href="classCVariable.html#aedac20571208b480adb2aff58797981a">dlevel</a> (void)
<li>int <a class="el" href="classCVariable.html#a106db2a07df4461da1ccfdf17faa8cdf">in_new_cl</a> (void)
<li>void <a class="el" href="classCVariable.html#a74c853f04808a514d7c99514a7583e2d">set_in_new_cl</a> (int phase)
<li>int & <a class="el" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a> (int i)
<li>bool <a class="el" href="classCVariable.html#a8be2f24a39402da9c9047c701c0e0486">is_marked</a> (void)
<li>void <a class="el" href="classCVariable.html#a605e80794f39e7aa307d94fd13017431">set_marked</a> (void)
<li>void <a class="el" href="classCVariable.html#a474d619248f352afcaa3fd4fb6c8788d">clear_marked</a> (void)
<li><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> <a class="el" href="classCVariable.html#a92a4c6ae0e4b566d1f664add2aeb39e9">get_antecedence</a> (void)
<li>void <a class="el" href="classCVariable.html#ab10578bfddce9b0dfb959b84395d799c">set_antecedence</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> ante)
<li>vector< <a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * > & <a class="el" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a> (int i)
<li>void <a class="el" href="classCVariable.html#ae03057639e30c735148c083c2305ae75">dump</a> (ostream &os=cout)
</ul>
<h2><a name="pro-attribs"></a>
Protected Attributes</h2>
<ul>
<li>bool <a class="el" href="classCVariable.html#a50e9a718302d737d0108c7aa443a842a">_is_marked</a>: 1
<li>int <a class="el" href="classCVariable.html#ab84b85036f11ce8252d38cfab388ff4b">_in_new_cl</a>: 2
<li><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> <a class="el" href="classCVariable.html#add75b1771456c8373c055ce56795abb7">_antecedence</a>: 29
<li>short <a class="el" href="classCVariable.html#a68bb88b73fda42d5076bc8a34c490b33">_value</a>
<li>short <a class="el" href="classCVariable.html#aa099734654610fbe932b440ae9550cb6">_dlevel</a>
<li>vector< <a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * > <a class="el" href="classCVariable.html#aa33dc62f930de685f1e0a69c3c1c2cef">_ht_ptrs</a> [2]
<li>int <a class="el" href="classCVariable.html#a9b7f0efebea35da376d4db863bdfd2a9">_lits_count</a> [2]
<li>int <a class="el" href="classCVariable.html#a3679cd1ad89f8ae495bc8f31f36c0f60">_scores</a> [2]
<li>int <a class="el" href="classCVariable.html#ac0b464c860f8702f36f9e256836a4bf9">_var_score_pos</a>
</ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>ostream & <a class="el" href="classCVariable.html#ac3e0d4831cd8625025002e21998517cd">operator<<</a> (ostream &os, <a class="el" href="classCVariable.html">CVariable</a> &v)
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock"><p>Class**********************************************************************</p>
<p>Synopsis [Definition of a variable]</p>
<p>Description [<a class="el" href="classCVariable.html">CVariable</a> contains the necessary information for a variable. _ht_ptrs are the head/tail literals of this variable (int two phases)]</p>
<p>SeeAlso [<a class="el" href="classCDatabase.html">CDatabase</a>] </p>
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00224">224</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="ac4db0d1a0f6c5a42a2a746dff0013019"></a><!-- doxytag: member="CVariable::CVariable" ref="ac4db0d1a0f6c5a42a2a746dff0013019" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVariable::CVariable </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00254">254</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>References <a class="el" href="xchaff__base_8h_source.html#l00051">NULL_CLAUSE</a>, and <a class="el" href="xchaff__base_8h_source.html#l00048">UNKNOWN</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="acf5cbd17ee39aa733dd5445c5836ec81"></a><!-- doxytag: member="CVariable::score" ref="acf5cbd17ee39aa733dd5445c5836ec81" args="(int i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CVariable::score </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00249">249</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00617">CSolver::decide_next_branch()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00358">CSolver::restart()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00601">CSolver::update_var_stats()</a>.</p>
</div>
</div>
<a class="anchor" id="a519b8d883ea489998f7cabd31fae1ddb"></a><!-- doxytag: member="CVariable::score" ref="a519b8d883ea489998f7cabd31fae1ddb" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVariable::score </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00250">250</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>References <a class="el" href="xchaff__base_8h_source.html#l00250">score()</a>.</p>
<p>Referenced by <a class="el" href="xchaff__base_8h_source.html#l00250">score()</a>.</p>
</div>
</div>
<a class="anchor" id="a5d0f657e55242e1324c345bb8f6c9877"></a><!-- doxytag: member="CVariable::var_score_pos" ref="a5d0f657e55242e1324c345bb8f6c9877" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CVariable::var_score_pos </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00251">251</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00601">CSolver::update_var_stats()</a>.</p>
</div>
</div>
<a class="anchor" id="a7319394585df665256e74df1282f992f"></a><!-- doxytag: member="CVariable::value" ref="a7319394585df665256e74df1282f992f" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">short& CVariable::value </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00264">264</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00617">CSolver::decide_next_branch()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00852">CSolver::deduce()</a>, <a class="el" href="xchaff_8h_source.html#l00072">Xchaff::GetVarAssignment()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">CSolver::preprocess()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00296">CSolver::set_var_value()</a>.</p>
</div>
</div>
<a class="anchor" id="aedac20571208b480adb2aff58797981a"></a><!-- doxytag: member="CVariable::dlevel" ref="aedac20571208b480adb2aff58797981a" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">short& CVariable::dlevel </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00267">267</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">CSolver::preprocess()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00296">CSolver::set_var_value()</a>.</p>
</div>
</div>
<a class="anchor" id="a106db2a07df4461da1ccfdf17faa8cdf"></a><!-- doxytag: member="CVariable::in_new_cl" ref="a106db2a07df4461da1ccfdf17faa8cdf" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVariable::in_new_cl </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00270">270</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">CSolver::conflict_analysis_zchaff()</a>.</p>
</div>
</div>
<a class="anchor" id="a74c853f04808a514d7c99514a7583e2d"></a><!-- doxytag: member="CVariable::set_in_new_cl" ref="a74c853f04808a514d7c99514a7583e2d" args="(int phase)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVariable::set_in_new_cl </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>phase</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00273">273</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">CSolver::conflict_analysis_zchaff()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00231">CDatabase::mark_var_in_new_cl()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00890">CSolver::mark_vars_at_level()</a>.</p>
</div>
</div>
<a class="anchor" id="a200c0dd2b0b7cadd109b662fb20ec889"></a><!-- doxytag: member="CVariable::lits_count" ref="a200c0dd2b0b7cadd109b662fb20ec889" args="(int i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int& CVariable::lits_count </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00276">276</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00706">CSolver::preprocess()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00601">CSolver::update_var_stats()</a>.</p>
</div>
</div>
<a class="anchor" id="a8be2f24a39402da9c9047c701c0e0486"></a><!-- doxytag: member="CVariable::is_marked" ref="a8be2f24a39402da9c9047c701c0e0486" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVariable::is_marked </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00280">280</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">CSolver::conflict_analysis_zchaff()</a>.</p>
</div>
</div>
<a class="anchor" id="a605e80794f39e7aa307d94fd13017431"></a><!-- doxytag: member="CVariable::set_marked" ref="a605e80794f39e7aa307d94fd13017431" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVariable::set_marked </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00283">283</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00890">CSolver::mark_vars_at_level()</a>.</p>
</div>
</div>
<a class="anchor" id="a474d619248f352afcaa3fd4fb6c8788d"></a><!-- doxytag: member="CVariable::clear_marked" ref="a474d619248f352afcaa3fd4fb6c8788d" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVariable::clear_marked </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00286">286</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00916">CSolver::conflict_analysis_zchaff()</a>.</p>
</div>
</div>
<a class="anchor" id="a92a4c6ae0e4b566d1f664add2aeb39e9"></a><!-- doxytag: member="CVariable::get_antecedence" ref="a92a4c6ae0e4b566d1f664add2aeb39e9" args="(void)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> CVariable::get_antecedence </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00290">290</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00463">CSolver::dump_assignment_stack()</a>.</p>
</div>
</div>
<a class="anchor" id="ab10578bfddce9b0dfb959b84395d799c"></a><!-- doxytag: member="CVariable::set_antecedence" ref="ab10578bfddce9b0dfb959b84395d799c" args="(ClauseIdx ante)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVariable::set_antecedence </td>
<td>(</td>
<td class="paramtype"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td>
<td class="paramname"><em>ante</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00293">293</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00296">CSolver::set_var_value()</a>.</p>
</div>
</div>
<a class="anchor" id="aef0698f402345545601284fa7682e6f5"></a><!-- doxytag: member="CVariable::ht_ptr" ref="aef0698f402345545601284fa7682e6f5" args="(int i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> *>& CVariable::ht_ptr </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00297">297</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>Referenced by <a class="el" href="xchaff__solver_8cpp_source.html#l00179">CSolver::add_clause()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00062">CDatabase::compact_lit_pool()</a>, <a class="el" href="xchaff__dbase_8cpp_source.html#l00100">CDatabase::enlarge_lit_pool()</a>, <a class="el" href="xchaff__dbase_8h_source.html#l00188">CDatabase::mem_usage()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00296">CSolver::set_var_value()</a>, <a class="el" href="xchaff__solver_8cpp_source.html#l00368">CSolver::set_var_value_not_current_dl()</a>, and <a class="el" href="xchaff__solver_8cpp_source.html#l00321">CSolver::set_var_value_with_current_dl()</a>.</p>
</div>
</div>
<a class="anchor" id="ae03057639e30c735148c083c2305ae75"></a><!-- doxytag: member="CVariable::dump" ref="ae03057639e30c735148c083c2305ae75" args="(ostream &os=cout)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVariable::dump </td>
<td>(</td>
<td class="paramtype">ostream & </td>
<td class="paramname"><em>os</em> = <code>cout</code></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00300">300</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>.</p>
</div>
</div>
<hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="ac3e0d4831cd8625025002e21998517cd"></a><!-- doxytag: member="CVariable::operator<<" ref="ac3e0d4831cd8625025002e21998517cd" args="(ostream &os, CVariable &v)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ostream& operator<< </td>
<td>(</td>
<td class="paramtype">ostream & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVariable.html">CVariable</a> & </td>
<td class="paramname"><em>v</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00313">313</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a50e9a718302d737d0108c7aa443a842a"></a><!-- doxytag: member="CVariable::_is_marked" ref="a50e9a718302d737d0108c7aa443a842a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVariable.html#a50e9a718302d737d0108c7aa443a842a">CVariable::_is_marked</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00227">227</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div>
</div>
<a class="anchor" id="ab84b85036f11ce8252d38cfab388ff4b"></a><!-- doxytag: member="CVariable::_in_new_cl" ref="ab84b85036f11ce8252d38cfab388ff4b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCVariable.html#ab84b85036f11ce8252d38cfab388ff4b">CVariable::_in_new_cl</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00229">229</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div>
</div>
<a class="anchor" id="add75b1771456c8373c055ce56795abb7"></a><!-- doxytag: member="CVariable::_antecedence" ref="add75b1771456c8373c055ce56795abb7" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> <a class="el" href="classCVariable.html#add75b1771456c8373c055ce56795abb7">CVariable::_antecedence</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00236">236</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div>
</div>
<a class="anchor" id="a68bb88b73fda42d5076bc8a34c490b33"></a><!-- doxytag: member="CVariable::_value" ref="a68bb88b73fda42d5076bc8a34c490b33" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">short <a class="el" href="classCVariable.html#a68bb88b73fda42d5076bc8a34c490b33">CVariable::_value</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00238">238</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div>
</div>
<a class="anchor" id="aa099734654610fbe932b440ae9550cb6"></a><!-- doxytag: member="CVariable::_dlevel" ref="aa099734654610fbe932b440ae9550cb6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">short <a class="el" href="classCVariable.html#aa099734654610fbe932b440ae9550cb6">CVariable::_dlevel</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00240">240</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div>
</div>
<a class="anchor" id="aa33dc62f930de685f1e0a69c3c1c2cef"></a><!-- doxytag: member="CVariable::_ht_ptrs" ref="aa33dc62f930de685f1e0a69c3c1c2cef" args="[2]" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> *> <a class="el" href="classCVariable.html#aa33dc62f930de685f1e0a69c3c1c2cef">CVariable::_ht_ptrs</a>[2]<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00242">242</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div>
</div>
<a class="anchor" id="a9b7f0efebea35da376d4db863bdfd2a9"></a><!-- doxytag: member="CVariable::_lits_count" ref="a9b7f0efebea35da376d4db863bdfd2a9" args="[2]" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCVariable.html#a9b7f0efebea35da376d4db863bdfd2a9">CVariable::_lits_count</a>[2]<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00245">245</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div>
</div>
<a class="anchor" id="a3679cd1ad89f8ae495bc8f31f36c0f60"></a><!-- doxytag: member="CVariable::_scores" ref="a3679cd1ad89f8ae495bc8f31f36c0f60" args="[2]" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCVariable.html#a3679cd1ad89f8ae495bc8f31f36c0f60">CVariable::_scores</a>[2]<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00246">246</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div>
</div>
<a class="anchor" id="ac0b464c860f8702f36f9e256836a4bf9"></a><!-- doxytag: member="CVariable::_var_score_pos" ref="ac0b464c860f8702f36f9e256836a4bf9" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCVariable.html#ac0b464c860f8702f36f9e256836a4bf9">CVariable::_var_score_pos</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="xchaff__base_8h_source.html#l00247">247</a> of file <a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following file:<ul>
<li><a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</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>
