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 /test/unit/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 'test/unit/CMakeLists.txt')
| -rw-r--r-- | test/unit/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 4ba7205a5..4659f2647 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -89,5 +89,6 @@ add_subdirectory(expr) add_subdirectory(main) add_subdirectory(parser) add_subdirectory(prop) +add_subdirectory(proof) add_subdirectory(theory) add_subdirectory(util) |