CVariable Class Reference

#include <xchaff_base.h>

Collaboration diagram for CVariable:

List of all members.

Public Member Functions

• int & score (int i)
• int score (void)
• int & var_score_pos (void)
• CVariable (void)
• short & value (void)
• short & dlevel (void)
• int in_new_cl (void)
• void set_in_new_cl (int phase)
• int & lits_count (int i)
• bool is_marked (void)
• void set_marked (void)
• void clear_marked (void)
• ClauseIdx get_antecedence (void)
• void set_antecedence (ClauseIdx ante)
• vector< CLitPoolElement * > & ht_ptr (int i)
• void dump (ostream &os=cout)

Protected Attributes

• bool _is_marked: 1
• int _in_new_cl: 2
• ClauseIdx _antecedence: 29
• short _value
• short _dlevel
• vector< CLitPoolElement * > _ht_ptrs [2]
• int _lits_count [2]
• int _scores [2]
• int _var_score_pos

Friends

• ostream & operator<< (ostream &os, CVariable &v)

---

Detailed Description

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

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.

---

Constructor & Destructor Documentation

CVariable::CVariable

(

void

)

[inline]

Definition at line 254 of file xchaff_base.h.

References NULL_CLAUSE, and UNKNOWN.

---

Member Function Documentation

int& CVariable::score

(

int

i

)

[inline]

Definition at line 249 of file xchaff_base.h.

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.

References score().

Referenced by score().

int& CVariable::var_score_pos

(

void

)

[inline]

Definition at line 251 of file xchaff_base.h.

Referenced by CSolver::update_var_stats().

short& CVariable::value

(

void

)

[inline]

Definition at line 264 of file xchaff_base.h.

Referenced by CSolver::decide_next_branch(), CSolver::deduce(), Xchaff::GetVarAssignment(), CSolver::preprocess(), and CSolver::set_var_value().

short& CVariable::dlevel

(

void

)

[inline]

Definition at line 267 of file xchaff_base.h.

Referenced by CSolver::add_clause(), CSolver::preprocess(), and CSolver::set_var_value().

int CVariable::in_new_cl

(

void

)

[inline]

Definition at line 270 of file xchaff_base.h.

Referenced by CSolver::conflict_analysis_zchaff().

void CVariable::set_in_new_cl

(

int

phase

)

[inline]

Definition at line 273 of file xchaff_base.h.

Referenced by CSolver::conflict_analysis_zchaff(), 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.

Referenced by CSolver::add_clause(), CSolver::preprocess(), and CSolver::update_var_stats().

bool CVariable::is_marked

(

void

)

[inline]

Definition at line 280 of file xchaff_base.h.

Referenced by CSolver::conflict_analysis_zchaff().

void CVariable::set_marked

(

void

)

[inline]

Definition at line 283 of file xchaff_base.h.

Referenced by CSolver::mark_vars_at_level().

void CVariable::clear_marked

(

void

)

[inline]

Definition at line 286 of file xchaff_base.h.

Referenced by CSolver::conflict_analysis_zchaff().

ClauseIdx CVariable::get_antecedence

(

void

)

[inline]

Definition at line 290 of file xchaff_base.h.

Referenced by CSolver::dump_assignment_stack().

void CVariable::set_antecedence

(

ClauseIdx

ante

)

[inline]

Definition at line 293 of file xchaff_base.h.

Referenced by CSolver::set_var_value().

vector<CLitPoolElement *>& CVariable::ht_ptr

(

int

i

)

[inline]

Definition at line 297 of file xchaff_base.h.

Referenced by CSolver::add_clause(), CDatabase::compact_lit_pool(), CDatabase::enlarge_lit_pool(), CDatabase::mem_usage(), CSolver::set_var_value(), 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 std::endl().

---

Friends And Related Function Documentation

ostream& operator<<	(	ostream &	os,
		CVariable &	v
	)		[friend]

Definition at line 313 of file xchaff_base.h.

---

Member Data Documentation

bool CVariable::_is_marked [protected]

Definition at line 227 of file xchaff_base.h.

int CVariable::_in_new_cl [protected]

Definition at line 229 of file xchaff_base.h.

ClauseIdx CVariable::_antecedence [protected]

Definition at line 236 of file xchaff_base.h.

short CVariable::_value [protected]

Definition at line 238 of file xchaff_base.h.

short CVariable::_dlevel [protected]

Definition at line 240 of file xchaff_base.h.

vector<CLitPoolElement *> CVariable::_ht_ptrs[2] [protected]

Definition at line 242 of file xchaff_base.h.

int CVariable::_lits_count[2] [protected]

Definition at line 245 of file xchaff_base.h.

int CVariable::_scores[2] [protected]

Definition at line 246 of file xchaff_base.h.

int CVariable::_var_score_pos [protected]

Definition at line 247 of file xchaff_base.h.

---

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

• xchaff_base.h