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.

7 files changed, 1035 insertions, 19 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
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
new file mode 100644
index 000000000..452b64b11
--- /dev/null
+++ b/src/proof/er/er_proof.cpp
@@ -0,0 +1,383 @@
+/*********************                                                        */
+/*! \file er_proof.cpp
+ ** \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 ER Proof Format
+ **
+ ** Declares C++ types that represent an ER/TRACECHECK proof.
+ ** Defines serialization for these types.
+ **
+ ** You can find details about the way ER is encoded in the TRACECHECK
+ ** format at these locations:
+ **    https://github.com/benjaminkiesl/drat2er
+ **    http://www.cs.utexas.edu/users/marijn/publications/ijcar18.pdf
+ **/
+
+#include "proof/er/er_proof.h"
+
+#include <unistd.h>
+#include <algorithm>
+#include <fstream>
+#include <iostream>
+#include <iterator>
+#include <unordered_set>
+
+#include "base/cvc4_assert.h"
+#include "base/map_util.h"
+#include "proof/dimacs_printer.h"
+#include "proof/lfsc_proof_printer.h"
+#include "proof/proof_manager.h"
+
+#if CVC4_USE_DRAT2ER
+#include "drat2er.h"
+#include "drat2er_options.h"
+#endif
+
+namespace CVC4 {
+namespace proof {
+namespace er {
+
+TraceCheckProof TraceCheckProof::fromText(std::istream& in)
+{
+  TraceCheckProof pf;
+  TraceCheckIdx idx = 0;
+  int64_t token = 0;
+
+  // For each line of the proof, start with the idx
+  // If there is no idx, then you're done!
+  in >> idx;
+  for (; !in.eof(); in >> idx)
+  {
+    Assert(in.good());
+
+    // Then parse the clause (it's 0-terminated)
+    std::vector<prop::SatLiteral> clause;
+    in >> token;
+    for (; token != 0; in >> token)
+    {
+      clause.emplace_back(std::abs(token) - 1, token < 0);
+    }
+
+    // Then parse the chain of literals (it's also 0-terminated)
+    std::vector<TraceCheckIdx> chain;
+    in >> token;
+    for (; token != 0; in >> token)
+    {
+      Assert(token > 0);
+      chain.push_back(token);
+    }
+
+    // Add the line to the proof
+    pf.d_lines.emplace_back(idx, std::move(clause), std::move(chain));
+  }
+  return pf;
+}
+
+ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
+                                     const std::string& dratBinary)
+{
+  std::ostringstream cmd;
+  char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
+  char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
+  char tracecheckFilename[] = "/tmp/cvc4-tracecheck-er-XXXXXX";
+
+  int r;
+  r = mkstemp(formulaFilename);
+  AlwaysAssert(r > 0);
+  close(r);
+  r = mkstemp(dratFilename);
+  AlwaysAssert(r > 0);
+  close(r);
+  r = mkstemp(tracecheckFilename);
+  AlwaysAssert(r > 0);
+  close(r);
+
+  // Write the formula
+  std::ofstream formStream(formulaFilename);
+  printDimacs(formStream, usedClauses);
+  unlink(formulaFilename);
+
+  // Write the (binary) DRAT proof
+  std::ofstream dratStream(dratFilename);
+  dratStream << dratBinary;
+  unlink(dratFilename);
+
+  // Invoke drat2er
+#if CVC4_USE_DRAT2ER
+  drat2er::TransformDRATToExtendedResolution(formulaFilename,
+                                             dratFilename,
+                                             tracecheckFilename,
+                                             false,
+                                             drat2er::options::QUIET);
+
+#else
+  Unimplemented(
+      "ER proof production requires drat2er.\n"
+      "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+#endif
+
+  // Parse the resulting TRACECHECK proof into an ER proof.
+  std::ifstream tracecheckStream(tracecheckFilename);
+  ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream));
+  unlink(tracecheckFilename);
+
+  formStream.close();
+  dratStream.close();
+  tracecheckStream.close();
+
+
+
+  return proof;
+}
+
+ErProof::ErProof(const ClauseUseRecord& usedClauses,
+                 TraceCheckProof&& tracecheck)
+    : d_inputClauseIds(), d_definitions(), d_tracecheck(tracecheck)
+{
+  // Step zero, save input clause Ids for future printing
+  std::transform(usedClauses.begin(),
+                 usedClauses.end(),
+                 std::back_inserter(d_inputClauseIds),
+                 [](const std::pair<ClauseId, prop::SatClause>& pair) {
+                   return pair.first;
+                 });
+
+  // Step one, verify the formula starts the proof
+  if (Configuration::isAssertionBuild())
+  {
+    for (size_t i = 0, n = usedClauses.size(); i < n; ++i)
+    {
+      Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
+      Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
+      Assert(d_tracecheck.d_lines[i].d_clause.size()
+             == usedClauses[i].second.size());
+      for (size_t j = 0, m = usedClauses[i].second.size(); j < m; ++j)
+      {
+        Assert(usedClauses[i].second[j] == d_tracecheck.d_lines[i].d_clause[j]);
+      }
+    }
+  }
+
+  // Step two, identify definitions. They correspond to lines that follow the
+  // input lines, are in bounds, and have no justifying chain.
+  for (size_t i = usedClauses.size(), n = d_tracecheck.d_lines.size();
+       i < n && d_tracecheck.d_lines[i].d_chain.size() == 0;)
+  {
+    prop::SatClause c = d_tracecheck.d_lines[i].d_clause;
+    Assert(c.size() > 0);
+    Assert(!c[0].isNegated());
+
+    // Get the new variable of the definition -- the first variable of the
+    // first clause
+    prop::SatVariable newVar = c[0].getSatVariable();
+
+    // The rest of the literals in the clause of the 'other literals' of the def
+    std::vector<prop::SatLiteral> otherLiterals{++c.begin(), c.end()};
+
+    size_t nLinesForThisDef = 2 + otherLiterals.size();
+    // Look at the negation of the second literal in the second clause to get
+    // the old literal
+    AlwaysAssert(d_tracecheck.d_lines.size() > i + 1,
+        "Malformed definition in TRACECHECK proof from drat2er");
+    d_definitions.emplace_back(newVar,
+                               ~d_tracecheck.d_lines[i + 1].d_clause[1],
+                               std::move(otherLiterals));
+
+    // Advance over the lines for this definition
+    i += nLinesForThisDef;
+  }
+}
+
+void ErProof::outputAsLfsc(std::ostream& os) const
+{
+  // How many parens to close?
+  size_t parenCount = 0;
+  std::unordered_set<prop::SatVariable> newVariables;
+
+  // Print Definitions
+  for (const ErDefinition& def : d_definitions)
+  {
+    os << "\n    (decl_rat_elimination_def ("
+       << (def.d_oldLiteral.isNegated() ? "neg " : "pos ")
+       << ProofManager::getVarName(def.d_oldLiteral.getSatVariable(), "bb")
+       << ") ";
+    LFSCProofPrinter::printSatClause(def.d_otherLiterals, os, "bb");
+    os << " (\\ er.v" << def.d_newVariable << " (\\ er.def"
+       << def.d_newVariable;
+    newVariables.insert(def.d_newVariable);
+  }
+  parenCount += 3 * d_definitions.size();
+
+  // Clausify Definitions
+  TraceCheckIdx firstDefClause = d_inputClauseIds.size() + 1;
+  for (const ErDefinition& def : d_definitions)
+  {
+    os << "\n    (clausify_rat_elimination_def _ _ _ "
+       << "er.def " << def.d_newVariable << " _ _ (\\ er.c" << firstDefClause
+       << " (\\ er.c" << (firstDefClause + 1) << " (\\ er.cnf"
+       << def.d_newVariable;
+
+    firstDefClause += 2 + def.d_otherLiterals.size();
+  }
+  parenCount += 4 * d_definitions.size();
+
+  // Unroll proofs of CNFs to proofs of clauses
+  firstDefClause = d_inputClauseIds.size() + 1;
+  for (const ErDefinition& def : d_definitions)
+  {
+    for (size_t i = 0, n = def.d_otherLiterals.size(); i < n; ++i)
+    {
+      os << "\n    (cnfc_unroll _ _ ";
+      os << "er.cnf" << def.d_newVariable;
+      if (i != 0)
+      {
+        os << ".u" << i;
+      }
+      os << " (\\ er.c" << (firstDefClause + 2 + i);
+      os << " (\\ er.cnf" << def.d_newVariable << ".u" << (i + 1);
+    }
+    parenCount += 3 * def.d_otherLiterals.size();
+
+    firstDefClause += 2 + def.d_otherLiterals.size();
+  }
+
+  // NB: At this point `firstDefClause` points to the first clause resulting
+  // from a resolution chain
+
+  // Now, elaborate each resolution chain
+  for (size_t cId = firstDefClause, nLines = d_tracecheck.d_lines.size();
+       cId <= nLines;
+       ++cId)
+  {
+    const std::vector<TraceCheckIdx>& chain =
+        d_tracecheck.d_lines[cId - 1].d_chain;
+    const std::vector<prop::SatLiteral> pivots = computePivotsForChain(chain);
+    Assert(chain.size() > 0);
+    Assert(chain.size() == pivots.size() + 1);
+
+    os << "\n    (satlem_simplify _ _ _ ";
+    parenCount += 1;
+
+    // Print resolution openings (reverse order)
+    for (int64_t i = pivots.size() - 1; i >= 0; --i)
+    {
+      prop::SatLiteral pivot = pivots[i];
+      os << "(" << (pivot.isNegated() ? 'Q' : 'R') << " _ _ ";
+    }
+
+    // Print resolution start
+    writeIdForClauseProof(os, chain[0]);
+    os << " ";
+
+    // Print resolution closings (forward order)
+    for (size_t i = 0, n = pivots.size(); i < n; ++i)
+    {
+      prop::SatVariable pivotVar = pivots[i].getSatVariable();
+      TraceCheckIdx clauseId = chain[i + 1];
+      writeIdForClauseProof(os, clauseId);
+      os << " ";
+      if (ContainsKey(newVariables, pivotVar))
+      {
+        // This is a defined variable
+        os << "er.v" << pivotVar;
+      }
+      else
+      {
+        os << ProofManager::getVarName(pivotVar, "bb");
+      }
+      os << ") ";
+    }
+    os << "(\\ er.c" << cId;
+    parenCount += 1;
+  }
+
+  // Write proof of bottom
+  Assert(d_tracecheck.d_lines.back().d_clause.size() == 0,
+         "The TRACECHECK proof from drat2er did not prove bottom.");
+  os << "\n      er.c" << d_tracecheck.d_lines.back().d_idx
+     << " ; (holds cln)\n";
+
+  // Finally, close the parentheses!
+  std::fill_n(std::ostream_iterator<char>(os), parenCount, ')');
+}
+
+namespace {
+/**
+ * Resolves two clauses
+ *
+ * @param dest one of the inputs, and the output too. **This is an input and
+ *             output**
+ * @param src the other input
+ *
+ * @return the unique literal that was resolved on, with the polarization that
+ *         it originally had in `dest`.
+ *
+ * For example, if dest = (1 3 -4 5) and src = (1 -3 5), then 3 is returned and
+ * after the call dest = (1 -4 5).
+ */
+prop::SatLiteral resolveModify(
+    std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>& dest,
+    const prop::SatClause& src)
+{
+  bool foundPivot = false;
+  prop::SatLiteral pivot(0, false);
+
+  for (prop::SatLiteral lit : src)
+  {
+    auto negationLocation = dest.find(~lit);
+    if (negationLocation != dest.end())
+    {
+      Assert(!foundPivot);
+      foundPivot = true;
+      dest.erase(negationLocation);
+      pivot = ~lit;
+    }
+    dest.insert(lit);
+  }
+
+  Assert(foundPivot);
+  return pivot;
+}
+}  // namespace
+
+std::vector<prop::SatLiteral> ErProof::computePivotsForChain(
+    const std::vector<TraceCheckIdx>& chain) const
+{
+  std::vector<prop::SatLiteral> pivots;
+
+  const prop::SatClause& first = d_tracecheck.d_lines[chain[0] - 1].d_clause;
+  std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+      runningClause{first.begin(), first.end()};
+
+  for (auto idx = ++chain.cbegin(), end = chain.cend(); idx != end; ++idx)
+  {
+    pivots.push_back(
+        resolveModify(runningClause, d_tracecheck.d_lines[*idx - 1].d_clause));
+  }
+  return pivots;
+}
+
+void ErProof::writeIdForClauseProof(std::ostream& o, TraceCheckIdx i) const
+{
+  if (i <= d_inputClauseIds.size())
+  {
+    // This clause is an input clause! Ask the ProofManager for its name
+    o << ProofManager::getInputClauseName(d_inputClauseIds[i - 1], "bb");
+  }
+  else
+  {
+    // This clause was introduced by a definition or resolution chain
+    o << "er.c" << i;
+  }
+}
+
+}  // namespace er
+}  // namespace proof
+}  // namespace CVC4
diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h
new file mode 100644
index 000000000..0a0038738
--- /dev/null
+++ b/src/proof/er/er_proof.h
@@ -0,0 +1,208 @@
+/*********************                                                        */
+/*! \file er_proof.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 ER Proof Format
+ **
+ ** Declares C++ types that represent an ER/TRACECHECK proof.
+ ** Defines serialization for these types.
+ **
+ ** You can find details about the way ER is encoded in the TRACECHECK
+ ** format at these locations:
+ **    https://github.com/benjaminkiesl/drat2er
+ **    http://www.cs.utexas.edu/users/marijn/publications/ijcar18.pdf
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__ER__ER_PROOF_H
+#define __CVC4__PROOF__ER__ER_PROOF_H
+
+#include <memory>
+#include <vector>
+
+#include "proof/clause_id.h"
+#include "prop/sat_solver_types.h"
+
+namespace CVC4 {
+namespace proof {
+namespace er {
+
+using ClauseUseRecord = std::vector<std::pair<ClauseId, prop::SatClause>>;
+
+/**
+ * A definition of the form:
+ *    newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n)
+ */
+struct ErDefinition
+{
+  ErDefinition(prop::SatVariable newVariable,
+               prop::SatLiteral oldLiteral,
+               std::vector<prop::SatLiteral>&& otherLiterals)
+      : d_newVariable(newVariable),
+        d_oldLiteral(oldLiteral),
+        d_otherLiterals(otherLiterals)
+  {
+  }
+
+  // newVar
+  prop::SatVariable d_newVariable;
+  // p
+  prop::SatLiteral d_oldLiteral;
+  // A list of the x_i's
+  std::vector<prop::SatLiteral> d_otherLiterals;
+};
+
+// For representing a clause's index within a TRACECHECK proof.
+using TraceCheckIdx = size_t;
+
+/**
+ * A single line in a TRACECHECK proof.
+ *
+ * Consists of the index of a new clause, the literals of that clause, and the
+ * indices for preceding clauses which can be combined in a resolution chain to
+ * produce this new clause.
+ */
+struct TraceCheckLine
+{
+  TraceCheckLine(TraceCheckIdx idx,
+                 std::vector<prop::SatLiteral>&& clause,
+                 std::vector<TraceCheckIdx>&& chain)
+      : d_idx(idx), d_clause(clause), d_chain(chain)
+  {
+  }
+
+  // The index of the new clause
+  TraceCheckIdx d_idx;
+  // The new clause
+  std::vector<prop::SatLiteral> d_clause;
+  /**
+   * Indices of clauses which must be resolved to produce this new clause.
+   * While the TRACECHECK format does not specify the order, we require them to
+   * be in resolution-order.
+   */
+  std::vector<TraceCheckIdx> d_chain;
+};
+
+/**
+ * A TRACECHECK proof -- just a list of lines
+ */
+struct TraceCheckProof
+{
+  static TraceCheckProof fromText(std::istream& in);
+  TraceCheckProof() : d_lines() {}
+
+  // The lines of this proof.
+  std::vector<TraceCheckLine> d_lines;
+};
+
+/**
+ * An extended resolution proof.
+ * It supports resolution, along with extensions of the form
+ *
+ *    newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n)
+ */
+class ErProof
+{
+ public:
+  /**
+   * Construct an ER proof from a DRAT proof, using drat2er
+   *
+   * @param usedClauses The CNF formula that we're deriving bottom from.
+   * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream.
+   */
+  static ErProof fromBinaryDratProof(const ClauseUseRecord& usedClauses,
+                                     const std::string& dratBinary);
+
+  /**
+   * Construct an ER proof from a TRACECHECK ER proof
+   *
+   * This basically just identifies groups of lines which correspond to
+   * definitions, and extracts them.
+   *
+   * @param usedClauses The CNF formula that we're deriving bottom from.
+   * @param tracecheck  The TRACECHECK proof, as a stream.
+   */
+  ErProof(const ClauseUseRecord& usedClauses, TraceCheckProof&& tracecheck);
+
+  /**
+   * Write the ER proof as an LFSC value of type (holds cln).
+   * The format is from the LFSC signature er.plf
+   *
+   * Reads the current `ProofManager` to determine what the variables should be
+   * named.
+   *
+   * @param os the stream to write to
+   */
+  void outputAsLfsc(std::ostream& os) const;
+
+  const std::vector<ClauseId>& getInputClauseIds() const
+  {
+    return d_inputClauseIds;
+  }
+
+  const std::vector<ErDefinition>& getDefinitions() const
+  {
+    return d_definitions;
+  }
+
+  const TraceCheckProof& getTraceCheckProof() const { return d_tracecheck; }
+
+ private:
+  /**
+   * Creates an empty ErProof.
+   */
+  ErProof() : d_inputClauseIds(), d_definitions(), d_tracecheck() {}
+
+  /**
+   * Computes the pivots on the basis of which an in-order resolution chain is
+   * resolved.
+   *
+   * c0   c1
+   *   \ /               Clauses c_i being resolved in a chain around
+   *    v1  c2           pivots v_i.
+   *     \ /
+   *      v2  c3
+   *       \ /
+   *        v3  c4
+   *         \ /
+   *          v4
+   *
+   *
+   * @param chain the chain, of N clause indices
+   *
+   * @return a list of N - 1 variables, the list ( v_i ) from i = 1 to N - 1
+   */
+  std::vector<prop::SatLiteral> computePivotsForChain(
+      const std::vector<TraceCheckIdx>& chain) const;
+
+  /**
+   * Write the LFSC identifier for the proof of a clause
+   *
+   * @param o where to write to
+   * @param i the TRACECHECK index for the clause whose proof identifier to
+   *        print
+   */
+  void writeIdForClauseProof(std::ostream& o, TraceCheckIdx i) const;
+
+  // A list of the Ids for the input clauses, in order.
+  std::vector<ClauseId> d_inputClauseIds;
+  // A list of new variable definitions, in order.
+  std::vector<ErDefinition> d_definitions;
+  // The underlying TRACECHECK proof.
+  TraceCheckProof d_tracecheck;
+};
+
+}  // namespace er
+}  // namespace proof
+}  // namespace CVC4
+
+#endif  // __CVC4__PROOF__ER__ER_PROOF_H
diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt
index 00c893bdb..315c78d6f 100644
--- a/test/unit/proof/CMakeLists.txt
+++ b/test/unit/proof/CMakeLists.txt
@@ -2,5 +2,6 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(drat_proof_black proof)
+cvc4_add_unit_test_black(er_proof_black proof)
 cvc4_add_unit_test_black(lrat_proof_black proof)
 cvc4_add_unit_test_black(lfsc_proof_printer_black proof)
diff --git a/test/unit/proof/er_proof_black.h b/test/unit/proof/er_proof_black.h
new file mode 100644
index 000000000..1620bb113
--- /dev/null
+++ b/test/unit/proof/er_proof_black.h
@@ -0,0 +1,406 @@
+/*********************                                                        */
+/*! \file er_proof_black.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 Black box testing of the ER proof class
+ **
+ ** In particular, tests TRACECHECK parsing and ER LFSC output.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <algorithm>
+#include <cctype>
+#include <iostream>
+#include <iterator>
+#include <vector>
+
+#include "proof/clause_id.h"
+#include "proof/er/er_proof.h"
+#include "prop/sat_solver_types.h"
+#include "utils.h"
+
+using namespace CVC4;
+using namespace CVC4::proof::er;
+using namespace CVC4::prop;
+
+class ErProofBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override {}
+  void tearDown() override {}
+
+  void testTraceCheckParse1Line();
+  void testTraceCheckParse5Lines();
+  void testErTraceCheckParse();
+  void testErTraceCheckOutput();
+  void testErTraceCheckOutputMedium();
+};
+
+void ErProofBlack::testTraceCheckParse1Line()
+{
+  std::string tracecheckText = "1 -2 3 0 4 2 0\n";
+  std::istringstream stream(tracecheckText);
+  TraceCheckProof pf = TraceCheckProof::fromText(stream);
+  TS_ASSERT_EQUALS(pf.d_lines.size(), 1);
+
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_idx, 1);
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause.size(), 2);
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[0], SatLiteral(1, true));
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[1], SatLiteral(2, false));
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain.size(), 2);
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain[0], 4);
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain[1], 2);
+}
+
+void ErProofBlack::testTraceCheckParse5Lines()
+{
+  std::string tracecheckText =
+      "1 1 -2 3 0 0\n"
+      "2 -1 0 0\n"
+      "3 2 0 0\n"
+      "4 -3 0 0\n"
+      "5 0 1 2 4 3 0\n";
+  std::istringstream stream(tracecheckText);
+  TraceCheckProof pf = TraceCheckProof::fromText(stream);
+  TS_ASSERT_EQUALS(pf.d_lines.size(), 5);
+
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_idx, 1);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_idx, 5);
+
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause.size(), 3);
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[0], SatLiteral(0, false));
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[1], SatLiteral(1, true));
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[2], SatLiteral(2, false));
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain.size(), 0);
+
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain.size(), 4);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[0], 1);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[1], 2);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[2], 4);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[3], 3);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_clause.size(), 0);
+}
+
+void ErProofBlack::testErTraceCheckParse()
+{
+  std::string tracecheckText =
+      "1  1  2 -3 0 0\n"
+      "2 -1 -2  3 0 0\n"
+      "3  2  3 -4 0 0\n"
+      "4 -2 -3  4 0 0\n"
+      "5 -1 -3 -4 0 0\n"
+      "6  1  3  4 0 0\n"
+      "7 -1  2  4 0 0\n"
+      "8  1 -2 -4 0 0\n"
+      "9 5 0 0\n"
+      "10 5 1 0 0\n"
+      "11 4 5 2 0 10 7 0\n"
+      "12 -4 5 -3 0 10 5 0\n"
+      "13 3 5 -2 0 10 2 0\n"
+      "14 -2 -4 0 2 5 8 0\n"
+      "15 4 3 0 7 2 6 0\n"
+      "16 2 -3 0 7 5 1 0\n"
+      "17 2 0 3 15 16 0\n"
+      "18 0 4 15 14 17 0\n";
+  std::istringstream stream(tracecheckText);
+  TraceCheckProof tc = TraceCheckProof::fromText(stream);
+
+  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
+  usedClauses.emplace_back(
+      1,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
+  usedClauses.emplace_back(
+      2,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
+  usedClauses.emplace_back(
+      3,
+      std::vector<SatLiteral>{
+          SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      4,
+      std::vector<SatLiteral>{
+          SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      5,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      6,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      7,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      8,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
+  ErProof pf(usedClauses, std::move(tc));
+
+  TS_ASSERT_EQUALS(pf.getInputClauseIds()[0], 1);
+  TS_ASSERT_EQUALS(pf.getInputClauseIds()[7], 8);
+
+  TS_ASSERT_EQUALS(pf.getDefinitions().size(), 1)
+  TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_newVariable, SatVariable(4));
+  TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_oldLiteral, SatLiteral(0, true));
+  TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_otherLiterals.size(), 0);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines.size(), 18);
+
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_idx, 1);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_idx, 17);
+
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause.size(), 3);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[0], SatLiteral(0, false));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[1], SatLiteral(1, false));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[2], SatLiteral(2, true));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_chain.size(), 0);
+
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause.size(), 1);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause[0], SatLiteral(1, false));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain.size(), 3);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[0], 3);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[1], 15);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[2], 16);
+}
+
+void ErProofBlack::testErTraceCheckOutput()
+{
+  std::string tracecheckText =
+      "1  1  2 -3 0 0\n"
+      "2 -1 -2  3 0 0\n"
+      "3  2  3 -4 0 0\n"
+      "4 -2 -3  4 0 0\n"
+      "5 -1 -3 -4 0 0\n"
+      "6  1  3  4 0 0\n"
+      "7 -1  2  4 0 0\n"
+      "8  1 -2 -4 0 0\n"
+      "9 5 0 0\n"
+      "10 5 1 0 0\n"
+      "11 4 5 2 0 10 7 0\n"
+      "12 -4 5 -3 0 10 5 0\n"
+      "13 3 5 -2 0 10 2 0\n"
+      "14 -2 -4 0 2 5 8 0\n"
+      "15 4 3 0 7 2 6 0\n"
+      "16 2 -3 0 7 5 1 0\n"
+      "17 2 0 3 15 16 0\n"
+      "18 0 4 15 14 17 0\n";
+  std::istringstream stream(tracecheckText);
+  TraceCheckProof tc = TraceCheckProof::fromText(stream);
+
+  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
+  usedClauses.emplace_back(
+      1,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
+  usedClauses.emplace_back(
+      2,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
+  usedClauses.emplace_back(
+      3,
+      std::vector<SatLiteral>{
+          SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      4,
+      std::vector<SatLiteral>{
+          SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      5,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      6,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      7,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      8,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
+  ErProof pf(usedClauses, std::move(tc));
+
+  std::ostringstream lfsc;
+  pf.outputAsLfsc(lfsc);
+
+  std::string out = R"EOF(
+    (decl_rat_elimination_def
+      (neg bb.v0)
+      cln
+      (\ er.v4
+      (\ er.def4
+        (clausify_rat_elimination_def _ _ _ er.def4 _ _
+          (\ er.c9
+          (\ er.c10
+          (\ er.cnf4
+            (satlem_simplify _ _ _
+              (R _ _ er.c10 bb.pb7 bb.v0) (\ er.c11
+            (satlem_simplify _ _ _
+              (R _ _ er.c10 bb.pb5 bb.v0) (\ er.c12
+            (satlem_simplify _ _ _
+              (R _ _ er.c10 bb.pb2 bb.v0) (\ er.c13
+            (satlem_simplify _ _ _
+              (Q _ _ (R _ _ bb.pb2 bb.pb5 bb.v2) bb.pb8 bb.v0) (\ er.c14
+            (satlem_simplify _ _ _
+              (Q _ _ (R _ _ bb.pb7 bb.pb2 bb.v1) bb.pb6 bb.v0) (\ er.c15
+            (satlem_simplify _ _ _
+              (Q _ _ (R _ _ bb.pb7 bb.pb5 bb.v3) bb.pb1 bb.v0) (\ er.c16
+            (satlem_simplify _ _ _
+              (R _ _ (Q _ _ bb.pb3 er.c15 bb.v3) er.c16 bb.v2) (\ er.c17
+            (satlem_simplify _ _ _
+              (Q _ _ (R _ _ (Q _ _ bb.pb4 er.c15 bb.v2) er.c14 bb.v3)
+                  er.c17 bb.v1) (\ er.c18
+              er.c18 ; (holds cln)
+            ))))))))))))))))
+          )))
+        )
+      ))
+    )
+    )EOF";
+
+  TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(out));
+}
+
+/**
+ * This proof has been specially constructed to stress-test the proof
+ * machinery, while still being short. It's a bit meandering...
+ */
+void ErProofBlack::testErTraceCheckOutputMedium()
+{
+  std::string tracecheckText =
+      "1  1  2 -3 0 0\n"
+      "2 -1 -2  3 0 0\n"
+      "3  2  3 -4 0 0\n"
+      "4 -2 -3  4 0 0\n"
+      "5 -1 -3 -4 0 0\n"
+      "6  1  3  4 0 0\n"
+      "7 -1  2  4 0 0\n"
+      "8  1 -2 -4 0 0\n"
+
+      "9  5  2  4 0 0\n"    // Definition with 2 other variables
+      "10 5  1  0 0\n"
+      "11 2 -5 -1 0 0\n"
+      "12 4 -5 -1 0 0\n"
+
+      "13 6  0 0\n"       // Definition with no other variables
+      "14 6  -3  0 0\n"
+
+      "15 -3 4 0 11 1 10 7 4 0\n" // Chain w/ both def. and input clauses
+
+      "16 -2 -4 0 2 5 8 0\n" // The useful bit of the proof
+      "17 4 3 0 7 2 6 0\n"
+      "18 2 -3 0 7 5 1 0\n"
+      "19 2 0 3 17 18 0\n"
+      "20 0 4 17 16 19 0\n";
+
+  std::istringstream stream(tracecheckText);
+  TraceCheckProof tc = TraceCheckProof::fromText(stream);
+
+  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
+  usedClauses.emplace_back(
+      1,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
+  usedClauses.emplace_back(
+      2,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
+  usedClauses.emplace_back(
+      3,
+      std::vector<SatLiteral>{
+          SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      4,
+      std::vector<SatLiteral>{
+          SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      5,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      6,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      7,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      8,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
+  ErProof pf(usedClauses, std::move(tc));
+
+  std::ostringstream lfsc;
+  pf.outputAsLfsc(lfsc);
+
+  std::string out = R"EOF(
+    (decl_rat_elimination_def
+      (neg bb.v0)
+      (clc (pos bb.v1) (clc (pos bb.v3) cln))
+      (\ er.v4
+      (\ er.def4
+    (decl_rat_elimination_def
+      (pos bb.v2)
+      cln
+      (\ er.v5
+      (\ er.def5
+        (clausify_rat_elimination_def _ _ _ er.def4 _ _
+          (\ er.c9
+          (\ er.c10
+          (\ er.cnf4
+        (clausify_rat_elimination_def _ _ _ er.def5 _ _
+          (\ er.c13
+          (\ er.c14
+          (\ er.cnf5
+            (cnfc_unroll _ _ er.cnf4
+              (\ er.c11
+              (\ er.cnf4.u1
+            (cnfc_unroll _ _ er.cnf4.u1
+              (\ er.c12
+              (\ er.cnf4.u2
+                (satlem_simplify _ _ _
+                  (R _ _ (R _ _ (Q _ _ (Q _ _ er.c11 bb.pb1 bb.v0)
+                    er.c10 er.v4)
+                    bb.pb7 bb.v0)
+                    bb.pb4 bb.v1) (\ er.c15
+                (satlem_simplify _ _ _
+                  (Q _ _ (R _ _ bb.pb2 bb.pb5 bb.v2) bb.pb8 bb.v0) (\ er.c16
+                (satlem_simplify _ _ _
+                  (Q _ _ (R _ _ bb.pb7 bb.pb2 bb.v1) bb.pb6 bb.v0) (\ er.c17
+                (satlem_simplify _ _ _
+                  (Q _ _ (R _ _ bb.pb7 bb.pb5 bb.v3) bb.pb1 bb.v0) (\ er.c18
+                (satlem_simplify _ _ _
+                  (R _ _ (Q _ _ bb.pb3 er.c17 bb.v3) er.c18 bb.v2) (\ er.c19
+                (satlem_simplify _ _ _
+                  (Q _ _ (R _ _ (Q _ _ bb.pb4 er.c17 bb.v2) er.c16 bb.v3)
+                      er.c19 bb.v1) (\ er.c20
+                  er.c20 ; (holds cln)
+              ))))))))))))
+            )))
+            )))
+          )))
+        )
+          )))
+        )
+      ))
+    )
+      ))
+    )
+    )EOF";
+
+  TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(out));
+}
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;
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 <algorithm>
+#include <string>
+#include <cctype>
+#include <iterator>
+
+/**
+ * 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;
+}