diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-02-28 21:54:08 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-02-28 21:54:08 -0800 |
| commit | f93a68fdf2b62a40dd74bdb04aafb60ea7f1a69a (patch) | |
| tree | 387c98a460004e7e50c8424429a680a265a26408 /src/CMakeLists.txt | |
| parent | 933cd31e994148cd457cb110734aa23423777fec (diff) | |
ErProof class with LFSC output (#2812)
* ErProof class with LFSC output
* Created a TraceCheckProof class
* parsable from text
* Created an ErProof class
* constructible from a TraceCheckProof
* writable as LFSC
* A bunch of unit tests
* Reponded to Mathias's first set of comments.
Credits to Mathias for many of the fixes!
* Responed to Andres's first set, fixed tests
I accidentally deleted a "!" last time, causing stuff to fail.
* Use Configuration::isAssertionBuild
* Clarified comment
* Responded to Andres's 2nd review
* Gaurding against a memory error.
* Renaming a file.
* Aggressively unlinking temporary files.
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 0124bf4f9..e142ff46c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -139,6 +139,8 @@ libcvc4_add_sources( proof/dimacs_printer.h proof/drat/drat_proof.cpp proof/drat/drat_proof.h + proof/er/er_proof.cpp + proof/er/er_proof.h proof/lemma_proof.cpp proof/lemma_proof.h proof/lfsc_proof_printer.cpp |