ErProof class with LFSC output (#2812)
authorAlex Ozdemir <aozdemir@hmc.edu>
Fri, 1 Mar 2019 05:54:08 +0000 (21:54 -0800)
committerGitHub <noreply@github.com>
Fri, 1 Mar 2019 05:54:08 +0000 (21:54 -0800)
commitf93a68fdf2b62a40dd74bdb04aafb60ea7f1a69a
tree387c98a460004e7e50c8424429a680a265a26408
parent933cd31e994148cd457cb110734aa23423777fec
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.
src/CMakeLists.txt
src/proof/er/er_proof.cpp [new file with mode: 0644]
src/proof/er/er_proof.h [new file with mode: 0644]
test/unit/proof/CMakeLists.txt
test/unit/proof/er_proof_black.h [new file with mode: 0644]
test/unit/proof/lrat_proof_black.h
test/unit/proof/utils.h [new file with mode: 0644]