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

9 files changed, 403 insertions, 91 deletions

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);