pub fn mine_clauses(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Lit>>Expand description
The clause-bundle pass. Run every structure-mining contributor and union the implied clauses (no-goods) they discover. Each contributor’s soundness contract: every returned clause is implied by the formula, so the union preserves the solution set — a sound, never-worse enrichment that lets one method’s discovered structure accelerate the others (and CDCL). Contributors that find nothing are cheap, so this is safe to run before the fallback on any instance.