CSolver Class Reference

#include <xchaff_solver.h>

Inheritance diagram for CSolver:

[legend]Collaboration diagram for CSolver:

[legend]List of all members.

Public Member Functions

• CSolver ()
• ~CSolver ()
• void set_time_limit (float t)
• void set_mem_limit (int s)
• void set_decision_strategy (int s)
• void set_preprocess_strategy (int s)
• void enable_cls_deletion (bool allow)
• void set_cls_del_interval (int n)
• void set_max_unrelevance (int n)
• void set_min_num_clause_lits_for_delete (int n)
• void set_max_conflict_clause_length (int l)
• void set_allow_multiple_conflict (bool b=false)
• void set_allow_multiple_conflict_clause (bool b=false)
• void set_randomness (int n)
• void set_random_seed (int seed)
• void RegisterDLevelHook (void(*f)(void *, int), void *cookie)
• void RegisterDecisionHook (int(*f)(void *, bool *), void *cookie)
• void RegisterAssignmentHook (void(*f)(void *, int, int), void *cookie)
• void RegisterDeductionHook (void(*f)(void *), void *cookie)
• int outcome ()
• int num_decisions ()
• int & num_free_variables ()
• int max_dlevel ()
• int num_implications ()
• long long total_bubble_move (void)
• char * version (void)
• int current_cpu_time (void)
• int current_world_time (void)
• float elapsed_cpu_time ()
• float total_run_time ()
• float cpu_run_time ()
• float world_run_time ()
• int estimate_mem_usage ()
• int mem_usage (void)
• int & dlevel ()
• void add_hook (HookFunPtrT fun, int interval)
• void queue_implication (int lit, ClauseIdx ante_clause)
• int add_variables (int new_vars)
• ClauseIdx add_clause (vector< int > &lits, bool addConflicts=true)
• void verify_integrity (void)
• void restart (void)
• int solve (bool allowNewClauses)
• int continueCheck ()
• void dump_assignment_stack (ostream &os=cout)
• void output_current_stats (void)
• void dump (ostream &os=cout)

Protected Member Functions

• void real_solve (void)
• int preprocess (bool allowNewClauses)
• int deduce (void)
• bool decide_next_branch (void)
• int analyze_conflicts (void)
• int conflict_analysis_grasp (void)
• int conflict_analysis_zchaff (void)
• void back_track (int level)
• void init (void)
• void mark_vars_at_level (ClauseIdx cl, int var_idx, int dl)
• int find_max_clause_dlevel (ClauseIdx cl)
• void set_var_value (int var, int value, ClauseIdx ante, int dl)
• void set_var_value_not_current_dl (int v, vector< CLitPoolElement * > &neg_ht_clauses)
• void set_var_value_with_current_dl (int v, vector< CLitPoolElement * > &neg_ht_clauses)
• void unset_var_value (int var)
• void run_periodic_functions (void)
• void update_var_stats (void)
• bool time_out (void)
• void delete_unrelevant_clauses (void)

Protected Attributes

• int _dlevel
• vector< vector< int > * > _assignment_stack
• queue< pair< int, ClauseIdx > > _implication_queue
• CSolverParameters _params
• CSolverStats _stats
• vector< pair< int, pair< HookFunPtrT,
  int > > > _hooks
• int _max_score_pos
• vector< int > _last_var_lits_count [2]
• vector< pair< int, int > > _var_order
• int _num_marked
• vector< ClauseIdx > _conflicts
• vector< int > _conflict_lits
• void(* _dlevel_hook )(void *, int)
• int(* _decision_hook )(void *, bool *)
• void(* _assignment_hook )(void *, int, int)
• void(* _deduction_hook )(void *)
• void * _dlevel_hook_cookie
• void * _decision_hook_cookie
• void * _assignment_hook_cookie
• void * _deduction_hook_cookie
• vector< ClauseIdx > _addedUnitClauses

---

Detailed Description

Class**********************************************************************

Synopsis [Sat Solver]

Description [This class contains the process and datastructrues to solve the Sat problem.]

SeeAlso []

Definition at line 147 of file xchaff_solver.h.

---

Constructor & Destructor Documentation

CSolver::CSolver (   )

Definition at line 43 of file xchaff_solver.cpp. References _assignment_hook, _decision_hook, _deduction_hook, _dlevel, _dlevel_hook, _num_marked, _params, _stats, CSolverParameters::allow_clause_deletion, CSolverParameters::allow_multiple_conflict, CSolverParameters::allow_multiple_conflict_clause, CSolverParameters::allow_restart, CSolverParameters::back_track_complete, CSolverParameters::base_randomness, CSolverParameters::bubble_init_step, CSolverParameters::clause_deletion_interval, CSolverParameters::decision_strategy, dlevel(), CSolverStats::finish_cpu_time, CSolverStats::finish_world_time, CSolverStats::is_mem_out, CSolverStats::is_solver_started, CSolverStats::last_cpu_time, CSolverParameters::max_conflict_clause_length, CSolverStats::max_dlevel, CSolverParameters::max_unrelevance, CSolverParameters::min_num_clause_lits_for_delete, CSolverParameters::next_restart_backtrack, CSolverParameters::next_restart_time, CSolverStats::num_backtracks, CSolverStats::num_decisions, CSolverStats::num_implications, CSolverStats::outcome, CSolverParameters::preprocess_strategy, CSolverParameters::randomness, CSolverParameters::restart_backtrack_incr, CSolverParameters::restart_backtrack_incr_incr, CSolverParameters::restart_randomness, CSolverParameters::restart_time_incr_incr, CSolverParameters::restart_time_increment, CSolverStats::start_cpu_time, CSolverStats::start_world_time, CSolverParameters::time_limit, CSolverStats::total_bubble_move, UNKNOWN, and CSolverParameters::verbosity.

CSolver::~CSolver (   )

Definition at line 101 of file xchaff_solver.cpp. References _assignment_stack, _stats, CSolverStats::is_solver_started, and CDatabase::variables().

---

Member Function Documentation

void CSolver::real_solve (  void   )  [protected]

Definition at line 738 of file xchaff_solver.cpp. References _addedUnitClauses, _conflicts, _implication_queue, _stats, analyze_conflicts(), CONFLICT, decide_next_branch(), deduce(), CDatabase::find_unit_literal(), CSolverStats::is_mem_out, MEM_OUT, CSolverStats::outcome, queue_implication(), run_periodic_functions(), SATISFIABLE, TIME_OUT, time_out(), and UNSATISFIABLE. Referenced by continueCheck(), and solve().

int CSolver::preprocess (  bool  allowNewClauses  )  [protected]

Definition at line 681 of file xchaff_solver.cpp. References _params, CDatabase::clause(), CDatabase::clauses(), CONFLICT, deduce(), CVariable::dlevel(), std::endl(), CDatabase::find_unit_literal(), CVariable::lits_count(), NO_CONFLICT, num_free_variables(), queue_implication(), UNKNOWN, CVariable::value(), CDatabase::variable(), CDatabase::variables(), and CSolverParameters::verbosity. Referenced by solve().

int CSolver::deduce (  void   )  [protected]

Definition at line 827 of file xchaff_solver.cpp. References _assignment_stack, _conflicts, _deduction_hook, _deduction_hook_cookie, _implication_queue, _params, CSolverParameters::back_track_complete, CONFLICT, dlevel(), find_max_clause_dlevel(), NO_CONFLICT, restart(), set_var_value(), UNKNOWN, CVariable::value(), CDatabase::variables(), and verify_integrity(). Referenced by preprocess(), and real_solve().

bool CSolver::decide_next_branch (  void   )  [protected]

Definition at line 615 of file xchaff_solver.cpp. References _decision_hook, _decision_hook_cookie, _dlevel_hook, _dlevel_hook_cookie, _implication_queue, _max_score_pos, _params, _stats, _var_order, CSolverParameters::base_randomness, dlevel(), std::endl(), CSolverStats::max_dlevel, CSolverStats::num_decisions, num_free_variables(), queue_implication(), CSolverParameters::randomness, CVariable::score(), UNKNOWN, CVariable::value(), and CDatabase::variables(). Referenced by real_solve().

int CSolver::analyze_conflicts (  void   )  [protected]

Definition at line 887 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 891 of file xchaff_solver.cpp. References _assignment_stack, _conflict_lits, _conflicts, _implication_queue, _num_marked, _params, _stats, add_clause(), back_track(), CSolverParameters::back_track_complete, CDatabase::clause(), CVariable::clear_marked(), dlevel(), dump_assignment_stack(), std::endl(), find_max_clause_dlevel(), CDatabase::find_unit_literal(), CVariable::in_new_cl(), CDatabase::is_conflict(), CSolverStats::is_mem_out, mark_vars_at_level(), max_dlevel(), queue_implication(), CVariable::set_in_new_cl(), CDatabase::variable(), and CDatabase::variables(). Referenced by analyze_conflicts().

void CSolver::back_track (  int  level  )  [protected]

Definition at line 805 of file xchaff_solver.cpp. References _assignment_stack, _dlevel_hook, _dlevel_hook_cookie, _stats, dlevel(), dump(), std::endl(), CSolverStats::num_backtracks, num_free_variables(), unset_var_value(), and verify_integrity(). 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 _assignment_stack, _last_var_lits_count, _stats, _var_order, current_cpu_time(), current_world_time(), dump(), CDatabase::init(), CSolverStats::is_solver_started, CSolverStats::num_free_variables, CDatabase::num_variables(), CSolverStats::start_cpu_time, CSolverStats::start_world_time, and CDatabase::variables(). Referenced by solve().

void CSolver::mark_vars_at_level (  ClauseIdx  cl, int  var_idx, int  dl )  [protected]

Definition at line 865 of file xchaff_solver.cpp. References _conflict_lits, _num_marked, CDatabase::clause(), dlevel(), CVariable::set_in_new_cl(), CVariable::set_marked(), and CDatabase::variable(). Referenced by conflict_analysis_zchaff().

int CSolver::find_max_clause_dlevel (  ClauseIdx  cl  )  [protected]

Definition at line 445 of file xchaff_solver.cpp. References CDatabase::_variables, CDatabase::clause(), dlevel(), CClause::literals(), and UNKNOWN. Referenced by conflict_analysis_zchaff(), and deduce().

void CSolver::set_var_value (  int  var, int  value, ClauseIdx  ante, int  dl )  [protected]

Definition at line 294 of file xchaff_solver.cpp. References _assignment_hook, _assignment_hook_cookie, _stats, CDatabase::_variables, dlevel(), CVariable::dlevel(), dump(), std::endl(), CVariable::ht_ptr(), num_free_variables(), CSolverStats::num_implications, CVariable::set_antecedence(), set_var_value_not_current_dl(), set_var_value_with_current_dl(), UNKNOWN, CVariable::value(), and verify_integrity(). Referenced by deduce().

void CSolver::set_var_value_not_current_dl (  int  v, vector< CLitPoolElement * > &  neg_ht_clauses )  [protected]

Definition at line 366 of file xchaff_solver.cpp. References _conflicts, CLitPoolElement::direction(), CVariable::dlevel(), CVariable::ht_ptr(), CLitPoolElement::is_ht(), CDatabase::literal_value(), queue_implication(), CLitPoolElement::s_var(), CLitPoolElement::unset_ht(), CLitPoolElement::val(), CLitPoolElement::var_index(), CLitPoolElement::var_sign(), and CDatabase::variable(). Referenced by set_var_value().

void CSolver::set_var_value_with_current_dl (  int  v, vector< CLitPoolElement * > &  neg_ht_clauses )  [protected]

Definition at line 319 of file xchaff_solver.cpp. References _conflicts, CLitPoolElement::direction(), CVariable::ht_ptr(), CLitPoolElement::is_ht(), CDatabase::literal_value(), queue_implication(), CLitPoolElement::s_var(), CLitPoolElement::unset_ht(), CLitPoolElement::val(), CLitPoolElement::var_index(), CLitPoolElement::var_sign(), and CDatabase::variable(). Referenced by set_var_value().

void CSolver::unset_var_value (  int  var  )  [protected]

Definition at line 431 of file xchaff_solver.cpp. References _assignment_hook, _assignment_hook_cookie, _max_score_pos, CVariable::dlevel(), std::endl(), CVariable::set_antecedence(), UNKNOWN, CVariable::value(), CVariable::var_score_pos(), and CDatabase::variable(). Referenced by back_track().

void CSolver::run_periodic_functions (  void   )  [protected]

Definition at line 109 of file xchaff_solver.cpp. References _hooks, _params, _stats, CSolverParameters::allow_clause_deletion, CSolverParameters::allow_restart, CSolverParameters::clause_deletion_interval, current_cpu_time(), delete_unrelevant_clauses(), std::endl(), CSolverParameters::next_restart_backtrack, CSolverParameters::next_restart_time, CSolverStats::num_backtracks, CSolverStats::num_decisions, CSolverParameters::randomness, restart(), CSolverParameters::restart_backtrack_incr, CSolverParameters::restart_backtrack_incr_incr, CSolverParameters::restart_randomness, CSolverParameters::restart_time_incr_incr, CSolverParameters::restart_time_increment, update_var_stats(), and CSolverParameters::verbosity. Referenced by real_solve().

void CSolver::update_var_stats (  void   )  [protected]

Definition at line 599 of file xchaff_solver.cpp. References _last_var_lits_count, _max_score_pos, _var_order, compare_var_stat(), CVariable::lits_count(), CVariable::score(), CVariable::var_score_pos(), CDatabase::variable(), and CDatabase::variables(). Referenced by restart(), and run_periodic_functions().

bool CSolver::time_out (  void   )  [protected]

Definition at line 585 of file xchaff_solver.cpp. References _params, _stats, current_cpu_time(), CSolverStats::start_cpu_time, and CSolverParameters::time_limit. Referenced by real_solve().

void CSolver::delete_unrelevant_clauses (  void   )  [protected]

Definition at line 511 of file xchaff_solver.cpp. References _params, CDatabase::_stats, CDatabase::_unused_clause_idx_queue, CDatabase::clauses(), dump(), std::endl(), CClause::in_use(), CDatabase::init_num_clauses(), CClause::literal(), CDatabase::literal_value(), CDatabase::mark_clause_deleted(), CSolverParameters::max_conflict_clause_length, CSolverParameters::max_unrelevance, CDatabaseStats::mem_used_up, CSolverParameters::min_num_clause_lits_for_delete, CDatabase::num_deleted_clauses(), CDatabase::num_deleted_literals(), CClause::num_lits(), and CDatabase::variables(). Referenced by run_periodic_functions().

void CSolver::set_time_limit (  float  t  )  [inline]

Definition at line 227 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 229 of file xchaff_solver.h. References CDatabase::set_mem_limit(). Referenced by Xchaff::SetMemLimit().

void CSolver::set_decision_strategy (  int  s  )  [inline]

Definition at line 232 of file xchaff_solver.h. References _params, and CSolverParameters::decision_strategy.

void CSolver::set_preprocess_strategy (  int  s  )  [inline]

Definition at line 234 of file xchaff_solver.h. References _params, and CSolverParameters::preprocess_strategy.

void CSolver::enable_cls_deletion (  bool  allow  )  [inline]

Definition at line 236 of file xchaff_solver.h. References _params, and CSolverParameters::allow_clause_deletion. Referenced by Xchaff::DisableClauseDeletion(), and Xchaff::EnableClauseDeletion().

void CSolver::set_cls_del_interval (  int  n  )  [inline]

Definition at line 238 of file xchaff_solver.h. References _params, and CSolverParameters::clause_deletion_interval.

void CSolver::set_max_unrelevance (  int  n  )  [inline]

Definition at line 240 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 242 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 244 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 246 of file xchaff_solver.h. References _params, CSolverParameters::allow_multiple_conflict, and b.

void CSolver::set_allow_multiple_conflict_clause (  bool  b = false  )  [inline]

Definition at line 249 of file xchaff_solver.h. References _params, CSolverParameters::allow_multiple_conflict_clause, and b.

void CSolver::set_randomness (  int  n  )  [inline]

Definition at line 252 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 255 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 263 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 265 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 267 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 269 of file xchaff_solver.h. References _deduction_hook, and _deduction_hook_cookie. Referenced by Xchaff::RegisterDeductionHook().

int CSolver::outcome (   )  [inline]

Definition at line 273 of file xchaff_solver.h. References _stats, and CSolverStats::outcome.

int CSolver::num_decisions (   )  [inline]

Definition at line 274 of file xchaff_solver.h. References _stats, and CSolverStats::num_decisions. Referenced by Xchaff::GetNumDecisions().

int& CSolver::num_free_variables (   )  [inline]

Definition at line 275 of file xchaff_solver.h. References _stats, and CSolverStats::num_free_variables. Referenced by back_track(), decide_next_branch(), preprocess(), and set_var_value().

int CSolver::max_dlevel (   )  [inline]

Definition at line 278 of file xchaff_solver.h. References _stats, and CSolverStats::max_dlevel. Referenced by conflict_analysis_zchaff(), and Xchaff::GetMaxDLevel().

int CSolver::num_implications (   )  [inline]

Definition at line 279 of file xchaff_solver.h. References _stats, and CSolverStats::num_implications. Referenced by Xchaff::GetNumImplications().

long long CSolver::total_bubble_move (  void   )  [inline]

Definition at line 280 of file xchaff_solver.h. References _stats, and CSolverStats::total_bubble_move.

char* CSolver::version (  void   )  [inline]

Definition at line 282 of file xchaff_solver.h.

int CSolver::current_cpu_time (  void   )  [inline]

Definition at line 286 of file xchaff_solver.h. Referenced by continueCheck(), elapsed_cpu_time(), init(), run_periodic_functions(), solve(), time_out(), and total_run_time().

int CSolver::current_world_time (  void   )  [inline]

Definition at line 295 of file xchaff_solver.h. Referenced by continueCheck(), init(), set_random_seed(), and solve().

float CSolver::elapsed_cpu_time (   )  [inline]

Definition at line 302 of file xchaff_solver.h. References _stats, current_cpu_time(), and CSolverStats::last_cpu_time.

float CSolver::total_run_time (   )  [inline]

Definition at line 309 of file xchaff_solver.h. References _stats, current_cpu_time(), CSolverStats::is_solver_started, and CSolverStats::start_cpu_time. Referenced by Xchaff::GetBudgetUsed(), and Xchaff::GetTotalTime().

float CSolver::cpu_run_time (   )  [inline]

Definition at line 315 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 320 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 325 of file xchaff_solver.h. References CDatabase::estimate_mem_usage(). Referenced by Xchaff::GetMemUsed().

int CSolver::mem_usage (  void   )  [inline]

Reimplemented from CDatabase. Definition at line 328 of file xchaff_solver.h. References _assignment_stack, _stats, CSolverStats::max_dlevel, and CDatabase::mem_usage().

int& CSolver::dlevel (  void   )  [inline]

Definition at line 336 of file xchaff_solver.h. References _dlevel. Referenced by add_clause(), back_track(), conflict_analysis_zchaff(), CSolver(), decide_next_branch(), deduce(), dump_assignment_stack(), find_max_clause_dlevel(), mark_vars_at_level(), restart(), and set_var_value().

void CSolver::add_hook (  HookFunPtrT  fun, int  interval )  [inline]

Definition at line 339 of file xchaff_solver.h. References _hooks.

void CSolver::queue_implication (  int  lit, ClauseIdx  ante_clause )  [inline]

Definition at line 344 of file xchaff_solver.h. References _implication_queue, and std::endl(). Referenced by add_clause(), conflict_analysis_zchaff(), decide_next_branch(), preprocess(), real_solve(), set_var_value_not_current_dl(), and set_var_value_with_current_dl().

int CSolver::add_variables (  int  new_vars  )

Definition at line 160 of file xchaff_solver.cpp. References _assignment_stack, _last_var_lits_count, _stats, _var_order, CSolverStats::is_solver_started, CSolverStats::num_free_variables, and CDatabase::variables(). Referenced by Xchaff::AddVariables().

ClauseIdx CSolver::add_clause (  vector< int > &  lits, bool  addConflicts = true )

Definition at line 179 of file xchaff_solver.cpp. References _addedUnitClauses, CDatabase::_clauses, _conflicts, CDatabase::_stats, _stats, CDatabase::_unused_clause_idx_queue, CDatabase::clause(), CVariable::dlevel(), dlevel(), CDatabase::enlarge_lit_pool(), CDatabase::find_unit_literal(), CVariable::ht_ptr(), CClause::init(), CDatabase::is_conflict(), CSolverStats::is_solver_started, CDatabase::lit_pool_end(), CDatabase::lit_pool_free_space(), CDatabase::lit_pool_push_back(), CDatabase::literal_value(), CClause::literals(), CVariable::lits_count(), CDatabaseStats::num_added_clauses, CDatabaseStats::num_added_literals, CClause::num_lits(), queue_implication(), CLitPoolElement::set_ht(), UNKNOWN, CLitPoolElement::var_index(), CLitPoolElement::var_sign(), CDatabase::variable(), and CDatabase::variables(). Referenced by Xchaff::AddClause(), and conflict_analysis_zchaff().

void CSolver::verify_integrity (  void   )

Definition at line 861 of file xchaff_solver.cpp. Referenced by back_track(), deduce(), and set_var_value().

void CSolver::restart (  void   )  [inline]

Definition at line 357 of file xchaff_solver.h. References _last_var_lits_count, _params, back_track(), dlevel(), std::endl(), CVariable::score(), update_var_stats(), CDatabase::variable(), CDatabase::variables(), and CSolverParameters::verbosity. Referenced by deduce(), and run_periodic_functions().

int CSolver::solve (  bool  allowNewClauses  )

Definition at line 779 of file xchaff_solver.cpp. References _dlevel_hook, _dlevel_hook_cookie, _stats, CONFLICT, current_cpu_time(), current_world_time(), CSolverStats::finish_cpu_time, CSolverStats::finish_world_time, init(), CSolverStats::outcome, preprocess(), real_solve(), and UNSATISFIABLE. Referenced by Xchaff::Satisfiable().

int CSolver::continueCheck (   )

Definition at line 797 of file xchaff_solver.cpp. References _stats, current_cpu_time(), current_world_time(), CSolverStats::finish_cpu_time, CSolverStats::finish_world_time, CSolverStats::outcome, and real_solve(). Referenced by Xchaff::Continue().

void CSolver::dump_assignment_stack (  ostream &  os = cout  )

Definition at line 461 of file xchaff_solver.cpp. References _assignment_stack, dlevel(), std::endl(), and CDatabase::variable(). 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 380 of file xchaff_solver.h. References CDatabase::dump(), and dump_assignment_stack(). Referenced by back_track(), delete_unrelevant_clauses(), init(), and set_var_value().

---

Member Data Documentation

int CSolver::_dlevel [protected]

Definition at line 150 of file xchaff_solver.h. Referenced by CSolver(), and dlevel().

vector<vector<int> *> CSolver::_assignment_stack [protected]

Definition at line 151 of file xchaff_solver.h. Referenced by add_variables(), back_track(), conflict_analysis_zchaff(), deduce(), dump_assignment_stack(), init(), mem_usage(), and ~CSolver().

queue<pair<int,ClauseIdx> > CSolver::_implication_queue [protected]

Definition at line 152 of file xchaff_solver.h. Referenced by conflict_analysis_zchaff(), decide_next_branch(), deduce(), queue_implication(), and real_solve().

CSolverParameters CSolver::_params [protected]

Definition at line 153 of file xchaff_solver.h. Referenced by conflict_analysis_zchaff(), CSolver(), decide_next_branch(), deduce(), delete_unrelevant_clauses(), enable_cls_deletion(), preprocess(), restart(), run_periodic_functions(), set_allow_multiple_conflict(), set_allow_multiple_conflict_clause(), set_cls_del_interval(), set_decision_strategy(), set_max_conflict_clause_length(), set_max_unrelevance(), set_min_num_clause_lits_for_delete(), set_preprocess_strategy(), set_randomness(), set_time_limit(), and time_out().

CSolverStats CSolver::_stats [protected]

Reimplemented from CDatabase. Definition at line 154 of file xchaff_solver.h. Referenced by add_clause(), add_variables(), back_track(), conflict_analysis_zchaff(), continueCheck(), cpu_run_time(), CSolver(), decide_next_branch(), elapsed_cpu_time(), init(), max_dlevel(), mem_usage(), num_decisions(), num_free_variables(), num_implications(), outcome(), real_solve(), run_periodic_functions(), set_var_value(), solve(), time_out(), total_bubble_move(), total_run_time(), world_run_time(), and ~CSolver().

vector<pair<int,pair< HookFunPtrT, int> > > CSolver::_hooks [protected]

Definition at line 156 of file xchaff_solver.h. Referenced by add_hook(), and run_periodic_functions().

int CSolver::_max_score_pos [protected]

Definition at line 159 of file xchaff_solver.h. Referenced by decide_next_branch(), unset_var_value(), and update_var_stats().

vector<int> CSolver::_last_var_lits_count[2] [protected]

Definition at line 160 of file xchaff_solver.h. Referenced by add_variables(), init(), restart(), and update_var_stats().

vector<pair<int,int> > CSolver::_var_order [protected]

Definition at line 161 of file xchaff_solver.h. Referenced by add_variables(), decide_next_branch(), init(), and update_var_stats().

int CSolver::_num_marked [protected]

Definition at line 164 of file xchaff_solver.h. Referenced by conflict_analysis_zchaff(), CSolver(), and mark_vars_at_level().

vector<ClauseIdx> CSolver::_conflicts [protected]

Definition at line 165 of file xchaff_solver.h. Referenced by add_clause(), conflict_analysis_zchaff(), deduce(), real_solve(), set_var_value_not_current_dl(), and set_var_value_with_current_dl().

vector<int> CSolver::_conflict_lits [protected]

Definition at line 166 of file xchaff_solver.h. Referenced by conflict_analysis_zchaff(), and mark_vars_at_level().

void(* CSolver::_dlevel_hook)(void *, int) [protected]

Referenced by back_track(), CSolver(), decide_next_branch(), RegisterDLevelHook(), and solve().

int(* CSolver::_decision_hook)(void *, bool *) [protected]

Referenced by CSolver(), decide_next_branch(), and RegisterDecisionHook().

void(* CSolver::_assignment_hook)(void *, int, int) [protected]

Referenced by CSolver(), RegisterAssignmentHook(), set_var_value(), and unset_var_value().

void(* CSolver::_deduction_hook)(void *) [protected]

Referenced by CSolver(), deduce(), and RegisterDeductionHook().

void* CSolver::_dlevel_hook_cookie [protected]

Definition at line 173 of file xchaff_solver.h. Referenced by back_track(), decide_next_branch(), RegisterDLevelHook(), and solve().

void* CSolver::_decision_hook_cookie [protected]

Definition at line 174 of file xchaff_solver.h. Referenced by decide_next_branch(), and RegisterDecisionHook().

void* CSolver::_assignment_hook_cookie [protected]

Definition at line 175 of file xchaff_solver.h. Referenced by RegisterAssignmentHook(), set_var_value(), and unset_var_value().

void* CSolver::_deduction_hook_cookie [protected]

Definition at line 176 of file xchaff_solver.h. Referenced by deduce(), and RegisterDeductionHook().

vector<ClauseIdx> CSolver::_addedUnitClauses [protected]

Definition at line 179 of file xchaff_solver.h. Referenced by add_clause(), and real_solve().

---

The documentation for this class was generated from the following files:

• xchaff_solver.h
• xchaff_solver.cpp

---