<!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: CVariable Class Reference</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 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="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
</div><!-- top -->
<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> |
<a href="classCVariable-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVariable Class Reference</div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="xchaff__base_8h_source.html">xchaff_base.h</a>></code></p>
<div class="dynheader">
Collaboration diagram for CVariable:</div>
<div class="dyncontent">
<div class="center"><img src="classCVariable__coll__graph.gif" border="0" usemap="#CVariable_coll__map" alt="Collaboration graph"/></div>
<map name="CVariable_coll__map" id="CVariable_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:acf5cbd17ee39aa733dd5445c5836ec81"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a> (int i)</td></tr>
<tr class="separator:acf5cbd17ee39aa733dd5445c5836ec81"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a519b8d883ea489998f7cabd31fae1ddb"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a519b8d883ea489998f7cabd31fae1ddb">score</a> (void)</td></tr>
<tr class="separator:a519b8d883ea489998f7cabd31fae1ddb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5d0f657e55242e1324c345bb8f6c9877"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a5d0f657e55242e1324c345bb8f6c9877">var_score_pos</a> (void)</td></tr>
<tr class="separator:a5d0f657e55242e1324c345bb8f6c9877"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac4db0d1a0f6c5a42a2a746dff0013019"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#ac4db0d1a0f6c5a42a2a746dff0013019">CVariable</a> (void)</td></tr>
<tr class="separator:ac4db0d1a0f6c5a42a2a746dff0013019"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7319394585df665256e74df1282f992f"><td class="memItemLeft" align="right" valign="top">short & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a> (void)</td></tr>
<tr class="separator:a7319394585df665256e74df1282f992f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aedac20571208b480adb2aff58797981a"><td class="memItemLeft" align="right" valign="top">short & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#aedac20571208b480adb2aff58797981a">dlevel</a> (void)</td></tr>
<tr class="separator:aedac20571208b480adb2aff58797981a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a106db2a07df4461da1ccfdf17faa8cdf"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a106db2a07df4461da1ccfdf17faa8cdf">in_new_cl</a> (void)</td></tr>
<tr class="separator:a106db2a07df4461da1ccfdf17faa8cdf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a74c853f04808a514d7c99514a7583e2d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a74c853f04808a514d7c99514a7583e2d">set_in_new_cl</a> (int phase)</td></tr>
<tr class="separator:a74c853f04808a514d7c99514a7583e2d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a200c0dd2b0b7cadd109b662fb20ec889"><td class="memItemLeft" align="right" valign="top">int & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a> (int i)</td></tr>
<tr class="separator:a200c0dd2b0b7cadd109b662fb20ec889"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8be2f24a39402da9c9047c701c0e0486"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a8be2f24a39402da9c9047c701c0e0486">is_marked</a> (void)</td></tr>
<tr class="separator:a8be2f24a39402da9c9047c701c0e0486"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a605e80794f39e7aa307d94fd13017431"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a605e80794f39e7aa307d94fd13017431">set_marked</a> (void)</td></tr>
<tr class="separator:a605e80794f39e7aa307d94fd13017431"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a474d619248f352afcaa3fd4fb6c8788d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a474d619248f352afcaa3fd4fb6c8788d">clear_marked</a> (void)</td></tr>
<tr class="separator:a474d619248f352afcaa3fd4fb6c8788d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a92a4c6ae0e4b566d1f664add2aeb39e9"><td class="memItemLeft" align="right" valign="top"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a92a4c6ae0e4b566d1f664add2aeb39e9">get_antecedence</a> (void)</td></tr>
<tr class="separator:a92a4c6ae0e4b566d1f664add2aeb39e9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab10578bfddce9b0dfb959b84395d799c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#ab10578bfddce9b0dfb959b84395d799c">set_antecedence</a> (<a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> ante)</td></tr>
<tr class="separator:ab10578bfddce9b0dfb959b84395d799c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aef0698f402345545601284fa7682e6f5"><td class="memItemLeft" align="right" valign="top">vector< <a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * > & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a> (int i)</td></tr>
<tr class="separator:aef0698f402345545601284fa7682e6f5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae03057639e30c735148c083c2305ae75"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#ae03057639e30c735148c083c2305ae75">dump</a> (ostream &os=cout)</td></tr>
<tr class="separator:ae03057639e30c735148c083c2305ae75"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pro-attribs"></a>
Protected Attributes</h2></td></tr>
<tr class="memitem:a50e9a718302d737d0108c7aa443a842a"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a50e9a718302d737d0108c7aa443a842a">_is_marked</a>: 1</td></tr>
<tr class="separator:a50e9a718302d737d0108c7aa443a842a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab84b85036f11ce8252d38cfab388ff4b"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#ab84b85036f11ce8252d38cfab388ff4b">_in_new_cl</a>: 2</td></tr>
<tr class="separator:ab84b85036f11ce8252d38cfab388ff4b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:add75b1771456c8373c055ce56795abb7"><td class="memItemLeft" align="right" valign="top"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#add75b1771456c8373c055ce56795abb7">_antecedence</a>: 29</td></tr>
<tr class="separator:add75b1771456c8373c055ce56795abb7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a68bb88b73fda42d5076bc8a34c490b33"><td class="memItemLeft" align="right" valign="top">short </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a68bb88b73fda42d5076bc8a34c490b33">_value</a></td></tr>
<tr class="separator:a68bb88b73fda42d5076bc8a34c490b33"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa099734654610fbe932b440ae9550cb6"><td class="memItemLeft" align="right" valign="top">short </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#aa099734654610fbe932b440ae9550cb6">_dlevel</a></td></tr>
<tr class="separator:aa099734654610fbe932b440ae9550cb6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa33dc62f930de685f1e0a69c3c1c2cef"><td class="memItemLeft" align="right" valign="top">vector< <a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> * > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#aa33dc62f930de685f1e0a69c3c1c2cef">_ht_ptrs</a> [2]</td></tr>
<tr class="separator:aa33dc62f930de685f1e0a69c3c1c2cef"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9b7f0efebea35da376d4db863bdfd2a9"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a9b7f0efebea35da376d4db863bdfd2a9">_lits_count</a> [2]</td></tr>
<tr class="separator:a9b7f0efebea35da376d4db863bdfd2a9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a3679cd1ad89f8ae495bc8f31f36c0f60"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#a3679cd1ad89f8ae495bc8f31f36c0f60">_scores</a> [2]</td></tr>
<tr class="separator:a3679cd1ad89f8ae495bc8f31f36c0f60"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac0b464c860f8702f36f9e256836a4bf9"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#ac0b464c860f8702f36f9e256836a4bf9">_var_score_pos</a></td></tr>
<tr class="separator:ac0b464c860f8702f36f9e256836a4bf9"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="friends"></a>
Friends</h2></td></tr>
<tr class="memitem:ac3e0d4831cd8625025002e21998517cd"><td class="memItemLeft" align="right" valign="top">ostream & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVariable.html#ac3e0d4831cd8625025002e21998517cd">operator<<</a> (ostream &os, <a class="el" href="classCVariable.html">CVariable</a> &v)</td></tr>
<tr class="separator:ac3e0d4831cd8625025002e21998517cd"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">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><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="ac4db0d1a0f6c5a42a2a746dff0013019"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVariable::CVariable </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="acf5cbd17ee39aa733dd5445c5836ec81"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<h2 class="groupheader">Friends And Related Function Documentation</h2>
<a class="anchor" id="ac3e0d4831cd8625025002e21998517cd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </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>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="a50e9a718302d737d0108c7aa443a842a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVariable::_is_marked</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVariable::_in_new_cl</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> CVariable::_antecedence</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">short CVariable::_value</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">short CVariable::_dlevel</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">vector<<a class="el" href="classCLitPoolElement.html">CLitPoolElement</a> *> CVariable::_ht_ptrs[2]</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVariable::_lits_count[2]</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVariable::_scores[2]</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVariable::_var_score_pos</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </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><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:17 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>
