CVC3
2.4.1
|
#include <xchaff_dbase.h>
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 |
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.
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.
|
inline |
Definition at line 109 of file xchaff_dbase.h.
References _lit_pool_start.
|
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().
|
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().
|
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().
|
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().
|
inline |
Definition at line 129 of file xchaff_dbase.h.
References _stats.
|
inline |
|
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().
|
inline |
Definition at line 137 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::init_num_literals.
Referenced by init().
|
inline |
Definition at line 138 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::num_added_clauses.
|
inline |
Definition at line 139 of file xchaff_dbase.h.
References _stats, and CDatabaseStats::num_added_literals.
|
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().
|
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().
|
inline |
Definition at line 144 of file xchaff_dbase.h.
References _lit_pool_start.
Referenced by compact_lit_pool().
|
inline |
Definition at line 147 of file xchaff_dbase.h.
References _lit_pool_finish.
Referenced by CSolver::add_clause().
|
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().
|
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().
|
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().
|
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().
|
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().
|
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().
|
inline |
Definition at line 203 of file xchaff_dbase.h.
References variables().
|
inline |
Definition at line 206 of file xchaff_dbase.h.
References variables().
|
inline |
Definition at line 210 of file xchaff_dbase.h.
References variables().
Referenced by Xchaff::GetFirstVar(), Xchaff::GetNextVar(), CSolver::init(), and Xchaff::NumVariables().
|
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().
|
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().
|
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().
|
inline |
Definition at line 231 of file xchaff_dbase.h.
References _num_var_in_new_cl, CVariable::set_in_new_cl(), and variable().
|
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().
|
protected |
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().
|
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().
|
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().
|
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().
|
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().
|
protected |
Definition at line 101 of file xchaff_dbase.h.
Referenced by CSolver::add_clause(), clause(), clauses(), dump(), and num_clauses().
|
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().
|
protected |
Definition at line 104 of file xchaff_dbase.h.
Referenced by mark_var_in_new_cl().
|
protected |
Definition at line 105 of file xchaff_dbase.h.
Referenced by CDatabase(), enlarge_lit_pool(), and set_mem_limit().