#include <xchaff_base.h>
Public Member Functions
- CClause (void)
- ~CClause ()
- void init (CLitPoolElement *head, int num_lits)
- CLitPoolElement * literals (void)
- CLitPoolElement *& first_lit (void)
- int & num_lits (void)
- bool & in_use (void)
- CLitPoolElement & literal (int idx)
- void dump (ostream &os=cout)
Protected Attributes
- CLitPoolElement * _first_lit
- int _num_lits
- bool _in_use
Friends
- ostream & operator<< (ostream &os, CClause &cl)
Detailed Description
Class**********************************************************************
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.
Constructor & Destructor Documentation
| 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.
Member Function Documentation
| void CClause::init | ( | CLitPoolElement * | head, |
| int | num_lits | ||
| ) | [inline] |
Definition at line 177 of file xchaff_base.h.
Referenced by CSolver::add_clause().
| CLitPoolElement* CClause::literals | ( | void | ) | [inline] |
Definition at line 183 of file xchaff_base.h.
Referenced by CSolver::add_clause(), CDatabase::detail_dump_cl(), CSolver::find_max_clause_dlevel(), CDatabase::find_unit_literal(), CDatabase::is_conflict(), and CDatabase::is_satisfied().
| CLitPoolElement* & CClause::first_lit | ( | void | ) | [inline] |
Definition at line 186 of file xchaff_base.h.
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.
Referenced by CSolver::add_clause(), CDatabase::compact_lit_pool(), CSolver::delete_unrelevant_clauses(), CDatabase::detail_dump_cl(), Xchaff::GetClauseLits(), CDatabase::mark_clause_deleted(), and CSolver::preprocess().
| bool& CClause::in_use | ( | void | ) | [inline] |
Definition at line 192 of file xchaff_base.h.
Referenced by CSolver::delete_unrelevant_clauses(), CDatabase::detail_dump_cl(), CDatabase::enlarge_lit_pool(), 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.
Referenced by CSolver::delete_unrelevant_clauses(), CDatabase::detail_dump_cl(), 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().
Friends And Related Function Documentation
| ostream& operator<< | ( | ostream & | os, |
| CClause & | cl | ||
| ) | [friend] |
Definition at line 207 of file xchaff_base.h.
Member Data Documentation
CLitPoolElement* CClause::_first_lit [protected] |
Definition at line 168 of file xchaff_base.h.
int CClause::_num_lits [protected] |
Definition at line 169 of file xchaff_base.h.
bool CClause::_in_use [protected] |
Definition at line 170 of file xchaff_base.h.
The documentation for this class was generated from the following file:
