ClausalBitvectorProof (#2786)

* [DRAT] ClausalBitvectorProof

Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)

It fits into the `BitvectorProof` class hierarchy like this:

```
              BitvectorProof
              /            \
             /              \
ClausalBitvectorProof  ResolutionBitvectorProof
```

This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
   * CnfStream
   * SatSolver (specifically the BvSatSolver)
   * CnfProof
   * TheoryProof
   * TheoryBV
   * Both bitblasters

And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.

This means that references to and interactions with (R)BVP were
pervasive.

Nevertheless, an SMT developer must persist.

The change summary:
  * Create a subclass of BVP, called ClausalBitvectorProof, which has
    most methods stubbed out.
  * Make a some modifications to BVP and ResolutionBitvectorProof as the
    natural division of labor between the different classes becomes
    clear.
  * Go through all the components in the first list and try to figure
    out which kind of BVP they should **actually** be interacting with,
    and how. Make tweaks accordingly.
  * Add a hook from CryptoMinisat which pipes the produced DRAT proof
    into the new ClausalBitvectorProof.
  * Add a debug statement to ClausalBitvectorProof which parses and
    prints that DRAT proof, for testing purposes.

Test:
  * `make check` to verify that we didn't break any old stuff, including
    lazy BB, and eager BB when using bvminisat.
  * `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
  -d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
     1. It crashed with "Unimplemented"
     2. Right before that it prints out the (textual) DRAT proof.

* Remove 2 unneeded methods

* Missed a rename

* Typos

Thanks Andres!

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

* Address Andres comments

* Reorder members of TBitblaster

28 files changed, 510 insertions, 151 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 502db63f4..d9fc80a92 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -130,6 +130,8 @@ libcvc4_add_sources(
   proof/array_proof.h
   proof/bitvector_proof.cpp
   proof/bitvector_proof.h
+  proof/clausal_bitvector_proof.cpp
+  proof/clausal_bitvector_proof.h
   proof/clause_id.h
   proof/cnf_proof.cpp
   proof/cnf_proof.h
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index ba3533cc3..90c0c9b30 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -18,10 +18,13 @@
 #include "options/proof_options.h"
 #include "proof/proof_output_channel.h"
 #include "proof/theory_proof.h"
+#include "prop/sat_solver_types.h"
 #include "theory/bv/bitblast/bitblaster.h"
 #include "theory/bv/theory_bv.h"
 
 namespace CVC4 {
+
+namespace proof {
 BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv,
                                TheoryProofEngine* proofEngine)
     : TheoryProof(bv, proofEngine),
@@ -118,13 +121,6 @@ std::string BitVectorProof::getBBTermName(Expr expr)
   return os.str();
 }
 
-void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
-                                  context::Context* cnf)
-{
-  Assert(d_cnfProof == nullptr);
-  d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb"));
-}
-
 void BitVectorProof::printOwnedTerm(Expr term,
                                     std::ostream& os,
                                     const ProofLetMap& map)
@@ -709,6 +705,8 @@ void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
   }
 }
 
+theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; }
+
 const std::set<Node>* BitVectorProof::getAtomsInBitblastingProof()
 {
   return &d_atomsInBitblastingProof;
@@ -774,4 +772,6 @@ void BitVectorProof::printRewriteProof(std::ostream& os,
   os << ")";
 }
 
+}  // namespace proof
+
 }  // namespace CVC4
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 466efa6a7..4b897a6c6 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -24,14 +24,28 @@
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
+
 #include "expr/expr.h"
 #include "proof/cnf_proof.h"
 #include "proof/theory_proof.h"
-#include "theory/bv/bitblast/bitblaster.h"
+#include "prop/sat_solver.h"
 #include "theory/bv/theory_bv.h"
 
+// Since TBitblaster and BitVectorProof are cyclically dependent, we need this
+// forward declaration
+namespace CVC4 {
+namespace theory {
+namespace bv {
+template <class T>
+class TBitblaster;
+}
+}  // namespace theory
+}  // namespace CVC4
+
 namespace CVC4 {
 
+namespace proof {
+
 typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
 typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
 typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
@@ -118,6 +132,8 @@ class BitVectorProof : public TheoryProof
    */
   std::unique_ptr<CnfProof> d_cnfProof;
 
+  theory::TheoryId getTheoryId() override;
+
  public:
   void printOwnedTerm(Expr term,
                       std::ostream& os,
@@ -132,6 +148,28 @@ class BitVectorProof : public TheoryProof
   virtual void calculateAtomsInBitblastingProof() = 0;
 
   /**
+   * Prints out a declaration of the bit-blasting, and the subsequent
+   * conversion of the result to CNF
+   *
+   * @param os the stream to print to
+   * @param paren a stream that will be placed at the back of the proof (for
+   *              closing parens)
+   * @param letMap The let-map, which contains information about LFSC
+   *               identifiers and the values they reference.
+   */
+  virtual void printBBDeclarationAndCnf(std::ostream& os,
+                                        std::ostream& paren,
+                                        ProofLetMap& letMap) = 0;
+
+  /**
+   * Prints a proof of the empty clause.
+   *
+   * @param os the stream to print to
+   * @param paren any parentheses to add to the end of the global proof
+   */
+  virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren) = 0;
+
+  /**
    * Read the d_atomsInBitblastingProof member.
    * See its documentation.
    */
@@ -153,13 +191,41 @@ class BitVectorProof : public TheoryProof
   /**
    * This must be done before registering any terms or atoms, since the CNF
    * proof must reflect the result of bitblasting those
+   *
+   * Feeds the SAT solver's true and false variables into the CNF stream.
    */
-  virtual void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx);
+  virtual void initCnfProof(prop::CnfStream* cnfStream,
+                            context::Context* cnf,
+                            prop::SatVariable trueVar,
+                            prop::SatVariable falseVar) = 0;
 
   CnfProof* getCnfProof() { return d_cnfProof.get(); }
 
+  /**
+   * Attaches this BVP to the given SAT solver, initializing a SAT proof.
+   *
+   * This must be invoked before `initCnfProof` because a SAT proof must already
+   * exist to initialize a CNF proof.
+   */
+  virtual void attachToSatSolver(prop::SatSolver& sat_solver) = 0;
+
   void setBitblaster(theory::bv::TBitblaster<Node>* bb);
 
+  /**
+   * Kind of a mess. Used for resulution-based BVP's, where in eager mode this
+   * must be invoked before printing a proof of the empty clause. In lazy mode
+   * the behavior and purpose are both highly unclear.
+   *
+   * This exists as a virtual method of BitVectorProof, and not
+   * ResolutionBitVectorProof, because the machinery that invokes it is
+   * high-level enough that it doesn't know the difference between clausal and
+   * resolution proofs.
+   *
+   * TODO(aozdemir) figure out what is going on and clean this up
+   * Issue: https://github.com/CVC4/CVC4/issues/2789
+   */
+  virtual void finalizeConflicts(std::vector<Expr>& conflicts){};
+
  private:
   ExprToString d_exprToVariableName;
 
@@ -206,6 +272,8 @@ class BitVectorProof : public TheoryProof
                          const Node& n2) override;
 };
 
+}  // namespace proof
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__BITVECTOR__PROOF_H */
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
new file mode 100644
index 000000000..bb875d1d8
--- /dev/null
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -0,0 +1,115 @@
+/*********************                                                        */
+/*! \file clausal_bitvector_proof.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Bitvector proof using the DRAT proof format
+ **
+ ** Contains DRAT-specific printing logic.
+ **/
+
+#include "cvc4_private.h"
+
+#include <algorithm>
+#include <iterator>
+#include <set>
+#include "options/bv_options.h"
+#include "proof/clausal_bitvector_proof.h"
+#include "proof/drat/drat_proof.h"
+#include "proof/lfsc_proof_printer.h"
+#include "theory/bv/theory_bv.h"
+
+namespace CVC4 {
+
+namespace proof {
+
+ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv,
+                                             TheoryProofEngine* proofEngine)
+    : BitVectorProof(bv, proofEngine), d_usedClauses(), d_binaryDratProof()
+{
+}
+
+void ClausalBitVectorProof::attachToSatSolver(prop::SatSolver& sat_solver)
+{
+  sat_solver.setClausalProofLog(this);
+}
+
+void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
+                                         context::Context* cnf,
+                                         prop::SatVariable trueVar,
+                                         prop::SatVariable falseVar)
+{
+  Assert(d_cnfProof == nullptr);
+  d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb"));
+
+  // Create a clause which forces the true variable to be true, and register it
+  int trueClauseId = ClauseId(ProofManager::currentPM()->nextId());
+  // with the CNF proof
+  d_cnfProof->registerTrueUnitClause(trueClauseId);
+  // and with (this) bit-vector proof
+  prop::SatClause c{prop::SatLiteral(trueVar, false)};
+  registerUsedClause(trueClauseId, c);
+
+  // The same for false.
+  int falseClauseId = ClauseId(ProofManager::currentPM()->nextId());
+  d_cnfProof->registerFalseUnitClause(falseClauseId);
+  c[0] = prop::SatLiteral(falseVar, true);
+  registerUsedClause(falseClauseId, c);
+}
+
+void ClausalBitVectorProof::registerUsedClause(ClauseId id,
+                                               prop::SatClause& clause)
+{
+  d_usedClauses.emplace_back(
+      id, std::unique_ptr<prop::SatClause>(new prop::SatClause(clause)));
+};
+
+void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
+{
+  if (Debug.isOn("bv::clausal"))
+  {
+    std::string serializedDratProof = d_binaryDratProof.str();
+    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"));
+  }
+  Unimplemented();
+}
+
+void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
+                                                      std::ostream& os,
+                                                      std::ostream& paren,
+                                                      const ProofLetMap& map)
+{
+  Unreachable(
+      "Clausal bit-vector proofs should only be used in combination with eager "
+      "bitblasting, which **does not use theory lemmas**");
+}
+
+void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
+                                                         std::ostream& paren,
+                                                         ProofLetMap& letMap)
+{
+  Unimplemented();
+}
+
+void LfscClausalBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                      std::ostream& paren)
+{
+  Unimplemented();
+}
+
+}  // namespace proof
+
+};  // namespace CVC4
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
new file mode 100644
index 000000000..85e409e0d
--- /dev/null
+++ b/src/proof/clausal_bitvector_proof.h
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \file clausal_bitvector_proof.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Bitvector proof for clausal (DRAT/LRAT) formats
+ **
+ ** An internal string stream is hooked up to CryptoMiniSat, which spits out a
+ ** binary DRAT proof. Depending on which kind of proof we're going to turn
+ ** that into, we process it in different ways.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+#define __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+
+#include <iostream>
+#include <sstream>
+#include <unordered_map>
+
+#include "expr/expr.h"
+#include "proof/bitvector_proof.h"
+#include "proof/drat/drat_proof.h"
+#include "proof/lrat/lrat_proof.h"
+#include "proof/theory_proof.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver_types.h"
+#include "theory/bv/theory_bv.h"
+
+namespace CVC4 {
+
+namespace proof {
+
+class ClausalBitVectorProof : public BitVectorProof
+{
+ public:
+  ClausalBitVectorProof(theory::bv::TheoryBV* bv,
+                        TheoryProofEngine* proofEngine);
+
+  ~ClausalBitVectorProof() = default;
+
+  void attachToSatSolver(prop::SatSolver& sat_solver) override;
+
+  void initCnfProof(prop::CnfStream* cnfStream,
+                    context::Context* cnf,
+                    prop::SatVariable trueVar,
+                    prop::SatVariable falseVar) override;
+
+  std::ostream& getDratOstream() { return d_binaryDratProof; }
+
+  void registerUsedClause(ClauseId id, prop::SatClause& clause);
+
+  void calculateAtomsInBitblastingProof() override;
+
+ protected:
+  // A list of all clauses and their ids which are passed into the SAT solver
+  std::vector<std::pair<ClauseId, std::unique_ptr<prop::SatClause>>>
+      d_usedClauses;
+  // Stores the proof recieved from the SAT solver.
+  std::ostringstream d_binaryDratProof;
+};
+
+/**
+ * A representation of a clausal proof of a bitvector problem's UNSAT nature
+ */
+class LfscClausalBitVectorProof : public ClausalBitVectorProof
+{
+ public:
+  LfscClausalBitVectorProof(theory::bv::TheoryBV* bv,
+                            TheoryProofEngine* proofEngine)
+      : ClausalBitVectorProof(bv, proofEngine)
+  {
+    // That's all!
+  }
+
+  void printTheoryLemmaProof(std::vector<Expr>& lemma,
+                             std::ostream& os,
+                             std::ostream& paren,
+                             const ProofLetMap& map) override;
+  void printBBDeclarationAndCnf(std::ostream& os,
+                                std::ostream& paren,
+                                ProofLetMap& letMap) override;
+  void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
+};
+
+}  // namespace proof
+
+}  // namespace CVC4
+
+#endif /* __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 016198735..4e8d20162 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -105,6 +105,30 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) {
   setClauseDefinition(clause, current_expr);
 }
 
+void CnfProof::registerTrueUnitClause(ClauseId clauseId)
+{
+  Node trueNode = NodeManager::currentNM()->mkConst<bool>(true);
+  pushCurrentAssertion(trueNode);
+  pushCurrentDefinition(trueNode);
+  registerConvertedClause(clauseId);
+  popCurrentAssertion();
+  popCurrentDefinition();
+  d_cnfStream->ensureLiteral(trueNode);
+  d_trueUnitClause = clauseId;
+}
+
+void CnfProof::registerFalseUnitClause(ClauseId clauseId)
+{
+  Node falseNode = NodeManager::currentNM()->mkConst<bool>(false).notNode();
+  pushCurrentAssertion(falseNode);
+  pushCurrentDefinition(falseNode);
+  registerConvertedClause(clauseId);
+  popCurrentAssertion();
+  popCurrentDefinition();
+  d_cnfStream->ensureLiteral(falseNode);
+  d_falseUnitClause = clauseId;
+}
+
 void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
   Debug("proof:cnf") << "CnfProof::setClauseAssertion "
                      << clause << " assertion " << expr << std::endl;
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 32833d9a1..78ddeebd0 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -78,6 +78,11 @@ protected:
 
   ClauseIdSet d_explanations;
 
+  // The clause ID of the unit clause defining the true SAT literal.
+  ClauseId d_trueUnitClause;
+  // The clause ID of the unit clause defining the false SAT literal.
+  ClauseId d_falseUnitClause;
+
   bool isDefinition(Node node);
 
   Node getDefinitionForClause(ClauseId clause);
@@ -110,6 +115,14 @@ public:
   // already in CNF
   void registerConvertedClause(ClauseId clause, bool explanation=false);
 
+  // The CNF proof has a special relationship to true and false.
+  // In particular, it need to know the identity of clauses defining
+  // canonical true and false literals in the underlying SAT solver.
+  void registerTrueUnitClause(ClauseId clauseId);
+  void registerFalseUnitClause(ClauseId clauseId);
+  inline ClauseId getTrueUnitClause() { return d_trueUnitClause; };
+  inline ClauseId getFalseUnitClause() { return d_falseUnitClause; };
+
   /** Clause is one of the clauses defining the node expression*/
   void setClauseDefinition(ClauseId clause, Node node);
 
diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp
index 667d630f8..1db673949 100644
--- a/src/proof/resolution_bitvector_proof.cpp
+++ b/src/proof/resolution_bitvector_proof.cpp
@@ -26,6 +26,7 @@
 #include "proof/proof_utils.h"
 #include "proof/sat_proof_implementation.h"
 #include "prop/bvminisat/bvminisat.h"
+#include "prop/sat_solver_types.h"
 #include "theory/bv/bitblast/bitblaster.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
@@ -54,32 +55,22 @@ void ResolutionBitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver)
   d_resolutionProof.reset(new BVSatProof(solver, &d_fakeContext, "bb", true));
 }
 
-theory::TheoryId ResolutionBitVectorProof::getTheoryId()
+void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
+                                            context::Context* cnf,
+                                            prop::SatVariable trueVar,
+                                            prop::SatVariable falseVar)
 {
-  return theory::THEORY_BV;
+  Assert(d_resolutionProof != NULL);
+  Assert(d_cnfProof == nullptr);
+  d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb"));
+
+  d_cnfProof->registerTrueUnitClause(d_resolutionProof->getTrueUnit());
+  d_cnfProof->registerFalseUnitClause(d_resolutionProof->getFalseUnit());
 }
 
-void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
-                                            context::Context* cnf)
+void ResolutionBitVectorProof::attachToSatSolver(prop::SatSolver& sat_solver)
 {
-  Assert(d_resolutionProof != NULL);
-  BitVectorProof::initCnfProof(cnfStream, cnf);
-
-  // true and false have to be setup in a special way
-  Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
-  Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode();
-
-  d_cnfProof->pushCurrentAssertion(true_node);
-  d_cnfProof->pushCurrentDefinition(true_node);
-  d_cnfProof->registerConvertedClause(d_resolutionProof->getTrueUnit());
-  d_cnfProof->popCurrentAssertion();
-  d_cnfProof->popCurrentDefinition();
-
-  d_cnfProof->pushCurrentAssertion(false_node);
-  d_cnfProof->pushCurrentDefinition(false_node);
-  d_cnfProof->registerConvertedClause(d_resolutionProof->getFalseUnit());
-  d_cnfProof->popCurrentAssertion();
-  d_cnfProof->popCurrentDefinition();
+  sat_solver.setResolutionProofLog(this);
 }
 
 BVSatProof* ResolutionBitVectorProof::getSatProof()
@@ -258,13 +249,15 @@ void ResolutionBitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts)
   }
 }
 
-void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
-                                               std::ostream& os,
-                                               std::ostream& paren,
-                                               const ProofLetMap& map)
+void LfscResolutionBitVectorProof::printTheoryLemmaProof(
+    std::vector<Expr>& lemma,
+    std::ostream& os,
+    std::ostream& paren,
+    const ProofLetMap& map)
 {
-  Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called"
-                  << std::endl;
+  Debug("pf::bv")
+      << "(pf::bv) LfscResolutionBitVectorProof::printTheoryLemmaProof called"
+      << std::endl;
   Expr conflict = utils::mkSortedExpr(kind::OR, lemma);
   Debug("pf::bv") << "\tconflict = " << conflict << std::endl;
 
@@ -467,7 +460,7 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
   }
 }
 
-void LFSCBitVectorProof::calculateAtomsInBitblastingProof()
+void LfscResolutionBitVectorProof::calculateAtomsInBitblastingProof()
 {
   // Collect the input clauses used
   IdToSatClause used_lemmas;
@@ -477,9 +470,9 @@ void LFSCBitVectorProof::calculateAtomsInBitblastingProof()
   Assert(used_lemmas.empty());
 }
 
-void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
-                                              std::ostream& paren,
-                                              ProofLetMap& letMap)
+void LfscResolutionBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
+                                                            std::ostream& paren,
+                                                            ProofLetMap& letMap)
 {
   // print mapping between theory atoms and internal SAT variables
   os << std::endl << ";; BB atom mapping\n" << std::endl;
@@ -517,6 +510,16 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
   proof::LFSCProofPrinter::printResolutions(d_resolutionProof.get(), os, paren);
 }
 
-} /* namespace proof */
+void LfscResolutionBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                         std::ostream& paren)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+  proof::LFSCProofPrinter::printResolutionEmptyClause(
+      d_resolutionProof.get(), os, paren);
+}
+
+}  // namespace proof
 
 } /* namespace CVC4 */
diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h
index ccb288f6e..6c2ae589f 100644
--- a/src/proof/resolution_bitvector_proof.h
+++ b/src/proof/resolution_bitvector_proof.h
@@ -24,32 +24,16 @@
 #include "context/context.h"
 #include "expr/expr.h"
 #include "proof/bitvector_proof.h"
+#include "proof/sat_proof.h"
 #include "proof/theory_proof.h"
 #include "prop/bvminisat/core/Solver.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver_types.h"
+#include "theory/bv/bitblast/bitblaster.h"
+#include "theory/bv/theory_bv.h"
 
 namespace CVC4 {
 
-namespace theory {
-namespace bv {
-class TheoryBV;
-template <class T>
-class TBitblaster;
-}  // namespace bv
-}  // namespace theory
-
-// TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream
-// header cycle and remove this.
-namespace prop {
-class CnfStream;
-}
-
-} /* namespace CVC4 */
-
-
-namespace CVC4 {
-
-template <class Solver>
-class TSatProof;
 typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof;
 
 namespace proof {
@@ -76,13 +60,7 @@ class ResolutionBitVectorProof : public BitVectorProof
 
   BVSatProof* getSatProof();
 
-  /**
-   * Kind of a mess.
-   * In eager mode this must be invoked before printing a proof of the empty
-   * clause. In lazy mode the behavior is ???
-   * TODO(aozdemir) clean this up.
-   */
-  void finalizeConflicts(std::vector<Expr>& conflicts);
+  void finalizeConflicts(std::vector<Expr>& conflicts) override;
 
   void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
   void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
@@ -91,13 +69,14 @@ class ResolutionBitVectorProof : public BitVectorProof
   void markAssumptionConflict() { d_isAssumptionConflict = true; }
   bool isAssumptionConflict() const { return d_isAssumptionConflict; }
 
-  virtual void printResolutionProof(std::ostream& os,
-                                    std::ostream& paren,
-                                    ProofLetMap& letMap) = 0;
-
-  void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override;
+  void initCnfProof(prop::CnfStream* cnfStream,
+                    context::Context* cnf,
+                    prop::SatVariable trueVar,
+                    prop::SatVariable falseVar) override;
 
  protected:
+  void attachToSatSolver(prop::SatSolver& sat_solver) override;
+
   context::Context d_fakeContext;
 
   // The CNF formula that results from bit-blasting will need a proof.
@@ -106,13 +85,13 @@ class ResolutionBitVectorProof : public BitVectorProof
 
   bool d_isAssumptionConflict;
 
-  theory::TheoryId getTheoryId() override;
 };
 
-class LFSCBitVectorProof : public ResolutionBitVectorProof
+class LfscResolutionBitVectorProof : public ResolutionBitVectorProof
 {
  public:
-  LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
+  LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv,
+                               TheoryProofEngine* proofEngine)
       : ResolutionBitVectorProof(bv, proofEngine)
   {
   }
@@ -120,9 +99,10 @@ class LFSCBitVectorProof : public ResolutionBitVectorProof
                              std::ostream& os,
                              std::ostream& paren,
                              const ProofLetMap& map) override;
-  void printResolutionProof(std::ostream& os,
-                            std::ostream& paren,
-                            ProofLetMap& letMap) override;
+  void printBBDeclarationAndCnf(std::ostream& os,
+                                std::ostream& paren,
+                                ProofLetMap& letMap) override;
+  void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
   void calculateAtomsInBitblastingProof() override;
 };
 
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index ee06fbfa0..fe9acfef3 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -22,6 +22,7 @@
 #include "options/proof_options.h"
 #include "proof/arith_proof.h"
 #include "proof/array_proof.h"
+#include "proof/clausal_bitvector_proof.h"
 #include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
 #include "proof/proof_manager.h"
@@ -46,7 +47,7 @@
 
 namespace CVC4 {
 
-using proof::LFSCBitVectorProof;
+using proof::LfscResolutionBitVectorProof;
 using proof::ResolutionBitVectorProof;
 
 unsigned CVC4::ProofLetCount::counter = 0;
@@ -80,9 +81,20 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
       }
 
       if (id == theory::THEORY_BV) {
-        auto bv_theory = static_cast<theory::bv::TheoryBV*>(th);
-        ResolutionBitVectorProof* bvp = new LFSCBitVectorProof(bv_theory, this);
-        d_theoryProofTable[id] = bvp;
+        auto thBv = static_cast<theory::bv::TheoryBV*>(th);
+        if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
+            && options::bvSatSolver() == theory::bv::SAT_SOLVER_CRYPTOMINISAT)
+        {
+          proof::BitVectorProof* bvp =
+              new proof::LfscClausalBitVectorProof(thBv, this);
+          d_theoryProofTable[id] = bvp;
+        }
+        else
+        {
+          proof::BitVectorProof* bvp =
+              new proof::LfscResolutionBitVectorProof(thBv, this);
+          d_theoryProofTable[id] = bvp;
+        }
         return;
       }
 
@@ -105,10 +117,11 @@ void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) {
   if (th) {
     theory::TheoryId id = th->getId();
     if (id == theory::THEORY_BV) {
+      theory::bv::TheoryBV* bv_th = static_cast<theory::bv::TheoryBV*>(th);
       Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end());
-      ResolutionBitVectorProof* bvp =
-          (ResolutionBitVectorProof*)d_theoryProofTable[id];
-      ((theory::bv::TheoryBV*)th)->setResolutionProofLog(bvp);
+      proof::BitVectorProof* bvp =
+          static_cast<proof::BitVectorProof*>(d_theoryProofTable[id]);
+      bv_th->setProofLog(bvp);
       return;
     }
   }
@@ -533,9 +546,8 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std
     }
   }
 
-  ResolutionBitVectorProof* bv = ProofManager::getBitVectorProof();
+  proof::BitVectorProof* bv = ProofManager::getBitVectorProof();
   bv->finalizeConflicts(bv_lemmas);
-  //  bv->printResolutionProof(os, paren, letMap);
 }
 
 void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
@@ -550,7 +562,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
   }
 
   //  finalizeBvConflicts(lemmas, os, paren, map);
-  ProofManager::getBitVectorProof()->printResolutionProof(os, paren, map);
+  ProofManager::getBitVectorProof()->printBBDeclarationAndCnf(os, paren, map);
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     Assert (lemmas.size() == 1);
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 55710092b..57ef8ef30 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -104,7 +104,8 @@ void BVMinisatSatSolver::popAssumption() {
   d_minisat->popAssumption();
 }
 
-void BVMinisatSatSolver::setProofLog(proof::ResolutionBitVectorProof* bvp)
+void BVMinisatSatSolver::setResolutionProofLog(
+    proof::ResolutionBitVectorProof* bvp)
 {
   d_minisat->setProofLog( bvp );
 }
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 16489b172..efb90a3f0 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -119,7 +119,7 @@ public:
 
   void popAssumption() override;
 
-  void setProofLog(proof::ResolutionBitVectorProof* bvp) override;
+  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) override;
 
  private:
   /* Disable the default constructor. */
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index cdb850ce2..84c315547 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -79,19 +79,22 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
     }
   }
 
-  PROOF(if (d_cnfProof) d_cnfProof->pushCurrentDefinition(node););
+  if (PROOF_ON() && d_cnfProof)
+  {
+    d_cnfProof->pushCurrentDefinition(node);
+  }
 
   ClauseId clause_id = d_satSolver->addClause(c, d_removable);
   if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added)
 
-  PROOF
-    (
-     if (d_cnfProof) {
-       Assert (clause_id != ClauseIdError);
-       d_cnfProof->registerConvertedClause(clause_id);
-       d_cnfProof->popCurrentDefinition();
-     }
-    );
+  if (PROOF_ON() && d_cnfProof)
+  {
+    if (clause_id != ClauseIdError)
+    {
+      d_cnfProof->registerConvertedClause(clause_id);
+    }
+    d_cnfProof->popCurrentDefinition();
+  };
 }
 
 void CnfStream::assertClause(TNode node, SatLiteral a) {
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index df5a20791..c04fb8b56 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -62,10 +62,11 @@ void toInternalClause(SatClause& clause,
 
 CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
                                          const std::string& name)
-: d_solver(new CMSat::SATSolver())
-, d_numVariables(0)
-, d_okay(true)
-, d_statistics(registry, name)
+    : d_solver(new CMSat::SATSolver()),
+      d_bvp(nullptr),
+      d_numVariables(0),
+      d_okay(true),
+      d_statistics(registry, name)
 {
   d_true = newVar();
   d_false = newVar();
@@ -117,9 +118,17 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
   
   std::vector<CMSat::Lit> internal_clause;
   toInternalClause(clause, internal_clause);
-  bool res = d_solver->add_clause(internal_clause);
-  d_okay &= res;
-  return ClauseIdError;
+  bool nowOkay = d_solver->add_clause(internal_clause);
+  ClauseId freshId = ClauseId(ProofManager::currentPM()->nextId());
+
+  THEORY_PROOF(
+      // If this clause results in a conflict, then `nowOkay` may be false, but
+      // we still need to register this clause as used. Thus, we look at
+      // `d_okay` instead
+      if (d_bvp && d_okay) { d_bvp->registerUsedClause(freshId, clause); })
+
+  d_okay &= nowOkay;
+  return freshId;
 }
 
 bool CryptoMinisatSolver::ok() const {
@@ -193,6 +202,12 @@ unsigned CryptoMinisatSolver::getAssertionLevel() const {
   return -1; 
 }
 
+void CryptoMinisatSolver::setClausalProofLog(proof::ClausalBitVectorProof* bvp)
+{
+  d_bvp = bvp;
+  d_solver->set_drat(&bvp->getDratOstream(), false);
+}
+
 // Satistics for CryptoMinisatSolver
 
 CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index c5345cb86..17cc1568c 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -21,6 +21,7 @@
 
 #ifdef CVC4_USE_CRYPTOMINISAT
 
+#include "proof/clausal_bitvector_proof.h"
 #include "prop/sat_solver.h"
 
 // Cryptominisat has name clashes with the other Minisat implementations since
@@ -39,6 +40,7 @@ class CryptoMinisatSolver : public SatSolver {
 
 private:
   std::unique_ptr<CMSat::SATSolver> d_solver;
+  proof::ClausalBitVectorProof* d_bvp;
   unsigned d_numVariables;
   bool d_okay;
   SatVariable d_true;
@@ -71,6 +73,7 @@ public:
   SatValue modelValue(SatLiteral l) override;
 
   unsigned getAssertionLevel() const override;
+  void setClausalProofLog(proof::ClausalBitVectorProof* bvp) override;
 
   class Statistics {
   public:
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 49064c20f..70e46eceb 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -26,7 +26,6 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "proof/resolution_bitvector_proof.h"
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
 #include "prop/bv_sat_solver_notify.h"
@@ -34,6 +33,11 @@
 
 namespace CVC4 {
 
+namespace proof {
+class ClausalBitVectorProof;
+class ResolutionBitVectorProof;
+}  // namespace proof
+
 namespace prop {
 
 class TheoryProxy;
@@ -97,7 +101,9 @@ public:
   /** Check if the solver is in an inconsistent state */
   virtual bool ok() const = 0;
 
-  virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {}
+  virtual void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) {}
+
+  virtual void setClausalProofLog(proof::ClausalBitVectorProof* drat_proof) {}
 
 };/* class SatSolver */
 
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 73b4d19c7..b1fc084ed 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -24,6 +24,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "proof/bitvector_proof.h"
 #include "prop/bv_sat_solver_notify.h"
 #include "prop/sat_solver_types.h"
 #include "theory/bv/bitblast/bitblast_strategies_template.h"
@@ -31,6 +32,7 @@
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
 
+
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -59,6 +61,10 @@ class TBitblaster
   // caches and mappings
   TermDefMap d_termCache;
   ModelCache d_modelCache;
+  // sat solver used for bitblasting and associated CnfStream
+  std::unique_ptr<context::Context> d_nullContext;
+  std::unique_ptr<prop::CnfStream> d_cnfStream;
+  proof::BitVectorProof* d_bvp;
 
   void initAtomBBStrategies();
   void initTermBBStrategies();
@@ -69,6 +75,8 @@ class TBitblaster
   TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
   AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
   virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
+  virtual prop::SatSolver* getSatSolver() = 0;
+
 
  public:
   TBitblaster();
@@ -83,6 +91,8 @@ class TBitblaster
   bool hasBBTerm(TNode node) const;
   void getBBTerm(TNode node, Bits& bits) const;
   virtual void storeBBTerm(TNode term, const Bits& bits);
+  void setProofLog(proof::BitVectorProof* bvp);
+
   /**
    * Return a constant representing the value of a in the  model.
    * If fullModel is true set unconstrained bits to 0. If not return
@@ -171,7 +181,12 @@ void TBitblaster<T>::initTermBBStrategies()
 }
 
 template <class T>
-TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache()
+TBitblaster<T>::TBitblaster()
+    : d_termCache(),
+      d_modelCache(),
+      d_nullContext(new context::Context()),
+      d_cnfStream(),
+      d_bvp(nullptr)
 {
   initAtomBBStrategies();
   initTermBBStrategies();
@@ -202,6 +217,20 @@ void TBitblaster<T>::invalidateModelCache()
 }
 
 template <class T>
+void TBitblaster<T>::setProofLog(proof::BitVectorProof* bvp)
+{
+  if (THEORY_PROOF_ON())
+  {
+    d_bvp = bvp;
+    prop::SatSolver* satSolver = getSatSolver();
+    bvp->attachToSatSolver(*satSolver);
+    prop::SatVariable t = satSolver->trueVar();
+    prop::SatVariable f = satSolver->falseVar();
+    bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f);
+  }
+}
+
+template <class T>
 Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
 {
   if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node];
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 019918c2f..1e557bb64 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -32,11 +32,8 @@ namespace bv {
 EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
     : TBitblaster<Node>(),
       d_context(c),
-      d_nullContext(new context::Context()),
       d_satSolver(),
       d_bitblastingRegistrar(new BitblastingRegistrar(this)),
-      d_cnfStream(),
-      d_bvp(nullptr),
       d_bv(theory_bv),
       d_bbAtoms(),
       d_variables(),
@@ -268,13 +265,6 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
   return true;
 }
 
-void EagerBitblaster::setResolutionProofLog(
-    proof::ResolutionBitVectorProof* bvp)
-{
-  THEORY_PROOF(d_bvp = bvp; d_satSolver->setProofLog(bvp);
-               bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());)
-}
-
 bool EagerBitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index 3299ffc54..1c183b509 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -55,19 +55,13 @@ class EagerBitblaster : public TBitblaster<Node>
   bool solve();
   bool solve(const std::vector<Node>& assumptions);
   bool collectModelInfo(TheoryModel* m, bool fullModel);
-  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
 
  private:
   context::Context* d_context;
-  std::unique_ptr<context::Context> d_nullContext;
 
   typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-  // sat solver used for bitblasting and associated CnfStream
   std::unique_ptr<prop::SatSolver> d_satSolver;
   std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
-  std::unique_ptr<prop::CnfStream> d_cnfStream;
-
-  BitVectorProof* d_bvp;
 
   TheoryBV* d_bv;
   TNodeSet d_bbAtoms;
@@ -77,6 +71,7 @@ class EagerBitblaster : public TBitblaster<Node>
   std::unique_ptr<MinisatEmptyNotify> d_notify;
 
   Node getModelFromSatSolver(TNode a, bool fullModel) override;
+  prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
   bool isSharedTerm(TNode node);
 };
 
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 529f0373b..2a47c2315 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -64,10 +64,8 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
                                  bool emptyNotify)
     : TBitblaster<Node>(),
       d_bv(bv),
-      d_bvp(nullptr),
       d_ctx(c),
       d_nullRegistrar(new prop::NullRegistrar()),
-      d_nullContext(new context::Context()),
       d_assertedAtoms(new (true) context::CDList<prop::SatLiteral>(c)),
       d_explanations(new (true) ExplanationMap(c)),
       d_variables(),
@@ -566,11 +564,12 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
   return true;
 }
 
-void TLazyBitblaster::setProofLog(proof::ResolutionBitVectorProof* bvp)
+void TLazyBitblaster::setProofLog(proof::BitVectorProof* bvp)
 {
-  d_bvp = bvp;
-  d_satSolver->setProofLog( bvp );
-  bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());
+  THEORY_PROOF(d_bvp = bvp; bvp->attachToSatSolver(*d_satSolver);
+               prop::SatVariable t = d_satSolver->trueVar();
+               prop::SatVariable f = d_satSolver->falseVar();
+               bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f));
 }
 
 void TLazyBitblaster::clearSolver() {
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 1195d3590..9af74d8db 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -77,7 +77,7 @@ class TLazyBitblaster : public TBitblaster<Node>
    * constants to equivalence classes that don't already have them
    */
   bool collectModelInfo(TheoryModel* m, bool fullModel);
-  void setProofLog(proof::ResolutionBitVectorProof* bvp);
+  void setProofLog(proof::BitVectorProof* bvp);
 
   typedef TNodeSet::const_iterator vars_iterator;
   vars_iterator beginVars() { return d_variables.begin(); }
@@ -126,15 +126,11 @@ class TLazyBitblaster : public TBitblaster<Node>
   };
 
   TheoryBV* d_bv;
-  proof::ResolutionBitVectorProof* d_bvp;
   context::Context* d_ctx;
 
   std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
-  std::unique_ptr<context::Context> d_nullContext;
-  // sat solver used for bitblasting and associated CnfStream
   std::unique_ptr<prop::BVSatSolverInterface> d_satSolver;
   std::unique_ptr<prop::BVSatSolverNotify> d_satSolverNotify;
-  std::unique_ptr<prop::CnfStream> d_cnfStream;
 
   AssertionList*
       d_assertedAtoms;            /**< context dependent list storing the atoms
@@ -155,6 +151,7 @@ class TLazyBitblaster : public TBitblaster<Node>
   void addAtom(TNode atom);
   bool hasValue(TNode a);
   Node getModelFromSatSolver(TNode a, bool fullModel) override;
+  prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
 
   class Statistics
   {
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 119195c4a..336529dfd 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -56,7 +56,7 @@ void EagerBitblastSolver::initialize() {
   } else {
     d_bitblaster.reset(new EagerBitblaster(d_bv, d_context));
     THEORY_PROOF(if (d_bvp) {
-      d_bitblaster->setResolutionProofLog(d_bvp);
+      d_bitblaster->setProofLog(d_bvp);
       d_bvp->setBitblaster(d_bitblaster.get());
     });
   }
@@ -127,8 +127,7 @@ bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
   return d_bitblaster->collectModelInfo(m, fullModel);
 }
 
-void EagerBitblastSolver::setResolutionProofLog(
-    proof::ResolutionBitVectorProof* bvp)
+void EagerBitblastSolver::setProofLog(proof::BitVectorProof* bvp)
 {
   d_bvp = bvp;
 }
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 7f688b3ae..0b518ca4a 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -48,7 +48,7 @@ class EagerBitblastSolver {
   bool isInitialized();
   void initialize();
   bool collectModelInfo(theory::TheoryModel* m, bool fullModel);
-  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
+  void setProofLog(proof::BitVectorProof* bvp);
 
  private:
   context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
@@ -61,7 +61,7 @@ class EagerBitblastSolver {
   bool d_useAig;
 
   TheoryBV* d_bv;
-  proof::ResolutionBitVectorProof* d_bvp;
+  proof::BitVectorProof* d_bvp;
 };  // class EagerBitblastSolver
 
 }  // namespace bv
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 31c542e0b..e2b649841 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -26,7 +26,7 @@
 namespace CVC4 {
 
 namespace proof {
-class ResolutionBitVectorProof;
+class BitVectorProof;
 }
 
 namespace theory {
@@ -93,7 +93,7 @@ class SubtheorySolver {
     return res;
   }
   virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
-  virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {}
+  virtual void setProofLog(proof::BitVectorProof* bvp) {}
   AssertionQueue::const_iterator assertionsBegin() {
     return d_assertionQueue.begin();
   }
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index ff9dd52c2..ceb02af40 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -276,7 +276,7 @@ void BitblastSolver::setConflict(TNode conflict) {
   d_bv->setConflict(final_conflict);
 }
 
-void BitblastSolver::setProofLog(proof::ResolutionBitVectorProof* bvp)
+void BitblastSolver::setProofLog(proof::BitVectorProof* bvp)
 {
   d_bitblaster->setProofLog( bvp );
   bvp->setBitblaster(d_bitblaster.get());
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index aa2c90c43..e028dbbdc 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -79,7 +79,7 @@ public:
   void bitblastQueue();
   void setAbstraction(AbstractionModule* module);
   uint64_t computeAtomWeight(TNode atom);
-  void setProofLog(proof::ResolutionBitVectorProof* bvp) override;
+  void setProofLog(proof::BitVectorProof* bvp) override;
 };
 
 } /* namespace CVC4::theory::bv */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 949a3d738..04a6cf52c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -986,10 +986,10 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
   return changed;
 }
 
-void TheoryBV::setResolutionProofLog(proof::ResolutionBitVectorProof* bvp)
+void TheoryBV::setProofLog(proof::BitVectorProof* bvp)
 {
   if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
-    d_eagerSolver->setResolutionProofLog(bvp);
+    d_eagerSolver->setProofLog(bvp);
   }else{
     for( unsigned i=0; i< d_subtheories.size(); i++ ){
       d_subtheories[i]->setProofLog( bvp );
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index afa9f4b4f..3d151cfb1 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -31,6 +31,14 @@
 #include "util/hash.h"
 #include "util/statistics_registry.h"
 
+// Forward declarations, needed because the BV theory and the BV Proof classes
+// are cyclically dependent
+namespace CVC4 {
+namespace proof {
+class BitVectorProof;
+}
+}  // namespace CVC4
+
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -104,7 +112,7 @@ public:
 
   bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
 
-  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
+  void setProofLog(proof::BitVectorProof* bvp);
 
  private: