CVC3  2.4.1
Public Member Functions | Protected Attributes | List of all members
CDatabase Class Reference

#include <xchaff_dbase.h>

Inheritance diagram for CDatabase:
CSolver

Public Member Functions

 CDatabase ()
 
 ~CDatabase ()
 
void init (void)
 
vector< CVariable > & variables (void)
 
vector< CClause > & clauses (void)
 
CVariablevariable (int idx)
 
CClauseclause (ClauseIdx idx)
 
CDatabaseStatsstats (void)
 
void set_mem_limit (int n)
 
int & init_num_clauses ()
 
int & init_num_literals ()
 
int & num_added_clauses ()
 
int & num_added_literals ()
 
int & num_deleted_clauses ()
 
int & num_deleted_literals ()
 
CLitPoolElementlit_pool_begin (void)
 
CLitPoolElementlit_pool_end (void)
 
void lit_pool_push_back (int value)
 
int lit_pool_size (void)
 
int lit_pool_free_space (void)
 
CLitPoolElementlit_pool (int i)
 
void output_lit_pool_state (void)
 
bool enlarge_lit_pool (void)
 
void compact_lit_pool (void)
 
int estimate_mem_usage (void)
 
int mem_usage (void)
 
void set_variable_number (int n)
 
int add_variable (void)
 
int num_variables (void)
 
int num_clauses (void)
 
int num_literals (void)
 
void mark_clause_deleted (CClause &cl)
 
void mark_var_in_new_cl (int v_idx, int phase)
 
int literal_value (CLitPoolElement l)
 
int find_unit_literal (ClauseIdx cl)
 
bool is_conflict (ClauseIdx cl)
 
bool is_satisfied (ClauseIdx cl)
 
void detail_dump_cl (ClauseIdx cl_idx, ostream &os=cout)
 
void dump (ostream &os=cout)
 

Protected Attributes

CDatabaseStats _stats
 
CLitPoolElement_lit_pool_start
 
CLitPoolElement_lit_pool_finish
 
CLitPoolElement_lit_pool_end_storage
 
vector< CVariable_variables
 
vector< CClause_clauses
 
queue< ClauseIdx_unused_clause_idx_queue
 
int _num_var_in_new_cl
 
int _mem_limit
 

Detailed Description

Class**********************************************************************

Synopsis [Definition of clause database ]

Description [Clause Database is the place where the information of the SAT problem are stored. it is a parent class of CSolver ]

SeeAlso [CSolver]

Definition at line 90 of file xchaff_dbase.h.

Constructor & Destructor Documentation

CDatabase::CDatabase ( )
CDatabase::~CDatabase ( )
inline

Definition at line 109 of file xchaff_dbase.h.

References _lit_pool_start.

Member Function Documentation

void CDatabase::init ( void  )
inline

Definition at line 112 of file xchaff_dbase.h.

References init_num_clauses(), init_num_literals(), num_clauses(), and num_literals().

Referenced by CSolver::init().

vector<CVariable>& CDatabase::variables ( void  )
inline
vector<CClause>& CDatabase::clauses ( void  )
inline
CVariable& CDatabase::variable ( int  idx)
inline
CClause& CDatabase::clause ( ClauseIdx  idx)
inline
CDatabaseStats& CDatabase::stats ( void  )
inline

Definition at line 129 of file xchaff_dbase.h.

References _stats.

void CDatabase::set_mem_limit ( int  n)
inline

Definition at line 132 of file xchaff_dbase.h.

Referenced by CSolver::set_mem_limit().

int& CDatabase::init_num_clauses ( )
inline
int& CDatabase::init_num_literals ( )
inline

Definition at line 137 of file xchaff_dbase.h.

References CDatabaseStats::init_num_literals.

Referenced by init().

int& CDatabase::num_added_clauses ( )
inline

Definition at line 138 of file xchaff_dbase.h.

References CDatabaseStats::num_added_clauses.

int& CDatabase::num_added_literals ( )
inline

Definition at line 139 of file xchaff_dbase.h.

References CDatabaseStats::num_added_literals.

int& CDatabase::num_deleted_clauses ( )
inline
int& CDatabase::num_deleted_literals ( )
inline
CLitPoolElement* CDatabase::lit_pool_begin ( void  )
inline

Definition at line 144 of file xchaff_dbase.h.

References _lit_pool_start.

Referenced by compact_lit_pool().

CLitPoolElement* CDatabase::lit_pool_end ( void  )
inline

Definition at line 147 of file xchaff_dbase.h.

References _lit_pool_finish.

Referenced by CSolver::add_clause().

void CDatabase::lit_pool_push_back ( int  value)
inline

Definition at line 150 of file xchaff_dbase.h.

References _lit_pool_finish, and CLitPoolElement::val().

Referenced by CSolver::add_clause(), and CDatabase().

int CDatabase::lit_pool_size ( void  )
inline
int CDatabase::lit_pool_free_space ( void  )
inline
CLitPoolElement& CDatabase::lit_pool ( int  i)
inline

Definition at line 161 of file xchaff_dbase.h.

Referenced by compact_lit_pool(), estimate_mem_usage(), and mem_usage().

void CDatabase::output_lit_pool_state ( void  )
bool CDatabase::enlarge_lit_pool ( void  )
void CDatabase::compact_lit_pool ( void  )
int CDatabase::estimate_mem_usage ( void  )
inline
int CDatabase::mem_usage ( void  )
inline
void CDatabase::set_variable_number ( int  n)
inline

Definition at line 203 of file xchaff_dbase.h.

References variables().

int CDatabase::add_variable ( void  )
inline

Definition at line 206 of file xchaff_dbase.h.

References variables().

int CDatabase::num_variables ( void  )
inline
int CDatabase::num_clauses ( void  )
inline

Definition at line 214 of file xchaff_dbase.h.

Referenced by enlarge_lit_pool(), init(), Xchaff::NumClauses(), and output_lit_pool_state().

int CDatabase::num_literals ( void  )
inline
void CDatabase::mark_clause_deleted ( CClause cl)
inline
void CDatabase::mark_var_in_new_cl ( int  v_idx,
int  phase 
)
inline

Definition at line 231 of file xchaff_dbase.h.

References _num_var_in_new_cl, CVariable::set_in_new_cl(), and variable().

int CDatabase::literal_value ( CLitPoolElement  l)
inline
int CDatabase::find_unit_literal ( ClauseIdx  cl)
bool CDatabase::is_conflict ( ClauseIdx  cl)
bool CDatabase::is_satisfied ( ClauseIdx  cl)

Definition at line 488 of file xchaff_solver.cpp.

References clause(), literal_value(), and CClause::literals().

void CDatabase::detail_dump_cl ( ClauseIdx  cl_idx,
ostream &  os = cout 
)
void CDatabase::dump ( ostream &  os = cout)

Definition at line 197 of file xchaff_dbase.cpp.

References _clauses, _variables, detail_dump_cl(), std::endl(), and variable().

Referenced by CSolver::dump().

Member Data Documentation

CDatabaseStats CDatabase::_stats
protected
CLitPoolElement* CDatabase::_lit_pool_start
protected

Definition at line 96 of file xchaff_dbase.h.

Referenced by CDatabase(), enlarge_lit_pool(), lit_pool_begin(), lit_pool_size(), and ~CDatabase().

CLitPoolElement* CDatabase::_lit_pool_finish
protected
CLitPoolElement* CDatabase::_lit_pool_end_storage
protected

Definition at line 98 of file xchaff_dbase.h.

Referenced by CDatabase(), and enlarge_lit_pool().

vector<CVariable> CDatabase::_variables
protected
vector<CClause> CDatabase::_clauses
protected

Definition at line 101 of file xchaff_dbase.h.

Referenced by CSolver::add_clause(), clauses(), and dump().

queue<ClauseIdx> CDatabase::_unused_clause_idx_queue
protected

Definition at line 102 of file xchaff_dbase.h.

Referenced by CSolver::add_clause(), and CSolver::delete_unrelevant_clauses().

int CDatabase::_num_var_in_new_cl
protected

Definition at line 104 of file xchaff_dbase.h.

Referenced by mark_var_in_new_cl().

int CDatabase::_mem_limit
protected

Definition at line 105 of file xchaff_dbase.h.

Referenced by CDatabase(), and enlarge_lit_pool().


The documentation for this class was generated from the following files: