CDatabase Class Reference

#include <xchaff_dbase.h>

Inherited by CSolver.

Collaboration diagram for CDatabase:

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, CDatabaseStats::num_deleted_literals, and STARTUP_LIT_POOL_SIZE.

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().

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(), Xchaff::GetFirstClause(), 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::GetClauseLits(), 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.

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, CHECK, clause(), clauses(), compact_lit_pool(), std::endl(), estimate_mem_usage(), CClause::first_lit(), CVariable::ht_ptr(), CClause::in_use(), 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, CHECK, clause(), std::endl(), CClause::first_lit(), CVariable::ht_ptr(), CLitPoolElement::is_ht(), 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().

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().

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(), 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 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 497 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 479 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 488 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(), 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().

---

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:

• xchaff_dbase.h
• xchaff_dbase.cpp
• xchaff_solver.cpp