Struct SubsumptionChecker 

pub struct SubsumptionChecker { /* private fields */ }

Subsumption checker for learned clauses

Implementations

impl SubsumptionChecker

pub fn new(max_check_size: usize) -> Self

Create a new subsumption checker

pub fn stats(&self) -> &SubsumptionStats

Get statistics

pub fn check_forward_subsumption( &mut self, new_clause: &[Lit], clauses: &ClauseDatabase, ) -> Vec<ClauseId>

Check if a newly learned clause subsumes any existing clauses

Returns a list of clause IDs that are subsumed by the new clause

pub fn check_backward_subsumption( &mut self, new_clause: &[Lit], clauses: &ClauseDatabase, ) -> bool

Check if a newly learned clause is subsumed by any existing clause

Returns true if the new clause is subsumed (redundant)

pub fn check_subsumption( &mut self, new_clause: &[Lit], clauses: &ClauseDatabase, ) -> (bool, Vec<ClauseId>)

Perform full subsumption check for a new clause

Returns (is_subsumed, subsumed_clauses)

• is_subsumed: true if the new clause is redundant
• subsumed_clauses: list of clause IDs that the new clause makes redundant

pub fn reset_stats(&mut self)

Reset statistics