CClause Class Reference

#include <xchaff_base.h>

Collaboration diagram for CClause:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Attributes

Friends


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:
Generated on Tue Jul 3 14:35:24 2007 for CVC3 by  doxygen 1.5.1