diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-13 13:21:24 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-13 13:21:24 -0800 |
| commit | 300560dda47178cae18f5f4ad2edb381eabddb30 (patch) | |
| tree | 17105907162c56850f0122e0b56a8ab7574b06f6 /src/proof/clausal_bitvector_proof.cpp | |
| parent | c652449ac9f4a54fc8f37796f0bff3960434cf40 (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.
Diffstat (limited to 'src/proof/clausal_bitvector_proof.cpp')
0 files changed, 0 insertions, 0 deletions