pub fn emit_dpr(
num_vars: usize,
original: &[Vec<Lit>],
steps: &[ProofStep],
) -> Result<String, EmitError>Expand description
Emit a DPR proof: RUP additions as bare clauses, PR additions as C 0 ω 0 (witness ω
re-verified and laid out pivot-first per the dpr-trim convention), deletions as d C 0. A
Pr step whose witness is irreducibly SR yields EmitError::RequiresSubstitutionRedundancy.