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/utils.h | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 test/unit/proof/utils.h (limited to 'test/unit/proof/utils.h') diff --git a/test/unit/proof/utils.h b/test/unit/proof/utils.h new file mode 100644 index 000000000..19b24f4c3 --- /dev/null +++ b/test/unit/proof/utils.h @@ -0,0 +1,34 @@ +/********************* */ +/*! \file utils.h + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utilities for proof testing + **/ + +#include +#include +#include +#include + +/** + * 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; +} -- cgit v1.2.3