Struct DynamicSubsumption 

pub struct DynamicSubsumption { /* private fields */ }

Dynamic subsumption engine.

Implementations

impl DynamicSubsumption

pub fn new() -> Self

Create a new dynamic subsumption engine.

pub fn with_config(config: SubsumptionConfig) -> Self

Create with custom configuration.

pub fn stats(&self) -> &SubsumptionStats

Get statistics.

pub fn reset_stats(&mut self)

Reset statistics.

pub fn check_learned_clause( &mut self, learned_clause: &[Lit], clause_db: &ClauseDatabase, ) -> Vec<SubsumptionResult>

Check if a new learned clause C subsumes any existing clauses (forward) or is subsumed by any existing clause (backward).

Returns a list of subsumption results to process.

pub fn on_clause_added(&mut self, clause_id: ClauseId, literals: &[Lit])

Update occurrence lists when a clause is added.

pub fn on_clause_removed(&mut self, clause_id: ClauseId, literals: &[Lit])

Update occurrence lists when a clause is removed.

pub fn periodic_check( &mut self, clause_db: &ClauseDatabase, conflicts: u64, ) -> Vec<SubsumptionResult>

Perform periodic subsumption check.

pub fn clear(&mut self)

Clear all occurrence lists (e.g., on reset).

Trait Implementations

impl Default for DynamicSubsumption

fn default() -> Self

Returns the “default value” for a type.