CVC3
Public Member Functions | Protected Attributes | Friends | List of all members
CClause Class Reference

#include <xchaff_base.h>

Collaboration diagram for CClause:
Collaboration graph

Public Member Functions

 CClause (void)
 
 ~CClause ()
 
void init (CLitPoolElement *head, int num_lits)
 
CLitPoolElementliterals (void)
 
CLitPoolElement *& first_lit (void)
 
int & num_lits (void)
 
bool & in_use (void)
 
CLitPoolElementliteral (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
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

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: