diff options
Diffstat (limited to 'proofs/signatures')
| -rw-r--r-- | proofs/signatures/drat.plf | 9 | ||||
| -rw-r--r-- | proofs/signatures/lrat.plf | 4 |
2 files changed, 8 insertions, 5 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 diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf index ea1d90537..d16791624 100644 --- a/proofs/signatures/lrat.plf +++ b/proofs/signatures/lrat.plf @@ -361,14 +361,14 @@ ; unit, it modifies the global assignment to satisfy the clause, and returns ; the literal that was made SAT by the new mark. ; -; Fails if `c` is a TAUT +; If `c` is a tautology, reports `MRSat`, since it is (trivially) satisfied. (program clause_check_unit_and_maybe_mark ((c clause)) MarkResult (match (clause_is_sat c) (tt MRSat) (ff (match (clause_is_unsat c) (tt MRUnsat) (ff (match (is_t c) - (tt (fail MarkResult)) + (tt MRSat) (ff ; Dedent (match (clause_has_floating c) (tt (let first (clause_first_floating c) |