DRAT-Optimization (#2971)

This commit enables DRAT-optimization, which consists of two sub-processes:
1. removing unnecessary instructions from DRAT-proofs and
2. not proving clauses which are not needed by DRAT proofs.

These changes have the effect of dramatically shortening some some bit-vector proofs. Specifically,  proofs using lemmas in the ER, DRAT, and LRAT formats, since proofs in any of these formats are derived from a (now optimized!) DRAT proof produced by CryptoMiniSat. What follows is a description of the main parts of this PR:

## DRAT Optimization

The DRAT-optimization is done by `drat-trim`, which is bundled with `drat2er`. The (new) function `ClausalBitVectorProof::optimizeDratProof` is our interface to the optimization machinery, and most of the new logic in this PR is in that function.

## CNF Representation

The ability to not prove unused clauses requires a slight architectural change as well. In particular, we need to be able to describe **which** subset of the original clause set actually needs to be proved. To facilitate this, when the clause set for CryptoMiniSat is first formed it is represented as a (a) map from clause indices to clauses and (b) a list of indices. Then, when the CNF is optimized, we temporarily store a new list of the clauses in the optimized formula. This change in representation requires a number of small tweaks throughout the code.

## Small Fixes to Signatures

When we decided to check and accept two different kinds of DRAT, some of our DRAT-checking broke. In particular, when supporting one kind of DRAT, it is okay to `fail` (crash) when a proof fails to check. If you're supporting two kinds of DRAT, crashing in response to the first checker rejecting the proof denies the second checker an opportunity to check the proof. This PR tweaks the signatures slightly (and soundly!) to do something else instead of `fail`ing. 

12 files changed, 398 insertions, 148 deletions

diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf
index d0f647452..fa7ca3055 100644
--- a/proofs/signatures/drat.plf
+++ b/proofs/signatures/drat.plf
@@ -113,9 +113,10 @@
                                       ((clc l c') (cnf_has_bottom rest))))))
 
 ; Return a new cnf with one copy of this clause removed.
+; If the clause is absent, returns the original cnf.
 (program cnf_remove_clause ((c clause) (cs cnf)) cnf
          (match cs
-                (cnfn (fail cnf))
+                (cnfn cnfn)
                 ((cnfc c' cs')
                  (match (clause_eq c c')
                         (tt cs')
@@ -224,9 +225,11 @@
                 (tt tt)
                 (ff (match (is_at cs c)
                            (tt tt)
-                           (ff (are_all_at
+                           (ff (match c
+                                      (cln ff)
+                                      ((clc a b) (are_all_at ; dedent
                                  cs
-                                 (collect_pseudo_resolvents cs c)))))))
+                                 (collect_pseudo_resolvents cs c)))))))))
 
 ; Is this proof a valid DRAT proof of bottom?
 (program is_specified_drat_proof ((f cnf) (proof DRATProof)) bool
diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf
index ea1d90537..d16791624 100644
--- a/proofs/signatures/lrat.plf
+++ b/proofs/signatures/lrat.plf
@@ -361,14 +361,14 @@
 ; unit, it modifies the global assignment to satisfy the clause, and returns
 ; the literal that was made SAT by the new mark.
 ;
-; Fails if `c` is a TAUT
+; If `c` is a tautology, reports `MRSat`, since it is (trivially) satisfied.
 (program clause_check_unit_and_maybe_mark ((c clause)) MarkResult
          (match (clause_is_sat c)
                 (tt MRSat)
                 (ff (match (clause_is_unsat c)
                            (tt MRUnsat)
                            (ff (match (is_t c)
-                                      (tt (fail MarkResult))
+                                      (tt MRSat)
                                       (ff ; Dedent
          (match (clause_has_floating c)
                 (tt (let first (clause_first_floating c)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cff31dbcd..011ba6ab5 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -137,8 +137,8 @@ libcvc4_add_sources(
   proof/clause_id.h
   proof/cnf_proof.cpp
   proof/cnf_proof.h
-  proof/dimacs_printer.cpp
-  proof/dimacs_printer.h
+  proof/dimacs.cpp
+  proof/dimacs.h
   proof/drat/drat_proof.cpp
   proof/drat/drat_proof.h
   proof/er/er_proof.cpp
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index eed295b1a..07589fd07 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -17,24 +17,35 @@
 #include "cvc4_private.h"
 
 #include <algorithm>
+#include <iostream>
 #include <iterator>
-#include <set>
+#include <unordered_set>
 
 #include "options/bv_options.h"
 #include "proof/clausal_bitvector_proof.h"
+#include "proof/dimacs.h"
 #include "proof/drat/drat_proof.h"
 #include "proof/er/er_proof.h"
 #include "proof/lfsc_proof_printer.h"
 #include "proof/lrat/lrat_proof.h"
 #include "theory/bv/theory_bv.h"
 
+#if CVC4_USE_DRAT2ER
+#include "drat2er_options.h"
+#include "drat_trim_interface.h"
+#endif
+
 namespace CVC4 {
 
 namespace proof {
 
 ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv,
                                              TheoryProofEngine* proofEngine)
-    : BitVectorProof(bv, proofEngine), d_usedClauses(), d_binaryDratProof()
+    : BitVectorProof(bv, proofEngine),
+      d_clauses(),
+      d_originalClauseIndices(),
+      d_binaryDratProof(),
+      d_coreClauseIndices()
 {
 }
 
@@ -69,33 +80,151 @@ void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
 void ClausalBitVectorProof::registerUsedClause(ClauseId id,
                                                prop::SatClause& clause)
 {
-  d_usedClauses.emplace_back(id, clause);
+  d_clauses.emplace(id, clause);
+  d_originalClauseIndices.push_back(id);
 };
 
 void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
 {
+  optimizeDratProof();
+
   // Debug dump of DRAT Proof
   if (Debug.isOn("bv::clausal"))
   {
     std::string serializedDratProof = d_binaryDratProof.str();
+    Debug("bv::clausal") << "option: " << options::bvOptimizeSatProof()
+                         << std::endl;
     Debug("bv::clausal") << "binary DRAT proof byte count: "
                          << serializedDratProof.size() << std::endl;
-    Debug("bv::clausal") << "Parsing DRAT proof ... " << std::endl;
-    drat::DratProof dratProof =
-        drat::DratProof::fromBinary(serializedDratProof);
-
-    Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl;
-    dratProof.outputAsText(Debug("bv::clausal"));
+    Debug("bv::clausal") << "clause count: " << d_coreClauseIndices.size()
+                         << std::endl;
   }
 
   // Empty any old record of which atoms were used
   d_atomsInBitblastingProof.clear();
+  Assert(d_atomsInBitblastingProof.size() == 0);
 
   // For each used clause, ask the CNF proof which atoms are used in it
-  for (const auto& usedIndexAndClause : d_usedClauses)
+  for (const ClauseId usedIdx : d_coreClauseIndices)
   {
-    d_cnfProof->collectAtoms(&usedIndexAndClause.second,
-                             d_atomsInBitblastingProof);
+    d_cnfProof->collectAtoms(&d_clauses.at(usedIdx), d_atomsInBitblastingProof);
+  }
+}
+
+void ClausalBitVectorProof::optimizeDratProof()
+{
+  if (options::bvOptimizeSatProof()
+          == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF
+      || options::bvOptimizeSatProof()
+             == theory::bv::BvOptimizeSatProof::
+                    BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
+  {
+    Debug("bv::clausal") << "Optimizing DRAT" << std::endl;
+    char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
+    char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
+    char optDratFilename[] = "/tmp/cvc4-optimized-drat-XXXXXX";
+    char optFormulaFilename[] = "/tmp/cvc4-optimized-formula-XXXXXX";
+    int r;
+    r = mkstemp(formulaFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+    r = mkstemp(dratFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+    r = mkstemp(optDratFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+    r = mkstemp(optFormulaFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+
+    std::ofstream formStream(formulaFilename);
+    printDimacs(formStream, d_clauses, d_originalClauseIndices);
+    formStream.close();
+
+    std::ofstream dratStream(dratFilename);
+    dratStream << d_binaryDratProof.str();
+    dratStream.close();
+
+#if CVC4_USE_DRAT2ER
+    int dratTrimExitCode =
+        drat2er::drat_trim::OptimizeWithDratTrim(formulaFilename,
+                                                 dratFilename,
+                                                 optFormulaFilename,
+                                                 optDratFilename,
+                                                 drat2er::options::QUIET);
+    AlwaysAssert(
+        dratTrimExitCode == 0, "drat-trim exited with %d", dratTrimExitCode);
+#else
+    Unimplemented(
+        "Proof production when using CryptoMiniSat requires drat2er.\n"
+        "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+#endif
+
+    d_binaryDratProof.str("");
+    Assert(d_binaryDratProof.str().size() == 0);
+
+    std::ifstream lratStream(optDratFilename);
+    std::copy(std::istreambuf_iterator<char>(lratStream),
+              std::istreambuf_iterator<char>(),
+              std::ostreambuf_iterator<char>(d_binaryDratProof));
+
+    if (options::bvOptimizeSatProof()
+        == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
+    {
+      std::ifstream optFormulaStream{optFormulaFilename};
+      std::vector<prop::SatClause> core = parseDimacs(optFormulaStream);
+      optFormulaStream.close();
+
+      // Now we need to compute the clause indices for the UNSAT core. This is a
+      // bit difficult because drat-trim may have reordered clauses, and/or
+      // removed duplicate literals. We use literal sets as the canonical clause
+      // form.
+      std::unordered_map<
+          std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>,
+          ClauseId,
+          prop::SatClauseSetHashFunction>
+          cannonicalClausesToIndices;
+      for (const auto& kv : d_clauses)
+      {
+        cannonicalClausesToIndices.emplace(
+            std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>{
+                kv.second.begin(), kv.second.end()},
+            kv.first);
+      }
+
+      d_coreClauseIndices.clear();
+      std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+          coreClauseCanonical;
+      for (const prop::SatClause& coreClause : core)
+      {
+        coreClauseCanonical.insert(coreClause.begin(), coreClause.end());
+        d_coreClauseIndices.push_back(
+            cannonicalClausesToIndices.at(coreClauseCanonical));
+        coreClauseCanonical.clear();
+      }
+      Debug("bv::clausal") << "Optimizing the DRAT proof and the formula"
+                           << std::endl;
+    }
+    else
+    {
+      Debug("bv::clausal") << "Optimizing the DRAT proof but not the formula"
+                           << std::endl;
+      d_coreClauseIndices = d_originalClauseIndices;
+    }
+
+    Assert(d_coreClauseIndices.size() > 0);
+    remove(formulaFilename);
+    remove(dratFilename);
+    remove(optDratFilename);
+    remove(optFormulaFilename);
+    Debug("bv::clausal") << "Optimized DRAT" << std::endl;
+  }
+  else
+  {
+    Debug("bv::clausal") << "Not optimizing the formula or the DRAT proof"
+                         << std::endl;
+    d_coreClauseIndices = d_originalClauseIndices;
   }
 }
 
@@ -120,10 +249,9 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
   d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
 
   os << "\n;; BB-CNF proofs\n";
-  for (const auto& idAndClause : d_usedClauses)
+  for (const ClauseId id : d_coreClauseIndices)
   {
-    d_cnfProof->printCnfProofForClause(
-        idAndClause.first, &idAndClause.second, os, paren);
+    d_cnfProof->printCnfProofForClause(id, &d_clauses.at(id), os, paren);
   }
 }
 
@@ -137,13 +265,8 @@ void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
   os << "\n;; Proof of input to SAT solver\n";
   os << "(@ proofOfSatInput ";
   paren << ")";
-  std::vector<ClauseId> usedIds;
-  usedIds.reserve(d_usedClauses.size());
-  for (const auto& idAnd : d_usedClauses)
-  {
-    usedIds.push_back(idAnd.first);
-  };
-  LFSCProofPrinter::printSatInputProof(usedIds, os, "bb");
+
+  LFSCProofPrinter::printSatInputProof(d_coreClauseIndices, os, "bb");
 
   os << "\n;; DRAT Proof Value\n";
   os << "(@ dratProof ";
@@ -166,19 +289,13 @@ void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
   os << "\n;; Proof of input to SAT solver\n";
   os << "(@ proofOfCMap ";
   paren << ")";
-  std::vector<ClauseId> usedIds;
-  usedIds.reserve(d_usedClauses.size());
-  for (const auto& idAnd : d_usedClauses)
-  {
-    usedIds.push_back(idAnd.first);
-  };
-  LFSCProofPrinter::printCMapProof(usedIds, os, "bb");
+  LFSCProofPrinter::printCMapProof(d_coreClauseIndices, os, "bb");
 
   os << "\n;; DRAT Proof Value\n";
   os << "(@ lratProof ";
   paren << ")";
-  lrat::LratProof pf =
-      lrat::LratProof::fromDratProof(d_usedClauses, d_binaryDratProof.str());
+  lrat::LratProof pf = lrat::LratProof::fromDratProof(
+      d_clauses, d_coreClauseIndices, d_binaryDratProof.str());
   pf.outputAsLfsc(os);
   os << "\n";
 
@@ -194,8 +311,8 @@ void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os,
          "the BV theory should only be proving bottom directly in the eager "
          "bitblasting mode");
 
-  er::ErProof pf =
-      er::ErProof::fromBinaryDratProof(d_usedClauses, d_binaryDratProof.str());
+  er::ErProof pf = er::ErProof::fromBinaryDratProof(
+      d_clauses, d_coreClauseIndices, d_binaryDratProof.str());
 
   pf.outputAsLfsc(os);
 }
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
index b10b1ad1c..a410b5b38 100644
--- a/src/proof/clausal_bitvector_proof.h
+++ b/src/proof/clausal_bitvector_proof.h
@@ -61,9 +61,16 @@ class ClausalBitVectorProof : public BitVectorProof
 
  protected:
   // A list of all clauses and their ids which are passed into the SAT solver
-  std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
+  std::unordered_map<ClauseId, prop::SatClause> d_clauses{};
+  std::vector<ClauseId> d_originalClauseIndices{};
   // Stores the proof recieved from the SAT solver.
-  std::ostringstream d_binaryDratProof;
+  std::ostringstream d_binaryDratProof{};
+  std::vector<ClauseId> d_coreClauseIndices{};
+
+ private:
+  // Optimizes the DRAT proof stored in `d_binaryDratProof` and returns a list
+  // of clause actually needed to check that proof (a smaller UNSAT core)
+  void optimizeDratProof();
 };
 
 /**
diff --git a/src/proof/dimacs_printer.cpp b/src/proof/dimacs.cpp
index 04f880e11..cced98660 100644
--- a/src/proof/dimacs_printer.cpp
+++ b/src/proof/dimacs.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file dimacs_printer.cpp
+/*! \file dimacs.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Alex Ozdemir
@@ -14,7 +14,9 @@
  ** Defines serialization for SAT problems as DIMACS
  **/
 
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
+
+#include "base/cvc4_assert.h"
 
 #include <iostream>
 
@@ -43,14 +45,15 @@ std::ostream& textOut(std::ostream& o, const prop::SatClause& c)
   return o << "0";
 }
 
-void printDimacs(
-    std::ostream& o,
-    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses)
+void printDimacs(std::ostream& o,
+                 const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+                 const std::vector<ClauseId>& usedIndices)
 {
   size_t maxVar = 0;
-  for (const auto& c : usedClauses)
+  for (const ClauseId i : usedIndices)
   {
-    for (const auto& l : c.second)
+    const prop::SatClause& c = clauses.at(i);
+    for (const auto& l : c)
     {
       if (l.getSatVariable() + 1 > maxVar)
       {
@@ -58,10 +61,11 @@ void printDimacs(
       }
     }
   }
-  o << "p cnf " << maxVar << " " << usedClauses.size() << '\n';
-  for (const auto& idAndClause : usedClauses)
+  o << "p cnf " << maxVar << " " << usedIndices.size() << '\n';
+  for (const ClauseId i : usedIndices)
   {
-    for (const auto& l : idAndClause.second)
+    const prop::SatClause& c = clauses.at(i);
+    for (const auto& l : c)
     {
       if (l.isNegated())
       {
@@ -73,5 +77,44 @@ void printDimacs(
   }
 }
 
+std::vector<prop::SatClause> parseDimacs(std::istream& in)
+{
+  std::string tag;
+  uint64_t nVars;
+  uint64_t nClauses;
+
+  in >> tag;
+  Assert(in.good());
+  Assert(tag == "p");
+
+  in >> tag;
+  Assert(in.good());
+  Assert(tag == "cnf");
+
+  in >> nVars;
+  Assert(nVars >= 0);
+
+  in >> nClauses;
+  Assert(nClauses >= 0);
+
+  std::vector<prop::SatClause> cnf;
+  for (uint64_t i = 0; i < nClauses; ++i)
+  {
+    cnf.emplace_back();
+    int64_t lit;
+    in >> lit;
+    Assert(in.good());
+    while (lit != 0)
+    {
+      cnf.back().emplace_back(std::abs(lit) - 1, lit < 0);
+      in >> lit;
+      Assert(static_cast<uint64_t>(std::abs(lit)) <= nVars);
+      Assert(in.good());
+    }
+  }
+
+  return cnf;
+}
+
 }  // namespace proof
 }  // namespace CVC4
diff --git a/src/proof/dimacs_printer.h b/src/proof/dimacs.h
index 2ae4abefa..5956c5d26 100644
--- a/src/proof/dimacs_printer.h
+++ b/src/proof/dimacs.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file dimacs_printer.h
+/*! \file dimacs.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Alex Ozdemir
@@ -11,16 +11,17 @@
  **
  ** \brief DIMACS SAT Problem Format
  **
- ** Defines serialization for SAT problems as DIMACS
+ ** Defines serialization/deserialization for SAT problems as DIMACS
  **/
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__PROOF__DIMACS_PRINTER_H
-#define CVC4__PROOF__DIMACS_PRINTER_H
+#ifndef CVC4__PROOF__DIMACS_H
+#define CVC4__PROOF__DIMACS_H
 
 #include <iosfwd>
 #include <memory>
+#include <unordered_map>
 
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
@@ -56,11 +57,13 @@ std::ostream& textOut(std::ostream& o, const prop::SatClause& c);
  * @param o where to print to
  * @param usedClauses the CNF formula
  */
-void printDimacs(
-    std::ostream& o,
-    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses);
+void printDimacs(std::ostream& o,
+                 const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+                 const std::vector<ClauseId>& usedIndices);
+
+std::vector<prop::SatClause> parseDimacs(std::istream& i);
 
 }  // namespace proof
 }  // namespace CVC4
 
-#endif  // CVC4__PROOF__DIMACS_PRINTER_H
+#endif  // CVC4__PROOF__DIMACS_H
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 22903c3c9..9160546f9 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -31,7 +31,7 @@
 
 #include "base/cvc4_assert.h"
 #include "base/map_util.h"
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
 #include "proof/lfsc_proof_printer.h"
 #include "proof/proof_manager.h"
 
@@ -80,8 +80,10 @@ TraceCheckProof TraceCheckProof::fromText(std::istream& in)
   return pf;
 }
 
-ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
-                                     const std::string& dratBinary)
+ErProof ErProof::fromBinaryDratProof(
+    const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+    const std::vector<ClauseId>& usedIds,
+    const std::string& dratBinary)
 {
   std::ostringstream cmd;
   char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
@@ -101,7 +103,7 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
 
   // Write the formula
   std::ofstream formStream(formulaFilename);
-  printDimacs(formStream, usedClauses);
+  printDimacs(formStream, clauses, usedIds);
   formStream.close();
 
   // Write the (binary) DRAT proof
@@ -126,7 +128,8 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
 
   // Parse the resulting TRACECHECK proof into an ER proof.
   std::ifstream tracecheckStream(tracecheckFilename);
-  ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream));
+  TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream);
+  ErProof proof(clauses, usedIds, std::move(pf));
   tracecheckStream.close();
 
   remove(formulaFilename);
@@ -136,17 +139,21 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
   return proof;
 }
 
-ErProof::ErProof(const ClauseUseRecord& usedClauses,
+ErProof::ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+                 const std::vector<ClauseId>& usedIds,
                  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;
-                 });
+  d_inputClauseIds = usedIds;
+
+  // Make a list of (idx, clause pairs), the used ones.
+  std::vector<std::pair<ClauseId, prop::SatClause>> usedClauses;
+  std::transform(
+      usedIds.begin(),
+      usedIds.end(),
+      std::back_inserter(usedClauses),
+      [&](const ClauseId& i) { return make_pair(i, clauses.at(i)); });
 
   // Step one, verify the formula starts the proof
   if (Configuration::isAssertionBuild())
@@ -162,14 +169,6 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses,
           originalClause{usedClauses[i].second.begin(),
                          usedClauses[i].second.end()};
       Assert(traceCheckClause == originalClause);
-      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]);
-      }
     }
   }
 
diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h
index f5af0783b..d6cbd9213 100644
--- a/src/proof/er/er_proof.h
+++ b/src/proof/er/er_proof.h
@@ -27,6 +27,7 @@
 #define CVC4__PROOF__ER__ER_PROOF_H
 
 #include <memory>
+#include <unordered_map>
 #include <vector>
 
 #include "proof/clause_id.h"
@@ -36,8 +37,6 @@ 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)
@@ -116,11 +115,14 @@ class ErProof
   /**
    * 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.
+   * @param clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
+   * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream
    */
-  static ErProof fromBinaryDratProof(const ClauseUseRecord& usedClauses,
-                                     const std::string& dratBinary);
+  static ErProof fromBinaryDratProof(
+      const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+      const std::vector<ClauseId>& usedIds,
+      const std::string& dratBinary);
 
   /**
    * Construct an ER proof from a TRACECHECK ER proof
@@ -128,10 +130,13 @@ class ErProof
    * 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 clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
    * @param tracecheck  The TRACECHECK proof, as a stream.
    */
-  ErProof(const ClauseUseRecord& usedClauses, TraceCheckProof&& tracecheck);
+  ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+          const std::vector<ClauseId>& usedIds,
+          TraceCheckProof&& tracecheck);
 
   /**
    * Write the ER proof as an LFSC value of type (holds cln).
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index a1939ec92..e414c64c9 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -26,7 +26,7 @@
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
 #include "proof/lfsc_proof_printer.h"
 
 #if CVC4_USE_DRAT2ER
@@ -104,6 +104,7 @@ void printHints(std::ostream& o,
  */
 void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
 {
+  Assert(indices.size() > 0);
   // Verify that the indices are sorted!
   for (size_t i = 0, n = indices.size() - 1; i < n; ++i)
   {
@@ -123,7 +124,8 @@ void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
 // Prints the LRAT addition line in textual format
 
 LratProof LratProof::fromDratProof(
-    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
+    const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+    const std::vector<ClauseId> usedIds,
     const std::string& dratBinary)
 {
   std::ostringstream cmd;
@@ -141,7 +143,7 @@ LratProof LratProof::fromDratProof(
   AlwaysAssert(r > 0);
   close(r);
   std::ofstream formStream(formulaFilename);
-  printDimacs(formStream, usedClauses);
+  printDimacs(formStream, clauses, usedIds);
   formStream.close();
 
   std::ofstream dratStream(dratFilename);
@@ -206,10 +208,13 @@ LratProof::LratProof(std::istream& textualProof)
         }
         clauses.push_back(di);
       }
-      std::sort(clauses.begin(), clauses.end());
-      std::unique_ptr<LratInstruction> instr(
-          new LratDeletion(clauseIdx, std::move(clauses)));
-      d_instructions.push_back(std::move(instr));
+      if (clauses.size() > 0)
+      {
+        std::sort(clauses.begin(), clauses.end());
+        std::unique_ptr<LratInstruction> instr(
+            new LratDeletion(clauseIdx, std::move(clauses)));
+        d_instructions.push_back(std::move(instr));
+      }
     }
     else
     {
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index 33b2fad3f..54db1837d 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -129,15 +129,13 @@ class LratProof
   /**
    * @brief Construct an LRAT proof from a DRAT proof, using drat-trim
    *
-   * @param usedClauses The CNF formula that we're deriving bottom from.
-   *                    It's a map because other parts of the system represent
-   *                    it this way.
-   * @param clauseOrder A record of the order in which those clauses were
-   *                    given to the SAT solver.
+   * @param clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
    * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream.
    */
   static LratProof fromDratProof(
-      const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
+      const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+      const std::vector<ClauseId> usedIds,
       const std::string& dratBinary);
   /**
    * @brief Construct an LRAT proof from its textual representation
diff --git a/test/unit/proof/er_proof_black.h b/test/unit/proof/er_proof_black.h
index 1620bb113..9089cee5f 100644
--- a/test/unit/proof/er_proof_black.h
+++ b/test/unit/proof/er_proof_black.h
@@ -20,6 +20,7 @@
 #include <cctype>
 #include <iostream>
 #include <iterator>
+#include <unordered_map>
 #include <vector>
 
 #include "proof/clause_id.h"
@@ -44,6 +45,23 @@ class ErProofBlack : public CxxTest::TestSuite
   void testErTraceCheckOutputMedium();
 };
 
+/**
+ * @brief Add a new clause to the clause store and list of used clauses
+ *
+ * @param clauses the clause store
+ * @param usedIds the used clauses
+ * @param id the id of the new clause
+ * @param clause the clause itself
+ */
+void addClause(std::unordered_map<ClauseId, SatClause>& clauses,
+               std::vector<ClauseId>& usedIds,
+               ClauseId id,
+               SatClause&& clause)
+{
+  clauses.emplace(id, std::move(clause));
+  usedIds.push_back(id);
+}
+
 void ErProofBlack::testTraceCheckParse1Line()
 {
   std::string tracecheckText = "1 -2 3 0 4 2 0\n";
@@ -113,40 +131,56 @@ void ErProofBlack::testErTraceCheckParse()
   std::istringstream stream(tracecheckText);
   TraceCheckProof tc = TraceCheckProof::fromText(stream);
 
-  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
-  usedClauses.emplace_back(
+  std::unordered_map<ClauseId, SatClause> clauses;
+  std::vector<ClauseId> usedIds;
+  addClause(
+      clauses,
+      usedIds,
       1,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       2,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       3,
       std::vector<SatLiteral>{
           SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       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(
+  addClause(clauses,
+            usedIds,
+            5,
+            std::vector<SatLiteral>{
+                SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  addClause(
+      clauses,
+      usedIds,
       6,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       7,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       8,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
-  ErProof pf(usedClauses, std::move(tc));
+  ErProof pf(clauses, usedIds, std::move(tc));
 
   TS_ASSERT_EQUALS(pf.getInputClauseIds()[0], 1);
   TS_ASSERT_EQUALS(pf.getInputClauseIds()[7], 8);
@@ -161,13 +195,17 @@ void ErProofBlack::testErTraceCheckParse()
   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_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_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);
@@ -198,40 +236,56 @@ void ErProofBlack::testErTraceCheckOutput()
   std::istringstream stream(tracecheckText);
   TraceCheckProof tc = TraceCheckProof::fromText(stream);
 
-  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
-  usedClauses.emplace_back(
+  std::unordered_map<ClauseId, SatClause> clauses;
+  std::vector<ClauseId> usedIds;
+  addClause(
+      clauses,
+      usedIds,
       1,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       2,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       3,
       std::vector<SatLiteral>{
           SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       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(
+  addClause(clauses,
+            usedIds,
+            5,
+            std::vector<SatLiteral>{
+                SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  addClause(
+      clauses,
+      usedIds,
       6,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       7,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       8,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
-  ErProof pf(usedClauses, std::move(tc));
+  ErProof pf(clauses, usedIds, std::move(tc));
 
   std::ostringstream lfsc;
   pf.outputAsLfsc(lfsc);
@@ -290,17 +344,17 @@ void ErProofBlack::testErTraceCheckOutputMedium()
       "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
+      "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
+      "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
+      "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
+      "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"
@@ -309,40 +363,56 @@ void ErProofBlack::testErTraceCheckOutputMedium()
   std::istringstream stream(tracecheckText);
   TraceCheckProof tc = TraceCheckProof::fromText(stream);
 
-  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
-  usedClauses.emplace_back(
+  std::unordered_map<ClauseId, SatClause> clauses;
+  std::vector<ClauseId> usedIds;
+  addClause(
+      clauses,
+      usedIds,
       1,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       2,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       3,
       std::vector<SatLiteral>{
           SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       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(
+  addClause(clauses,
+            usedIds,
+            5,
+            std::vector<SatLiteral>{
+                SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  addClause(
+      clauses,
+      usedIds,
       6,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       7,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       8,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
-  ErProof pf(usedClauses, std::move(tc));
+  ErProof pf(clauses, usedIds, std::move(tc));
 
   std::ostringstream lfsc;
   pf.outputAsLfsc(lfsc);