39 #ifndef __BASIC_CLASSES__
40 #define __BASIC_CLASSES__
51 #define NULL_CLAUSE -1
102 return ( (_val>> 2)& 0x1);
108 _val = (((v<<1) + s)<< 2);
112 return ((_val&0x03) - 2);
118 _val = _val & (0x0fffffffc);
121 _val = _val + dir + 2;
141 void dump(ostream & os= cout) {
142 os << (var_sign()?
" -":
" +") << var_index();
143 if (is_ht()) os <<
"*";
179 _num_lits = num_lits;
196 return literals()[idx];
199 void dump(ostream & os = cout) {
201 os <<
"\t\t\t======removed=====";
202 for (
int i=0, sz=num_lits(); i<sz; ++i)
242 vector<CLitPoolElement *> _ht_ptrs[2];
249 int &
score(
int i) {
return _scores[i]; }
260 _scores[0] = _scores[1] = 0;
261 _var_score_pos = _lits_count[0] = _lits_count[1] = 0;
277 return _lits_count[i];
297 vector<CLitPoolElement *> &
ht_ptr(
int i) {
return _ht_ptrs[i]; }
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() <<
" " ;