<!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_base.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_base.h</div> </div>
</div>
<div class="contents">
<a href="xchaff__base_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */</span>
<a name="l00002"></a>00002
<a name="l00003"></a>00003 <span class="comment">/*********************************************************************</span>
<a name="l00004"></a>00004 <span class="comment"> Copyright 2000-2001, Princeton University. All rights reserved. </span>
<a name="l00005"></a>00005 <span class="comment"> By using this software the USER indicates that he or she has read, </span>
<a name="l00006"></a>00006 <span class="comment"> understood and will comply with the following:</span>
<a name="l00007"></a>00007 <span class="comment"></span>
<a name="l00008"></a>00008 <span class="comment"> --- Princeton University hereby grants USER nonexclusive permission </span>
<a name="l00009"></a>00009 <span class="comment"> to use, copy and/or modify this software for internal, noncommercial,</span>
<a name="l00010"></a>00010 <span class="comment"> research purposes only. Any distribution, including commercial sale </span>
<a name="l00011"></a>00011 <span class="comment"> or license, of this software, copies of the software, its associated </span>
<a name="l00012"></a>00012 <span class="comment"> documentation and/or modifications of either is strictly prohibited </span>
<a name="l00013"></a>00013 <span class="comment"> without the prior consent of Princeton University. Title to copyright</span>
<a name="l00014"></a>00014 <span class="comment"> to this software and its associated documentation shall at all times </span>
<a name="l00015"></a>00015 <span class="comment"> remain with Princeton University. Appropriate copyright notice shall </span>
<a name="l00016"></a>00016 <span class="comment"> be placed on all software copies, and a complete copy of this notice </span>
<a name="l00017"></a>00017 <span class="comment"> shall be included in all copies of the associated documentation. </span>
<a name="l00018"></a>00018 <span class="comment"> No right is granted to use in advertising, publicity or otherwise </span>
<a name="l00019"></a>00019 <span class="comment"> any trademark, service mark, or the name of Princeton University. </span>
<a name="l00020"></a>00020 <span class="comment"></span>
<a name="l00021"></a>00021 <span class="comment"></span>
<a name="l00022"></a>00022 <span class="comment"> --- This software and any associated documentation is provided "as is" </span>
<a name="l00023"></a>00023 <span class="comment"></span>
<a name="l00024"></a>00024 <span class="comment"> PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS </span>
<a name="l00025"></a>00025 <span class="comment"> OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A </span>
<a name="l00026"></a>00026 <span class="comment"> PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR </span>
<a name="l00027"></a>00027 <span class="comment"> ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, </span>
<a name="l00028"></a>00028 <span class="comment"> TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. </span>
<a name="l00029"></a>00029 <span class="comment"></span>
<a name="l00030"></a>00030 <span class="comment"> Princeton University shall not be liable under any circumstances for </span>
<a name="l00031"></a>00031 <span class="comment"> any direct, indirect, special, incidental, or consequential damages </span>
<a name="l00032"></a>00032 <span class="comment"> with respect to any claim by USER or any third party on account of </span>
<a name="l00033"></a>00033 <span class="comment"> or arising from the use, or inability to use, this software or its </span>
<a name="l00034"></a>00034 <span class="comment"> associated documentation, even if Princeton University has been advised</span>
<a name="l00035"></a>00035 <span class="comment"> of the possibility of those damages.</span>
<a name="l00036"></a>00036 <span class="comment">*********************************************************************/</span>
<a name="l00037"></a>00037
<a name="l00038"></a>00038
<a name="l00039"></a>00039 <span class="preprocessor">#ifndef __BASIC_CLASSES__</span>
<a name="l00040"></a>00040 <span class="preprocessor"></span><span class="preprocessor">#define __BASIC_CLASSES__</span>
<a name="l00041"></a>00041 <span class="preprocessor"></span>
<a name="l00042"></a>00042 <span class="preprocessor">#include <vector></span>
<a name="l00043"></a>00043 <span class="preprocessor">#include <iostream></span>
<a name="l00044"></a>00044 <span class="preprocessor">#include <assert.h></span>
<a name="l00045"></a>00045 <span class="keyword">using namespace </span>std;
<a name="l00046"></a>00046
<a name="l00047"></a><a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855">00047</a> <span class="keyword">typedef</span> <span class="keyword">enum</span> <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855">Unknown</a> {
<a name="l00048"></a><a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">00048</a> <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a> = -1
<a name="l00049"></a>00049 } <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855">Unknown</a>;
<a name="l00050"></a>00050
<a name="l00051"></a><a class="code" href="xchaff__base_8h.html#abd4c1edc3bf20c1f93ebaca33c9b2b64">00051</a> <span class="preprocessor">#define NULL_CLAUSE -1</span>
<a name="l00052"></a><a class="code" href="xchaff__base_8h.html#aa5981a99705aebbb4ca38799d15e0e79">00052</a> <span class="preprocessor"></span><span class="preprocessor">#define FLIPPED -2</span>
<a name="l00053"></a>00053 <span class="preprocessor"></span>
<a name="l00054"></a><a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">00054</a> <span class="keyword">typedef</span> <span class="keywordtype">int</span> <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a>; <span class="comment">//used to refer a clause. Because of dynamic </span>
<a name="l00055"></a>00055 <span class="comment">//allocation of vector storage, no pointer is allowered</span>
<a name="l00056"></a>00056 <span class="comment"></span>
<a name="l00057"></a>00057 <span class="comment">/**Class**********************************************************************</span>
<a name="l00058"></a>00058 <span class="comment"></span>
<a name="l00059"></a>00059 <span class="comment"> Synopsis [Definition of a literal]</span>
<a name="l00060"></a>00060 <span class="comment"></span>
<a name="l00061"></a>00061 <span class="comment"> Description [A literal is a variable with phase. Two thing determing a lteral: </span>
<a name="l00062"></a>00062 <span class="comment"> it's "sign", and the variable index. One bit is used to mark it's</span>
<a name="l00063"></a>00063 <span class="comment"> sign. 0->positive, 1->negative.</span>
<a name="l00064"></a>00064 <span class="comment"></span>
<a name="l00065"></a>00065 <span class="comment"> For every clause with literal count larger than 1, there are two</span>
<a name="l00066"></a>00066 <span class="comment"> special literals which are designated ht_literal (stands for </span>
<a name="l00067"></a>00067 <span class="comment"> head/tail literal to imitate SATO) It is specially marked with 2 bits: </span>
<a name="l00068"></a>00068 <span class="comment"> 00->not ht; dir = 1; or dir = -1; 10 is not valid.</span>
<a name="l00069"></a>00069 <span class="comment"> Each literal is represented by a 32 bit integer, with one bit </span>
<a name="l00070"></a>00070 <span class="comment"> representing it's phase and 2 bits indicate h/t property.</span>
<a name="l00071"></a>00071 <span class="comment"></span>
<a name="l00072"></a>00072 <span class="comment"> All the literals are collected in a storage space called literal</span>
<a name="l00073"></a>00073 <span class="comment"> pool. An element in a literal pool can be a literal or special</span>
<a name="l00074"></a>00074 <span class="comment"> spacing element to indicate the termination of a clause. The </span>
<a name="l00075"></a>00075 <span class="comment"> spacing element has negative value of the clause index.]</span>
<a name="l00076"></a>00076 <span class="comment"></span>
<a name="l00077"></a>00077 <span class="comment"> SeeAlso [CDatabase, CClause]</span>
<a name="l00078"></a>00078 <span class="comment"></span>
<a name="l00079"></a>00079 <span class="comment">******************************************************************************/</span>
<a name="l00080"></a>00080
<a name="l00081"></a><a class="code" href="classCLitPoolElement.html">00081</a> <span class="keyword">class </span><a class="code" href="classCLitPoolElement.html">CLitPoolElement</a>
<a name="l00082"></a>00082 {
<a name="l00083"></a>00083 <span class="keyword">protected</span>:
<a name="l00084"></a><a class="code" href="classCLitPoolElement.html#a8f1cfa5155dfefbc9b2fbddd7e3852ee">00084</a> <span class="keywordtype">int</span> <a class="code" href="classCLitPoolElement.html#a8f1cfa5155dfefbc9b2fbddd7e3852ee">_val</a>;
<a name="l00085"></a>00085 <span class="keyword">public</span>:
<a name="l00086"></a>00086 <span class="comment">//======constructors & destructors============</span>
<a name="l00087"></a><a class="code" href="classCLitPoolElement.html#a4061f5f6e8ae014f6d2bb7536ae52e31">00087</a> <a class="code" href="classCLitPoolElement.html#a4061f5f6e8ae014f6d2bb7536ae52e31">CLitPoolElement</a>(<span class="keywordtype">void</span>) {
<a name="l00088"></a>00088 _val=0;
<a name="l00089"></a>00089 }
<a name="l00090"></a><a class="code" href="classCLitPoolElement.html#a461b807c0815a6084f2d1b0c88260b68">00090</a> <a class="code" href="classCLitPoolElement.html#a461b807c0815a6084f2d1b0c88260b68">CLitPoolElement</a>(<span class="keywordtype">int</span> val):_val(val){}
<a name="l00091"></a>00091 <span class="comment">//=========member access function=============</span>
<a name="l00092"></a><a class="code" href="classCLitPoolElement.html#a253daa80c6f47528feb0b69e1a5c4623">00092</a> <span class="keywordtype">int</span> & <a class="code" href="classCLitPoolElement.html#a253daa80c6f47528feb0b69e1a5c4623">val</a>(<span class="keywordtype">void</span>) {
<a name="l00093"></a>00093 <span class="keywordflow">return</span> _val;
<a name="l00094"></a>00094 }
<a name="l00095"></a><a class="code" href="classCLitPoolElement.html#a19281557172f9102172f404bf9f69cbc">00095</a> <span class="keywordtype">int</span> <a class="code" href="classCLitPoolElement.html#a19281557172f9102172f404bf9f69cbc">s_var</a>(<span class="keywordtype">void</span>) { <span class="comment">//stands for signed variable, i.e. 2*var_idx + sign</span>
<a name="l00096"></a>00096 <span class="keywordflow">return</span> _val>>2;
<a name="l00097"></a>00097 }
<a name="l00098"></a><a class="code" href="classCLitPoolElement.html#a98d4a07830b749d83c74943efdf9669b">00098</a> <span class="keywordtype">int</span> <a class="code" href="classCLitPoolElement.html#a98d4a07830b749d83c74943efdf9669b">var_index</a>(<span class="keywordtype">void</span>) {
<a name="l00099"></a>00099 <span class="keywordflow">return</span> _val>>3;
<a name="l00100"></a>00100 }
<a name="l00101"></a><a class="code" href="classCLitPoolElement.html#add6c6301567da71e72923b3c372081cd">00101</a> <span class="keywordtype">bool</span> <a class="code" href="classCLitPoolElement.html#add6c6301567da71e72923b3c372081cd">var_sign</a>(<span class="keywordtype">void</span>) {
<a name="l00102"></a>00102 <span class="keywordflow">return</span> ( (_val>> 2)& 0x1);
<a name="l00103"></a>00103 }
<a name="l00104"></a><a class="code" href="classCLitPoolElement.html#a6eed77f12eacecf47984cbe3d939605c">00104</a> <span class="keywordtype">void</span> <span class="keyword">set</span> (<span class="keywordtype">int</span> s_var) {
<a name="l00105"></a>00105 _val = (s_var << 2);
<a name="l00106"></a>00106 }
<a name="l00107"></a><a class="code" href="classCLitPoolElement.html#aed2c173d66f31327ee011ecfba8da498">00107</a> <span class="keywordtype">void</span> <span class="keyword">set</span>(<span class="keywordtype">int</span> v, <span class="keywordtype">int</span> s) {
<a name="l00108"></a>00108 _val = (((v<<1) + s)<< 2);
<a name="l00109"></a>00109 }
<a name="l00110"></a>00110 <span class="comment">//following are the functions for the special head/tail literals for FAST_BCP</span>
<a name="l00111"></a><a class="code" href="classCLitPoolElement.html#a5810e79233dd5430fa52f56e5ef1f3ed">00111</a> <span class="keywordtype">int</span> <a class="code" href="classCLitPoolElement.html#a5810e79233dd5430fa52f56e5ef1f3ed">direction</a> (<span class="keywordtype">void</span>) {
<a name="l00112"></a>00112 <span class="keywordflow">return</span> ((_val&0x03) - 2);
<a name="l00113"></a>00113 }
<a name="l00114"></a><a class="code" href="classCLitPoolElement.html#aeaa93c7cfdbbe94aed9b9b6f07458a00">00114</a> <span class="keywordtype">bool</span> <a class="code" href="classCLitPoolElement.html#aeaa93c7cfdbbe94aed9b9b6f07458a00">is_ht</a>(<span class="keywordtype">void</span>) {
<a name="l00115"></a>00115 <span class="keywordflow">return</span> _val&0x03;
<a name="l00116"></a>00116 }
<a name="l00117"></a><a class="code" href="classCLitPoolElement.html#af96c5ff47035816003a5c33b6d2591d7">00117</a> <span class="keywordtype">void</span> <a class="code" href="classCLitPoolElement.html#af96c5ff47035816003a5c33b6d2591d7">unset_ht</a>(<span class="keywordtype">void</span>) {
<a name="l00118"></a>00118 _val = _val & (0x0fffffffc);
<a name="l00119"></a>00119 }
<a name="l00120"></a><a class="code" href="classCLitPoolElement.html#a61ae125841707c699b3587e0f5a668bc">00120</a> <span class="keywordtype">void</span> <a class="code" href="classCLitPoolElement.html#a61ae125841707c699b3587e0f5a668bc">set_ht</a>(<span class="keywordtype">int</span> dir) {
<a name="l00121"></a>00121 _val = _val + dir + 2;
<a name="l00122"></a>00122 }
<a name="l00123"></a>00123
<a name="l00124"></a>00124 <span class="comment">//following are used for spacing (e.g. indicate clause's end)</span>
<a name="l00125"></a><a class="code" href="classCLitPoolElement.html#a2dee34c54abc3e808105de6b901d1aec">00125</a> <span class="keywordtype">bool</span> <a class="code" href="classCLitPoolElement.html#a2dee34c54abc3e808105de6b901d1aec">is_literal</a>(<span class="keywordtype">void</span>) {
<a name="l00126"></a>00126 <span class="keywordflow">return</span> _val > 0;
<a name="l00127"></a>00127 }
<a name="l00128"></a><a class="code" href="classCLitPoolElement.html#afdd809e9982d0c46aa8bf344c9dc21cb">00128</a> <span class="keywordtype">void</span> <a class="code" href="classCLitPoolElement.html#afdd809e9982d0c46aa8bf344c9dc21cb">set_clause_index</a>(<span class="keywordtype">int</span> cl_idx) {
<a name="l00129"></a>00129 _val = - cl_idx;
<a name="l00130"></a>00130 }
<a name="l00131"></a><a class="code" href="classCLitPoolElement.html#a9e90329d95ea56eba41fb6b21eeb1fb7">00131</a> <span class="keywordtype">int</span> <a class="code" href="classCLitPoolElement.html#a9e90329d95ea56eba41fb6b21eeb1fb7">get_clause_index</a>(<span class="keywordtype">void</span>) {
<a name="l00132"></a>00132 <span class="keywordflow">return</span> -_val;
<a name="l00133"></a>00133 }
<a name="l00134"></a>00134 <span class="comment">//misc functions</span>
<a name="l00135"></a><a class="code" href="classCLitPoolElement.html#a0cf9273cb1861b2f2c30a20a5d0b8066">00135</a> <span class="keywordtype">int</span> <a class="code" href="classCLitPoolElement.html#a0cf9273cb1861b2f2c30a20a5d0b8066">find_clause_idx</a>(<span class="keywordtype">void</span>) {
<a name="l00136"></a>00136 <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * ptr;
<a name="l00137"></a>00137 <span class="keywordflow">for</span> (ptr = <span class="keyword">this</span>; ptr-><a class="code" href="classCLitPoolElement.html#a2dee34c54abc3e808105de6b901d1aec">is_literal</a>(); ++ ptr);
<a name="l00138"></a>00138 <span class="keywordflow">return</span> ptr-><a class="code" href="classCLitPoolElement.html#a9e90329d95ea56eba41fb6b21eeb1fb7">get_clause_index</a>();
<a name="l00139"></a>00139 }
<a name="l00140"></a>00140
<a name="l00141"></a><a class="code" href="classCLitPoolElement.html#a126db84fe04eea19bbe9db75820fa424">00141</a> <span class="keywordtype">void</span> <a class="code" href="classCLitPoolElement.html#a126db84fe04eea19bbe9db75820fa424">dump</a>(ostream & os= cout) {
<a name="l00142"></a>00142 os << (var_sign()?<span class="stringliteral">" -"</span>:<span class="stringliteral">" +"</span>) << var_index();
<a name="l00143"></a>00143 <span class="keywordflow">if</span> (is_ht()) os << <span class="stringliteral">"*"</span>;
<a name="l00144"></a>00144 }
<a name="l00145"></a><a class="code" href="classCLitPoolElement.html#abdc5b59a15137d65846abeaaf6f2bf0b">00145</a> <span class="keyword">friend</span> ostream & <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator << </a>( ostream & os, <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> & l) {
<a name="l00146"></a>00146 l.<a class="code" href="classCLitPoolElement.html#a126db84fe04eea19bbe9db75820fa424">dump</a>(os);
<a name="l00147"></a>00147 <span class="keywordflow">return</span> os;
<a name="l00148"></a>00148 }
<a name="l00149"></a>00149 };
<a name="l00150"></a>00150 <span class="comment"></span>
<a name="l00151"></a>00151 <span class="comment">/**Class**********************************************************************</span>
<a name="l00152"></a>00152 <span class="comment"></span>
<a name="l00153"></a>00153 <span class="comment"> Synopsis [Definition of a clause]</span>
<a name="l00154"></a>00154 <span class="comment"></span>
<a name="l00155"></a>00155 <span class="comment"> Description [A clause is consisted of a certain number of literals. </span>
<a name="l00156"></a>00156 <span class="comment"> All literals are collected in a single large vector, we call it</span>
<a name="l00157"></a>00157 <span class="comment"> literal pool. Each clause has a pointer to the beginning position</span>
<a name="l00158"></a>00158 <span class="comment"> of it's literals in the pool. The boolean propagation mechanism</span>
<a name="l00159"></a>00159 <span class="comment"> use two pointers (called head/tail pointer, by sato's convention)</span>
<a name="l00160"></a>00160 <span class="comment"> which always point to the last assigned literals of this clause.]</span>
<a name="l00161"></a>00161 <span class="comment"></span>
<a name="l00162"></a>00162 <span class="comment"> SeeAlso [CDatabase]</span>
<a name="l00163"></a>00163 <span class="comment"></span>
<a name="l00164"></a>00164 <span class="comment">******************************************************************************/</span>
<a name="l00165"></a><a class="code" href="classCClause.html">00165</a> <span class="keyword">class </span><a class="code" href="classCClause.html">CClause</a>
<a name="l00166"></a>00166 {
<a name="l00167"></a>00167 <span class="keyword">protected</span>:
<a name="l00168"></a><a class="code" href="classCClause.html#a5a69f02bb5d7a29aa859105c21f93622">00168</a> <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * <a class="code" href="classCClause.html#a5a69f02bb5d7a29aa859105c21f93622">_first_lit</a>; <span class="comment">//pointer to the first literal in literal pool</span>
<a name="l00169"></a><a class="code" href="classCClause.html#ad52e9eeb7316e0b9be73c4f556f38856">00169</a> <span class="keywordtype">int</span> <a class="code" href="classCClause.html#ad52e9eeb7316e0b9be73c4f556f38856">_num_lits</a>; <span class="comment">//number of literals</span>
<a name="l00170"></a><a class="code" href="classCClause.html#a94169375b0ac79972818318e157751b8">00170</a> <span class="keywordtype">bool</span> <a class="code" href="classCClause.html#a94169375b0ac79972818318e157751b8">_in_use</a>; <span class="comment">//indicate if this clause has been deleted or not</span>
<a name="l00171"></a>00171 <span class="keyword">public</span>:
<a name="l00172"></a>00172 <span class="comment">//constructors & destructors</span>
<a name="l00173"></a><a class="code" href="classCClause.html#aadb77f8245e78c2c6e3571c888d0883a">00173</a> <a class="code" href="classCClause.html#aadb77f8245e78c2c6e3571c888d0883a">CClause</a>(<span class="keywordtype">void</span>){}
<a name="l00174"></a>00174
<a name="l00175"></a><a class="code" href="classCClause.html#a989337392671ea2855b3131c456a52a4">00175</a> <a class="code" href="classCClause.html#a989337392671ea2855b3131c456a52a4">~CClause</a>() {}
<a name="l00176"></a>00176 <span class="comment">//initialization & clear up</span>
<a name="l00177"></a><a class="code" href="classCClause.html#a9dea20f5f7e41be18dfbe01105c58f2c">00177</a> <span class="keywordtype">void</span> <a class="code" href="classCClause.html#a9dea20f5f7e41be18dfbe01105c58f2c">init</a>(<a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * head, <span class="keywordtype">int</span> num_lits) { <span class="comment">//initialization of a clause</span>
<a name="l00178"></a>00178 _first_lit = head;
<a name="l00179"></a>00179 _num_lits = num_lits;
<a name="l00180"></a>00180 _in_use = <span class="keyword">true</span>;
<a name="l00181"></a>00181 }
<a name="l00182"></a>00182 <span class="comment">//member access function</span>
<a name="l00183"></a><a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">00183</a> <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * <a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>(<span class="keywordtype">void</span>) { <span class="comment">//literals()[i] is it's the i-th literal</span>
<a name="l00184"></a>00184 <span class="keywordflow">return</span> _first_lit;
<a name="l00185"></a>00185 }
<a name="l00186"></a><a class="code" href="classCClause.html#a08b669c2f239c65df9cae46603cab85f">00186</a> <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * & <a class="code" href="classCClause.html#a08b669c2f239c65df9cae46603cab85f">first_lit</a>(<span class="keywordtype">void</span>) { <span class="comment">//use it only if you want to modify _first_lit</span>
<a name="l00187"></a>00187 <span class="keywordflow">return</span> _first_lit;
<a name="l00188"></a>00188 }
<a name="l00189"></a><a class="code" href="classCClause.html#ae4f9f5a951b75aab530b5b05a3232082">00189</a> <span class="keywordtype">int</span> & <a class="code" href="classCClause.html#ae4f9f5a951b75aab530b5b05a3232082">num_lits</a>(<span class="keywordtype">void</span>) {
<a name="l00190"></a>00190 <span class="keywordflow">return</span> _num_lits;
<a name="l00191"></a>00191 }
<a name="l00192"></a><a class="code" href="classCClause.html#accc3ecb433cd7ba00affc3180b0911d4">00192</a> <span class="keywordtype">bool</span> & <a class="code" href="classCClause.html#accc3ecb433cd7ba00affc3180b0911d4">in_use</a>(<span class="keywordtype">void</span>) {
<a name="l00193"></a>00193 <span class="keywordflow">return</span> _in_use;
<a name="l00194"></a>00194 }
<a name="l00195"></a><a class="code" href="classCClause.html#aa9e91f96e80b94da2b28e3ab381b9acc">00195</a> <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> & <a class="code" href="classCClause.html#aa9e91f96e80b94da2b28e3ab381b9acc">literal</a>(<span class="keywordtype">int</span> idx) { <span class="comment">//return the idx-th literal</span>
<a name="l00196"></a>00196 <span class="keywordflow">return</span> literals()[idx];
<a name="l00197"></a>00197 }
<a name="l00198"></a>00198 <span class="comment">//misc functions</span>
<a name="l00199"></a><a class="code" href="classCClause.html#af3bf6d35dd865946c571aeb3ac5405c1">00199</a> <span class="keywordtype">void</span> <a class="code" href="classCClause.html#af3bf6d35dd865946c571aeb3ac5405c1">dump</a>(ostream & os = cout) {
<a name="l00200"></a>00200 <span class="keywordflow">if</span> (!in_use())
<a name="l00201"></a>00201 os << <span class="stringliteral">"\t\t\t======removed====="</span>;
<a name="l00202"></a>00202 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0, sz=num_lits(); i<sz; ++i)
<a name="l00203"></a>00203 os << literal(i);
<a name="l00204"></a>00204 os << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00205"></a>00205 }
<a name="l00206"></a>00206 <span class="comment">// friend ostream & operator << (ostream & os, CClause & cl);</span>
<a name="l00207"></a><a class="code" href="classCClause.html#a03f918c95f5c21a52e38a1879c53dc95">00207</a> <span class="keyword">friend</span> ostream & <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator << </a>( ostream & os, <a class="code" href="classCClause.html">CClause</a> & cl) {
<a name="l00208"></a>00208 cl.<a class="code" href="classCClause.html#af3bf6d35dd865946c571aeb3ac5405c1">dump</a>(os);
<a name="l00209"></a>00209 <span class="keywordflow">return</span> os;
<a name="l00210"></a>00210 }
<a name="l00211"></a>00211 };
<a name="l00212"></a>00212
<a name="l00213"></a>00213 <span class="comment"></span>
<a name="l00214"></a>00214 <span class="comment">/**Class**********************************************************************</span>
<a name="l00215"></a>00215 <span class="comment"></span>
<a name="l00216"></a>00216 <span class="comment"> Synopsis [Definition of a variable]</span>
<a name="l00217"></a>00217 <span class="comment"></span>
<a name="l00218"></a>00218 <span class="comment"> Description [CVariable contains the necessary information for a variable.</span>
<a name="l00219"></a>00219 <span class="comment"> _ht_ptrs are the head/tail literals of this variable (int two phases)]</span>
<a name="l00220"></a>00220 <span class="comment"></span>
<a name="l00221"></a>00221 <span class="comment"> SeeAlso [CDatabase]</span>
<a name="l00222"></a>00222 <span class="comment"></span>
<a name="l00223"></a>00223 <span class="comment">******************************************************************************/</span>
<a name="l00224"></a><a class="code" href="classCVariable.html">00224</a> <span class="keyword">class </span><a class="code" href="classCVariable.html">CVariable</a>
<a name="l00225"></a>00225 {
<a name="l00226"></a>00226 <span class="keyword">protected</span>:
<a name="l00227"></a><a class="code" href="classCVariable.html#a50e9a718302d737d0108c7aa443a842a">00227</a> <span class="keywordtype">bool</span> _is_marked : 1; <span class="comment">//used in conflict analysis.</span>
<a name="l00228"></a>00228
<a name="l00229"></a><a class="code" href="classCVariable.html#ab84b85036f11ce8252d38cfab388ff4b">00229</a> <span class="keywordtype">int</span> _in_new_cl : 2; <span class="comment">//it can take 3 value 0: pos phase, </span>
<a name="l00230"></a>00230 <span class="comment">//1: neg phase, -1 : not in new clause;</span>
<a name="l00231"></a>00231 <span class="comment">//used to keep track of literals appearing</span>
<a name="l00232"></a>00232 <span class="comment">//in newly added clause so that a. each</span>
<a name="l00233"></a>00233 <span class="comment">//variable can only appearing in one phase</span>
<a name="l00234"></a>00234 <span class="comment">//b. same literal won't appear more than once.</span>
<a name="l00235"></a>00235
<a name="l00236"></a><a class="code" href="classCVariable.html#add75b1771456c8373c055ce56795abb7">00236</a> <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> _antecedence : 29; <span class="comment">//used in conflict analysis</span>
<a name="l00237"></a>00237
<a name="l00238"></a><a class="code" href="classCVariable.html#a68bb88b73fda42d5076bc8a34c490b33">00238</a> <span class="keywordtype">short</span> <a class="code" href="classCVariable.html#a68bb88b73fda42d5076bc8a34c490b33">_value</a>; <span class="comment">//can be 1, 0 or UNKNOWN</span>
<a name="l00239"></a>00239
<a name="l00240"></a><a class="code" href="classCVariable.html#aa099734654610fbe932b440ae9550cb6">00240</a> <span class="keywordtype">short</span> <a class="code" href="classCVariable.html#aa099734654610fbe932b440ae9550cb6">_dlevel</a>; <span class="comment">//decision level this variable being assigned</span>
<a name="l00241"></a>00241
<a name="l00242"></a><a class="code" href="classCVariable.html#aa33dc62f930de685f1e0a69c3c1c2cef">00242</a> vector<CLitPoolElement *> _ht_ptrs[2]; <span class="comment">//literal of this var appearing in h/t. 0: pos, 1: neg</span>
<a name="l00243"></a>00243
<a name="l00244"></a>00244 <span class="keyword">protected</span>:
<a name="l00245"></a><a class="code" href="classCVariable.html#a9b7f0efebea35da376d4db863bdfd2a9">00245</a> <span class="keywordtype">int</span> _lits_count[2];
<a name="l00246"></a><a class="code" href="classCVariable.html#a3679cd1ad89f8ae495bc8f31f36c0f60">00246</a> <span class="keywordtype">int</span> _scores[2];
<a name="l00247"></a><a class="code" href="classCVariable.html#ac0b464c860f8702f36f9e256836a4bf9">00247</a> <span class="keywordtype">int</span> <a class="code" href="classCVariable.html#ac0b464c860f8702f36f9e256836a4bf9">_var_score_pos</a>;
<a name="l00248"></a>00248 <span class="keyword">public</span>:
<a name="l00249"></a><a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">00249</a> <span class="keywordtype">int</span> & <a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a>(<span class="keywordtype">int</span> i) { <span class="keywordflow">return</span> _scores[i]; }
<a name="l00250"></a><a class="code" href="classCVariable.html#a519b8d883ea489998f7cabd31fae1ddb">00250</a> <span class="keywordtype">int</span> <a class="code" href="classCVariable.html#a519b8d883ea489998f7cabd31fae1ddb">score</a>(<span class="keywordtype">void</span>) { <span class="keywordflow">return</span> <a class="code" href="classCVariable.html#a519b8d883ea489998f7cabd31fae1ddb">score</a>(0)><a class="code" href="classCVariable.html#a519b8d883ea489998f7cabd31fae1ddb">score</a>(1)?<a class="code" href="classCVariable.html#a519b8d883ea489998f7cabd31fae1ddb">score</a>(0):<a class="code" href="classCVariable.html#a519b8d883ea489998f7cabd31fae1ddb">score</a>(1); }
<a name="l00251"></a><a class="code" href="classCVariable.html#a5d0f657e55242e1324c345bb8f6c9877">00251</a> <span class="keywordtype">int</span> & <a class="code" href="classCVariable.html#a5d0f657e55242e1324c345bb8f6c9877">var_score_pos</a>(<span class="keywordtype">void</span>) { <span class="keywordflow">return</span> _var_score_pos; }
<a name="l00252"></a>00252 <span class="keyword">public</span>:
<a name="l00253"></a>00253 <span class="comment">//constructors & destructors</span>
<a name="l00254"></a><a class="code" href="classCVariable.html#ac4db0d1a0f6c5a42a2a746dff0013019">00254</a> <a class="code" href="classCVariable.html#ac4db0d1a0f6c5a42a2a746dff0013019">CVariable</a>(<span class="keywordtype">void</span>) {
<a name="l00255"></a>00255 _value = <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>;
<a name="l00256"></a>00256 _antecedence=<a class="code" href="xchaff__base_8h.html#abd4c1edc3bf20c1f93ebaca33c9b2b64">NULL_CLAUSE</a>;
<a name="l00257"></a>00257 _dlevel = -1;
<a name="l00258"></a>00258 _in_new_cl = -1;
<a name="l00259"></a>00259 _is_marked = <span class="keyword">false</span>;
<a name="l00260"></a>00260 _scores[0] = _scores[1] = 0;
<a name="l00261"></a>00261 _var_score_pos = _lits_count[0] = _lits_count[1] = 0;
<a name="l00262"></a>00262 }
<a name="l00263"></a>00263 <span class="comment">//member access function</span>
<a name="l00264"></a><a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">00264</a> <span class="keywordtype">short</span> & <a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>(<span class="keywordtype">void</span>) {
<a name="l00265"></a>00265 <span class="keywordflow">return</span> _value;
<a name="l00266"></a>00266 }
<a name="l00267"></a><a class="code" href="classCVariable.html#aedac20571208b480adb2aff58797981a">00267</a> <span class="keywordtype">short</span> & <a class="code" href="classCVariable.html#aedac20571208b480adb2aff58797981a">dlevel</a>(<span class="keywordtype">void</span>) {
<a name="l00268"></a>00268 <span class="keywordflow">return</span> _dlevel;
<a name="l00269"></a>00269 }
<a name="l00270"></a><a class="code" href="classCVariable.html#a106db2a07df4461da1ccfdf17faa8cdf">00270</a> <span class="keywordtype">int</span> <a class="code" href="classCVariable.html#a106db2a07df4461da1ccfdf17faa8cdf">in_new_cl</a>(<span class="keywordtype">void</span>) {
<a name="l00271"></a>00271 <span class="keywordflow">return</span> _in_new_cl;
<a name="l00272"></a>00272 }
<a name="l00273"></a><a class="code" href="classCVariable.html#a74c853f04808a514d7c99514a7583e2d">00273</a> <span class="keywordtype">void</span> <a class="code" href="classCVariable.html#a74c853f04808a514d7c99514a7583e2d">set_in_new_cl</a>(<span class="keywordtype">int</span> phase) {
<a name="l00274"></a>00274 _in_new_cl = phase;
<a name="l00275"></a>00275 }
<a name="l00276"></a><a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">00276</a> <span class="keywordtype">int</span> & <a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a>(<span class="keywordtype">int</span> i) {
<a name="l00277"></a>00277 <span class="keywordflow">return</span> _lits_count[i];
<a name="l00278"></a>00278 }
<a name="l00279"></a>00279
<a name="l00280"></a><a class="code" href="classCVariable.html#a8be2f24a39402da9c9047c701c0e0486">00280</a> <span class="keywordtype">bool</span> <a class="code" href="classCVariable.html#a8be2f24a39402da9c9047c701c0e0486">is_marked</a>(<span class="keywordtype">void</span>) {
<a name="l00281"></a>00281 <span class="keywordflow">return</span> _is_marked;
<a name="l00282"></a>00282 }
<a name="l00283"></a><a class="code" href="classCVariable.html#a605e80794f39e7aa307d94fd13017431">00283</a> <span class="keywordtype">void</span> <a class="code" href="classCVariable.html#a605e80794f39e7aa307d94fd13017431">set_marked</a>(<span class="keywordtype">void</span>) {
<a name="l00284"></a>00284 _is_marked = <span class="keyword">true</span>;
<a name="l00285"></a>00285 }
<a name="l00286"></a><a class="code" href="classCVariable.html#a474d619248f352afcaa3fd4fb6c8788d">00286</a> <span class="keywordtype">void</span> <a class="code" href="classCVariable.html#a474d619248f352afcaa3fd4fb6c8788d">clear_marked</a>(<span class="keywordtype">void</span>) {
<a name="l00287"></a>00287 _is_marked = <span class="keyword">false</span>;
<a name="l00288"></a>00288 }
<a name="l00289"></a>00289
<a name="l00290"></a><a class="code" href="classCVariable.html#a92a4c6ae0e4b566d1f664add2aeb39e9">00290</a> <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> <a class="code" href="classCVariable.html#a92a4c6ae0e4b566d1f664add2aeb39e9">get_antecedence</a>(<span class="keywordtype">void</span>) {
<a name="l00291"></a>00291 <span class="keywordflow">return</span> _antecedence;
<a name="l00292"></a>00292 }
<a name="l00293"></a><a class="code" href="classCVariable.html#ab10578bfddce9b0dfb959b84395d799c">00293</a> <span class="keywordtype">void</span> <a class="code" href="classCVariable.html#ab10578bfddce9b0dfb959b84395d799c">set_antecedence</a>(<a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> ante) {
<a name="l00294"></a>00294 _antecedence = ante;
<a name="l00295"></a>00295 }
<a name="l00296"></a>00296
<a name="l00297"></a><a class="code" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">00297</a> vector<CLitPoolElement *> & <a class="code" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a>(<span class="keywordtype">int</span> i) { <span class="keywordflow">return</span> _ht_ptrs[i]; }
<a name="l00298"></a>00298
<a name="l00299"></a>00299 <span class="comment">//misc functions</span>
<a name="l00300"></a><a class="code" href="classCVariable.html#ae03057639e30c735148c083c2305ae75">00300</a> <span class="keywordtype">void</span> <a class="code" href="classCVariable.html#ae03057639e30c735148c083c2305ae75">dump</a>(ostream & os=cout) {
<a name="l00301"></a>00301 <span class="keywordflow">if</span> (is_marked()) os << <span class="stringliteral">"*"</span> ;
<a name="l00302"></a>00302 os << <span class="stringliteral">"V: "</span> << _value << <span class="stringliteral">" DL: "</span> << _dlevel
<a name="l00303"></a>00303 << <span class="stringliteral">" Ante: "</span> << _antecedence << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00304"></a>00304 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> j=0; j< 2; ++j) {
<a name="l00305"></a>00305 os << (j==0?<span class="stringliteral">"Pos "</span>:<span class="stringliteral">"Neg "</span>) << <span class="stringliteral">"("</span> ;
<a name="l00306"></a>00306 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i=0; i< ht_ptr(j).size(); ++i )
<a name="l00307"></a>00307 os << ht_ptr(j)[i]->find_clause_idx() << <span class="stringliteral">" "</span> ;
<a name="l00308"></a>00308 os << <span class="stringliteral">")"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00309"></a>00309 }
<a name="l00310"></a>00310 os << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00311"></a>00311 }
<a name="l00312"></a>00312 <span class="comment">// friend ostream & operator << (ostream & os, CVariable & v);</span>
<a name="l00313"></a><a class="code" href="classCVariable.html#ac3e0d4831cd8625025002e21998517cd">00313</a> <span class="keyword">friend</span> ostream & <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator << </a>( ostream & os, <a class="code" href="classCVariable.html">CVariable</a> & v) {
<a name="l00314"></a>00314 v.<a class="code" href="classCVariable.html#ae03057639e30c735148c083c2305ae75">dump</a>(os);
<a name="l00315"></a>00315 <span class="keywordflow">return</span> os;
<a name="l00316"></a>00316 }
<a name="l00317"></a>00317 };
<a name="l00318"></a>00318 <span class="preprocessor">#endif</span>
<a name="l00319"></a>00319 <span class="preprocessor"></span>
<a name="l00320"></a>00320
<a name="l00321"></a>00321
<a name="l00322"></a>00322
<a name="l00323"></a>00323
<a name="l00324"></a>00324
<a name="l00325"></a>00325
<a name="l00326"></a>00326
<a name="l00327"></a>00327
<a name="l00328"></a>00328
<a name="l00329"></a>00329
</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>
