pub fn assert_not(p: &Pred, cnf: &mut Cnf)Expand description
Assert ¬p into cnf — the refutation obligation for a miter, clausified STRAIGHT FROM THE
GATE DAG. Emits exactly the clauses Cnf::assert(&Not(pred_to_proof(p))) emits, in the same
order, over the same variables; it just never builds the tree to read them off.