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(), 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().

---

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

---