diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-03-03 21:24:43 -0800 |
|---|---|---|
| committer | Alex Ozdemir <aozdemir@hmc.edu> | 2019-03-03 21:24:43 -0800 |
| commit | e4f3ffc1a2c8305b5e56fabc01a91e85d20aab45 (patch) | |
| tree | a3030b5cfe77988935c383969bcc2fbcdd8183c3 | |
| parent | 0887a032badd631fa5be2eac83cadfaccff893d1 (diff) | |
Another DRAT/LRAT compatibility bug
There was a problem in which if a DRAT proof failed to meet the
specifified requirements in the final addition of the empty clause.
Specifically, the empty clause would not be an AT, and then resolution
search would trigger and fail because the empty clause can't resolve
with stuff. Now we just return false, causing operational DRAT checking
to start.
| -rw-r--r-- | proofs/signatures/drat.plf | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index b7c12a7e4..c5a346f36 100644 --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -224,9 +224,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 |