From f93a68fdf2b62a40dd74bdb04aafb60ea7f1a69a Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 28 Feb 2019 21:54:08 -0800 Subject: 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. --- test/unit/proof/lrat_proof_black.h | 20 +------------------- 1 file changed, 1 insertion(+), 19 deletions(-) (limited to 'test/unit/proof/lrat_proof_black.h') 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 -#include -#include #include -#include #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> instructions; -- cgit v1.2.3