#include <xchaff_base.h>
Collaboration diagram for CVariable:
Synopsis [Definition of a variable]
Description [CVariable contains the necessary information for a variable. _ht_ptrs are the head/tail literals of this variable (int two phases)]
SeeAlso [CDatabase]
Definition at line 224 of file xchaff_base.h.
CVariable::CVariable | ( | void | ) | [inline] |
Definition at line 254 of file xchaff_base.h.
References _antecedence, _dlevel, _in_new_cl, _is_marked, _lits_count, _scores, _value, _var_score_pos, NULL_CLAUSE, and UNKNOWN.
int& CVariable::score | ( | int | i | ) | [inline] |
Definition at line 249 of file xchaff_base.h.
References _scores.
Referenced by CSolver::decide_next_branch(), CSolver::restart(), and CSolver::update_var_stats().
int CVariable::score | ( | void | ) | [inline] |
Definition at line 250 of file xchaff_base.h.
int& CVariable::var_score_pos | ( | void | ) | [inline] |
Definition at line 251 of file xchaff_base.h.
References _var_score_pos.
Referenced by CSolver::update_var_stats().
short& CVariable::value | ( | void | ) | [inline] |
Definition at line 264 of file xchaff_base.h.
References _value.
Referenced by CSolver::decide_next_branch(), CSolver::deduce(), Xchaff::GetVarAssignment(), and CSolver::preprocess().
short& CVariable::dlevel | ( | void | ) | [inline] |
Definition at line 267 of file xchaff_base.h.
References _dlevel.
Referenced by CSolver::add_clause().
int CVariable::in_new_cl | ( | void | ) | [inline] |
void CVariable::set_in_new_cl | ( | int | phase | ) | [inline] |
Definition at line 273 of file xchaff_base.h.
References _in_new_cl.
Referenced by CDatabase::mark_var_in_new_cl(), and CSolver::mark_vars_at_level().
int& CVariable::lits_count | ( | int | i | ) | [inline] |
Definition at line 276 of file xchaff_base.h.
References _lits_count.
Referenced by CSolver::add_clause().
bool CVariable::is_marked | ( | void | ) | [inline] |
void CVariable::set_marked | ( | void | ) | [inline] |
Definition at line 283 of file xchaff_base.h.
References _is_marked.
Referenced by CSolver::mark_vars_at_level().
void CVariable::clear_marked | ( | void | ) | [inline] |
Definition at line 286 of file xchaff_base.h.
References _is_marked.
Referenced by CSolver::conflict_analysis_zchaff().
ClauseIdx CVariable::get_antecedence | ( | void | ) | [inline] |
void CVariable::set_antecedence | ( | ClauseIdx | ante | ) | [inline] |
vector<CLitPoolElement *>& CVariable::ht_ptr | ( | int | i | ) | [inline] |
Definition at line 297 of file xchaff_base.h.
References _ht_ptrs.
Referenced by CSolver::add_clause(), CDatabase::compact_lit_pool(), dump(), CDatabase::enlarge_lit_pool(), CDatabase::mem_usage(), CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
void CVariable::dump | ( | ostream & | os = cout |
) | [inline] |
Definition at line 300 of file xchaff_base.h.
References _antecedence, _dlevel, _value, std::endl(), ht_ptr(), and is_marked().
ostream& operator<< | ( | ostream & | os, | |
CVariable & | v | |||
) | [friend] |
Definition at line 313 of file xchaff_base.h.
bool CVariable::_is_marked [protected] |
Definition at line 227 of file xchaff_base.h.
Referenced by clear_marked(), CVariable(), is_marked(), and set_marked().
int CVariable::_in_new_cl [protected] |
Definition at line 229 of file xchaff_base.h.
Referenced by CVariable(), in_new_cl(), and set_in_new_cl().
ClauseIdx CVariable::_antecedence [protected] |
Definition at line 236 of file xchaff_base.h.
Referenced by CVariable(), dump(), get_antecedence(), and set_antecedence().
short CVariable::_value [protected] |
short CVariable::_dlevel [protected] |
vector<CLitPoolElement *> CVariable::_ht_ptrs[2] [protected] |
int CVariable::_lits_count[2] [protected] |
int CVariable::_scores[2] [protected] |
int CVariable::_var_score_pos [protected] |