CVC3
2.4.1
|
#include <xchaff_solver.h>
Class**********************************************************************
Synopsis [Sat Solver]
Description [This class contains the process and datastructrues to solve the Sat problem.]
SeeAlso []
CSolver::CSolver | ( | void | ) |
Definition at line 43 of file xchaff_solver.cpp.
References dlevel(), _params, CSolverParameters::time_limit, CSolverParameters::decision_strategy, CSolverParameters::preprocess_strategy, CSolverParameters::allow_clause_deletion, CSolverParameters::clause_deletion_interval, CSolverParameters::max_unrelevance, CSolverParameters::min_num_clause_lits_for_delete, CSolverParameters::max_conflict_clause_length, CSolverParameters::bubble_init_step, CSolverParameters::randomness, CSolverParameters::verbosity, CSolverParameters::back_track_complete, CSolverParameters::allow_multiple_conflict, CSolverParameters::allow_multiple_conflict_clause, CSolverParameters::allow_restart, CSolverParameters::next_restart_time, CSolverParameters::restart_time_increment, CSolverParameters::restart_time_incr_incr, CSolverParameters::next_restart_backtrack, CSolverParameters::restart_backtrack_incr, CSolverParameters::restart_backtrack_incr_incr, CSolverParameters::restart_randomness, CSolverParameters::base_randomness, _stats, CSolverStats::is_solver_started, CSolverStats::outcome, UNKNOWN, CSolverStats::is_mem_out, CSolverStats::start_cpu_time, CSolverStats::finish_cpu_time, CSolverStats::last_cpu_time, CSolverStats::start_world_time, CSolverStats::finish_world_time, CSolverStats::num_decisions, CSolverStats::num_backtracks, CSolverStats::max_dlevel, CSolverStats::num_implications, _num_marked, _dlevel, CSolverStats::total_bubble_move, _dlevel_hook, _decision_hook, _assignment_hook, and _deduction_hook.
CSolver::~CSolver | ( | ) |
Definition at line 101 of file xchaff_solver.cpp.
References _stats, CSolverStats::is_solver_started, CDatabase::variables(), and _assignment_stack.
void CSolver::real_solve | ( | void | ) | [protected] |
Definition at line 763 of file xchaff_solver.cpp.
References run_periodic_functions(), decide_next_branch(), _implication_queue, _conflicts, deduce(), CONFLICT, analyze_conflicts(), _stats, CSolverStats::outcome, UNSATISFIABLE, _addedUnitClauses, CDatabase::find_unit_literal(), queue_implication(), SATISFIABLE, time_out(), TIME_OUT, CSolverStats::is_mem_out, and MEM_OUT.
Referenced by solve(), and continueCheck().
int CSolver::preprocess | ( | bool | allowNewClauses | ) | [protected] |
Definition at line 706 of file xchaff_solver.cpp.
References CDatabase::variables(), CDatabase::variable(), CVariable::lits_count(), CVariable::value(), CVariable::dlevel(), num_free_variables(), _params, CSolverParameters::verbosity, std::endl(), UNKNOWN, queue_implication(), NULL_CLAUSE, CDatabase::clauses(), CDatabase::clause(), CClause::num_lits(), CDatabase::find_unit_literal(), deduce(), CONFLICT, and NO_CONFLICT.
Referenced by solve().
int CSolver::deduce | ( | void | ) | [protected] |
Definition at line 852 of file xchaff_solver.cpp.
References restart(), _implication_queue, _conflicts, CDatabase::variables(), CVariable::value(), UNKNOWN, _params, CSolverParameters::back_track_complete, dlevel(), find_max_clause_dlevel(), set_var_value(), _assignment_stack, CHECK, verify_integrity(), _deduction_hook, _deduction_hook_cookie, CONFLICT, and NO_CONFLICT.
Referenced by preprocess(), and real_solve().
bool CSolver::decide_next_branch | ( | void | ) | [protected] |
Definition at line 617 of file xchaff_solver.cpp.
References _stats, CSolverStats::num_decisions, _implication_queue, _max_score_pos, _var_order, CDatabase::variables(), CVariable::value(), UNKNOWN, _params, CSolverParameters::randomness, CSolverParameters::base_randomness, num_free_variables(), CVariable::score(), _decision_hook, _decision_hook_cookie, _conflicts, dlevel(), _dlevel_hook, _dlevel_hook_cookie, CSolverStats::max_dlevel, CHECK, std::endl(), queue_implication(), and NULL_CLAUSE.
Referenced by real_solve().
int CSolver::analyze_conflicts | ( | void | ) | [protected] |
Definition at line 912 of file xchaff_solver.cpp.
References conflict_analysis_zchaff().
Referenced by real_solve().
int CSolver::conflict_analysis_grasp | ( | void | ) | [protected] |
int CSolver::conflict_analysis_zchaff | ( | void | ) | [protected] |
Definition at line 916 of file xchaff_solver.cpp.
References _conflicts, _implication_queue, _num_marked, CDatabase::is_conflict(), _conflict_lits, CDatabase::variable(), CVariable::in_new_cl(), CVariable::set_in_new_cl(), max_dlevel(), find_max_clause_dlevel(), mark_vars_at_level(), _assignment_stack, CVariable::is_marked(), CVariable::clear_marked(), CDatabase::variables(), NULL_CLAUSE, add_clause(), _stats, CSolverStats::is_mem_out, CHECK, CDatabase::clause(), std::endl(), back_track(), _params, CSolverParameters::back_track_complete, CDatabase::find_unit_literal(), dlevel(), queue_implication(), and dump_assignment_stack().
Referenced by analyze_conflicts().
void CSolver::back_track | ( | int | level | ) | [protected] |
Definition at line 830 of file xchaff_solver.cpp.
References CHECK, dlevel(), std::endl(), CHECK_FULL, dump(), verify_integrity(), _assignment_stack, unset_var_value(), num_free_variables(), _dlevel_hook, _dlevel_hook_cookie, _stats, and CSolverStats::num_backtracks.
Referenced by conflict_analysis_zchaff(), and restart().
void CSolver::init | ( | void | ) | [protected] |
Reimplemented from CDatabase.
Definition at line 142 of file xchaff_solver.cpp.
References _stats, CSolverStats::is_solver_started, CSolverStats::start_cpu_time, current_cpu_time(), CSolverStats::start_world_time, current_world_time(), CSolverStats::num_free_variables, CDatabase::num_variables(), CDatabase::variables(), _assignment_stack, _var_order, _last_var_lits_count, CHECK, and dump().
Referenced by solve().
void CSolver::mark_vars_at_level | ( | ClauseIdx | cl, |
int | var_idx, | ||
int | dl | ||
) | [protected] |
Definition at line 890 of file xchaff_solver.cpp.
References CDatabase::clause(), CDatabase::variable(), dlevel(), CVariable::set_marked(), _num_marked, CVariable::set_in_new_cl(), and _conflict_lits.
Referenced by conflict_analysis_zchaff().
int CSolver::find_max_clause_dlevel | ( | ClauseIdx | cl | ) | [protected] |
Definition at line 447 of file xchaff_solver.cpp.
References NULL_CLAUSE, FLIPPED, dlevel(), CDatabase::clause(), CClause::literals(), CDatabase::_variables, and UNKNOWN.
Referenced by deduce(), and conflict_analysis_zchaff().
void CSolver::set_var_value | ( | int | var, |
int | value, | ||
ClauseIdx | ante, | ||
int | dl | ||
) | [protected] |
Definition at line 296 of file xchaff_solver.cpp.
References CHECK_FULL, dump(), CHECK, verify_integrity(), std::endl(), _stats, CSolverStats::num_implications, num_free_variables(), _assignment_hook, _assignment_hook_cookie, CDatabase::_variables, CVariable::value(), UNKNOWN, CVariable::dlevel(), CVariable::set_antecedence(), CVariable::ht_ptr(), dlevel(), set_var_value_with_current_dl(), and set_var_value_not_current_dl().
Referenced by deduce().
void CSolver::set_var_value_not_current_dl | ( | int | v, |
vector< CLitPoolElement * > & | neg_ht_clauses | ||
) | [protected] |
Definition at line 368 of file xchaff_solver.cpp.
References CLitPoolElement::direction(), CLitPoolElement::val(), CDatabase::variable(), CLitPoolElement::var_index(), dlevel(), CVariable::ht_ptr(), CLitPoolElement::unset_ht(), CDatabase::literal_value(), _conflicts, queue_implication(), and CLitPoolElement::s_var().
Referenced by set_var_value().
void CSolver::set_var_value_with_current_dl | ( | int | v, |
vector< CLitPoolElement * > & | neg_ht_clauses | ||
) | [protected] |
Definition at line 321 of file xchaff_solver.cpp.
References CLitPoolElement::direction(), CLitPoolElement::val(), CDatabase::literal_value(), _conflicts, queue_implication(), CLitPoolElement::s_var(), CLitPoolElement::var_index(), CDatabase::variable(), CVariable::ht_ptr(), and CLitPoolElement::unset_ht().
Referenced by set_var_value().
void CSolver::unset_var_value | ( | int | var | ) | [protected] |
Definition at line 433 of file xchaff_solver.cpp.
References CHECK, CDatabase::variable(), std::endl(), _max_score_pos, UNKNOWN, NULL_CLAUSE, _assignment_hook, and _assignment_hook_cookie.
Referenced by back_track().
void CSolver::run_periodic_functions | ( | void | ) | [protected] |
Definition at line 109 of file xchaff_solver.cpp.
References _params, CSolverParameters::allow_clause_deletion, _stats, CSolverStats::num_backtracks, CSolverParameters::clause_deletion_interval, delete_unrelevant_clauses(), CSolverParameters::allow_restart, CSolverParameters::next_restart_backtrack, CSolverParameters::restart_backtrack_incr, CSolverParameters::restart_backtrack_incr_incr, current_cpu_time(), CSolverParameters::next_restart_time, CSolverParameters::verbosity, std::endl(), CSolverParameters::restart_time_increment, CSolverParameters::restart_time_incr_incr, CSolverParameters::randomness, CSolverParameters::restart_randomness, restart(), CSolverStats::num_decisions, update_var_stats(), and _hooks.
Referenced by real_solve().
void CSolver::update_var_stats | ( | void | ) | [protected] |
Definition at line 601 of file xchaff_solver.cpp.
References CDatabase::variables(), CDatabase::variable(), CVariable::score(), CVariable::lits_count(), _last_var_lits_count, _var_order, compare_var_stat(), CVariable::var_score_pos(), and _max_score_pos.
Referenced by run_periodic_functions(), and restart().
bool CSolver::time_out | ( | void | ) | [protected] |
Definition at line 587 of file xchaff_solver.cpp.
References current_cpu_time(), _stats, CSolverStats::start_cpu_time, _params, and CSolverParameters::time_limit.
Referenced by real_solve().
void CSolver::delete_unrelevant_clauses | ( | void | ) | [protected] |
Definition at line 513 of file xchaff_solver.cpp.
References CHECK_FULL, dump(), CDatabase::num_deleted_clauses(), CDatabase::_stats, _stats, _params, CSolverParameters::max_unrelevance, CSolverParameters::min_num_clause_lits_for_delete, CSolverParameters::max_conflict_clause_length, CHECK, std::endl(), CDatabase::clauses(), CDatabase::init_num_clauses(), CClause::in_use(), CClause::num_lits(), CDatabase::literal_value(), CClause::literal(), CDatabase::mark_clause_deleted(), CDatabase::_unused_clause_idx_queue, CDatabase::variables(), and CDatabase::num_deleted_literals().
Referenced by run_periodic_functions().
void CSolver::set_time_limit | ( | float | t | ) | [inline] |
Definition at line 228 of file xchaff_solver.h.
References _params, and CSolverParameters::time_limit.
Referenced by Xchaff::SetBudget().
void CSolver::set_mem_limit | ( | int | s | ) | [inline] |
Reimplemented from CDatabase.
Definition at line 230 of file xchaff_solver.h.
Referenced by Xchaff::SetMemLimit().
void CSolver::set_decision_strategy | ( | int | s | ) | [inline] |
Definition at line 233 of file xchaff_solver.h.
References _params, and CSolverParameters::decision_strategy.
void CSolver::set_preprocess_strategy | ( | int | s | ) | [inline] |
Definition at line 235 of file xchaff_solver.h.
References _params, and CSolverParameters::preprocess_strategy.
void CSolver::enable_cls_deletion | ( | bool | allow | ) | [inline] |
Definition at line 237 of file xchaff_solver.h.
References _params, and CSolverParameters::allow_clause_deletion.
Referenced by Xchaff::EnableClauseDeletion(), and Xchaff::DisableClauseDeletion().
void CSolver::set_cls_del_interval | ( | int | n | ) | [inline] |
Definition at line 239 of file xchaff_solver.h.
References _params, and CSolverParameters::clause_deletion_interval.
void CSolver::set_max_unrelevance | ( | int | n | ) | [inline] |
Definition at line 241 of file xchaff_solver.h.
References _params, and CSolverParameters::max_unrelevance.
void CSolver::set_min_num_clause_lits_for_delete | ( | int | n | ) | [inline] |
Definition at line 243 of file xchaff_solver.h.
References _params, and CSolverParameters::min_num_clause_lits_for_delete.
void CSolver::set_max_conflict_clause_length | ( | int | l | ) | [inline] |
Definition at line 245 of file xchaff_solver.h.
References _params, and CSolverParameters::max_conflict_clause_length.
void CSolver::set_allow_multiple_conflict | ( | bool | b = false | ) | [inline] |
Definition at line 247 of file xchaff_solver.h.
References _params, and CSolverParameters::allow_multiple_conflict.
void CSolver::set_allow_multiple_conflict_clause | ( | bool | b = false | ) | [inline] |
Definition at line 250 of file xchaff_solver.h.
References _params, and CSolverParameters::allow_multiple_conflict_clause.
void CSolver::set_randomness | ( | int | n | ) | [inline] |
Definition at line 253 of file xchaff_solver.h.
References _params, and CSolverParameters::base_randomness.
Referenced by Xchaff::SetRandomness().
void CSolver::set_random_seed | ( | int | seed | ) | [inline] |
Definition at line 256 of file xchaff_solver.h.
References current_world_time().
Referenced by Xchaff::SetRandSeed().
void CSolver::RegisterDLevelHook | ( | void(*)(void *, int) | f, |
void * | cookie | ||
) | [inline] |
Definition at line 264 of file xchaff_solver.h.
References _dlevel_hook, and _dlevel_hook_cookie.
Referenced by Xchaff::RegisterDLevelHook().
void CSolver::RegisterDecisionHook | ( | int(*)(void *, bool *) | f, |
void * | cookie | ||
) | [inline] |
Definition at line 266 of file xchaff_solver.h.
References _decision_hook, and _decision_hook_cookie.
Referenced by Xchaff::RegisterDecisionHook().
void CSolver::RegisterAssignmentHook | ( | void(*)(void *, int, int) | f, |
void * | cookie | ||
) | [inline] |
Definition at line 268 of file xchaff_solver.h.
References _assignment_hook, and _assignment_hook_cookie.
Referenced by Xchaff::RegisterAssignmentHook().
void CSolver::RegisterDeductionHook | ( | void(*)(void *) | f, |
void * | cookie | ||
) | [inline] |
Definition at line 270 of file xchaff_solver.h.
References _deduction_hook, and _deduction_hook_cookie.
Referenced by Xchaff::RegisterDeductionHook().
int CSolver::outcome | ( | ) | [inline] |
Definition at line 274 of file xchaff_solver.h.
References _stats, and CSolverStats::outcome.
int CSolver::num_decisions | ( | ) | [inline] |
Definition at line 275 of file xchaff_solver.h.
References _stats, and CSolverStats::num_decisions.
Referenced by Xchaff::GetNumDecisions().
int& CSolver::num_free_variables | ( | ) | [inline] |
Definition at line 276 of file xchaff_solver.h.
References _stats, and CSolverStats::num_free_variables.
Referenced by set_var_value(), decide_next_branch(), preprocess(), and back_track().
int CSolver::max_dlevel | ( | ) | [inline] |
Definition at line 279 of file xchaff_solver.h.
References _stats, and CSolverStats::max_dlevel.
Referenced by Xchaff::GetMaxDLevel(), and conflict_analysis_zchaff().
int CSolver::num_implications | ( | ) | [inline] |
Definition at line 280 of file xchaff_solver.h.
References _stats, and CSolverStats::num_implications.
Referenced by Xchaff::GetNumImplications().
long CSolver::total_bubble_move | ( | void | ) | [inline] |
Definition at line 281 of file xchaff_solver.h.
References _stats, and CSolverStats::total_bubble_move.
const char* CSolver::version | ( | void | ) | [inline] |
Definition at line 283 of file xchaff_solver.h.
int CSolver::current_cpu_time | ( | void | ) | [inline] |
Definition at line 287 of file xchaff_solver.h.
Referenced by run_periodic_functions(), init(), time_out(), solve(), continueCheck(), elapsed_cpu_time(), and total_run_time().
int CSolver::current_world_time | ( | void | ) | [inline] |
Definition at line 296 of file xchaff_solver.h.
Referenced by init(), solve(), continueCheck(), and set_random_seed().
float CSolver::elapsed_cpu_time | ( | ) | [inline] |
Definition at line 303 of file xchaff_solver.h.
References current_cpu_time(), _stats, and CSolverStats::last_cpu_time.
float CSolver::total_run_time | ( | ) | [inline] |
Definition at line 310 of file xchaff_solver.h.
References _stats, CSolverStats::is_solver_started, current_cpu_time(), and CSolverStats::start_cpu_time.
Referenced by Xchaff::GetBudgetUsed(), and Xchaff::GetTotalTime().
float CSolver::cpu_run_time | ( | ) | [inline] |
Definition at line 316 of file xchaff_solver.h.
References _stats, CSolverStats::finish_cpu_time, and CSolverStats::start_cpu_time.
float CSolver::world_run_time | ( | ) | [inline] |
Definition at line 321 of file xchaff_solver.h.
References _stats, CSolverStats::finish_world_time, and CSolverStats::start_world_time.
int CSolver::estimate_mem_usage | ( | void | ) | [inline] |
Reimplemented from CDatabase.
Definition at line 326 of file xchaff_solver.h.
Referenced by Xchaff::GetMemUsed().
int CSolver::mem_usage | ( | void | ) | [inline] |
Reimplemented from CDatabase.
Definition at line 329 of file xchaff_solver.h.
References _stats, CSolverStats::max_dlevel, and _assignment_stack.
int& CSolver::dlevel | ( | void | ) | [inline] |
Definition at line 337 of file xchaff_solver.h.
References _dlevel.
Referenced by CSolver(), add_clause(), set_var_value(), set_var_value_not_current_dl(), find_max_clause_dlevel(), dump_assignment_stack(), decide_next_branch(), back_track(), deduce(), mark_vars_at_level(), conflict_analysis_zchaff(), and restart().
void CSolver::add_hook | ( | HookFunPtrT | fun, |
int | interval | ||
) | [inline] |
Definition at line 340 of file xchaff_solver.h.
References _hooks.
void CSolver::queue_implication | ( | int | lit, |
ClauseIdx | ante_clause | ||
) | [inline] |
Definition at line 345 of file xchaff_solver.h.
References CHECK, std::endl(), and _implication_queue.
Referenced by add_clause(), set_var_value_with_current_dl(), set_var_value_not_current_dl(), decide_next_branch(), preprocess(), real_solve(), and conflict_analysis_zchaff().
int CSolver::add_variables | ( | int | new_vars | ) |
Definition at line 160 of file xchaff_solver.cpp.
References CDatabase::variables(), _stats, CSolverStats::is_solver_started, CSolverStats::num_free_variables, _assignment_stack, _var_order, and _last_var_lits_count.
Referenced by Xchaff::AddVariables().
Definition at line 179 of file xchaff_solver.cpp.
References CDatabase::lit_pool_free_space(), CDatabase::enlarge_lit_pool(), CDatabase::_unused_clause_idx_queue, CDatabase::_clauses, CDatabase::clause(), CClause::init(), CDatabase::lit_pool_end(), CDatabase::is_conflict(), CDatabase::variables(), CDatabase::lit_pool_push_back(), CDatabase::variable(), CVariable::lits_count(), CDatabase::literal_value(), _stats, CSolverStats::is_solver_started, CClause::num_lits(), CClause::literals(), CLitPoolElement::var_index(), UNKNOWN, CLitPoolElement::var_sign(), CVariable::ht_ptr(), CLitPoolElement::set_ht(), dlevel(), CVariable::dlevel(), _addedUnitClauses, CDatabase::find_unit_literal(), queue_implication(), and _conflicts.
Referenced by Xchaff::AddClause(), and conflict_analysis_zchaff().
void CSolver::verify_integrity | ( | void | ) |
Definition at line 886 of file xchaff_solver.cpp.
Referenced by set_var_value(), back_track(), and deduce().
void CSolver::restart | ( | void | ) | [inline] |
Definition at line 358 of file xchaff_solver.h.
References _params, CSolverParameters::verbosity, std::endl(), dlevel(), CDatabase::variables(), CDatabase::variable(), CVariable::score(), _last_var_lits_count, update_var_stats(), and back_track().
Referenced by run_periodic_functions(), and deduce().
int CSolver::solve | ( | bool | allowNewClauses | ) |
Definition at line 804 of file xchaff_solver.cpp.
References init(), preprocess(), CONFLICT, _stats, CSolverStats::outcome, UNSATISFIABLE, _dlevel_hook, _dlevel_hook_cookie, real_solve(), CSolverStats::finish_cpu_time, current_cpu_time(), CSolverStats::finish_world_time, and current_world_time().
Referenced by Xchaff::Satisfiable().
int CSolver::continueCheck | ( | ) |
Definition at line 822 of file xchaff_solver.cpp.
References real_solve(), _stats, CSolverStats::finish_cpu_time, current_cpu_time(), CSolverStats::finish_world_time, current_world_time(), and CSolverStats::outcome.
Referenced by Xchaff::Continue().
void CSolver::dump_assignment_stack | ( | ostream & | os = cout | ) |
Definition at line 463 of file xchaff_solver.cpp.
References dlevel(), _assignment_stack, CDatabase::variable(), CVariable::get_antecedence(), FLIPPED, and std::endl().
Referenced by conflict_analysis_zchaff(), and dump().
void CSolver::output_current_stats | ( | void | ) |
void CSolver::dump | ( | ostream & | os = cout | ) | [inline] |
Reimplemented from CDatabase.
Definition at line 381 of file xchaff_solver.h.
References dump_assignment_stack().
Referenced by init(), set_var_value(), delete_unrelevant_clauses(), and back_track().
int CSolver::_dlevel [protected] |
Definition at line 151 of file xchaff_solver.h.
vector<vector<int> *> CSolver::_assignment_stack [protected] |
Definition at line 152 of file xchaff_solver.h.
Referenced by ~CSolver(), init(), add_variables(), dump_assignment_stack(), back_track(), deduce(), conflict_analysis_zchaff(), and mem_usage().
queue<pair<int,ClauseIdx> > CSolver::_implication_queue [protected] |
Definition at line 153 of file xchaff_solver.h.
Referenced by decide_next_branch(), real_solve(), deduce(), conflict_analysis_zchaff(), and queue_implication().
CSolverParameters CSolver::_params [protected] |
Definition at line 154 of file xchaff_solver.h.
Referenced by CSolver(), run_periodic_functions(), delete_unrelevant_clauses(), time_out(), decide_next_branch(), preprocess(), deduce(), conflict_analysis_zchaff(), set_time_limit(), set_decision_strategy(), set_preprocess_strategy(), enable_cls_deletion(), set_cls_del_interval(), set_max_unrelevance(), set_min_num_clause_lits_for_delete(), set_max_conflict_clause_length(), set_allow_multiple_conflict(), set_allow_multiple_conflict_clause(), set_randomness(), and restart().
CSolverStats CSolver::_stats [protected] |
Reimplemented from CDatabase.
Definition at line 155 of file xchaff_solver.h.
Referenced by CSolver(), ~CSolver(), run_periodic_functions(), init(), add_variables(), add_clause(), set_var_value(), delete_unrelevant_clauses(), time_out(), decide_next_branch(), real_solve(), solve(), continueCheck(), back_track(), conflict_analysis_zchaff(), outcome(), num_decisions(), num_free_variables(), max_dlevel(), num_implications(), total_bubble_move(), elapsed_cpu_time(), total_run_time(), cpu_run_time(), world_run_time(), and mem_usage().
vector<pair<int,pair< HookFunPtrT, int> > > CSolver::_hooks [protected] |
Definition at line 157 of file xchaff_solver.h.
Referenced by run_periodic_functions(), and add_hook().
int CSolver::_max_score_pos [protected] |
Definition at line 160 of file xchaff_solver.h.
Referenced by unset_var_value(), update_var_stats(), and decide_next_branch().
vector<int> CSolver::_last_var_lits_count[2] [protected] |
Definition at line 161 of file xchaff_solver.h.
Referenced by init(), add_variables(), update_var_stats(), and restart().
vector<pair<int,int> > CSolver::_var_order [protected] |
Definition at line 162 of file xchaff_solver.h.
Referenced by init(), add_variables(), update_var_stats(), and decide_next_branch().
int CSolver::_num_marked [protected] |
Definition at line 165 of file xchaff_solver.h.
Referenced by CSolver(), mark_vars_at_level(), and conflict_analysis_zchaff().
vector<ClauseIdx> CSolver::_conflicts [protected] |
Definition at line 166 of file xchaff_solver.h.
Referenced by add_clause(), set_var_value_with_current_dl(), set_var_value_not_current_dl(), decide_next_branch(), real_solve(), deduce(), and conflict_analysis_zchaff().
vector<long> CSolver::_conflict_lits [protected] |
Definition at line 167 of file xchaff_solver.h.
Referenced by mark_vars_at_level(), and conflict_analysis_zchaff().
void(* CSolver::_dlevel_hook)(void *, int) [protected] |
Definition at line 170 of file xchaff_solver.h.
Referenced by CSolver(), decide_next_branch(), solve(), back_track(), and RegisterDLevelHook().
int(* CSolver::_decision_hook)(void *, bool *) [protected] |
Definition at line 171 of file xchaff_solver.h.
Referenced by CSolver(), decide_next_branch(), and RegisterDecisionHook().
void(* CSolver::_assignment_hook)(void *, int, int) [protected] |
Definition at line 172 of file xchaff_solver.h.
Referenced by CSolver(), set_var_value(), unset_var_value(), and RegisterAssignmentHook().
void(* CSolver::_deduction_hook)(void *) [protected] |
Definition at line 173 of file xchaff_solver.h.
Referenced by CSolver(), deduce(), and RegisterDeductionHook().
void* CSolver::_dlevel_hook_cookie [protected] |
Definition at line 174 of file xchaff_solver.h.
Referenced by decide_next_branch(), solve(), back_track(), and RegisterDLevelHook().
void* CSolver::_decision_hook_cookie [protected] |
Definition at line 175 of file xchaff_solver.h.
Referenced by decide_next_branch(), and RegisterDecisionHook().
void* CSolver::_assignment_hook_cookie [protected] |
Definition at line 176 of file xchaff_solver.h.
Referenced by set_var_value(), unset_var_value(), and RegisterAssignmentHook().
void* CSolver::_deduction_hook_cookie [protected] |
Definition at line 177 of file xchaff_solver.h.
Referenced by deduce(), and RegisterDeductionHook().
vector<ClauseIdx> CSolver::_addedUnitClauses [protected] |
Definition at line 180 of file xchaff_solver.h.
Referenced by add_clause(), and real_solve().