#include <xchaff_base.h>
Synopsis [Definition of a literal]
Description [A literal is a variable with phase. Two thing determing a lteral: it's "sign", and the variable index. One bit is used to mark it's sign. 0->positive, 1->negative.
For every clause with literal count larger than 1, there are two special literals which are designated ht_literal (stands for head/tail literal to imitate SATO) It is specially marked with 2 bits: 00->not ht; dir = 1; or dir = -1; 10 is not valid. Each literal is represented by a 32 bit integer, with one bit representing it's phase and 2 bits indicate h/t property.
All the literals are collected in a storage space called literal pool. An element in a literal pool can be a literal or special spacing element to indicate the termination of a clause. The spacing element has negative value of the clause index.]
Definition at line 81 of file xchaff_base.h.
CLitPoolElement::CLitPoolElement | ( | void | ) | [inline] |
CLitPoolElement::CLitPoolElement | ( | int | val | ) | [inline] |
Definition at line 90 of file xchaff_base.h.
int& CLitPoolElement::val | ( | void | ) | [inline] |
Definition at line 92 of file xchaff_base.h.
References _val.
Referenced by CDatabase::compact_lit_pool(), CDatabase::lit_pool_push_back(), CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
int CLitPoolElement::s_var | ( | void | ) | [inline] |
Definition at line 95 of file xchaff_base.h.
References _val.
Referenced by Xchaff::GetClauseLits(), CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
int CLitPoolElement::var_index | ( | void | ) | [inline] |
Definition at line 98 of file xchaff_base.h.
References _val.
Referenced by CSolver::add_clause(), CDatabase::compact_lit_pool(), CDatabase::detail_dump_cl(), dump(), CDatabase::literal_value(), CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
bool CLitPoolElement::var_sign | ( | void | ) | [inline] |
Definition at line 101 of file xchaff_base.h.
References _val.
Referenced by CSolver::add_clause(), CDatabase::compact_lit_pool(), dump(), and CDatabase::literal_value().
void CLitPoolElement::set | ( | int | s_var | ) | [inline] |
void CLitPoolElement::set | ( | int | v, | |
int | s | |||
) | [inline] |
int CLitPoolElement::direction | ( | void | ) | [inline] |
Definition at line 111 of file xchaff_base.h.
References _val.
Referenced by CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
bool CLitPoolElement::is_ht | ( | void | ) | [inline] |
void CLitPoolElement::unset_ht | ( | void | ) | [inline] |
Definition at line 117 of file xchaff_base.h.
References _val.
Referenced by CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
void CLitPoolElement::set_ht | ( | int | dir | ) | [inline] |
bool CLitPoolElement::is_literal | ( | void | ) | [inline] |
void CLitPoolElement::set_clause_index | ( | int | cl_idx | ) | [inline] |
int CLitPoolElement::get_clause_index | ( | void | ) | [inline] |
int CLitPoolElement::find_clause_idx | ( | void | ) | [inline] |
void CLitPoolElement::dump | ( | ostream & | os = cout |
) | [inline] |
ostream& operator<< | ( | ostream & | os, | |
CLitPoolElement & | l | |||
) | [friend] |
Definition at line 145 of file xchaff_base.h.
int CLitPoolElement::_val [protected] |
Definition at line 84 of file xchaff_base.h.
Referenced by CLitPoolElement(), direction(), get_clause_index(), is_ht(), is_literal(), s_var(), set(), set_clause_index(), set_ht(), unset_ht(), val(), var_index(), and var_sign().