diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-06 19:32:42 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-06 19:32:42 +0100 |
| commit | 610952322417e3758f2b62300f618721c269b2b3 (patch) | |
| tree | 0680b2770b35cb0f688d853417391aa70c97af85 /src/CMakeLists.txt | |
| parent | 716626f2f41f51cda38834e5c9dc691b0c4fd664 (diff) | |
[DRAT] DRAT data structure (#2767)
* Copied old DRAT data-structure files.
Next step: clean up the code, and adapt them to our current usage plans.
* Polished the DRAT class.
Notably, removed the idea of lazy-parsing, this is now just a DRAT
wrapper class.
More explicit about whether methods handle binary or text.
Better constructor patterns
* Added implementation of textual DRAT output
* reordered the DratInstruction structure.
* removed the public modifier from the above struct
* removed the operator << implementation for DratInstruction
* use emplace_back
* Addressing Yoni's first review
* Extracted "write literal in DIMACS format" idea as a function
* Replaced some spurious Debug streams with `os`. (they were left over
from an earlier refactor)
* Improved some documentation
* Removed aside about std::string
* Addressed Mathias' comments
Specifically
* SCREAMING_SNAKE_CASED enum variants.
* Extracted some common logic from two branches of a conditional.
* Cleaned out some undefined behavior from bit manipulation.
* Unit tests for binary DRAT parsing
* Added text output test
* s/white/black/ derp
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 a0d191f15..502db63f4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -133,6 +133,8 @@ libcvc4_add_sources( proof/clause_id.h proof/cnf_proof.cpp proof/cnf_proof.h + proof/drat/drat_proof.cpp + proof/drat/drat_proof.h proof/lemma_proof.cpp proof/lemma_proof.h proof/lfsc_proof_printer.cpp |