Struct UnitSearch

pub struct UnitSearch<L: Literal, S: LiteralStorage<L>, A: Assignment>(/* private fields */);

A simple unit propagation strategy that iterates through all clauses.

Trait Implementations

impl<L: Clone + Literal, S: Clone + LiteralStorage<L>, A: Clone + Assignment> Clone for UnitSearch<L, S, A>

fn clone(&self) -> UnitSearch<L, S, A>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<L: Debug + Literal, S: Debug + LiteralStorage<L>, A: Debug + Assignment> Debug for UnitSearch<L, S, A>

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

Formats the value using the given formatter.

impl<L: Default + Literal, S: Default + LiteralStorage<L>, A: Default + Assignment> Default for UnitSearch<L, S, A>

fn default() -> UnitSearch<L, S, A>

Returns the “default value” for a type.

impl<L: PartialEq + Literal, S: PartialEq + LiteralStorage<L>, A: PartialEq + Assignment> PartialEq for UnitSearch<L, S, A>

fn eq(&self, other: &UnitSearch<L, S, A>) -> 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<L: Literal, S: LiteralStorage<L>, A: Assignment> Propagator<L, S, A> for UnitSearch<L, S, A>

fn new(_: &Cnf<L, S>) -> Self

Creates a new propagator instance

fn add_clause(&mut self, _: &Clause<L, S>, _: usize)

Informs the propagator about a new clause being added to the formula. This is particularly relevant for watched literal schemes to set up watches.

fn propagate( &mut self, trail: &mut Trail<L, S>, assignment: &mut A, cnf: &mut Cnf<L, S>, ) -> Option<usize>

Performs propagation based on the current assignments in the trail.

fn num_propagations(&self) -> usize

Returns the total number of propagations performed by this instance.

fn cleanup_learnt(&mut self, _: usize)

Cleans up internal propagator state related to learnt clauses.

fn add_propagation(lit: L, clause_idx: usize, trail: &mut Trail<L, S>)

Helper function to add a propagated literal to the trail.

impl<L: Eq + Literal, S: Eq + LiteralStorage<L>, A: Eq + Assignment> Eq for UnitSearch<L, S, A>

impl<L: Literal, S: LiteralStorage<L>, A: Assignment> StructuralPartialEq for UnitSearch<L, S, A>