CVC3  2.4.1
Public Member Functions | Protected Attributes | Friends | List of all members
CVariable Class Reference

#include <xchaff_base.h>

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
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
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
int& CVariable::lits_count ( int  i)
inline
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
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: