pub fn emit_drat(
num_vars: usize,
original: &[Vec<Lit>],
steps: &[ProofStep],
) -> Result<String, EmitError>Expand description
Emit a DRAT proof (additions + deletions, no hints, no witnesses). Returns
EmitError::PrInRupOnlyFormat if any step is a Pr step — DRAT cannot carry a PR witness;
use emit_dpr for those. The trailing empty clause is appended iff it is RUP.