#include <xchaff_base.h>
Collaboration diagram for CClause:
Synopsis [Definition of a clause]
Description [A clause is consisted of a certain number of literals. All literals are collected in a single large vector, we call it literal pool. Each clause has a pointer to the beginning position of it's literals in the pool. The boolean propagation mechanism use two pointers (called head/tail pointer, by sato's convention) which always point to the last assigned literals of this clause.]
SeeAlso [CDatabase]
Definition at line 165 of file xchaff_base.h.
CClause::CClause | ( | void | ) | [inline] |
Definition at line 173 of file xchaff_base.h.
CClause::~CClause | ( | ) | [inline] |
Definition at line 175 of file xchaff_base.h.
void CClause::init | ( | CLitPoolElement * | head, | |
int | num_lits | |||
) | [inline] |
Definition at line 177 of file xchaff_base.h.
References _first_lit, _in_use, and _num_lits.
Referenced by CSolver::add_clause().
CLitPoolElement* CClause::literals | ( | void | ) | [inline] |
Definition at line 183 of file xchaff_base.h.
References _first_lit.
Referenced by CSolver::add_clause(), CDatabase::detail_dump_cl(), CDatabase::is_conflict(), CDatabase::is_satisfied(), and literal().
CLitPoolElement* & CClause::first_lit | ( | void | ) | [inline] |
Definition at line 186 of file xchaff_base.h.
References _first_lit.
Referenced by CDatabase::compact_lit_pool(), and CDatabase::enlarge_lit_pool().
int& CClause::num_lits | ( | void | ) | [inline] |
Definition at line 189 of file xchaff_base.h.
References _num_lits.
Referenced by CSolver::add_clause(), CDatabase::compact_lit_pool(), CDatabase::detail_dump_cl(), dump(), Xchaff::GetClauseLits(), and CDatabase::mark_clause_deleted().
bool& CClause::in_use | ( | void | ) | [inline] |
Definition at line 192 of file xchaff_base.h.
References _in_use.
Referenced by CDatabase::detail_dump_cl(), dump(), Xchaff::GetClause(), Xchaff::GetFirstClause(), Xchaff::GetNextClause(), and CDatabase::mark_clause_deleted().
CLitPoolElement& CClause::literal | ( | int | idx | ) | [inline] |
Definition at line 195 of file xchaff_base.h.
References literals().
Referenced by CDatabase::detail_dump_cl(), dump(), Xchaff::GetClauseLits(), and CDatabase::mark_clause_deleted().
void CClause::dump | ( | ostream & | os = cout |
) | [inline] |
Definition at line 199 of file xchaff_base.h.
References std::endl(), in_use(), literal(), and num_lits().
ostream& operator<< | ( | ostream & | os, | |
CClause & | cl | |||
) | [friend] |
Definition at line 207 of file xchaff_base.h.
CLitPoolElement* CClause::_first_lit [protected] |
int CClause::_num_lits [protected] |
bool CClause::_in_use [protected] |