xchaff_base.h

Go to the documentation of this file.
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 

Generated on Tue Jul 3 14:33:42 2007 for CVC3 by  doxygen 1.5.1