diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-04 09:57:27 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-04 09:57:27 +0100 |
| commit | 491a7c8d1889dfb848de31d5581d0c784167eaec (patch) | |
| tree | cc064c98ea3f7fc4af23c2b3bffe2738dbb849d8 /test | |
| parent | b06f9b64b55780de693ce9e1a38565f1e34cc5a0 (diff) | |
[LRAT] A C++ data structure for LRAT. (#2737)
* [LRAT] A C++ data structure for LRAT.
Added a data structure for storing (abstract) LRAT proofs.
The constructor will take a drat binary proof and convert it to LRAT
using drat-trim. However, this is unimplemented in this PR.
Subsequent PRs will add:
* LFSC representation of LRAT
* Bitvector Proofs based on LRAT
* Enabled tests for those proofs
* Documenting LRAT constructors
* Apply suggestions from code review
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Responding to Andres' review
Consisting of
* Naming nits
* Closed fds
* Better implementation of disjoint union for LratInstruction
* DRAT -> LRAT conversion is no longer an LratProof constructor
* include reorder
* Update src/proof/lrat/lrat_proof.h
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
* ANonymous namespaces and name resolution?
* Remove inlines, fix i negation
Thanks Andres!
* Use `std::abs`
Credit to Andres
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Remove uneeded public
Diffstat (limited to 'test')
0 files changed, 0 insertions, 0 deletions