CClause Class Reference

#include <xchaff_base.h>

Collaboration diagram for CClause:

[legend]List of all members.

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. 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(), CSolver::find_max_clause_dlevel(), CDatabase::find_unit_literal(), 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(), CSolver::delete_unrelevant_clauses(), CDatabase::detail_dump_cl(), dump(), 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 CSolver::delete_unrelevant_clauses(), 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 CSolver::delete_unrelevant_clauses(), CDatabase::detail_dump_cl(), dump(), 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().

---

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. Referenced by first_lit(), init(), and literals().

int CClause::_num_lits [protected]

Definition at line 169 of file xchaff_base.h. Referenced by init(), and num_lits().

bool CClause::_in_use [protected]

Definition at line 170 of file xchaff_base.h. Referenced by in_use(), and init().

---

The documentation for this class was generated from the following file:

• xchaff_base.h

---