CVC3
|
#include <minisat_varorder.h>
Public Member Functions | |
VarOrder (const std::vector< signed char > &ass, const std::vector< double > &act) | |
void | newVar (void) |
void | newVar (int varIndex) |
void | update (Var x) |
void | undo (Var x) |
Var | select (double random_freq=.0) |
Private Attributes | |
const std::vector< signed char > & | assigns |
const std::vector< double > & | activity |
Heap< VarOrder_lt > | heap |
double | random_seed |
Definition at line 60 of file minisat_varorder.h.
|
inline |
Definition at line 67 of file minisat_varorder.h.
|
inline |
Definition at line 79 of file minisat_varorder.h.
References assigns, heap, MiniSat::Heap< C >::insert(), and MiniSat::Heap< C >::setBounds().
Referenced by MiniSat::Solver::registerVar().
|
inline |
Definition at line 85 of file minisat_varorder.h.
References assigns, heap, MiniSat::Heap< C >::insert(), and MiniSat::Heap< C >::setBounds().
|
inline |
Definition at line 91 of file minisat_varorder.h.
References heap, MiniSat::Heap< C >::increase(), and MiniSat::Heap< C >::inHeap().
Referenced by MiniSat::Solver::varBumpActivity().
|
inline |
Definition at line 97 of file minisat_varorder.h.
References heap, MiniSat::Heap< C >::inHeap(), and MiniSat::Heap< C >::insert().
Referenced by MiniSat::Solver::backtrack(), MiniSat::Solver::pop(), and MiniSat::Solver::propLookahead().
|
inline |
Definition at line 104 of file minisat_varorder.h.
References assigns, MiniSat::Heap< C >::empty(), MiniSat::Heap< C >::getMin(), heap, MiniSat::l_Undef, MiniSat::toLbool(), and MiniSat::var_Undef.
Referenced by MiniSat::Solver::propLookahead(), and MiniSat::Solver::search().
|
private |
Definition at line 61 of file minisat_varorder.h.
|
private |
Definition at line 62 of file minisat_varorder.h.
|
private |
|
private |
Definition at line 64 of file minisat_varorder.h.