CVC3
|
#include <xchaff_base.h>
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) |
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.
|
inline |
Definition at line 173 of file xchaff_base.h.
|
inline |
Definition at line 175 of file xchaff_base.h.
|
inline |
Definition at line 177 of file xchaff_base.h.
Referenced by CSolver::add_clause().
|
inline |
Definition at line 183 of file xchaff_base.h.
Referenced by CSolver::add_clause(), CDatabase::detail_dump_cl(), CSolver::find_max_clause_dlevel(), CDatabase::find_unit_literal(), CDatabase::is_conflict(), and CDatabase::is_satisfied().
|
inline |
Definition at line 186 of file xchaff_base.h.
Referenced by CDatabase::compact_lit_pool(), and CDatabase::enlarge_lit_pool().
|
inline |
Definition at line 189 of file xchaff_base.h.
Referenced by CSolver::add_clause(), CDatabase::compact_lit_pool(), CSolver::delete_unrelevant_clauses(), CDatabase::detail_dump_cl(), Xchaff::GetClauseLits(), CDatabase::mark_clause_deleted(), and CSolver::preprocess().
|
inline |
Definition at line 192 of file xchaff_base.h.
Referenced by CSolver::delete_unrelevant_clauses(), CDatabase::detail_dump_cl(), CDatabase::enlarge_lit_pool(), Xchaff::GetClause(), Xchaff::GetFirstClause(), Xchaff::GetNextClause(), and CDatabase::mark_clause_deleted().
|
inline |
Definition at line 195 of file xchaff_base.h.
Referenced by CSolver::delete_unrelevant_clauses(), CDatabase::detail_dump_cl(), Xchaff::GetClauseLits(), and CDatabase::mark_clause_deleted().
|
inline |
Definition at line 199 of file xchaff_base.h.
References std::endl().
|
friend |
Definition at line 207 of file xchaff_base.h.
|
protected |
Definition at line 168 of file xchaff_base.h.
|
protected |
Definition at line 169 of file xchaff_base.h.
|
protected |
Definition at line 170 of file xchaff_base.h.