CDatabase Class Reference

#include <xchaff_dbase.h>

Inheritance diagram for CDatabase:

[legend]Collaboration diagram for CDatabase:

[legend]List of all members.

Public Member Functions

CDatabase ()
~CDatabase ()
void init (void)
vector< CVariable > & variables (void)
vector< CClause > & clauses (void)
CVariable & variable (int idx)
CClause & clause (ClauseIdx idx)
CDatabaseStats & stats (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 ()
CLitPoolElement * lit_pool_begin (void)
CLitPoolElement * lit_pool_end (void)
void lit_pool_push_back (int value)
int lit_pool_size (void)
int lit_pool_free_space (void)
CLitPoolElement & lit_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 ( )

Definition at line 41 of file xchaff_dbase.cpp.
References _lit_pool_end_storage, _lit_pool_finish, _lit_pool_start, _mem_limit, _stats, CDatabaseStats::init_num_clauses, CDatabaseStats::init_num_literals, lit_pool_push_back(), CDatabaseStats::mem_used_up, CDatabaseStats::mem_used_up_counts, CDatabaseStats::num_added_clauses, CDatabaseStats::num_added_literals, CDatabaseStats::num_deleted_clauses, and CDatabaseStats::num_deleted_literals.

CDatabase::~CDatabase ( ) [inline]

Definition at line 109 of file xchaff_dbase.h.
References _lit_pool_start.

Member Function Documentation

void CDatabase::init ( void ) [inline]

Reimplemented in CSolver.
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]

Definition at line 117 of file xchaff_dbase.h.
References _variables.
Referenced by CSolver::add_clause(), add_variable(), CSolver::add_variables(), compact_lit_pool(), CSolver::conflict_analysis_zchaff(), CSolver::decide_next_branch(), CSolver::deduce(), CSolver::delete_unrelevant_clauses(), enlarge_lit_pool(), estimate_mem_usage(), CSolver::init(), mem_usage(), num_variables(), CSolver::preprocess(), CSolver::restart(), set_variable_number(), CSolver::update_var_stats(), and CSolver::~CSolver().

vector<CClause>& CDatabase::clauses ( void ) [inline]

Definition at line 120 of file xchaff_dbase.h.
References _clauses.
Referenced by CSolver::delete_unrelevant_clauses(), enlarge_lit_pool(), estimate_mem_usage(), mem_usage(), and CSolver::preprocess().

CVariable& CDatabase::variable ( int idx ) [inline]

Definition at line 123 of file xchaff_dbase.h.
References _variables.
Referenced by CSolver::add_clause(), compact_lit_pool(), CSolver::conflict_analysis_zchaff(), detail_dump_cl(), dump(), CSolver::dump_assignment_stack(), enlarge_lit_pool(), Xchaff::GetVarAssignment(), literal_value(), mark_clause_deleted(), mark_var_in_new_cl(), CSolver::mark_vars_at_level(), mem_usage(), CSolver::preprocess(), CSolver::restart(), CSolver::set_var_value_not_current_dl(), CSolver::set_var_value_with_current_dl(), CSolver::unset_var_value(), and CSolver::update_var_stats().

CClause& CDatabase::clause ( ClauseIdx idx ) [inline]

Definition at line 126 of file xchaff_dbase.h.
References _clauses.
Referenced by CSolver::add_clause(), compact_lit_pool(), CSolver::conflict_analysis_zchaff(), detail_dump_cl(), enlarge_lit_pool(), CSolver::find_max_clause_dlevel(), find_unit_literal(), Xchaff::GetClause(), Xchaff::GetFirstClause(), Xchaff::GetNextClause(), is_conflict(), is_satisfied(), CSolver::mark_vars_at_level(), and CSolver::preprocess().

CDatabaseStats& CDatabase::stats ( void ) [inline]

Definition at line 129 of file xchaff_dbase.h.
References _stats.

void CDatabase::set_mem_limit ( int n ) [inline]

Reimplemented in CSolver.
Definition at line 132 of file xchaff_dbase.h.
References _mem_limit.
Referenced by CSolver::set_mem_limit().

int& CDatabase::init_num_clauses ( ) [inline]

Definition at line 136 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::init_num_clauses.
Referenced by CSolver::delete_unrelevant_clauses(), Xchaff::GetClause(), and init().

int& CDatabase::init_num_literals ( ) [inline]

Definition at line 137 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::init_num_literals.
Referenced by init().

int& CDatabase::num_added_clauses ( ) [inline]

Definition at line 138 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::num_added_clauses.

int& CDatabase::num_added_literals ( ) [inline]

Definition at line 139 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::num_added_literals.

int& CDatabase::num_deleted_clauses ( ) [inline]

Definition at line 140 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::num_deleted_clauses.
Referenced by CSolver::delete_unrelevant_clauses(), and Xchaff::GetNumDeletedClauses().

int& CDatabase::num_deleted_literals ( ) [inline]

Definition at line 141 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::num_deleted_literals.
Referenced by CSolver::delete_unrelevant_clauses(), and Xchaff::GetNumDeletedLiterals().

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_end_storage, _lit_pool_finish, and CLitPoolElement::val().
Referenced by CSolver::add_clause(), and CDatabase().

int CDatabase::lit_pool_size ( void ) [inline]

Definition at line 155 of file xchaff_dbase.h.
References _lit_pool_finish, and _lit_pool_start.
Referenced by compact_lit_pool(), enlarge_lit_pool(), estimate_mem_usage(), mem_usage(), and output_lit_pool_state().

int CDatabase::lit_pool_free_space ( void ) [inline]

Definition at line 158 of file xchaff_dbase.h.
References _lit_pool_end_storage, and _lit_pool_finish.
Referenced by CSolver::add_clause(), estimate_mem_usage(), mem_usage(), and output_lit_pool_state().

CLitPoolElement& CDatabase::lit_pool ( int i ) [inline]

Definition at line 161 of file xchaff_dbase.h.
References _lit_pool_start.
Referenced by compact_lit_pool(), estimate_mem_usage(), and mem_usage().

void CDatabase::output_lit_pool_state ( void )

Definition at line 167 of file xchaff_dbase.cpp.
References std::endl(), lit_pool_free_space(), lit_pool_size(), num_clauses(), and num_literals().
Referenced by compact_lit_pool(), and enlarge_lit_pool().

bool CDatabase::enlarge_lit_pool ( void )

Definition at line 100 of file xchaff_dbase.cpp.
References _lit_pool_end_storage, _lit_pool_finish, _lit_pool_start, _mem_limit, _stats, clause(), clauses(), compact_lit_pool(), std::endl(), estimate_mem_usage(), CClause::first_lit(), CVariable::ht_ptr(), lit_pool_size(), CDatabaseStats::mem_used_up, num_clauses(), num_literals(), output_lit_pool_state(), variable(), and variables().
Referenced by CSolver::add_clause().

void CDatabase::compact_lit_pool ( void )

Definition at line 62 of file xchaff_dbase.cpp.
References _lit_pool_finish, clause(), std::endl(), CClause::first_lit(), CVariable::ht_ptr(), lit_pool(), lit_pool_begin(), lit_pool_size(), CClause::num_lits(), output_lit_pool_state(), CLitPoolElement::val(), CLitPoolElement::var_index(), CLitPoolElement::var_sign(), variable(), and variables().
Referenced by enlarge_lit_pool().

int CDatabase::estimate_mem_usage ( void ) [inline]

Reimplemented in CSolver.
Definition at line 172 of file xchaff_dbase.h.
References _unused_clause_idx_queue, clauses(), lit_pool(), lit_pool_free_space(), lit_pool_size(), and variables().
Referenced by enlarge_lit_pool(), and CSolver::estimate_mem_usage().

int CDatabase::mem_usage ( void ) [inline]

Reimplemented in CSolver.
Definition at line 188 of file xchaff_dbase.h.
References _unused_clause_idx_queue, clauses(), CVariable::ht_ptr(), lit_pool(), lit_pool_free_space(), lit_pool_size(), variable(), and variables().
Referenced by CSolver::mem_usage().

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]

Definition at line 210 of file xchaff_dbase.h.
References variables().
Referenced by Xchaff::GetFirstVar(), Xchaff::GetNextVar(), CSolver::init(), and Xchaff::NumVariables().

int CDatabase::num_clauses ( void ) [inline]

Definition at line 214 of file xchaff_dbase.h.
References _clauses, and _unused_clause_idx_queue.
Referenced by enlarge_lit_pool(), init(), Xchaff::NumClauses(), and output_lit_pool_state().

int CDatabase::num_literals ( void ) [inline]

Definition at line 217 of file xchaff_dbase.h.
References _stats, CDatabaseStats::num_added_literals, and CDatabaseStats::num_deleted_literals.
Referenced by enlarge_lit_pool(), Xchaff::GetNumLiterals(), init(), and output_lit_pool_state().

void CDatabase::mark_clause_deleted ( CClause & cl ) [inline]

Definition at line 221 of file xchaff_dbase.h.
References _stats, CClause::in_use(), CClause::literal(), CVariable::lits_count(), CDatabaseStats::num_deleted_clauses, CDatabaseStats::num_deleted_literals, CClause::num_lits(), CLitPoolElement::val(), CLitPoolElement::var_index(), CLitPoolElement::var_sign(), and variable().
Referenced by CSolver::delete_unrelevant_clauses().

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]

Definition at line 239 of file xchaff_dbase.h.
References CVariable::value(), CLitPoolElement::var_index(), CLitPoolElement::var_sign(), and variable().
Referenced by CSolver::add_clause(), CSolver::delete_unrelevant_clauses(), detail_dump_cl(), is_conflict(), is_satisfied(), CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().

int CDatabase::find_unit_literal ( ClauseIdx cl )

Definition at line 495 of file xchaff_solver.cpp.
References _variables, clause(), CClause::literals(), CLitPoolElement::s_var(), and UNKNOWN.
Referenced by CSolver::add_clause(), CSolver::conflict_analysis_zchaff(), CSolver::preprocess(), and CSolver::real_solve().

bool CDatabase::is_conflict ( ClauseIdx cl )

Definition at line 477 of file xchaff_solver.cpp.
References clause(), literal_value(), and CClause::literals().
Referenced by CSolver::add_clause(), and CSolver::conflict_analysis_zchaff().

bool CDatabase::is_satisfied ( ClauseIdx cl )

Definition at line 486 of file xchaff_solver.cpp.
References clause(), literal_value(), and CClause::literals().

void CDatabase::detail_dump_cl ( ClauseIdx cl_idx,

ostream & os = cout

)

Definition at line 176 of file xchaff_dbase.cpp.
References clause(), CVariable::dlevel(), std::endl(), CClause::in_use(), CClause::literal(), literal_value(), CClause::literals(), CClause::num_lits(), CLitPoolElement::var_index(), and variable().
Referenced by dump().

void CDatabase::dump ( ostream & os = cout )

Reimplemented in CSolver.
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]

Reimplemented in CSolver.
Definition at line 93 of file xchaff_dbase.h.
Referenced by CSolver::add_clause(), CDatabase(), CSolver::delete_unrelevant_clauses(), enlarge_lit_pool(), init_num_clauses(), init_num_literals(), mark_clause_deleted(), num_added_clauses(), num_added_literals(), num_deleted_clauses(), num_deleted_literals(), num_literals(), and stats().

CLitPoolElement* CDatabase::_lit_pool_start [protected]

Definition at line 96 of file xchaff_dbase.h.
Referenced by CDatabase(), enlarge_lit_pool(), lit_pool(), lit_pool_begin(), lit_pool_size(), and ~CDatabase().

CLitPoolElement* CDatabase::_lit_pool_finish [protected]

Definition at line 97 of file xchaff_dbase.h.
Referenced by CDatabase(), compact_lit_pool(), enlarge_lit_pool(), lit_pool_end(), lit_pool_free_space(), lit_pool_push_back(), and lit_pool_size().

CLitPoolElement* CDatabase::_lit_pool_end_storage [protected]

Definition at line 98 of file xchaff_dbase.h.
Referenced by CDatabase(), enlarge_lit_pool(), lit_pool_free_space(), and lit_pool_push_back().

vector<CVariable> CDatabase::_variables [protected]

Definition at line 100 of file xchaff_dbase.h.
Referenced by dump(), CSolver::find_max_clause_dlevel(), find_unit_literal(), CSolver::set_var_value(), variable(), and variables().

vector<CClause> CDatabase::_clauses [protected]

Definition at line 101 of file xchaff_dbase.h.
Referenced by CSolver::add_clause(), clause(), clauses(), dump(), and num_clauses().

queue<ClauseIdx> CDatabase::_unused_clause_idx_queue [protected]

Definition at line 102 of file xchaff_dbase.h.
Referenced by CSolver::add_clause(), CSolver::delete_unrelevant_clauses(), estimate_mem_usage(), mem_usage(), and num_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(), enlarge_lit_pool(), and set_mem_limit().

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

Generated on Thu Apr 13 16:57:37 2006 for CVC Lite by

1.4.4