Enum LearnedClauseSortingStrategy

pub enum LearnedClauseSortingStrategy {
    Activity,
    Lbd,
}

The sorting strategy which is used when considering removal from the clause database.

Variants

Activity

Sorts based on the activity, the activity is bumped when a literal is encountered during conflict analysis.

Lbd

Sorts based on the literal block distance (LBD) which is an indication of how “good” a learned clause is.

Trait Implementations

impl Clone for LearnedClauseSortingStrategy

fn clone(&self) -> LearnedClauseSortingStrategy

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LearnedClauseSortingStrategy

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for LearnedClauseSortingStrategy

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl PartialEq for LearnedClauseSortingStrategy

fn eq(&self, other: &LearnedClauseSortingStrategy) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for LearnedClauseSortingStrategy

impl Eq for LearnedClauseSortingStrategy

impl StructuralPartialEq for LearnedClauseSortingStrategy