pub fn vivify(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> (Vec<Vec<Lit>>, Vec<ProofStep>)Expand description
Vivify the whole database: replace each clause with its RUP-strengthened form, emitting an
Rup(shorter) then Delete(original) per improvement. Shorter clauses propagate and delete
better. The composed steps keep the run independently checkable.