Struct NoClauseManagement 

pub struct NoClauseManagement;

A clause management strategy that performs no operations.

This strategy does not clean the clause database, bump activities, or decay them.

Type Parameters

• L: The type of Literal.
• S: The LiteralStorage type.

Trait Implementations

impl ClauseManagement for NoClauseManagement

fn new<L: Literal, S: LiteralStorage<L>>(_clauses: &[Clause<L, S>]) -> Self

Creates a new NoClauseManagement instance. The clauses argument is ignored.

fn on_conflict<L: Literal, S: LiteralStorage<L>>( &mut self, _cnf: &mut Cnf<L, S>, )

This is a no-op for NoClauseManagement.

fn should_clean_db(&self) -> bool

Always returns false as this strategy never cleans the database.

fn clean_clause_db<L: Literal, S: LiteralStorage<L>, P: Propagator<L, S, A>, A: Assignment>( &mut self, _cnf: &mut Cnf<L, S>, _trail: &mut Trail<L, S>, _propagator: &mut P, _assignment: &mut A, )

This is a no-op for NoClauseManagement.

fn bump_involved_clause_activities<L: Literal, S: LiteralStorage<L>>( &mut self, _cnf: &mut Cnf<L, S>, _c_ref: usize, )

This is a no-op for NoClauseManagement.

fn num_removed(&self) -> usize

Always returns 0 as no clauses are ever removed.

impl Clone for NoClauseManagement

fn clone(&self) -> NoClauseManagement

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for NoClauseManagement

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

Formats the value using the given formatter.

impl Default for NoClauseManagement

fn default() -> NoClauseManagement

Returns the “default value” for a type.

impl PartialEq for NoClauseManagement

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

impl Eq for NoClauseManagement

impl StructuralPartialEq for NoClauseManagement