projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c652449) | patch
LFSC LRAT Output (#2787)
authorAlex Ozdemir <aozdemir@hmc.edu>
Sun, 13 Jan 2019 21:21:24 +0000 (13:21 -0800)
committerGitHub <noreply@github.com>
Sun, 13 Jan 2019 21:21:24 +0000 (13:21 -0800)
commit300560dda47178cae18f5f4ad2edb381eabddb30
tree17105907162c56850f0122e0b56a8ab7574b06f6tree
parentc652449ac9f4a54fc8f37796f0bff3960434cf40commit | diff
LFSC LRAT Output (#2787)

* LFSC ouput & unit test

* Renamed lrat unit test file

* s/DRAT/LRAT/

Thanks Andres!

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments

1. Extracted a filter whitespace function.
2. Added @param annotations.

* Addressing Yoni's comments

Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.
src/proof/lrat/lrat_proof.cpp diff | blob | history
src/proof/lrat/lrat_proof.h diff | blob | history
test/unit/proof/CMakeLists.txt diff | blob | history
test/unit/proof/lrat_proof_black.h [new file with mode: 0644] blob