Skip to main content

parse_dpr

Function parse_dpr 

Source
pub fn parse_dpr(text: &str) -> Result<Vec<ProofStep>, String>
Expand description

Parse a DRAT/DPR proof body back into ProofSteps — one clause per line. A bare C 0 line is a RUP addition; C 0 ω 0 is a PR addition with an Witness::Assignment; d C 0 is a deletion. Used to round-trip our own emission through our own checker.