CVC3
|
#include <xchaff_base.h>
Public Member Functions | |
CLitPoolElement (void) | |
CLitPoolElement (int val) | |
int & | val (void) |
int | s_var (void) |
int | var_index (void) |
bool | var_sign (void) |
void | set (int s_var) |
void | set (int v, int s) |
int | direction (void) |
bool | is_ht (void) |
void | unset_ht (void) |
void | set_ht (int dir) |
bool | is_literal (void) |
void | set_clause_index (int cl_idx) |
int | get_clause_index (void) |
int | find_clause_idx (void) |
void | dump (ostream &os=cout) |
Protected Attributes | |
int | _val |
Friends | |
ostream & | operator<< (ostream &os, CLitPoolElement &l) |
Class**********************************************************************
Synopsis [Definition of a literal]
Description [A literal is a variable with phase. Two thing determing a lteral: it's "sign", and the variable index. One bit is used to mark it's sign. 0->positive, 1->negative.
For every clause with literal count larger than 1, there are two special literals which are designated ht_literal (stands for head/tail literal to imitate SATO) It is specially marked with 2 bits: 00->not ht; dir = 1; or dir = -1; 10 is not valid. Each literal is represented by a 32 bit integer, with one bit representing it's phase and 2 bits indicate h/t property.
All the literals are collected in a storage space called literal pool. An element in a literal pool can be a literal or special spacing element to indicate the termination of a clause. The spacing element has negative value of the clause index.]
Definition at line 81 of file xchaff_base.h.
|
inline |
Definition at line 87 of file xchaff_base.h.
|
inline |
Definition at line 90 of file xchaff_base.h.
|
inline |
Definition at line 92 of file xchaff_base.h.
Referenced by CDatabase::compact_lit_pool(), CDatabase::lit_pool_push_back(), CDatabase::mark_clause_deleted(), CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
|
inline |
Definition at line 95 of file xchaff_base.h.
Referenced by CDatabase::find_unit_literal(), Xchaff::GetClauseLits(), CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
|
inline |
Definition at line 98 of file xchaff_base.h.
Referenced by CSolver::add_clause(), CDatabase::compact_lit_pool(), CDatabase::detail_dump_cl(), CDatabase::literal_value(), CDatabase::mark_clause_deleted(), CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
|
inline |
Definition at line 101 of file xchaff_base.h.
Referenced by CSolver::add_clause(), CDatabase::compact_lit_pool(), CDatabase::literal_value(), and CDatabase::mark_clause_deleted().
|
inline |
Definition at line 104 of file xchaff_base.h.
|
inline |
Definition at line 107 of file xchaff_base.h.
|
inline |
Definition at line 111 of file xchaff_base.h.
Referenced by CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
|
inline |
Definition at line 114 of file xchaff_base.h.
Referenced by CDatabase::compact_lit_pool().
|
inline |
Definition at line 117 of file xchaff_base.h.
Referenced by CSolver::set_var_value_not_current_dl(), and CSolver::set_var_value_with_current_dl().
|
inline |
Definition at line 120 of file xchaff_base.h.
Referenced by CSolver::add_clause().
|
inline |
Definition at line 125 of file xchaff_base.h.
Referenced by find_clause_idx().
|
inline |
Definition at line 128 of file xchaff_base.h.
|
inline |
Definition at line 131 of file xchaff_base.h.
Referenced by find_clause_idx().
|
inline |
Definition at line 135 of file xchaff_base.h.
References get_clause_index(), and is_literal().
|
inline |
Definition at line 141 of file xchaff_base.h.
|
friend |
Definition at line 145 of file xchaff_base.h.
|
protected |
Definition at line 84 of file xchaff_base.h.