CVariable Class Reference

#include <xchaff_base.h>

Collaboration diagram for CVariable:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Attributes

Friends


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 _antecedence, _dlevel, _in_new_cl, _is_marked, _lits_count, _scores, _value, _var_score_pos, NULL_CLAUSE, and UNKNOWN.


Member Function Documentation

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]

Definition at line 270 of file xchaff_base.h.

References _in_new_cl.

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]

Definition at line 280 of file xchaff_base.h.

References _is_marked.

Referenced by dump().

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]

Definition at line 290 of file xchaff_base.h.

References _antecedence.

void CVariable::set_antecedence ( ClauseIdx  ante  )  [inline]

Definition at line 293 of file xchaff_base.h.

References _antecedence.

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().


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.

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]

Definition at line 238 of file xchaff_base.h.

Referenced by CVariable(), dump(), and value().

short CVariable::_dlevel [protected]

Definition at line 240 of file xchaff_base.h.

Referenced by CVariable(), dlevel(), and dump().

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

Definition at line 242 of file xchaff_base.h.

Referenced by ht_ptr().

int CVariable::_lits_count[2] [protected]

Definition at line 245 of file xchaff_base.h.

Referenced by CVariable(), and lits_count().

int CVariable::_scores[2] [protected]

Definition at line 246 of file xchaff_base.h.

Referenced by CVariable(), and score().

int CVariable::_var_score_pos [protected]

Definition at line 247 of file xchaff_base.h.

Referenced by CVariable(), and var_score_pos().


The documentation for this class was generated from the following file:
Generated on Tue Jul 3 14:35:24 2007 for CVC3 by  doxygen 1.5.1