1 /* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */ 2 3 /********************************************************************* 4 Copyright 2000-2001, Princeton University. All rights reserved. 5 By using this software the USER indicates that he or she has read, 6 understood and will comply with the following: 7 8 --- Princeton University hereby grants USER nonexclusive permission 9 to use, copy and/or modify this software for internal, noncommercial, 10 research purposes only. Any distribution, including commercial sale 11 or license, of this software, copies of the software, its associated 12 documentation and/or modifications of either is strictly prohibited 13 without the prior consent of Princeton University. Title to copyright 14 to this software and its associated documentation shall at all times 15 remain with Princeton University. Appropriate copyright notice shall 16 be placed on all software copies, and a complete copy of this notice 17 shall be included in all copies of the associated documentation. 18 No right is granted to use in advertising, publicity or otherwise 19 any trademark, service mark, or the name of Princeton University. 20 21 22 --- This software and any associated documentation is provided "as is" 23 24 PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS 25 OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A 26 PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR 27 ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, 28 TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. 29 30 Princeton University shall not be liable under any circumstances for 31 any direct, indirect, special, incidental, or consequential damages 32 with respect to any claim by USER or any third party on account of 33 or arising from the use, or inability to use, this software or its 34 associated documentation, even if Princeton University has been advised 35 of the possibility of those damages. 36 *********************************************************************/ 37 38 39 #ifndef __BASIC_CLASSES__ 40 #define __BASIC_CLASSES__ 41 42 #include <vector> 43 #include <iostream> 44 #include <assert.h> 45 using namespace std; 46 47 typedef enum Unknown { 48 UNKNOWN = -1 49 } Unknown; 50 51 #define NULL_CLAUSE -1 52 #define FLIPPED -2 53 54 typedef int ClauseIdx; //used to refer a clause. Because of dynamic 55 //allocation of vector storage, no pointer is allowered 56 57 /**Class********************************************************************** 58 59 Synopsis [Definition of a literal] 60 61 Description [A literal is a variable with phase. Two thing determing a lteral: 62 it's "sign", and the variable index. One bit is used to mark it's 63 sign. 0->positive, 1->negative. 64 65 For every clause with literal count larger than 1, there are two 66 special literals which are designated ht_literal (stands for 67 head/tail literal to imitate SATO) It is specially marked with 2 bits: 68 00->not ht; dir = 1; or dir = -1; 10 is not valid. 69 Each literal is represented by a 32 bit integer, with one bit 70 representing it's phase and 2 bits indicate h/t property. 71 72 All the literals are collected in a storage space called literal 73 pool. An element in a literal pool can be a literal or special 74 spacing element to indicate the termination of a clause. The 75 spacing element has negative value of the clause index.] 76 77 SeeAlso [CDatabase, CClause] 78 79 ******************************************************************************/ 80 81 class CLitPoolElement 82 { 83 protected: 84 int _val; 85 public: 86 //======constructors & destructors============ CLitPoolElement(void)87 CLitPoolElement(void) { 88 _val=0; 89 } CLitPoolElement(int val)90 CLitPoolElement(int val):_val(val){} 91 //=========member access function============= val(void)92 int & val(void) { 93 return _val; 94 } s_var(void)95 int s_var(void) { //stands for signed variable, i.e. 2*var_idx + sign 96 return _val>>2; 97 } var_index(void)98 int var_index(void) { 99 return _val>>3; 100 } var_sign(void)101 bool var_sign(void) { 102 return ( (_val>> 2)& 0x1); 103 } set(int s_var)104 void set (int s_var) { 105 _val = (s_var << 2); 106 } set(int v,int s)107 void set(int v, int s) { 108 _val = (((v<<1) + s)<< 2); 109 } 110 //following are the functions for the special head/tail literals for FAST_BCP direction(void)111 int direction (void) { 112 return ((_val&0x03) - 2); 113 } is_ht(void)114 bool is_ht(void) { 115 return _val&0x03; 116 } unset_ht(void)117 void unset_ht(void) { 118 _val = _val & (0x0fffffffc); 119 } set_ht(int dir)120 void set_ht(int dir) { 121 _val = _val + dir + 2; 122 } 123 124 //following are used for spacing (e.g. indicate clause's end) is_literal(void)125 bool is_literal(void) { 126 return _val > 0; 127 } set_clause_index(int cl_idx)128 void set_clause_index(int cl_idx) { 129 _val = - cl_idx; 130 } get_clause_index(void)131 int get_clause_index(void) { 132 return -_val; 133 } 134 //misc functions find_clause_idx(void)135 int find_clause_idx(void) { 136 CLitPoolElement * ptr; 137 for (ptr = this; ptr->is_literal(); ++ ptr); 138 return ptr->get_clause_index(); 139 } 140 141 void dump(ostream & os= cout) { 142 os << (var_sign()?" -":" +") << var_index(); 143 if (is_ht()) os << "*"; 144 } 145 friend ostream & operator << ( ostream & os, CLitPoolElement & l) { 146 l.dump(os); 147 return os; 148 } 149 }; 150 151 /**Class********************************************************************** 152 153 Synopsis [Definition of a clause] 154 155 Description [A clause is consisted of a certain number of literals. 156 All literals are collected in a single large vector, we call it 157 literal pool. Each clause has a pointer to the beginning position 158 of it's literals in the pool. The boolean propagation mechanism 159 use two pointers (called head/tail pointer, by sato's convention) 160 which always point to the last assigned literals of this clause.] 161 162 SeeAlso [CDatabase] 163 164 ******************************************************************************/ 165 class CClause 166 { 167 protected: 168 CLitPoolElement * _first_lit; //pointer to the first literal in literal pool 169 int _num_lits; //number of literals 170 bool _in_use; //indicate if this clause has been deleted or not 171 public: 172 //constructors & destructors CClause(void)173 CClause(void){} 174 ~CClause()175 ~CClause() {} 176 //initialization & clear up init(CLitPoolElement * head,int num_lits)177 void init(CLitPoolElement * head, int num_lits) { //initialization of a clause 178 _first_lit = head; 179 _num_lits = num_lits; 180 _in_use = true; 181 } 182 //member access function literals(void)183 CLitPoolElement * literals(void) { //literals()[i] is it's the i-th literal 184 return _first_lit; 185 } first_lit(void)186 CLitPoolElement * & first_lit(void) { //use it only if you want to modify _first_lit 187 return _first_lit; 188 } num_lits(void)189 int & num_lits(void) { 190 return _num_lits; 191 } in_use(void)192 bool & in_use(void) { 193 return _in_use; 194 } literal(int idx)195 CLitPoolElement & literal(int idx) { //return the idx-th literal 196 return literals()[idx]; 197 } 198 //misc functions 199 void dump(ostream & os = cout) { 200 if (!in_use()) 201 os << "\t\t\t======removed====="; 202 for (int i=0, sz=num_lits(); i<sz; ++i) 203 os << literal(i); 204 os << endl; 205 } 206 // friend ostream & operator << (ostream & os, CClause & cl); 207 friend ostream & operator << ( ostream & os, CClause & cl) { 208 cl.dump(os); 209 return os; 210 } 211 }; 212 213 214 /**Class********************************************************************** 215 216 Synopsis [Definition of a variable] 217 218 Description [CVariable contains the necessary information for a variable. 219 _ht_ptrs are the head/tail literals of this variable (int two phases)] 220 221 SeeAlso [CDatabase] 222 223 ******************************************************************************/ 224 class CVariable 225 { 226 protected: 227 bool _is_marked : 1; //used in conflict analysis. 228 229 int _in_new_cl : 2; //it can take 3 value 0: pos phase, 230 //1: neg phase, -1 : not in new clause; 231 //used to keep track of literals appearing 232 //in newly added clause so that a. each 233 //variable can only appearing in one phase 234 //b. same literal won't appear more than once. 235 236 ClauseIdx _antecedence : 29; //used in conflict analysis 237 238 short _value; //can be 1, 0 or UNKNOWN 239 240 short _dlevel; //decision level this variable being assigned 241 242 vector<CLitPoolElement *> _ht_ptrs[2]; //literal of this var appearing in h/t. 0: pos, 1: neg 243 244 protected: 245 int _lits_count[2]; 246 int _scores[2]; 247 int _var_score_pos; 248 public: score(int i)249 int & score(int i) { return _scores[i]; } score(void)250 int score(void) { return score(0)>score(1)?score(0):score(1); } var_score_pos(void)251 int & var_score_pos(void) { return _var_score_pos; } 252 public: 253 //constructors & destructors CVariable(void)254 CVariable(void) { 255 _value = UNKNOWN; 256 _antecedence=NULL_CLAUSE; 257 _dlevel = -1; 258 _in_new_cl = -1; 259 _is_marked = false; 260 _scores[0] = _scores[1] = 0; 261 _var_score_pos = _lits_count[0] = _lits_count[1] = 0; 262 } 263 //member access function value(void)264 short & value(void) { 265 return _value; 266 } dlevel(void)267 short & dlevel(void) { 268 return _dlevel; 269 } in_new_cl(void)270 int in_new_cl(void) { 271 return _in_new_cl; 272 } set_in_new_cl(int phase)273 void set_in_new_cl(int phase) { 274 _in_new_cl = phase; 275 } lits_count(int i)276 int & lits_count(int i) { 277 return _lits_count[i]; 278 } 279 is_marked(void)280 bool is_marked(void) { 281 return _is_marked; 282 } set_marked(void)283 void set_marked(void) { 284 _is_marked = true; 285 } clear_marked(void)286 void clear_marked(void) { 287 _is_marked = false; 288 } 289 get_antecedence(void)290 ClauseIdx get_antecedence(void) { 291 return _antecedence; 292 } set_antecedence(ClauseIdx ante)293 void set_antecedence(ClauseIdx ante) { 294 _antecedence = ante; 295 } 296 ht_ptr(int i)297 vector<CLitPoolElement *> & ht_ptr(int i) { return _ht_ptrs[i]; } 298 299 //misc functions 300 void dump(ostream & os=cout) { 301 if (is_marked()) os << "*" ; 302 os << "V: " << _value << " DL: " << _dlevel 303 << " Ante: " << _antecedence << endl; 304 for (int j=0; j< 2; ++j) { 305 os << (j==0?"Pos ":"Neg ") << "(" ; 306 for (unsigned i=0; i< ht_ptr(j).size(); ++i ) 307 os << ht_ptr(j)[i]->find_clause_idx() << " " ; 308 os << ")" << endl; 309 } 310 os << endl; 311 } 312 // friend ostream & operator << (ostream & os, CVariable & v); 313 friend ostream & operator << ( ostream & os, CVariable & v) { 314 v.dump(os); 315 return os; 316 } 317 }; 318 #endif 319 320 321 322 323 324 325 326 327 328 329 330