From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Tue, 2 Jul 2019 09:37:44 +0000 (-0700)
Subject: Optimize DRAT optimization: clause matching (#3074)
X-Git-Tag: cvc5-1.0.0~4096
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c5a8e7bee22e9b154a5ac65c52cc04d3d2ba3c0;p=cvc5.git

Optimize DRAT optimization: clause matching (#3074)

* improved proof production statistics

This commit creates new statistics which will help us understand what is
so expensive about proof production.

There are already statistics for:
* Net time spent building/printing the LFSC proof.
* Size of the LFSC proof.

This commit adds statistics for:
* The time cost of DRAT optimization:
   * net time
   * tool time (drat-trim)
   * clause matching time (matching core clauses with input clauses)
      * Non-trivial because drat-trim can (and does) dedup and reorder
        literals
* The advantage of DRAT optimization (proof/formula size before/after)
* The time cost of DRAT translation [to LRAT or ER] (net time, tool time)
* The time cost of skeleton traversal
* The time cost of printing declatations
* The time cost of printing CNF proofs
* The time cost of printing theory lemmas
* The time cost of printing final UNSAT proof.

There is a method, toStream, which is responsible for much of proof
production. The whole method was timed, but subsections were not. The
timings above consider subsections of it.

I also wanted to better understand the cost of DRAT optimization and
translation.

* [BV Proof] Optimize DRAT optimization

tldr: I made a bad data-structure/algorithm choice when implementing
part of DRAT/CNF-optimization, which consumed **a lot** of time on some
bechmarks. This commit fixes that choice.

Long Version:

Set-Keyed Maps Considered Harmful
=================================

Algorithmic Problem
-------------------

The DRAT optimization process spits out a unsatifiable core of the CNF.
The clauses in the core are all from the original formula, but their
literals may have been reordered and deduplicated.  We must match the
old clauses with new ones, so we know which old clauses are in the core.

Old (BAD) Solution
------------------

Before I didn't really think about this process very much. I built a
solution in which clauses were canonically represented by hash sets of
literals, and made a hash map from canonical clauses to clause indices
into the original CNF.

Problem With Old Solution
-------------------------

In hindsight this was a bad idea. First, it required a new hash set to
be heap-allocated for every clause in the CNF. Second, the map lookups
required set-hashes (reasonable -- linear time, once) and hash-set
equality (not reasonable -- quadratic time, multiple times) on every
lookup.

New Solution
------------

The ideal solution is probably to have the map from clauses to clause
ids be something like a trie. STL doesn't have a trie, but representing
clauses as sorted, deduped vectors of literal in a tree based on
lexicographical comparison is pretty closed to this. On randomly chosen
examples it seems to be a huge improvement over the old
map-keyed-by-sets solution, and I'm in the process of running a full set
of bechmarks.

Also, we store pointers to the clauses already stored elsewhere in the
proof, instead of allocating new memory for them.

Future Work
-----------

It may also be reasonable to do a hash map of sorted, deduped, vector
clauses. I haven't tried this, yet (there's a TODO in the code).

* Update src/proof/clausal_bitvector_proof.h

Thanks andres!

Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>

* Respond to Andres' Review: better use of CodeTimer

* Removed commented code (Andres)
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3b0e14976..885b26078 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -221,6 +221,7 @@ libcvc4_add_sources(
   prop/sat_solver_factory.cpp
   prop/sat_solver_factory.h
   prop/bv_sat_solver_notify.h
+  prop/sat_solver_types.cpp
   prop/sat_solver_types.h
   prop/theory_proxy.cpp
   prop/theory_proxy.h
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index 5d6641e49..9d6d0d193 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -19,7 +19,7 @@
 #include <algorithm>
 #include <iostream>
 #include <iterator>
-#include <unordered_set>
+#include <map>
 
 #include "options/bv_options.h"
 #include "proof/clausal_bitvector_proof.h"
@@ -28,6 +28,8 @@
 #include "proof/er/er_proof.h"
 #include "proof/lfsc_proof_printer.h"
 #include "proof/lrat/lrat_proof.h"
+#include "prop/sat_solver_types.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/theory_bv.h"
 
 #if CVC4_USE_DRAT2ER
@@ -45,7 +47,9 @@ ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv,
       d_clauses(),
       d_originalClauseIndices(),
       d_binaryDratProof(),
-      d_coreClauseIndices()
+      d_coreClauseIndices(),
+      d_dratTranslationStatistics(),
+      d_dratOptimizationStatistics()
 {
 }
 
@@ -80,7 +84,9 @@ void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
 void ClausalBitVectorProof::registerUsedClause(ClauseId id,
                                                prop::SatClause& clause)
 {
-  d_clauses.emplace(id, clause);
+  prop::SatClause& emplaced_clause =
+      d_clauses.emplace(id, clause).first->second;
+  canonicalizeClause(emplaced_clause);
   d_originalClauseIndices.push_back(id);
 };
 
@@ -111,8 +117,20 @@ void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
   }
 }
 
+struct SatClausePointerComparator
+{
+  inline bool operator()(const prop::SatClause* const& l,
+                         const prop::SatClause* const& r) const
+  {
+    prop::SatClauseLessThan cmp;
+    return cmp(*l, *r);
+  }
+};
+
 void ClausalBitVectorProof::optimizeDratProof()
 {
+  TimerStat::CodeTimer optimizeDratProofTimer{
+      d_dratOptimizationStatistics.d_totalTime};
   if (options::bvOptimizeSatProof()
           == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF
       || options::bvOptimizeSatProof()
@@ -125,70 +143,93 @@ void ClausalBitVectorProof::optimizeDratProof()
     std::string optDratFilename("cvc4-optimized-drat-XXXXXX");
     std::string optFormulaFilename("cvc4-optimized-formula-XXXXXX");
 
-    std::fstream formStream = openTmpFile(&formulaFilename);
-    printDimacs(formStream, d_clauses, d_originalClauseIndices);
-    formStream.close();
+    {
+      std::fstream formStream = openTmpFile(&formulaFilename);
+      const int64_t startPos = static_cast<int64_t>(formStream.tellp());
+      printDimacs(formStream, d_clauses, d_originalClauseIndices);
+      d_dratOptimizationStatistics.d_initialFormulaSize.setData(
+          static_cast<int64_t>(formStream.tellp()) - startPos);
+      formStream.close();
+    }
 
-    std::fstream dratStream = openTmpFile(&dratFilename);
-    dratStream << d_binaryDratProof.str();
-    dratStream.close();
+    {
+      std::fstream dratStream = openTmpFile(&dratFilename);
+      const int64_t startPos = static_cast<int64_t>(dratStream.tellp());
+      dratStream << d_binaryDratProof.str();
+      d_dratOptimizationStatistics.d_initialDratSize.setData(
+          static_cast<int64_t>(dratStream.tellp()) - startPos);
+      dratStream.close();
+    }
 
     std::fstream optDratStream = openTmpFile(&optDratFilename);
     std::fstream optFormulaStream = openTmpFile(&optFormulaFilename);
 
 #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);
+    {
+      TimerStat::CodeTimer runDratTimeOptimizationTimer{
+          d_dratOptimizationStatistics.d_toolTime};
+      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::copy(std::istreambuf_iterator<char>(optDratStream),
-              std::istreambuf_iterator<char>(),
-              std::ostreambuf_iterator<char>(d_binaryDratProof));
+    {
+      d_binaryDratProof.str("");
+      Assert(d_binaryDratProof.str().size() == 0);
+
+      const int64_t startPos = static_cast<int64_t>(d_binaryDratProof.tellp());
+      std::ifstream lratStream(optDratFilename);
+      std::copy(std::istreambuf_iterator<char>(lratStream),
+                std::istreambuf_iterator<char>(),
+                std::ostreambuf_iterator<char>(d_binaryDratProof));
+      d_dratOptimizationStatistics.d_optimizedDratSize.setData(
+          static_cast<int64_t>(d_binaryDratProof.tellp()) - startPos);
+    }
 
     if (options::bvOptimizeSatProof()
         == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
     {
+      std::ifstream optFormulaStream{optFormulaFilename};
+      const int64_t startPos = static_cast<int64_t>(optFormulaStream.tellg());
       std::vector<prop::SatClause> core = parseDimacs(optFormulaStream);
+      d_dratOptimizationStatistics.d_optimizedFormulaSize.setData(
+          static_cast<int64_t>(optFormulaStream.tellg()) - startPos);
+      optFormulaStream.close();
+
+      CodeTimer clauseMatchingTimer{
+          d_dratOptimizationStatistics.d_clauseMatchingTime};
 
       // 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>
+      //
+      // TODO (aozdemir) It may be better to use a hash map instead of a tree
+      // map here.
+      std::map<const prop::SatClause*, ClauseId, SatClausePointerComparator>
           cannonicalClausesToIndices;
       for (const auto& kv : d_clauses)
       {
-        cannonicalClausesToIndices.emplace(
-            std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>{
-                kv.second.begin(), kv.second.end()},
-            kv.first);
+        cannonicalClausesToIndices[&kv.second] = kv.first;
       }
 
       d_coreClauseIndices.clear();
-      std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
-          coreClauseCanonical;
-      for (const prop::SatClause& coreClause : core)
+
+      for (prop::SatClause& coreClause : core)
       {
-        coreClauseCanonical.insert(coreClause.begin(), coreClause.end());
+        canonicalizeClause(coreClause);
         d_coreClauseIndices.push_back(
-            cannonicalClausesToIndices.at(coreClauseCanonical));
-        coreClauseCanonical.clear();
+            cannonicalClausesToIndices.at(&coreClause));
       }
       Debug("bv::clausal") << "Optimizing the DRAT proof and the formula"
                            << std::endl;
@@ -217,6 +258,57 @@ void ClausalBitVectorProof::optimizeDratProof()
   }
 }
 
+void ClausalBitVectorProof::canonicalizeClause(prop::SatClause& clause)
+{
+  std::sort(clause.begin(), clause.end());
+  clause.erase(std::unique(clause.begin(), clause.end()), clause.end());
+}
+
+ClausalBitVectorProof::DratTranslationStatistics::DratTranslationStatistics()
+    : d_totalTime("proof::bv::dratTranslation::totalTime"),
+      d_toolTime("proof::bv::dratTranslation::toolTime")
+{
+  smtStatisticsRegistry()->registerStat(&d_totalTime);
+  smtStatisticsRegistry()->registerStat(&d_toolTime);
+}
+
+ClausalBitVectorProof::DratTranslationStatistics::~DratTranslationStatistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_totalTime);
+  smtStatisticsRegistry()->unregisterStat(&d_toolTime);
+}
+
+ClausalBitVectorProof::DratOptimizationStatistics::DratOptimizationStatistics()
+    : d_totalTime("proof::bv::dratOptimization::totalTime"),
+      d_toolTime("proof::bv::dratOptimization::toolTime"),
+      d_clauseMatchingTime("proof::bv::dratOptimization::clauseMatchingTime"),
+      d_initialDratSize("proof::bv::dratOptimization::initialDratSize", 0),
+      d_optimizedDratSize("proof::bv::dratOptimization::optimizedDratSize", 0),
+      d_initialFormulaSize("proof::bv::dratOptimization::initialFormulaSize",
+                           0),
+      d_optimizedFormulaSize(
+          "proof::bv::dratOptimization::optimizedFormulaSize", 0)
+{
+  smtStatisticsRegistry()->registerStat(&d_totalTime);
+  smtStatisticsRegistry()->registerStat(&d_toolTime);
+  smtStatisticsRegistry()->registerStat(&d_clauseMatchingTime);
+  smtStatisticsRegistry()->registerStat(&d_initialDratSize);
+  smtStatisticsRegistry()->registerStat(&d_optimizedDratSize);
+  smtStatisticsRegistry()->registerStat(&d_initialFormulaSize);
+  smtStatisticsRegistry()->registerStat(&d_optimizedFormulaSize);
+}
+
+ClausalBitVectorProof::DratOptimizationStatistics::~DratOptimizationStatistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_totalTime);
+  smtStatisticsRegistry()->unregisterStat(&d_toolTime);
+  smtStatisticsRegistry()->unregisterStat(&d_clauseMatchingTime);
+  smtStatisticsRegistry()->unregisterStat(&d_initialDratSize);
+  smtStatisticsRegistry()->unregisterStat(&d_optimizedDratSize);
+  smtStatisticsRegistry()->unregisterStat(&d_initialFormulaSize);
+  smtStatisticsRegistry()->unregisterStat(&d_optimizedFormulaSize);
+}
+
 void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
                                                       std::ostream& os,
                                                       std::ostream& paren,
@@ -260,7 +352,10 @@ void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
   os << "\n;; DRAT Proof Value\n";
   os << "(@ dratProof ";
   paren << ")";
-  drat::DratProof::fromBinary(d_binaryDratProof.str()).outputAsLfsc(os, 2);
+  d_dratTranslationStatistics.d_totalTime.start();
+  drat::DratProof pf = drat::DratProof::fromBinary(d_binaryDratProof.str());
+  d_dratTranslationStatistics.d_totalTime.stop();
+  pf.outputAsLfsc(os, 2);
   os << "\n";
 
   os << "\n;; Verification of DRAT Proof\n";
@@ -283,8 +378,13 @@ void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
   os << "\n;; DRAT Proof Value\n";
   os << "(@ lratProof ";
   paren << ")";
-  lrat::LratProof pf = lrat::LratProof::fromDratProof(
-      d_clauses, d_coreClauseIndices, d_binaryDratProof.str());
+  d_dratTranslationStatistics.d_totalTime.start();
+  lrat::LratProof pf =
+      lrat::LratProof::fromDratProof(d_clauses,
+                                     d_coreClauseIndices,
+                                     d_binaryDratProof.str(),
+                                     d_dratTranslationStatistics.d_toolTime);
+  d_dratTranslationStatistics.d_totalTime.stop();
   pf.outputAsLfsc(os);
   os << "\n";
 
@@ -300,8 +400,13 @@ 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_clauses, d_coreClauseIndices, d_binaryDratProof.str());
+  d_dratTranslationStatistics.d_totalTime.start();
+  er::ErProof pf =
+      er::ErProof::fromBinaryDratProof(d_clauses,
+                                       d_coreClauseIndices,
+                                       d_binaryDratProof.str(),
+                                       d_dratTranslationStatistics.d_toolTime);
+  d_dratTranslationStatistics.d_totalTime.stop();
 
   pf.outputAsLfsc(os);
 }
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
index a410b5b38..2047e325c 100644
--- a/src/proof/clausal_bitvector_proof.h
+++ b/src/proof/clausal_bitvector_proof.h
@@ -33,6 +33,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_types.h"
 #include "theory/bv/theory_bv.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
@@ -67,10 +68,53 @@ class ClausalBitVectorProof : public BitVectorProof
   std::ostringstream d_binaryDratProof{};
   std::vector<ClauseId> d_coreClauseIndices{};
 
+  struct DratTranslationStatistics
+  {
+    DratTranslationStatistics();
+    ~DratTranslationStatistics();
+
+    // Total time spent doing translation (optimized binary DRAT -> in memory
+    // target format including IO, postprocessing, etc.)
+    TimerStat d_totalTime;
+    // Time that the external tool actually spent
+    TimerStat d_toolTime;
+  };
+
+  DratTranslationStatistics d_dratTranslationStatistics;
+
  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();
+
+  // Given reference to a SAT clause encoded as a vector of literals, puts the
+  // literals into a canonical order
+  static void canonicalizeClause(prop::SatClause& clause);
+
+  struct DratOptimizationStatistics
+  {
+    DratOptimizationStatistics();
+    ~DratOptimizationStatistics();
+
+    // Total time spent using drat-trim to optimize the DRAT proof/formula
+    // (including IO, etc.)
+    TimerStat d_totalTime;
+    // Time that drat-trim actually spent optimizing the DRAT proof/formula
+    TimerStat d_toolTime;
+    // Time that was spent matching clauses in drat-trim's output to clauses in
+    // its input
+    TimerStat d_clauseMatchingTime;
+    // Bytes in binary DRAT proof before optimization
+    IntStat d_initialDratSize;
+    // Bytes in binary DRAT proof after optimization
+    IntStat d_optimizedDratSize;
+    // Bytes in textual DIMACS bitblasted formula before optimization
+    IntStat d_initialFormulaSize;
+    // Bytes in textual DIMACS bitblasted formula after optimization
+    IntStat d_optimizedFormulaSize;
+  };
+
+  DratOptimizationStatistics d_dratOptimizationStatistics;
 };
 
 /**
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 9952e6b3e..ab07875b2 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -83,7 +83,8 @@ TraceCheckProof TraceCheckProof::fromText(std::istream& in)
 ErProof ErProof::fromBinaryDratProof(
     const std::unordered_map<ClauseId, prop::SatClause>& clauses,
     const std::vector<ClauseId>& usedIds,
-    const std::string& dratBinary)
+    const std::string& dratBinary,
+    TimerStat& toolTimer)
 {
   std::string formulaFilename("cvc4-dimacs-XXXXXX");
   std::string dratFilename("cvc4-drat-XXXXXX");
@@ -102,18 +103,21 @@ ErProof ErProof::fromBinaryDratProof(
   std::fstream tracecheckStream = openTmpFile(&tracecheckFilename);
 
   // Invoke drat2er
+  {
+    CodeTimer blockTimer{toolTimer};
 #if CVC4_USE_DRAT2ER
-  drat2er::TransformDRATToExtendedResolution(formulaFilename,
-                                             dratFilename,
-                                             tracecheckFilename,
-                                             false,
-                                             drat2er::options::QUIET,
-                                             false);
+    drat2er::TransformDRATToExtendedResolution(formulaFilename,
+                                               dratFilename,
+                                               tracecheckFilename,
+                                               false,
+                                               drat2er::options::QUIET,
+                                               false);
 #else
-  Unimplemented(
-      "ER proof production requires drat2er.\n"
-      "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+    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.
   TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream);
diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h
index d6cbd9213..9fc40e64e 100644
--- a/src/proof/er/er_proof.h
+++ b/src/proof/er/er_proof.h
@@ -32,6 +32,7 @@
 
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace proof {
@@ -118,11 +119,15 @@ class ErProof
    * @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
+   *
+   * @return the Er proof and a timer of the execution of drat2er
    */
   static ErProof fromBinaryDratProof(
       const std::unordered_map<ClauseId, prop::SatClause>& clauses,
       const std::vector<ClauseId>& usedIds,
-      const std::string& dratBinary);
+      const std::string& dratBinary,
+      TimerStat& toolTimer
+      );
 
   /**
    * Construct an ER proof from a TRACECHECK ER proof
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index d2f347807..79a92fe73 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -127,7 +127,8 @@ void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
 LratProof LratProof::fromDratProof(
     const std::unordered_map<ClauseId, prop::SatClause>& clauses,
     const std::vector<ClauseId> usedIds,
-    const std::string& dratBinary)
+    const std::string& dratBinary,
+    TimerStat& toolTimer)
 {
   std::ostringstream cmd;
   std::string formulaFilename("cvc4-dimacs-XXXXXX");
@@ -144,14 +145,17 @@ LratProof LratProof::fromDratProof(
 
   std::fstream lratStream = openTmpFile(&lratFilename);
 
+  {
+    CodeTimer blockTimer{toolTimer};
 #if CVC4_USE_DRAT2ER
-  drat2er::drat_trim::CheckAndConvertToLRAT(
-      formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET);
+    drat2er::drat_trim::CheckAndConvertToLRAT(
+        formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET);
 #else
-  Unimplemented(
-      "LRAT proof production requires drat2er.\n"
-      "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+    Unimplemented(
+        "LRAT proof production requires drat2er.\n"
+        "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
 #endif
+  }
 
   LratProof lrat(lratStream);
   remove(formulaFilename.c_str());
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index 54db1837d..f5a11fd4e 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -29,11 +29,13 @@
 #include <iosfwd>
 #include <string>
 #include <unordered_map>
+#include <utility>
 #include <vector>
 
 #include "proof/clause_id.h"
 // Included because we need operator<< for the SAT types
 #include "prop/sat_solver.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace proof {
@@ -132,11 +134,14 @@ class LratProof
    * @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.
+   *
+   * @return an LRAT proof an a timer for how long it took to run drat-trim
    */
   static LratProof fromDratProof(
       const std::unordered_map<ClauseId, prop::SatClause>& clauses,
       const std::vector<ClauseId> usedIds,
-      const std::string& dratBinary);
+      const std::string& dratBinary,
+      TimerStat& toolTimer);
   /**
    * @brief Construct an LRAT proof from its textual representation
    *
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 005a23378..f68d5937c 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -561,184 +561,243 @@ void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const
 void LFSCProof::toStream(std::ostream& out) const
 {
   TimerStat::CodeTimer proofProductionTimer(
-      *ProofManager::currentPM()->getProofProductionTime());
+      ProofManager::currentPM()->getStats().d_proofProductionTime);
 
-  Assert(!d_satProof->proofConstructed());
-  d_satProof->constructProof();
-
-  // collecting leaf clauses in resolution proof
   IdToSatClause used_lemmas;
   IdToSatClause used_inputs;
-  d_satProof->collectClausesUsed(used_inputs,
-                                 used_lemmas);
+  std::set<Node> atoms;
+  NodePairSet rewrites;
+  NodeSet used_assertions;
 
-  IdToSatClause::iterator it2;
-  Debug("pf::pm") << std::endl << "Used inputs: " << std::endl;
-  for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) {
-    Debug("pf::pm") << "\t input = " << *(it2->second) << std::endl;
-  }
-  Debug("pf::pm") << std::endl;
-
-  // Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
-  // for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) {
-  //   Debug("pf::pm") << "\t lemma = " << *(it2->second) << std::endl;
-  // }
-  // Debug("pf::pm") << std::endl;
-  Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
-  for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) {
-
-    std::vector<Expr> clause_expr;
-    for(unsigned i = 0; i < it2->second->size(); ++i) {
-      prop::SatLiteral lit = (*(it2->second))[i];
-      Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr();
-      if (atom.isConst()) {
-        Assert (atom == utils::mkTrue());
-        continue;
-      }
-      Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom;
-      clause_expr.push_back(expr_lit);
-    }
+  {
+    CodeTimer skeletonProofTimer{
+        ProofManager::currentPM()->getStats().d_skeletonProofTraceTime};
+    Assert(!d_satProof->proofConstructed());
+    d_satProof->constructProof();
 
-    Debug("pf::pm") << "\t lemma " << it2->first << " = " << *(it2->second) << std::endl;
-    Debug("pf::pm") << "\t";
-    for (unsigned i = 0; i < clause_expr.size(); ++i) {
-      Debug("pf::pm") << clause_expr[i] << " ";
+    // collecting leaf clauses in resolution proof
+    d_satProof->collectClausesUsed(used_inputs, used_lemmas);
+
+    IdToSatClause::iterator it2;
+    Debug("pf::pm") << std::endl << "Used inputs: " << std::endl;
+    for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2)
+    {
+      Debug("pf::pm") << "\t input = " << *(it2->second) << std::endl;
     }
     Debug("pf::pm") << std::endl;
-  }
-  Debug("pf::pm") << std::endl;
 
-  // collecting assertions that lead to the clauses being asserted
-  NodeSet used_assertions;
-  d_cnfProof->collectAssertionsForClauses(used_inputs, used_assertions);
-
-  NodeSet::iterator it3;
-  Debug("pf::pm") << std::endl << "Used assertions: " << std::endl;
-  for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
-    Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
+    Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
+    for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2)
+    {
+      std::vector<Expr> clause_expr;
+      for (unsigned i = 0; i < it2->second->size(); ++i)
+      {
+        prop::SatLiteral lit = (*(it2->second))[i];
+        Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr();
+        if (atom.isConst())
+        {
+          Assert(atom == utils::mkTrue());
+          continue;
+        }
+        Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
+        clause_expr.push_back(expr_lit);
+      }
 
-  std::set<Node> atoms;
+      Debug("pf::pm") << "\t lemma " << it2->first << " = " << *(it2->second)
+                      << std::endl;
+      Debug("pf::pm") << "\t";
+      for (unsigned i = 0; i < clause_expr.size(); ++i)
+      {
+        Debug("pf::pm") << clause_expr[i] << " ";
+      }
+      Debug("pf::pm") << std::endl;
+    }
+    Debug("pf::pm") << std::endl;
 
-  NodePairSet rewrites;
-  // collects the atoms in the clauses
-  d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
-
-  if (!rewrites.empty()) {
-    Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl;
-    NodePairSet::const_iterator rewriteIt;
-    for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end(); ++rewriteIt) {
-      Debug("pf::pm") << "\t" << rewriteIt->first << " --> " << rewriteIt->second << std::endl;
+    // collecting assertions that lead to the clauses being asserted
+    d_cnfProof->collectAssertionsForClauses(used_inputs, used_assertions);
+
+    NodeSet::iterator it3;
+    Debug("pf::pm") << std::endl << "Used assertions: " << std::endl;
+    for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
+      Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
+
+    // collects the atoms in the clauses
+    d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
+
+    if (!rewrites.empty())
+    {
+      Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl;
+      NodePairSet::const_iterator rewriteIt;
+      for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end();
+           ++rewriteIt)
+      {
+        Debug("pf::pm") << "\t" << rewriteIt->first << " --> "
+                        << rewriteIt->second << std::endl;
+      }
+      Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl;
+    }
+    else
+    {
+      Debug("pf::pm") << "No rewrites in lemmas found" << std::endl;
     }
-    Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl;
-  } else {
-    Debug("pf::pm") << "No rewrites in lemmas found" << std::endl;
-  }
 
-  // The derived/unrewritten atoms may not have CNF literals required later on.
-  // If they don't, add them.
-  std::set<Node>::const_iterator it;
-  for (it = atoms.begin(); it != atoms.end(); ++it) {
-    Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl;
-    if (!d_cnfProof->hasLiteral(*it)) {
-      // For arithmetic: these literals are not normalized, causing an error in Arith.
-      if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) {
-        d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver.
-      } else {
-        d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration.
+    // The derived/unrewritten atoms may not have CNF literals required later
+    // on. If they don't, add them.
+    std::set<Node>::const_iterator it;
+    for (it = atoms.begin(); it != atoms.end(); ++it)
+    {
+      Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl;
+      if (!d_cnfProof->hasLiteral(*it))
+      {
+        // For arithmetic: these literals are not normalized, causing an error
+        // in Arith.
+        if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH)
+        {
+          d_cnfProof->ensureLiteral(
+              *it,
+              true);  // This disables preregistration with the theory solver.
+        }
+        else
+        {
+          d_cnfProof->ensureLiteral(
+              *it);  // Normal method, with theory solver preregisteration.
+        }
       }
     }
-  }
 
-  d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
-  d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
+    d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
+    d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
 
-  // collects the atoms in the assertions
-  for (NodeSet::const_iterator it = used_assertions.begin();
-       it != used_assertions.end(); ++it) {
-    utils::collectAtoms(*it, atoms);
-    // utils::collectAtoms(*it, newAtoms);
-  }
+    // collects the atoms in the assertions
+    for (NodeSet::const_iterator it = used_assertions.begin();
+         it != used_assertions.end();
+         ++it)
+    {
+      utils::collectAtoms(*it, atoms);
+    }
 
-  std::set<Node>::iterator atomIt;
-  Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: "
-                  << std::endl << std::endl;
-  for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
-    Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl;
+    std::set<Node>::iterator atomIt;
+    Debug("pf::pm") << std::endl
+                    << "Dumping atoms from lemmas, inputs and assertions: "
+                    << std::endl
+                    << std::endl;
+    for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt)
+    {
+      Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl;
+    }
   }
+
   smt::SmtScope scope(d_smtEngine);
+  ProofLetMap globalLetMap;
   std::ostringstream paren;
-  out << "(check\n";
-  paren << ")";
-  out << " ;; Declarations\n";
-
-  // declare the theory atoms
-  Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl;
-  for(it = atoms.begin(); it != atoms.end(); ++it) {
-    Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
-    d_theoryProof->registerTerm((*it).toExpr());
-  }
-
-  Debug("pf::pm") << std::endl << "Term registration done!" << std::endl << std::endl;
-
-  Debug("pf::pm") << std::endl << "LFSCProof::toStream: starting to print assertions" << std::endl;
-
-  // print out all the original assertions
-  d_theoryProof->registerTermsFromAssertions();
-  d_theoryProof->printSortDeclarations(out, paren);
-  d_theoryProof->printTermDeclarations(out, paren);
-  d_theoryProof->printAssertions(out, paren);
-
-  Debug("pf::pm") << std::endl << "LFSCProof::toStream: print assertions DONE" << std::endl;
+  {
+    CodeTimer declTimer{
+        ProofManager::currentPM()->getStats().d_proofDeclarationsTime};
+    out << "(check\n";
+    paren << ")";
+    out << " ;; Declarations\n";
+
+    // declare the theory atoms
+    Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl;
+    for (std::set<Node>::const_iterator it = atoms.begin(); it != atoms.end(); ++it)
+    {
+      Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
+      d_theoryProof->registerTerm((*it).toExpr());
+    }
 
-  out << "(: (holds cln)\n\n";
-  paren << ")";
+    Debug("pf::pm") << std::endl
+                    << "Term registration done!" << std::endl
+                    << std::endl;
 
-  // Have the theory proofs print deferred declarations, e.g. for skolem variables.
-  out << " ;; Printing deferred declarations \n\n";
-  d_theoryProof->printDeferredDeclarations(out, paren);
+    Debug("pf::pm") << std::endl
+                    << "LFSCProof::toStream: starting to print assertions"
+                    << std::endl;
 
-  out << "\n ;; Printing the global let map";
-  d_theoryProof->finalizeBvConflicts(used_lemmas, out);
-  ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
-  ProofLetMap globalLetMap;
-  if (options::lfscLetification()) {
-    ProofManager::currentPM()->printGlobalLetMap(atoms, globalLetMap, out, paren);
-  }
+    // print out all the original assertions
+    d_theoryProof->registerTermsFromAssertions();
+    d_theoryProof->printSortDeclarations(out, paren);
+    d_theoryProof->printTermDeclarations(out, paren);
+    d_theoryProof->printAssertions(out, paren);
 
-  out << " ;; Printing aliasing declarations \n\n";
-  d_theoryProof->printAliasingDeclarations(out, paren, globalLetMap);
+    Debug("pf::pm") << std::endl
+                    << "LFSCProof::toStream: print assertions DONE"
+                    << std::endl;
 
-  out << " ;; Rewrites for Lemmas \n";
-  d_theoryProof->printLemmaRewrites(rewrites, out, paren);
+    out << "(: (holds cln)\n\n";
+    paren << ")";
 
-  // print trust that input assertions are their preprocessed form
-  printPreprocessedAssertions(used_assertions, out, paren, globalLetMap);
+    // Have the theory proofs print deferred declarations, e.g. for skolem
+    // variables.
+    out << " ;; Printing deferred declarations \n\n";
+    d_theoryProof->printDeferredDeclarations(out, paren);
+
+    out << "\n ;; Printing the global let map";
+    d_theoryProof->finalizeBvConflicts(used_lemmas, out);
+    ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
+    if (options::lfscLetification())
+    {
+      ProofManager::currentPM()->printGlobalLetMap(
+          atoms, globalLetMap, out, paren);
+    }
 
-  // print mapping between theory atoms and internal SAT variables
-  out << ";; Printing mapping from preprocessed assertions into atoms \n";
-  d_cnfProof->printAtomMapping(atoms, out, paren, globalLetMap);
+    out << " ;; Printing aliasing declarations \n\n";
+    d_theoryProof->printAliasingDeclarations(out, paren, globalLetMap);
 
-  Debug("pf::pm") << std::endl << "Printing cnf proof for clauses" << std::endl;
+    out << " ;; Rewrites for Lemmas \n";
+    d_theoryProof->printLemmaRewrites(rewrites, out, paren);
 
-  IdToSatClause::const_iterator cl_it = used_inputs.begin();
-  // print CNF conversion proof for each clause
-  for (; cl_it != used_inputs.end(); ++cl_it) {
-    d_cnfProof->printCnfProofForClause(cl_it->first, cl_it->second, out, paren);
+    // print trust that input assertions are their preprocessed form
+    printPreprocessedAssertions(used_assertions, out, paren, globalLetMap);
   }
 
-  Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl;
+  {
+    CodeTimer cnfProofTimer{
+        ProofManager::currentPM()->getStats().d_cnfProofTime};
+    // print mapping between theory atoms and internal SAT variables
+    out << ";; Printing mapping from preprocessed assertions into atoms \n";
+    d_cnfProof->printAtomMapping(atoms, out, paren, globalLetMap);
+
+    Debug("pf::pm") << std::endl
+                    << "Printing cnf proof for clauses" << std::endl;
+
+    IdToSatClause::const_iterator cl_it = used_inputs.begin();
+    // print CNF conversion proof for each clause
+    for (; cl_it != used_inputs.end(); ++cl_it)
+    {
+      d_cnfProof->printCnfProofForClause(
+          cl_it->first, cl_it->second, out, paren);
+    }
+  }
 
-  Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
-  d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap);
-  Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
+  {
+    CodeTimer theoryLemmaTimer{
+        ProofManager::currentPM()->getStats().d_theoryLemmaTime};
+    Debug("pf::pm") << std::endl
+                    << "Printing cnf proof for clauses DONE" << std::endl;
+
+    Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
+    d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap);
+    Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!"
+                    << std::endl;
+  }
 
-  out << ";; Printing final unsat proof \n";
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
-    ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren);
-  } else {
-    // print actual resolution proof
-    proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren);
-    proof::LFSCProofPrinter::printResolutionEmptyClause(d_satProof, out, paren);
+  {
+    CodeTimer finalProofTimer{
+        ProofManager::currentPM()->getStats().d_finalProofTime};
+    out << ";; Printing final unsat proof \n";
+    if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
+        && ProofManager::getBitVectorProof())
+    {
+      ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren);
+    }
+    else
+    {
+      // print actual resolution proof
+      proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren);
+      proof::LFSCProofPrinter::printResolutionEmptyClause(
+          d_satProof, out, paren);
+    }
   }
 
   out << paren.str();
@@ -1074,14 +1133,32 @@ void ProofManager::printTrustedTerm(Node term,
 }
 
 ProofManager::ProofManagerStatistics::ProofManagerStatistics()
-    : d_proofProductionTime("proof::ProofManager::proofProductionTime")
+    : d_proofProductionTime("proof::ProofManager::proofProductionTime"),
+      d_theoryLemmaTime(
+          "proof::ProofManager::proofProduction::theoryLemmaTime"),
+      d_skeletonProofTraceTime(
+          "proof::ProofManager::proofProduction::skeletonProofTraceTime"),
+      d_proofDeclarationsTime(
+          "proof::ProofManager::proofProduction::proofDeclarationsTime"),
+      d_cnfProofTime("proof::ProofManager::proofProduction::cnfProofTime"),
+      d_finalProofTime("proof::ProofManager::proofProduction::finalProofTime")
 {
   smtStatisticsRegistry()->registerStat(&d_proofProductionTime);
+  smtStatisticsRegistry()->registerStat(&d_theoryLemmaTime);
+  smtStatisticsRegistry()->registerStat(&d_skeletonProofTraceTime);
+  smtStatisticsRegistry()->registerStat(&d_proofDeclarationsTime);
+  smtStatisticsRegistry()->registerStat(&d_cnfProofTime);
+  smtStatisticsRegistry()->registerStat(&d_finalProofTime);
 }
 
 ProofManager::ProofManagerStatistics::~ProofManagerStatistics()
 {
   smtStatisticsRegistry()->unregisterStat(&d_proofProductionTime);
+  smtStatisticsRegistry()->unregisterStat(&d_theoryLemmaTime);
+  smtStatisticsRegistry()->unregisterStat(&d_skeletonProofTraceTime);
+  smtStatisticsRegistry()->unregisterStat(&d_proofDeclarationsTime);
+  smtStatisticsRegistry()->unregisterStat(&d_cnfProofTime);
+  smtStatisticsRegistry()->unregisterStat(&d_finalProofTime);
 }
 
 } /* CVC4  namespace */
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index eb5942bea..ec845e41d 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -298,12 +298,6 @@ public:
                          std::ostream& out,
                          std::ostringstream& paren);
 
-  TimerStat* getProofProductionTime() { return &d_stats.d_proofProductionTime; }
-
- private:
-  void constructSatProof();
-  std::set<Node> satClauseToNodeSet(prop::SatClause* clause);
-
   struct ProofManagerStatistics
   {
     ProofManagerStatistics();
@@ -314,8 +308,41 @@ public:
      * information)
      */
     TimerStat d_proofProductionTime;
+
+    /**
+     * Time spent printing proofs of theory lemmas
+     */
+    TimerStat d_theoryLemmaTime;
+
+    /**
+     * Time spent tracing the proof of the boolean skeleton
+     * (e.g. figuring out which assertions are needed, etc.)
+     */
+    TimerStat d_skeletonProofTraceTime;
+
+    /**
+     * Time spent processing and printing declarations in the proof
+     */
+    TimerStat d_proofDeclarationsTime;
+
+    /**
+     * Time spent printing the CNF proof
+     */
+    TimerStat d_cnfProofTime;
+
+    /**
+     * Time spent printing the final proof of UNSAT
+     */
+    TimerStat d_finalProofTime;
+
   }; /* struct ProofManagerStatistics */
 
+  ProofManagerStatistics& getStats() { return d_stats; }
+
+ private:
+  void constructSatProof();
+  std::set<Node> satClauseToNodeSet(prop::SatClause* clause);
+
   ProofManagerStatistics d_stats;
 
 };/* class ProofManager */
diff --git a/src/prop/sat_solver_types.cpp b/src/prop/sat_solver_types.cpp
new file mode 100644
index 000000000..078c5d54d
--- /dev/null
+++ b/src/prop/sat_solver_types.cpp
@@ -0,0 +1,28 @@
+/*********************                                                        */
+/*! \file sat_solver_types.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 Implementations of SAT solver type operations which require large
+ ** std headers.
+ **
+ **/
+
+#include "prop/sat_solver_types.h"
+
+#include <algorithm>
+
+namespace CVC4 {
+namespace prop {
+bool SatClauseLessThan::operator()(const SatClause& l, const SatClause& r) const
+{
+  return std::lexicographical_compare(l.begin(), l.end(), r.begin(), r.end());
+}
+}  // namespace prop
+}  // namespace CVC4
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index f1fd6233e..51d0c4cd5 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -121,6 +121,16 @@ public:
     return !(*this == other);
   }
 
+  /**
+   * Compare two literals
+   */
+  bool operator<(const SatLiteral& other) const
+  {
+    return getSatVariable() == other.getSatVariable()
+               ? isNegated() < other.isNegated()
+               : getSatVariable() < other.getSatVariable();
+  }
+
   /**
    * Returns a string representation of the literal.
    */
@@ -183,6 +193,11 @@ struct SatClauseSetHashFunction
   }
 };
 
+struct SatClauseLessThan
+{
+  bool operator()(const SatClause& l, const SatClause& r) const;
+};
+
 /**
  * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
  * so that the SAT solver can (or should) remove them when the lifespan is over.
@@ -221,5 +236,3 @@ enum SatSolverLifespan
 
 }
 }
-
-