CVC3
|
#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) |
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.
|
inline |
Definition at line 254 of file xchaff_base.h.
References NULL_CLAUSE, and UNKNOWN.
|
inline |
Definition at line 249 of file xchaff_base.h.
Referenced by CSolver::decide_next_branch(), CSolver::restart(), and CSolver::update_var_stats().
|
inline |
|
inline |
Definition at line 251 of file xchaff_base.h.
Referenced by CSolver::update_var_stats().
|
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().
|
inline |
Definition at line 267 of file xchaff_base.h.
Referenced by CSolver::add_clause(), CSolver::preprocess(), and CSolver::set_var_value().
|
inline |
Definition at line 270 of file xchaff_base.h.
Referenced by CSolver::conflict_analysis_zchaff().
|
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().
|
inline |
Definition at line 276 of file xchaff_base.h.
Referenced by CSolver::add_clause(), CSolver::preprocess(), and CSolver::update_var_stats().
|
inline |
Definition at line 280 of file xchaff_base.h.
Referenced by CSolver::conflict_analysis_zchaff().
|
inline |
Definition at line 283 of file xchaff_base.h.
Referenced by CSolver::mark_vars_at_level().
|
inline |
Definition at line 286 of file xchaff_base.h.
Referenced by CSolver::conflict_analysis_zchaff().
|
inline |
Definition at line 290 of file xchaff_base.h.
Referenced by CSolver::dump_assignment_stack().
|
inline |
Definition at line 293 of file xchaff_base.h.
Referenced by CSolver::set_var_value().
|
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().
|
inline |
Definition at line 300 of file xchaff_base.h.
References std::endl().
|
friend |
Definition at line 313 of file xchaff_base.h.
|
protected |
Definition at line 227 of file xchaff_base.h.
|
protected |
Definition at line 229 of file xchaff_base.h.
|
protected |
Definition at line 236 of file xchaff_base.h.
|
protected |
Definition at line 238 of file xchaff_base.h.
|
protected |
Definition at line 240 of file xchaff_base.h.
|
protected |
Definition at line 242 of file xchaff_base.h.
|
protected |
Definition at line 245 of file xchaff_base.h.
|
protected |
Definition at line 246 of file xchaff_base.h.
|
protected |
Definition at line 247 of file xchaff_base.h.