CVC3
2.4.1
|
#include <xchaff_dbase.h>
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]
CDatabase::CDatabase | ( | ) |
Definition at line 41 of file xchaff_dbase.cpp.
References _stats, CDatabaseStats::mem_used_up_counts, CDatabaseStats::mem_used_up, CDatabaseStats::init_num_clauses, CDatabaseStats::init_num_literals, CDatabaseStats::num_added_clauses, CDatabaseStats::num_added_literals, CDatabaseStats::num_deleted_clauses, CDatabaseStats::num_deleted_literals, _lit_pool_start, STARTUP_LIT_POOL_SIZE, _lit_pool_finish, _lit_pool_end_storage, lit_pool_push_back(), and _mem_limit.
CDatabase::~CDatabase | ( | ) | [inline] |
Definition at line 109 of file xchaff_dbase.h.
References _lit_pool_start.
void CDatabase::init | ( | void | ) | [inline] |
Reimplemented in CSolver.
Definition at line 112 of file xchaff_dbase.h.
References init_num_clauses(), num_clauses(), init_num_literals(), and num_literals().
Definition at line 117 of file xchaff_dbase.h.
References _variables.
Referenced by compact_lit_pool(), enlarge_lit_pool(), estimate_mem_usage(), mem_usage(), set_variable_number(), add_variable(), num_variables(), CSolver::~CSolver(), CSolver::init(), CSolver::add_variables(), CSolver::add_clause(), CSolver::delete_unrelevant_clauses(), CSolver::update_var_stats(), CSolver::decide_next_branch(), CSolver::preprocess(), CSolver::deduce(), CSolver::conflict_analysis_zchaff(), and CSolver::restart().
Definition at line 120 of file xchaff_dbase.h.
References _clauses.
Referenced by Xchaff::GetFirstClause(), enlarge_lit_pool(), estimate_mem_usage(), mem_usage(), CSolver::delete_unrelevant_clauses(), and CSolver::preprocess().
CVariable& CDatabase::variable | ( | int | idx | ) | [inline] |
Definition at line 123 of file xchaff_dbase.h.
References _variables.
Referenced by Xchaff::GetVarAssignment(), compact_lit_pool(), enlarge_lit_pool(), detail_dump_cl(), dump(), mem_usage(), mark_clause_deleted(), mark_var_in_new_cl(), literal_value(), CSolver::add_clause(), CSolver::set_var_value_with_current_dl(), CSolver::set_var_value_not_current_dl(), CSolver::unset_var_value(), CSolver::dump_assignment_stack(), CSolver::update_var_stats(), CSolver::preprocess(), CSolver::mark_vars_at_level(), CSolver::conflict_analysis_zchaff(), and CSolver::restart().
Definition at line 126 of file xchaff_dbase.h.
References _clauses.
Referenced by Xchaff::GetClause(), Xchaff::GetClauseLits(), Xchaff::GetFirstClause(), Xchaff::GetNextClause(), compact_lit_pool(), enlarge_lit_pool(), detail_dump_cl(), CSolver::add_clause(), CSolver::find_max_clause_dlevel(), is_conflict(), is_satisfied(), find_unit_literal(), CSolver::preprocess(), CSolver::mark_vars_at_level(), and CSolver::conflict_analysis_zchaff().
CDatabaseStats& CDatabase::stats | ( | void | ) | [inline] |
Definition at line 129 of file xchaff_dbase.h.
References _stats.
void CDatabase::set_mem_limit | ( | int | n | ) | [inline] |
int& CDatabase::init_num_clauses | ( | ) | [inline] |
Definition at line 136 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::init_num_clauses.
Referenced by Xchaff::GetClause(), init(), and CSolver::delete_unrelevant_clauses().
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 Xchaff::GetNumDeletedClauses(), and CSolver::delete_unrelevant_clauses().
int& CDatabase::num_deleted_literals | ( | ) | [inline] |
Definition at line 141 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::num_deleted_literals.
Referenced by Xchaff::GetNumDeletedLiterals(), and CSolver::delete_unrelevant_clauses().
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, _lit_pool_end_storage, and CLitPoolElement::val().
Referenced by CDatabase(), and CSolver::add_clause().
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(), output_lit_pool_state(), estimate_mem_usage(), and mem_usage().
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 output_lit_pool_state(), estimate_mem_usage(), mem_usage(), and CSolver::add_clause().
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 lit_pool_size(), lit_pool_free_space(), num_clauses(), num_literals(), and std::endl().
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 CHECK, output_lit_pool_state(), lit_pool_size(), num_clauses(), num_literals(), compact_lit_pool(), std::endl(), estimate_mem_usage(), _mem_limit, _stats, CDatabaseStats::mem_used_up, _lit_pool_start, _lit_pool_finish, _lit_pool_end_storage, clauses(), clause(), CClause::in_use(), CClause::first_lit(), variables(), variable(), and CVariable::ht_ptr().
Referenced by CSolver::add_clause().
void CDatabase::compact_lit_pool | ( | void | ) |
Definition at line 62 of file xchaff_dbase.cpp.
References CHECK, std::endl(), lit_pool_size(), lit_pool(), CLitPoolElement::val(), _lit_pool_finish, lit_pool_begin(), variables(), variable(), CVariable::ht_ptr(), CLitPoolElement::is_ht(), CLitPoolElement::var_index(), CLitPoolElement::var_sign(), clause(), CClause::first_lit(), CClause::num_lits(), and output_lit_pool_state().
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 lit_pool(), lit_pool_size(), lit_pool_free_space(), variables(), clauses(), and _unused_clause_idx_queue.
Referenced by enlarge_lit_pool().
int CDatabase::mem_usage | ( | void | ) | [inline] |
Reimplemented in CSolver.
Definition at line 188 of file xchaff_dbase.h.
References lit_pool(), lit_pool_size(), lit_pool_free_space(), variables(), clauses(), _unused_clause_idx_queue, variable(), and CVariable::ht_ptr().
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::NumVariables(), Xchaff::GetFirstVar(), Xchaff::GetNextVar(), and CSolver::init().
int CDatabase::num_clauses | ( | void | ) | [inline] |
Definition at line 214 of file xchaff_dbase.h.
References _clauses, and _unused_clause_idx_queue.
Referenced by Xchaff::NumClauses(), enlarge_lit_pool(), output_lit_pool_state(), and init().
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 Xchaff::GetNumLiterals(), enlarge_lit_pool(), output_lit_pool_state(), and init().
void CDatabase::mark_clause_deleted | ( | CClause & | cl | ) | [inline] |
Definition at line 221 of file xchaff_dbase.h.
References _stats, CDatabaseStats::num_deleted_clauses, CDatabaseStats::num_deleted_literals, CClause::num_lits(), CClause::in_use(), CClause::literal(), variable(), CLitPoolElement::var_index(), CLitPoolElement::var_sign(), and CLitPoolElement::val().
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 variable(), _num_var_in_new_cl, and CVariable::set_in_new_cl().
int CDatabase::literal_value | ( | CLitPoolElement | l | ) | [inline] |
Definition at line 239 of file xchaff_dbase.h.
References variable(), CLitPoolElement::var_index(), and CLitPoolElement::var_sign().
Referenced by detail_dump_cl(), CSolver::add_clause(), CSolver::set_var_value_with_current_dl(), CSolver::set_var_value_not_current_dl(), is_conflict(), is_satisfied(), and CSolver::delete_unrelevant_clauses().
int CDatabase::find_unit_literal | ( | ClauseIdx | cl | ) |
Definition at line 497 of file xchaff_solver.cpp.
References clause(), CClause::literals(), _variables, UNKNOWN, and CLitPoolElement::s_var().
Referenced by CSolver::add_clause(), CSolver::preprocess(), CSolver::real_solve(), and CSolver::conflict_analysis_zchaff().
bool CDatabase::is_conflict | ( | ClauseIdx | cl | ) |
Definition at line 479 of file xchaff_solver.cpp.
References clause(), CClause::literals(), and literal_value().
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(), CClause::literals(), and literal_value().
Definition at line 176 of file xchaff_dbase.cpp.
References clause(), CClause::in_use(), CClause::num_lits(), literal_value(), CClause::literals(), variable(), CClause::literal(), CLitPoolElement::var_index(), and std::endl().
Referenced by dump().
void CDatabase::dump | ( | ostream & | os = cout | ) |
Reimplemented in CSolver.
Definition at line 197 of file xchaff_dbase.cpp.
References std::endl(), _clauses, detail_dump_cl(), _variables, and variable().
CDatabaseStats CDatabase::_stats [protected] |
Reimplemented in CSolver.
Definition at line 93 of file xchaff_dbase.h.
Referenced by CDatabase(), enlarge_lit_pool(), stats(), init_num_clauses(), init_num_literals(), num_added_clauses(), num_added_literals(), num_deleted_clauses(), num_deleted_literals(), num_literals(), mark_clause_deleted(), and CSolver::delete_unrelevant_clauses().
CLitPoolElement* CDatabase::_lit_pool_start [protected] |
Definition at line 96 of file xchaff_dbase.h.
Referenced by CDatabase(), enlarge_lit_pool(), ~CDatabase(), lit_pool_begin(), lit_pool_size(), and lit_pool().
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_push_back(), lit_pool_size(), and lit_pool_free_space().
CLitPoolElement* CDatabase::_lit_pool_end_storage [protected] |
Definition at line 98 of file xchaff_dbase.h.
Referenced by CDatabase(), enlarge_lit_pool(), lit_pool_push_back(), and lit_pool_free_space().
vector<CVariable> CDatabase::_variables [protected] |
Definition at line 100 of file xchaff_dbase.h.
Referenced by dump(), variables(), variable(), CSolver::set_var_value(), CSolver::find_max_clause_dlevel(), and find_unit_literal().
vector<CClause> CDatabase::_clauses [protected] |
Definition at line 101 of file xchaff_dbase.h.
Referenced by dump(), clauses(), clause(), num_clauses(), and CSolver::add_clause().
queue<ClauseIdx> CDatabase::_unused_clause_idx_queue [protected] |
Definition at line 102 of file xchaff_dbase.h.
Referenced by estimate_mem_usage(), mem_usage(), num_clauses(), 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(), enlarge_lit_pool(), and set_mem_limit().