#include <xchaff_dbase.h>
Inheritance diagram for CDatabase:
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.
| 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] |
| 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(), 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().
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] |
| 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, CHECK, 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, CHECK, 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] |
| int CDatabase::add_variable | ( | void | ) | [inline] |
| 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(), 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(), 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().
Referenced by CSolver::dump().
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] |
int CDatabase::_mem_limit [protected] |
Definition at line 105 of file xchaff_dbase.h.
Referenced by CDatabase(), enlarge_lit_pool(), and set_mem_limit().
1.5.1