diff options
Diffstat (limited to 'proofs/signatures/drat.plf')
| -rw-r--r-- | proofs/signatures/drat.plf | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index d0f647452..fa7ca3055 100644 --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -113,9 +113,10 @@ ((clc l c') (cnf_has_bottom rest)))))) ; Return a new cnf with one copy of this clause removed. +; If the clause is absent, returns the original cnf. (program cnf_remove_clause ((c clause) (cs cnf)) cnf (match cs - (cnfn (fail cnf)) + (cnfn cnfn) ((cnfc c' cs') (match (clause_eq c c') (tt cs') @@ -224,9 +225,11 @@ (tt tt) (ff (match (is_at cs c) (tt tt) - (ff (are_all_at + (ff (match c + (cln ff) + ((clc a b) (are_all_at ; dedent cs - (collect_pseudo_resolvents cs c))))))) + (collect_pseudo_resolvents cs c))))))))) ; Is this proof a valid DRAT proof of bottom? (program is_specified_drat_proof ((f cnf) (proof DRATProof)) bool |