Enum RestartMode 

pub enum RestartMode {
    Adaptive,
    Glucose,
    Luby,
}

The restart heuristic. Glucose’s dynamic LBD policy restarts when recent learned-clause quality (literal-block distance) degrades relative to the global average, and blocks a restart when the trail is unusually long — a sign the search is closing in on a model. Luby is the classic universal sequence (Luby et al., 1993). Adaptive alternates the two in geometrically growing phases (the CaDiCaL/Kissat “stabilizing / non-stabilizing” idea): aggressive Glucose restarts to EXPLORE, then calm Luby restarts to let phase-saving EXPLOIT and dig toward a model — capturing the strength of each and avoiding the per-instance losses of either alone. The choice is a pure search-ORDER heuristic: it never changes a verdict.

Variants

Adaptive

Alternate Glucose (non-stabilizing) and Luby (stabilizing) phases — the default.

Glucose

Dynamic LBD restarts with blocking — the Glucose lever.

Luby

The Luby universal restart sequence.

Trait Implementations

impl Clone for RestartMode

fn clone(&self) -> RestartMode

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RestartMode

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

Formats the value using the given formatter.

impl PartialEq for RestartMode

fn eq(&self, other: &RestartMode) -> 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 RestartMode

impl Eq for RestartMode

impl StructuralPartialEq for RestartMode