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.

1 files changed, 1 insertions, 19 deletions

diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h
index 49d18ac53..48f571841 100644
--- a/test/unit/proof/lrat_proof_black.h
+++ b/test/unit/proof/lrat_proof_black.h
@@ -16,13 +16,11 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include <algorithm>
-#include <cctype>
 #include <iostream>
-#include <iterator>
 
 #include "proof/lrat/lrat_proof.h"
 #include "prop/sat_solver_types.h"
+#include "utils.h"
 
 using namespace CVC4::proof::lrat;
 using namespace CVC4::prop;
@@ -36,22 +34,6 @@ class LfscProofBlack : public CxxTest::TestSuite
   void testOutputAsLfsc();
 };
 
-/**
- * Creates a new stream with whitespace removed.
- *
- * @param s the source string
- *
- * @return a string without whitespace
- */
-std::string filterWhitespace(const std::string& s)
-{
-  std::string out;
-  std::copy_if(s.cbegin(), s.cend(), std::inserter(out, out.end()), [](char c) {
-    return !std::isspace(c);
-  });
-  return out;
-}
-
 void LfscProofBlack::testOutputAsLfsc()
 {
   std::vector<std::unique_ptr<LratInstruction>> instructions;