00001 /* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */ 00002 00003 /********************************************************************* 00004 Copyright 2000-2001, Princeton University. All rights reserved. 00005 By using this software the USER indicates that he or she has read, 00006 understood and will comply with the following: 00007 00008 --- Princeton University hereby grants USER nonexclusive permission 00009 to use, copy and/or modify this software for internal, noncommercial, 00010 research purposes only. Any distribution, including commercial sale 00011 or license, of this software, copies of the software, its associated 00012 documentation and/or modifications of either is strictly prohibited 00013 without the prior consent of Princeton University. Title to copyright 00014 to this software and its associated documentation shall at all times 00015 remain with Princeton University. Appropriate copyright notice shall 00016 be placed on all software copies, and a complete copy of this notice 00017 shall be included in all copies of the associated documentation. 00018 No right is granted to use in advertising, publicity or otherwise 00019 any trademark, service mark, or the name of Princeton University. 00020 00021 00022 --- This software and any associated documentation is provided "as is" 00023 00024 PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS 00025 OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A 00026 PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR 00027 ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, 00028 TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. 00029 00030 Princeton University shall not be liable under any circumstances for 00031 any direct, indirect, special, incidental, or consequential damages 00032 with respect to any claim by USER or any third party on account of 00033 or arising from the use, or inability to use, this software or its 00034 associated documentation, even if Princeton University has been advised 00035 of the possibility of those damages. 00036 *********************************************************************/ 00037 00038 00039 #ifndef __BASIC_CLASSES__ 00040 #define __BASIC_CLASSES__ 00041 00042 #include <vector> 00043 #include <iostream> 00044 #include <assert.h> 00045 using namespace std; 00046 00047 typedef enum Unknown { 00048 UNKNOWN = -1 00049 } Unknown; 00050 00051 #define NULL_CLAUSE -1 00052 #define FLIPPED -2 00053 00054 typedef int ClauseIdx; //used to refer a clause. Because of dynamic 00055 //allocation of vector storage, no pointer is allowered 00056 00057 /**Class********************************************************************** 00058 00059 Synopsis [Definition of a literal] 00060 00061 Description [A literal is a variable with phase. Two thing determing a lteral: 00062 it's "sign", and the variable index. One bit is used to mark it's 00063 sign. 0->positive, 1->negative. 00064 00065 For every clause with literal count larger than 1, there are two 00066 special literals which are designated ht_literal (stands for 00067 head/tail literal to imitate SATO) It is specially marked with 2 bits: 00068 00->not ht; dir = 1; or dir = -1; 10 is not valid. 00069 Each literal is represented by a 32 bit integer, with one bit 00070 representing it's phase and 2 bits indicate h/t property. 00071 00072 All the literals are collected in a storage space called literal 00073 pool. An element in a literal pool can be a literal or special 00074 spacing element to indicate the termination of a clause. The 00075 spacing element has negative value of the clause index.] 00076 00077 SeeAlso [CDatabase, CClause] 00078 00079 ******************************************************************************/ 00080 00081 class CLitPoolElement 00082 { 00083 protected: 00084 int _val; 00085 public: 00086 //======constructors & destructors============ 00087 CLitPoolElement(void) { 00088 _val=0; 00089 } 00090 CLitPoolElement(int val):_val(val){} 00091 //=========member access function============= 00092 int & val(void) { 00093 return _val; 00094 } 00095 int s_var(void) { //stands for signed variable, i.e. 2*var_idx + sign 00096 return _val>>2; 00097 } 00098 int var_index(void) { 00099 return _val>>3; 00100 } 00101 bool var_sign(void) { 00102 return ( (_val>> 2)& 0x1); 00103 } 00104 void set (int s_var) { 00105 _val = (s_var << 2); 00106 } 00107 void set(int v, int s) { 00108 _val = (((v<<1) + s)<< 2); 00109 } 00110 //following are the functions for the special head/tail literals for FAST_BCP 00111 int direction (void) { 00112 return ((_val&0x03) - 2); 00113 } 00114 bool is_ht(void) { 00115 return _val&0x03; 00116 } 00117 void unset_ht(void) { 00118 _val = _val & (0x0fffffffc); 00119 } 00120 void set_ht(int dir) { 00121 _val = _val + dir + 2; 00122 } 00123 00124 //following are used for spacing (e.g. indicate clause's end) 00125 bool is_literal(void) { 00126 return _val > 0; 00127 } 00128 void set_clause_index(int cl_idx) { 00129 _val = - cl_idx; 00130 } 00131 int get_clause_index(void) { 00132 return -_val; 00133 } 00134 //misc functions 00135 int find_clause_idx(void) { 00136 CLitPoolElement * ptr; 00137 for (ptr = this; ptr->is_literal(); ++ ptr); 00138 return ptr->get_clause_index(); 00139 } 00140 00141 void dump(ostream & os= cout) { 00142 os << (var_sign()?" -":" +") << var_index(); 00143 if (is_ht()) os << "*"; 00144 } 00145 friend ostream & operator << ( ostream & os, CLitPoolElement & l) { 00146 l.dump(os); 00147 return os; 00148 } 00149 }; 00150 00151 /**Class********************************************************************** 00152 00153 Synopsis [Definition of a clause] 00154 00155 Description [A clause is consisted of a certain number of literals. 00156 All literals are collected in a single large vector, we call it 00157 literal pool. Each clause has a pointer to the beginning position 00158 of it's literals in the pool. The boolean propagation mechanism 00159 use two pointers (called head/tail pointer, by sato's convention) 00160 which always point to the last assigned literals of this clause.] 00161 00162 SeeAlso [CDatabase] 00163 00164 ******************************************************************************/ 00165 class CClause 00166 { 00167 protected: 00168 CLitPoolElement * _first_lit; //pointer to the first literal in literal pool 00169 int _num_lits; //number of literals 00170 bool _in_use; //indicate if this clause has been deleted or not 00171 public: 00172 //constructors & destructors 00173 CClause(void){} 00174 00175 ~CClause() {} 00176 //initialization & clear up 00177 void init(CLitPoolElement * head, int num_lits) { //initialization of a clause 00178 _first_lit = head; 00179 _num_lits = num_lits; 00180 _in_use = true; 00181 } 00182 //member access function 00183 CLitPoolElement * literals(void) { //literals()[i] is it's the i-th literal 00184 return _first_lit; 00185 } 00186 CLitPoolElement * & first_lit(void) { //use it only if you want to modify _first_lit 00187 return _first_lit; 00188 } 00189 int & num_lits(void) { 00190 return _num_lits; 00191 } 00192 bool & in_use(void) { 00193 return _in_use; 00194 } 00195 CLitPoolElement & literal(int idx) { //return the idx-th literal 00196 return literals()[idx]; 00197 } 00198 //misc functions 00199 void dump(ostream & os = cout) { 00200 if (!in_use()) 00201 os << "\t\t\t======removed====="; 00202 for (int i=0, sz=num_lits(); i<sz; ++i) 00203 os << literal(i); 00204 os << endl; 00205 } 00206 // friend ostream & operator << (ostream & os, CClause & cl); 00207 friend ostream & operator << ( ostream & os, CClause & cl) { 00208 cl.dump(os); 00209 return os; 00210 } 00211 }; 00212 00213 00214 /**Class********************************************************************** 00215 00216 Synopsis [Definition of a variable] 00217 00218 Description [CVariable contains the necessary information for a variable. 00219 _ht_ptrs are the head/tail literals of this variable (int two phases)] 00220 00221 SeeAlso [CDatabase] 00222 00223 ******************************************************************************/ 00224 class CVariable 00225 { 00226 protected: 00227 bool _is_marked : 1; //used in conflict analysis. 00228 00229 int _in_new_cl : 2; //it can take 3 value 0: pos phase, 00230 //1: neg phase, -1 : not in new clause; 00231 //used to keep track of literals appearing 00232 //in newly added clause so that a. each 00233 //variable can only appearing in one phase 00234 //b. same literal won't appear more than once. 00235 00236 ClauseIdx _antecedence : 29; //used in conflict analysis 00237 00238 short _value; //can be 1, 0 or UNKNOWN 00239 00240 short _dlevel; //decision level this variable being assigned 00241 00242 vector<CLitPoolElement *> _ht_ptrs[2]; //literal of this var appearing in h/t. 0: pos, 1: neg 00243 00244 protected: 00245 int _lits_count[2]; 00246 int _scores[2]; 00247 int _var_score_pos; 00248 public: 00249 int & score(int i) { return _scores[i]; } 00250 int score(void) { return score(0)>score(1)?score(0):score(1); } 00251 int & var_score_pos(void) { return _var_score_pos; } 00252 public: 00253 //constructors & destructors 00254 CVariable(void) { 00255 _value = UNKNOWN; 00256 _antecedence=NULL_CLAUSE; 00257 _dlevel = -1; 00258 _in_new_cl = -1; 00259 _is_marked = false; 00260 _scores[0] = _scores[1] = 0; 00261 _var_score_pos = _lits_count[0] = _lits_count[1] = 0; 00262 } 00263 //member access function 00264 short & value(void) { 00265 return _value; 00266 } 00267 short & dlevel(void) { 00268 return _dlevel; 00269 } 00270 int in_new_cl(void) { 00271 return _in_new_cl; 00272 } 00273 void set_in_new_cl(int phase) { 00274 _in_new_cl = phase; 00275 } 00276 int & lits_count(int i) { 00277 return _lits_count[i]; 00278 } 00279 00280 bool is_marked(void) { 00281 return _is_marked; 00282 } 00283 void set_marked(void) { 00284 _is_marked = true; 00285 } 00286 void clear_marked(void) { 00287 _is_marked = false; 00288 } 00289 00290 ClauseIdx get_antecedence(void) { 00291 return _antecedence; 00292 } 00293 void set_antecedence(ClauseIdx ante) { 00294 _antecedence = ante; 00295 } 00296 00297 vector<CLitPoolElement *> & ht_ptr(int i) { return _ht_ptrs[i]; } 00298 00299 //misc functions 00300 void dump(ostream & os=cout) { 00301 if (is_marked()) os << "*" ; 00302 os << "V: " << _value << " DL: " << _dlevel 00303 << " Ante: " << _antecedence << endl; 00304 for (int j=0; j< 2; ++j) { 00305 os << (j==0?"Pos ":"Neg ") << "(" ; 00306 for (unsigned i=0; i< ht_ptr(j).size(); ++i ) 00307 os << ht_ptr(j)[i]->find_clause_idx() << " " ; 00308 os << ")" << endl; 00309 } 00310 os << endl; 00311 } 00312 // friend ostream & operator << (ostream & os, CVariable & v); 00313 friend ostream & operator << ( ostream & os, CVariable & v) { 00314 v.dump(os); 00315 return os; 00316 } 00317 }; 00318 #endif 00319 00320 00321 00322 00323 00324 00325 00326 00327 00328 00329