Public Member Functions | Protected Attributes | Friends

CClause Class Reference

#include <xchaff_base.h>

Collaboration diagram for CClause:
Collaboration graph

List of all members.

Public Member Functions

Protected Attributes


Detailed Description


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]
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]
bool& CClause::in_use ( void  ) [inline]
CLitPoolElement& CClause::literal ( int  idx) [inline]
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

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: