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 /src/CMakeLists.txt | |
| 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 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 889260045..a0d191f15 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -137,6 +137,8 @@ libcvc4_add_sources( proof/lemma_proof.h proof/lfsc_proof_printer.cpp proof/lfsc_proof_printer.h + proof/lrat/lrat_proof.cpp + proof/lrat/lrat_proof.h proof/proof.h proof/proof_manager.cpp proof/proof_manager.h |