Resolution proof: separate printing from proof (#1964)

Currently, we have an LFSCSatProof which inherits from TSatProof and
implements printing the proof. The seperation is not clean (e.g.
clauseName is used for printing only but is in TSatProof) and the
inheritance does not add any value while making dependencies more
confusing. The plan is that TSatProof becomes a self-contained part that
the MiniSat implementations generate and ProofManager prints out. This
commit is a first step in that direction. For SAT solvers with native
capabilities for producing proofs, we would simply implement a different
LFSC printer of their proof representation without changing the SAT
solver itself. The inheritance would make this awkward to deal with.

Additionally, the commit cleans up some unused functions and adjusts the
visibility of TSatProof methods and members.

8 files changed, 348 insertions, 233 deletions

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 0c3f0704c..8f001ffa1 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -15,11 +15,12 @@
 
 **/
 
+#include "proof/bitvector_proof.h"
 #include "options/bv_options.h"
 #include "options/proof_options.h"
 #include "proof/array_proof.h"
-#include "proof/bitvector_proof.h"
 #include "proof/clause_id.h"
+#include "proof/lfsc_proof_printer.h"
 #include "proof/proof_output_channel.h"
 #include "proof/proof_utils.h"
 #include "proof/sat_proof_implementation.h"
@@ -48,16 +49,15 @@ BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv,
 
 void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) {
   Assert (d_resolutionProof == NULL);
-  d_resolutionProof = new LFSCBVSatProof(solver, &d_fakeContext, "bb", true);
+  d_resolutionProof = new BVSatProof(solver, &d_fakeContext, "bb", true);
 }
 
 theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; }
 void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
                                   context::Context* cnf) {
+  Assert (d_resolutionProof != NULL);
   Assert (d_cnfProof == NULL);
   d_cnfProof = new LFSCCnfProof(cnfStream, cnf, "bb");
-  Assert (d_resolutionProof != NULL);
-  d_resolutionProof->setCnfProof(d_cnfProof);
 
   // true and false have to be setup in a special way
   Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
@@ -515,7 +515,8 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os
     Expr lem = utils::mkOr(lemma);
     Assert (d_bbConflictMap.find(lem) != d_bbConflictMap.end());
     ClauseId lemma_id = d_bbConflictMap[lem];
-    d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren);
+    proof::LFSCProofPrinter::printAssumptionsResolution(
+        d_resolutionProof, lemma_id, os, lemma_paren);
     os <<lemma_paren.str();
   } else {
 
@@ -615,7 +616,8 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os
         }
 
         ClauseId lemma_id = it->second;
-        d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren);
+        proof::LFSCProofPrinter::printAssumptionsResolution(
+            d_resolutionProof, lemma_id, os, lemma_paren);
         os <<lemma_paren.str();
 
         return;
@@ -1039,7 +1041,7 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
   }
 
   os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl;
-  d_resolutionProof->printResolutions(os, paren);
+  proof::LFSCProofPrinter::printResolutions(d_resolutionProof, os, paren);
 }
 
 std::string LFSCBitVectorProof::assignAlias(Expr expr) {
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 0bced2690..63f1cdf63 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -52,9 +52,6 @@ namespace CVC4 {
 template <class Solver> class TSatProof;
 typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof;
 
-template <class Solver> class LFSCSatProof;
-typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof;
-
 typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
 typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
 typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
diff --git a/src/proof/lfsc_proof_printer.cpp b/src/proof/lfsc_proof_printer.cpp
new file mode 100644
index 000000000..e1fa3acdb
--- /dev/null
+++ b/src/proof/lfsc_proof_printer.cpp
@@ -0,0 +1,176 @@
+/*********************                                                        */
+/*! \file lfsc_proof_printer.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Prints proofs in the LFSC format
+ **
+ ** Prints proofs in the LFSC format.
+ **/
+
+#include "proof/lfsc_proof_printer.h"
+
+#include <iostream>
+
+#include "prop/bvminisat/core/Solver.h"
+#include "prop/minisat/core/Solver.h"
+
+namespace CVC4 {
+namespace proof {
+
+template <class Solver>
+std::string LFSCProofPrinter::clauseName(TSatProof<Solver>* satProof,
+                                         ClauseId id)
+{
+  std::ostringstream os;
+  if (satProof->isInputClause(id))
+  {
+    os << ProofManager::getInputClauseName(id, satProof->getName());
+  }
+  else if (satProof->isLemmaClause(id))
+  {
+    os << ProofManager::getLemmaClauseName(id, satProof->getName());
+  }
+  else
+  {
+    os << ProofManager::getLearntClauseName(id, satProof->getName());
+  }
+  return os.str();
+}
+
+template <class Solver>
+void LFSCProofPrinter::printResolution(TSatProof<Solver>* satProof,
+                                       ClauseId id,
+                                       std::ostream& out,
+                                       std::ostream& paren)
+{
+  out << "(satlem_simplify _ _ _";
+  paren << ")";
+
+  const ResChain<Solver>& res = satProof->getResolutionChain(id);
+  const typename ResChain<Solver>::ResSteps& steps = res.getSteps();
+
+  for (int i = steps.size() - 1; i >= 0; i--)
+  {
+    out << " (";
+    out << (steps[i].sign ? "R" : "Q") << " _ _";
+  }
+
+  ClauseId start_id = res.getStart();
+  out << " " << clauseName(satProof, start_id);
+
+  for (unsigned i = 0; i < steps.size(); i++)
+  {
+    prop::SatVariable v =
+        prop::MinisatSatSolver::toSatVariable(var(steps[i].lit));
+    out << " " << clauseName(satProof, steps[i].id) << " "
+        << ProofManager::getVarName(v, satProof->getName()) << ")";
+  }
+
+  if (id == satProof->getEmptyClauseId())
+  {
+    out << " (\\ empty empty)";
+    return;
+  }
+
+  out << " (\\ " << clauseName(satProof, id) << "\n";  // bind to lemma name
+  paren << ")";
+}
+
+template <class Solver>
+void LFSCProofPrinter::printAssumptionsResolution(TSatProof<Solver>* satProof,
+                                                  ClauseId id,
+                                                  std::ostream& out,
+                                                  std::ostream& paren)
+{
+  Assert(satProof->isAssumptionConflict(id));
+  // print the resolution proving the assumption conflict
+  printResolution(satProof, id, out, paren);
+  // resolve out assumptions to prove empty clause
+  out << "(satlem_simplify _ _ _ ";
+  const std::vector<typename Solver::TLit>& confl =
+      *(satProof->getAssumptionConflicts().at(id));
+
+  Assert(confl.size());
+
+  for (unsigned i = 0; i < confl.size(); ++i)
+  {
+    prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]);
+    out << "(";
+    out << (lit.isNegated() ? "Q" : "R") << " _ _ ";
+  }
+
+  out << clauseName(satProof, id) << " ";
+  for (int i = confl.size() - 1; i >= 0; --i)
+  {
+    prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]);
+    prop::SatVariable v = lit.getSatVariable();
+    out << "unit" << v << " ";
+    out << ProofManager::getVarName(v, satProof->getName()) << ")";
+  }
+  out << "(\\ e e)\n";
+  paren << ")";
+}
+
+template <class Solver>
+void LFSCProofPrinter::printResolutions(TSatProof<Solver>* satProof,
+                                        std::ostream& out,
+                                        std::ostream& paren)
+{
+  Debug("bv-proof") << "; print resolutions" << std::endl;
+  std::set<ClauseId>::iterator it = satProof->getSeenLearnt().begin();
+  for (; it != satProof->getSeenLearnt().end(); ++it)
+  {
+    if (*it != satProof->getEmptyClauseId())
+    {
+      Debug("bv-proof") << "; print resolution for " << *it << std::endl;
+      printResolution(satProof, *it, out, paren);
+    }
+  }
+  Debug("bv-proof") << "; done print resolutions" << std::endl;
+}
+
+template <class Solver>
+void LFSCProofPrinter::printResolutionEmptyClause(TSatProof<Solver>* satProof,
+                                                  std::ostream& out,
+                                                  std::ostream& paren)
+{
+  printResolution(satProof, satProof->getEmptyClauseId(), out, paren);
+}
+
+// Template specializations
+template void LFSCProofPrinter::printAssumptionsResolution(
+    TSatProof<CVC4::Minisat::Solver>* satProof,
+    ClauseId id,
+    std::ostream& out,
+    std::ostream& paren);
+template void LFSCProofPrinter::printResolutions(
+    TSatProof<CVC4::Minisat::Solver>* satProof,
+    std::ostream& out,
+    std::ostream& paren);
+template void LFSCProofPrinter::printResolutionEmptyClause(
+    TSatProof<CVC4::Minisat::Solver>* satProof,
+    std::ostream& out,
+    std::ostream& paren);
+
+template void LFSCProofPrinter::printAssumptionsResolution(
+    TSatProof<CVC4::BVMinisat::Solver>* satProof,
+    ClauseId id,
+    std::ostream& out,
+    std::ostream& paren);
+template void LFSCProofPrinter::printResolutions(
+    TSatProof<CVC4::BVMinisat::Solver>* satProof,
+    std::ostream& out,
+    std::ostream& paren);
+template void LFSCProofPrinter::printResolutionEmptyClause(
+    TSatProof<CVC4::BVMinisat::Solver>* satProof,
+    std::ostream& out,
+    std::ostream& paren);
+}  // namespace proof
+}  // namespace CVC4
diff --git a/src/proof/lfsc_proof_printer.h b/src/proof/lfsc_proof_printer.h
new file mode 100644
index 000000000..bf4bfabad
--- /dev/null
+++ b/src/proof/lfsc_proof_printer.h
@@ -0,0 +1,105 @@
+/*********************                                                        */
+/*! \file lfsc_proof_printer.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Prints proofs in the LFSC format
+ **
+ ** Prints proofs in the LFSC format.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__LFSC_PROOF_PRINTER_H
+#define __CVC4__PROOF__LFSC_PROOF_PRINTER_H
+
+#include <iosfwd>
+#include <string>
+#include <vector>
+
+#include "proof/clause_id.h"
+#include "proof/proof_manager.h"
+#include "proof/sat_proof.h"
+#include "proof/sat_proof_implementation.h"
+#include "util/proof.h"
+
+namespace CVC4 {
+namespace proof {
+
+class LFSCProofPrinter
+{
+ public:
+  /**
+   * Prints the resolution proof for an assumption conflict.
+   *
+   * @param satProof The record of the reasoning done by the SAT solver
+   * @param id The clause to print a proof for
+   * @param out The stream to print to
+   * @param paren A stream for the closing parentheses
+   */
+  template <class Solver>
+  static void printAssumptionsResolution(TSatProof<Solver>* satProof,
+                                         ClauseId id,
+                                         std::ostream& out,
+                                         std::ostream& paren);
+
+  /**
+   * Prints the resolution proofs for learned clauses that have been used to
+   * deduce unsat.
+   *
+   * @param satProof The record of the reasoning done by the SAT solver
+   * @param out The stream to print to
+   * @param paren A stream for the closing parentheses
+   */
+  template <class Solver>
+  static void printResolutions(TSatProof<Solver>* satProof,
+                               std::ostream& out,
+                               std::ostream& paren);
+
+  /**
+   * Prints the resolution proof for the empty clause.
+   *
+   * @param satProof The record of the reasoning done by the SAT solver
+   * @param out The stream to print to
+   * @param paren A stream for the closing parentheses
+   */
+  template <class Solver>
+  static void printResolutionEmptyClause(TSatProof<Solver>* satProof,
+                                         std::ostream& out,
+                                         std::ostream& paren);
+
+ private:
+  /**
+   * Maps a clause id to a string identifier used in the LFSC proof.
+   *
+   * @param satProof The record of the reasoning done by the SAT solver
+   * @param id The clause to map to a string
+   */
+  template <class Solver>
+  static std::string clauseName(TSatProof<Solver>* satProof, ClauseId id);
+
+  /**
+   * Prints the resolution proof for a given clause.
+   *
+   * @param satProof The record of the reasoning done by the SAT solver
+   * @param id The clause to print a proof for
+   * @param out The stream to print to
+   * @param paren A stream for the closing parentheses
+   */
+  template <class Solver>
+  static void printResolution(TSatProof<Solver>* satProof,
+                              ClauseId id,
+                              std::ostream& out,
+                              std::ostream& paren);
+};
+
+}  // namespace proof
+}  // namespace CVC4
+
+#endif /* __CVC4__PROOF__LFSC_PROOF_PRINTER_H */
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index f2205e2ed..cc5332cfd 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -24,6 +24,7 @@
 #include "proof/bitvector_proof.h"
 #include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
+#include "proof/lfsc_proof_printer.h"
 #include "proof/proof_utils.h"
 #include "proof/sat_proof_implementation.h"
 #include "proof/theory_proof.h"
@@ -87,7 +88,7 @@ const Proof& ProofManager::getProof(SmtEngine* smt)
     Assert(currentPM()->d_format == LFSC);
     currentPM()->d_fullProof.reset(new LFSCProof(
         smt,
-        static_cast<LFSCCoreSatProof*>(getSatProof()),
+        static_cast<CoreSatProof*>(getSatProof()),
         static_cast<LFSCCnfProof*>(getCnfProof()),
         static_cast<LFSCTheoryProofEngine*>(getTheoryProofEngine())));
   }
@@ -141,18 +142,17 @@ SkolemizationManager* ProofManager::getSkolemizationManager() {
 void ProofManager::initSatProof(Minisat::Solver* solver) {
   Assert (currentPM()->d_satProof == NULL);
   Assert(currentPM()->d_format == LFSC);
-  currentPM()->d_satProof = new LFSCCoreSatProof(solver, d_context, "");
+  currentPM()->d_satProof = new CoreSatProof(solver, d_context, "");
 }
 
 void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
                                 context::Context* ctx) {
   ProofManager* pm = currentPM();
+  Assert(pm->d_satProof != NULL);
   Assert (pm->d_cnfProof == NULL);
   Assert (pm->d_format == LFSC);
   CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, "");
   pm->d_cnfProof = cnf;
-  Assert(pm-> d_satProof != NULL);
-  pm->d_satProof->setCnfProof(cnf);
 
   // true and false have to be setup in a special way
   Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
@@ -541,16 +541,14 @@ void ProofManager::setLogic(const LogicInfo& logic) {
   d_logic = logic;
 }
 
-
-
 LFSCProof::LFSCProof(SmtEngine* smtEngine,
-                     LFSCCoreSatProof* sat,
+                     CoreSatProof* sat,
                      LFSCCnfProof* cnf,
                      LFSCTheoryProofEngine* theory)
-  : d_satProof(sat)
-  , d_cnfProof(cnf)
-  , d_theoryProof(theory)
-  , d_smtEngine(smtEngine)
+    : d_satProof(sat),
+      d_cnfProof(cnf),
+      d_theoryProof(theory),
+      d_smtEngine(smtEngine)
 {}
 
 void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const
@@ -732,11 +730,12 @@ void LFSCProof::toStream(std::ostream& out) const
   Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
-    ProofManager::getBitVectorProof()->getSatProof()->printResolutionEmptyClause(out, paren);
+    proof::LFSCProofPrinter::printResolutionEmptyClause(
+        ProofManager::getBitVectorProof()->getSatProof(), out, paren);
   } else {
     // print actual resolution proof
-    d_satProof->printResolutions(out, paren);
-    d_satProof->printResolutionEmptyClause(out, paren);
+    proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren);
+    proof::LFSCProofPrinter::printResolutionEmptyClause(d_satProof, out, paren);
   }
 
   out << paren.str();
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 0defaac84..89aa66c2d 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -72,7 +72,7 @@ class ArrayProof;
 class BitVectorProof;
 
 template <class Solver> class LFSCSatProof;
-typedef LFSCSatProof< CVC4::Minisat::Solver> LFSCCoreSatProof;
+typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof;
 
 class LFSCCnfProof;
 class LFSCTheoryProofEngine;
@@ -299,7 +299,7 @@ class LFSCProof : public Proof
 {
  public:
   LFSCProof(SmtEngine* smtEngine,
-            LFSCCoreSatProof* sat,
+            CoreSatProof* sat,
             LFSCCnfProof* cnf,
             LFSCTheoryProofEngine* theory);
   ~LFSCProof() override {}
@@ -315,7 +315,7 @@ class LFSCProof : public Proof
 
   void checkUnrewrittenAssertion(const NodeSet& assertions) const;
 
-  LFSCCoreSatProof* d_satProof;
+  CoreSatProof* d_satProof;
   LFSCCnfProof* d_cnfProof;
   LFSCTheoryProofEngine* d_theoryProof;
   SmtEngine* d_smtEngine;
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 5ae078890..8fd2cb9eb 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -114,8 +114,7 @@ class TSatProof {
  public:
   TSatProof(Solver* solver, context::Context* context,
             const std::string& name, bool checkRes = false);
-  virtual ~TSatProof();
-  void setCnfProof(CnfProof* cnf_proof);
+  ~TSatProof();
 
   void startResChain(typename Solver::TLit start);
   void startResChain(typename Solver::TCRef start);
@@ -204,44 +203,34 @@ class TSatProof {
   bool derivedEmptyClause() const;
   prop::SatClause* buildClause(ClauseId id);
 
-  virtual void printResolution(ClauseId id, std::ostream& out,
-                               std::ostream& paren) = 0;
-  virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0;
-  virtual void printResolutionEmptyClause(std::ostream& out,
-                                          std::ostream& paren) = 0;
-  virtual void printAssumptionsResolution(ClauseId id, std::ostream& out,
-                                          std::ostream& paren) = 0;
-
   void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas);
 
   void storeClauseGlue(ClauseId clause, int glue);
 
- protected:
-  void print(ClauseId id) const;
-  void printRes(ClauseId id) const;
-  void printRes(const ResolutionChain& res) const;
-
   bool isInputClause(ClauseId id) const;
   bool isLemmaClause(ClauseId id) const;
   bool isAssumptionConflict(ClauseId id) const;
 
-  bool isUnit(ClauseId id) const;
-  typename Solver::TLit getUnit(ClauseId id) const;
-
-  bool isUnit(typename Solver::TLit lit) const;
-  ClauseId getUnitId(typename Solver::TLit lit) const;
-
-
-
   bool hasResolutionChain(ClauseId id) const;
 
   /** Returns the resolution chain associated with id. Assert fails if
    * hasResolution(id) does not hold. */
   const ResolutionChain& getResolutionChain(ClauseId id) const;
 
-  /** Returns a mutable pointer to the resolution chain associated with id.
-   * Assert fails if hasResolution(id) does not hold. */
-  ResolutionChain* getMutableResolutionChain(ClauseId id);
+  const std::string& getName() const { return d_name; }
+  const ClauseId& getEmptyClauseId() const { return d_emptyClauseId; }
+  const IdSet& getSeenLearnt() const { return d_seenLearnt; }
+  const IdToConflicts& getAssumptionConflicts() const
+  {
+    return d_assumptionConflictsDebug;
+  }
+
+ private:
+  bool isUnit(ClauseId id) const;
+  typename Solver::TLit getUnit(ClauseId id) const;
+
+  bool isUnit(typename Solver::TLit lit) const;
+  ClauseId getUnitId(typename Solver::TLit lit) const;
 
   void createLitSet(ClauseId id, LitSet& set);
 
@@ -263,10 +252,8 @@ class TSatProof {
 
 
   const typename Solver::TClause& getClause(typename Solver::TCRef ref) const;
-  typename Solver::TClause* getMutableClause(typename Solver::TCRef ref);
 
   void getLitVec(ClauseId id, LitVector& vec);
-  virtual void toStream(std::ostream& out);
 
   bool checkResolution(ClauseId id);
 
@@ -291,16 +278,33 @@ class TSatProof {
                   LitVector& removeStack, LitSet& inClause, LitSet& seen);
   void removeRedundantFromRes(ResChain<Solver>* res, ClauseId id);
 
-  std::string varName(typename Solver::TLit lit);
-  std::string clauseName(ClauseId id);
+  void print(ClauseId id) const;
+  void printRes(ClauseId id) const;
+  void printRes(const ResolutionChain& res) const;
+
+  std::unordered_map<ClauseId, int> d_glueMap;
+  struct Statistics {
+    IntStat d_numLearnedClauses;
+    IntStat d_numLearnedInProof;
+    IntStat d_numLemmasInProof;
+    AverageStat d_avgChainLength;
+    HistogramStat<uint64_t> d_resChainLengths;
+    HistogramStat<uint64_t> d_usedResChainLengths;
+    HistogramStat<uint64_t> d_clauseGlue;
+    HistogramStat<uint64_t> d_usedClauseGlue;
+    Statistics(const std::string& name);
+    ~Statistics();
+  };
+
+  std::string d_name;
 
-  void addToProofManager(ClauseId id, ClauseKind kind);
-  void addToCnfProof(ClauseId id);
+  const ClauseId d_emptyClauseId;
+  IdSet d_seenLearnt;
+  IdToConflicts d_assumptionConflictsDebug;
 
   // Internal data.
   Solver* d_solver;
   context::Context* d_context;
-  CnfProof* d_cnfProof;
 
   // clauses
   IdCRefMap d_idClause;
@@ -315,7 +319,6 @@ class TSatProof {
   VarSet d_assumptions;             // assumption literals for bv solver
   IdHashSet d_assumptionConflicts;  // assumption conflicts not actually added
                                     // to SAT solver
-  IdToConflicts d_assumptionConflictsDebug;
 
   // Resolutions.
 
@@ -336,7 +339,6 @@ class TSatProof {
   ResStack d_resStack;
   bool d_checkRes;
 
-  const ClauseId d_emptyClauseId;
   const ClauseId d_nullId;
 
   // temporary map for updating CRefs
@@ -349,49 +351,13 @@ class TSatProof {
   ClauseId d_trueLit;
   ClauseId d_falseLit;
 
-  std::string d_name;
-
-  IdSet d_seenLearnt;
   IdToSatClause d_seenInputs;
   IdToSatClause d_seenLemmas;
 
-   private:
-  std::unordered_map<ClauseId, int> d_glueMap;
-  struct Statistics {
-    IntStat d_numLearnedClauses;
-    IntStat d_numLearnedInProof;
-    IntStat d_numLemmasInProof;
-    AverageStat d_avgChainLength;
-    HistogramStat<uint64_t> d_resChainLengths;
-    HistogramStat<uint64_t> d_usedResChainLengths;
-    HistogramStat<uint64_t> d_clauseGlue;
-    HistogramStat<uint64_t> d_usedClauseGlue;
-    Statistics(const std::string& name);
-    ~Statistics();
-  };
-
   bool d_satProofConstructed;
   Statistics d_statistics;
 }; /* class TSatProof */
 
-template <class SatSolver>
-class LFSCSatProof : public TSatProof<SatSolver> {
- private:
- public:
-  LFSCSatProof(SatSolver* solver, context::Context* context,
-               const std::string& name, bool checkRes = false)
-    : TSatProof<SatSolver>(solver, context, name, checkRes) {}
-  void printResolution(ClauseId id,
-                       std::ostream& out,
-                       std::ostream& paren) override;
-  void printResolutions(std::ostream& out, std::ostream& paren) override;
-  void printResolutionEmptyClause(std::ostream& out,
-                                  std::ostream& paren) override;
-  void printAssumptionsResolution(ClauseId id,
-                                  std::ostream& out,
-                                  std::ostream& paren) override;
-}; /* class LFSCSatProof */
-
 template <class Solver>
 prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
 
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 82e7cb7b2..96f99be47 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -188,9 +188,12 @@ void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) {
 template <class Solver>
 TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
                              const std::string& name, bool checkRes)
-    : d_solver(solver),
+    : d_name(name),
+      d_emptyClauseId(ClauseIdEmpty),
+      d_seenLearnt(),
+      d_assumptionConflictsDebug(),
+      d_solver(solver),
       d_context(context),
-      d_cnfProof(NULL),
       d_idClause(),
       d_clauseId(),
       d_idUnit(context),
@@ -200,19 +203,15 @@ TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
       d_lemmaClauses(),
       d_assumptions(),
       d_assumptionConflicts(),
-      d_assumptionConflictsDebug(),
       d_resolutionChains(d_context),
       d_resStack(),
       d_checkRes(checkRes),
-      d_emptyClauseId(ClauseIdEmpty),
       d_nullId(-2),
       d_temp_clauseId(),
       d_temp_idClause(),
       d_unitConflictId(context),
       d_trueLit(ClauseIdUndef),
       d_falseLit(ClauseIdUndef),
-      d_name(name),
-      d_seenLearnt(),
       d_seenInputs(),
       d_seenLemmas(),
       d_satProofConstructed(false),
@@ -266,12 +265,6 @@ TSatProof<Solver>::~TSatProof() {
   }
 }
 
-template <class Solver>
-void TSatProof<Solver>::setCnfProof(CnfProof* cnf_proof) {
-  Assert(d_cnfProof == NULL);
-  d_cnfProof = cnf_proof;
-}
-
 /**
  * Returns true if the resolution chain corresponding to id
  * does resolve to the clause associated to id
@@ -448,14 +441,6 @@ TSatProof<Solver>::getResolutionChain(ClauseId id) const {
 }
 
 template <class Solver>
-typename TSatProof<Solver>::ResolutionChain*
-TSatProof<Solver>::getMutableResolutionChain(ClauseId id) {
-  Assert(hasResolutionChain(id));
-  ResolutionChain* chain = d_resolutionChains.find(id)->second;
-  return chain;
-}
-
-template <class Solver>
 bool TSatProof<Solver>::isInputClause(ClauseId id) const {
   return d_inputClauses.find(id) != d_inputClauses.end();
 }
@@ -767,15 +752,6 @@ void TSatProof<Solver>::endResChain(ClauseId id) {
   d_resStack.pop_back();
 }
 
-// template <class Solver>
-// void TSatProof<Solver>::endResChain(typename Solver::TCRef clause) {
-//   Assert(d_resStack.size() > 0);
-//   ClauseId id = registerClause(clause, LEARNT);
-//   ResChain<Solver>* res = d_resStack.back();
-//   registerResolution(id, res);
-//   d_resStack.pop_back();
-// }
-
 template <class Solver>
 void TSatProof<Solver>::endResChain(typename Solver::TLit lit) {
   Assert(d_resStack.size() > 0);
@@ -846,11 +822,6 @@ ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) {
   registerResolution(unit_id, res);
   return unit_id;
 }
-template <class Solver>
-void TSatProof<Solver>::toStream(std::ostream& out) {
-  Debug("proof:sat") << "TSatProof<Solver>::printProof\n";
-  Unimplemented("native proof printing not supported yet");
-}
 
 template <class Solver>
 ClauseId TSatProof<Solver>::storeUnitConflict(
@@ -985,21 +956,6 @@ bool TSatProof<Solver>::proofConstructed() const {
 }
 
 template <class Solver>
-std::string TSatProof<Solver>::clauseName(ClauseId id) {
-  std::ostringstream os;
-  if (isInputClause(id)) {
-    os << ProofManager::getInputClauseName(id, d_name);
-    return os.str();
-  } else if (isLemmaClause(id)) {
-    os << ProofManager::getLemmaClauseName(id, d_name);
-    return os.str();
-  } else {
-    os << ProofManager::getLearntClauseName(id, d_name);
-    return os.str();
-  }
-}
-
-template <class Solver>
 prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) {
   if (isUnit(id)) {
     typename Solver::TLit lit = getUnit(id);
@@ -1105,92 +1061,6 @@ TSatProof<Solver>::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue);
 }
 
-/// LFSCSatProof class
-template <class Solver>
-void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out,
-                                           std::ostream& paren) {
-  out << "(satlem_simplify _ _ _";
-  paren << ")";
-
-  const ResChain<Solver>& res = this->getResolutionChain(id);
-  const typename ResChain<Solver>::ResSteps& steps = res.getSteps();
-
-  for (int i = steps.size() - 1; i >= 0; i--) {
-    out << " (";
-    out << (steps[i].sign ? "R" : "Q") << " _ _";
-  }
-
-  ClauseId start_id = res.getStart();
-  out << " " << this->clauseName(start_id);
-
-  for (unsigned i = 0; i < steps.size(); i++) {
-    prop::SatVariable v =
-        prop::MinisatSatSolver::toSatVariable(var(steps[i].lit));
-    out << " " << this->clauseName(steps[i].id) << " "
-        << ProofManager::getVarName(v, this->d_name) << ")";
-  }
-
-  if (id == this->d_emptyClauseId) {
-    out <<" (\\ empty empty)";
-    return;
-  }
-
-  out << " (\\ " << this->clauseName(id) << "\n";   // bind to lemma name
-  paren << ")";
-}
-
-/// LFSCSatProof class
-template <class Solver>
-void LFSCSatProof<Solver>::printAssumptionsResolution(ClauseId id,
-                                                      std::ostream& out,
-                                                      std::ostream& paren) {
-  Assert(this->isAssumptionConflict(id));
-  // print the resolution proving the assumption conflict
-  printResolution(id, out, paren);
-  // resolve out assumptions to prove empty clause
-  out << "(satlem_simplify _ _ _ ";
-  std::vector<typename Solver::TLit>& confl =
-      *(this->d_assumptionConflictsDebug[id]);
-
-  Assert(confl.size());
-
-  for (unsigned i = 0; i < confl.size(); ++i) {
-    prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]);
-    out << "(";
-    out << (lit.isNegated() ? "Q" : "R") << " _ _ ";
-  }
-
-  out << this->clauseName(id) << " ";
-  for (int i = confl.size() - 1; i >= 0; --i) {
-    prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]);
-    prop::SatVariable v = lit.getSatVariable();
-    out << "unit" << v << " ";
-    out << ProofManager::getVarName(v, this->d_name) << ")";
-  }
-  out << "(\\ e e)\n";
-  paren << ")";
-}
-
-template <class Solver>
-void LFSCSatProof<Solver>::printResolutions(std::ostream& out,
-                                            std::ostream& paren) {
-  Debug("bv-proof") << "; print resolutions" << std::endl;
-  std::set<ClauseId>::iterator it = this->d_seenLearnt.begin();
-  for (; it != this->d_seenLearnt.end(); ++it) {
-    if (*it != this->d_emptyClauseId) {
-      Debug("bv-proof") << "; print resolution for " << *it << std::endl;
-      printResolution(*it, out, paren);
-    }
-  }
-  Debug("bv-proof") << "; done print resolutions" << std::endl;
-}
-
-template <class Solver>
-void LFSCSatProof<Solver>::printResolutionEmptyClause(std::ostream& out,
-                                                      std::ostream& paren) {
-  printResolution(this->d_emptyClauseId, out, paren);
-}
-
 inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) {
   switch (k) {
     case CVC4::INPUT: