BV: Add proof logging for bit-blasting. (#6373)

10 files changed, 372 insertions, 17 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 92944a7f4..fbeaea729 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -119,6 +119,47 @@ const char* toString(PfRule id)
     case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST";
     //================================================= Bit-Vector rules
     case PfRule::BV_BITBLAST: return "BV_BITBLAST";
+    case PfRule::BV_BITBLAST_CONST: return "BV_BITBLAST_CONST";
+    case PfRule::BV_BITBLAST_VAR: return "BV_BITBLAST_VAR";
+    case PfRule::BV_BITBLAST_EQUAL: return "BV_BITBLAST_EQUAL";
+    case PfRule::BV_BITBLAST_ULT: return "BV_BITBLAST_ULT";
+    case PfRule::BV_BITBLAST_ULE: return "BV_BITBLAST_ULE";
+    case PfRule::BV_BITBLAST_UGT: return "BV_BITBLAST_UGT";
+    case PfRule::BV_BITBLAST_UGE: return "BV_BITBLAST_UGE";
+    case PfRule::BV_BITBLAST_SLT: return "BV_BITBLAST_SLT";
+    case PfRule::BV_BITBLAST_SLE: return "BV_BITBLAST_SLE";
+    case PfRule::BV_BITBLAST_SGT: return "BV_BITBLAST_SGT";
+    case PfRule::BV_BITBLAST_SGE: return "BV_BITBLAST_SGE";
+    case PfRule::BV_BITBLAST_NOT: return "BV_BITBLAST_NOT";
+    case PfRule::BV_BITBLAST_CONCAT: return "BV_BITBLAST_CONCAT";
+    case PfRule::BV_BITBLAST_AND: return "BV_BITBLAST_AND";
+    case PfRule::BV_BITBLAST_OR: return "BV_BITBLAST_OR";
+    case PfRule::BV_BITBLAST_XOR: return "BV_BITBLAST_XOR";
+    case PfRule::BV_BITBLAST_XNOR: return "BV_BITBLAST_XNOR";
+    case PfRule::BV_BITBLAST_NAND: return "BV_BITBLAST_NAND";
+    case PfRule::BV_BITBLAST_NOR: return "BV_BITBLAST_NOR";
+    case PfRule::BV_BITBLAST_COMP: return "BV_BITBLAST_COMP";
+    case PfRule::BV_BITBLAST_MULT: return "BV_BITBLAST_MULT";
+    case PfRule::BV_BITBLAST_PLUS: return "BV_BITBLAST_PLUS";
+    case PfRule::BV_BITBLAST_SUB: return "BV_BITBLAST_SUB";
+    case PfRule::BV_BITBLAST_NEG: return "BV_BITBLAST_NEG";
+    case PfRule::BV_BITBLAST_UDIV: return "BV_BITBLAST_UDIV";
+    case PfRule::BV_BITBLAST_UREM: return "BV_BITBLAST_UREM";
+    case PfRule::BV_BITBLAST_SDIV: return "BV_BITBLAST_SDIV";
+    case PfRule::BV_BITBLAST_SREM: return "BV_BITBLAST_SREM";
+    case PfRule::BV_BITBLAST_SMOD: return "BV_BITBLAST_SMOD";
+    case PfRule::BV_BITBLAST_SHL: return "BV_BITBLAST_SHL";
+    case PfRule::BV_BITBLAST_LSHR: return "BV_BITBLAST_LSHR";
+    case PfRule::BV_BITBLAST_ASHR: return "BV_BITBLAST_ASHR";
+    case PfRule::BV_BITBLAST_ULTBV: return "BV_BITBLAST_ULTBV";
+    case PfRule::BV_BITBLAST_SLTBV: return "BV_BITBLAST_SLTBV";
+    case PfRule::BV_BITBLAST_ITE: return "BV_BITBLAST_ITE";
+    case PfRule::BV_BITBLAST_EXTRACT: return "BV_BITBLAST_EXTRACT";
+    case PfRule::BV_BITBLAST_REPEAT: return "BV_BITBLAST_REPEAT";
+    case PfRule::BV_BITBLAST_ZERO_EXTEND: return "BV_BITBLAST_ZERO_EXTEND";
+    case PfRule::BV_BITBLAST_SIGN_EXTEND: return "BV_BITBLAST_SIGN_EXTEND";
+    case PfRule::BV_BITBLAST_ROTATE_RIGHT: return "BV_BITBLAST_ROTATE_RIGHT";
+    case PfRule::BV_BITBLAST_ROTATE_LEFT: return "BV_BITBLAST_ROTATE_LEFT";
     case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM";
     //================================================= Datatype rules
     case PfRule::DT_UNIF: return "DT_UNIF";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index d2aa75d8c..88e344b8a 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -701,12 +701,74 @@ enum class PfRule : uint32_t
   ARRAYS_TRUST,
 
   //================================================= Bit-Vector rules
+  // Note: bitblast() represents the result of the bit-blasted term as a
+  //       bit-vector consisting of the output bits of the bit-blasted circuit
+  //       representation of the term. Terms are bit-blasted according to the
+  //       strategies defined in
+  //       theory/bv/bitblast/bitblast_strategies_template.h.
   // ======== Bitblast
   // Children: none
   // Arguments: (t)
   // ---------------------
   // Conclusion: (= t bitblast(t))
   BV_BITBLAST,
+  // ======== Bitblast Bit-Vector Constant
+  // Children: none
+  // Arguments: (= t bitblast(t))
+  // ---------------------
+  // Conclusion: (= t bitblast(t))
+  BV_BITBLAST_CONST,
+  // ======== Bitblast Bit-Vector Variable
+  // Children: none
+  // Arguments: (= t bitblast(t))
+  // ---------------------
+  // Conclusion: (= t bitblast(t))
+  BV_BITBLAST_VAR,
+  // ======== Bitblast Bit-Vector Terms
+  // TODO cvc4-projects issue #275
+  // Children: none
+  // Arguments: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
+  // ---------------------
+  // Conclusion: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
+  BV_BITBLAST_EQUAL,
+  BV_BITBLAST_ULT,
+  BV_BITBLAST_ULE,
+  BV_BITBLAST_UGT,
+  BV_BITBLAST_UGE,
+  BV_BITBLAST_SLT,
+  BV_BITBLAST_SLE,
+  BV_BITBLAST_SGT,
+  BV_BITBLAST_SGE,
+  BV_BITBLAST_NOT,
+  BV_BITBLAST_CONCAT,
+  BV_BITBLAST_AND,
+  BV_BITBLAST_OR,
+  BV_BITBLAST_XOR,
+  BV_BITBLAST_XNOR,
+  BV_BITBLAST_NAND,
+  BV_BITBLAST_NOR,
+  BV_BITBLAST_COMP,
+  BV_BITBLAST_MULT,
+  BV_BITBLAST_PLUS,
+  BV_BITBLAST_SUB,
+  BV_BITBLAST_NEG,
+  BV_BITBLAST_UDIV,
+  BV_BITBLAST_UREM,
+  BV_BITBLAST_SDIV,
+  BV_BITBLAST_SREM,
+  BV_BITBLAST_SMOD,
+  BV_BITBLAST_SHL,
+  BV_BITBLAST_LSHR,
+  BV_BITBLAST_ASHR,
+  BV_BITBLAST_ULTBV,
+  BV_BITBLAST_SLTBV,
+  BV_BITBLAST_ITE,
+  BV_BITBLAST_EXTRACT,
+  BV_BITBLAST_REPEAT,
+  BV_BITBLAST_ZERO_EXTEND,
+  BV_BITBLAST_SIGN_EXTEND,
+  BV_BITBLAST_ROTATE_RIGHT,
+  BV_BITBLAST_ROTATE_LEFT,
   // ======== Eager Atom
   // Children: none
   // Arguments: (F)
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index 2233dcc7b..18057e149 100644
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -133,6 +133,9 @@ Node TConvProofGenerator::registerRewriteStep(Node t,
                                               uint32_t tctx,
                                               bool isPre)
 {
+  Assert(!t.isNull());
+  Assert(!s.isNull());
+
   if (t == s)
   {
     return Node::null();
diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index 2f6f099a8..09448da8a 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -16,19 +16,79 @@
 
 #include <unordered_set>
 
+#include "expr/term_conversion_proof_generator.h"
+#include "options/proof_options.h"
 #include "theory/theory_model.h"
 
 namespace cvc5 {
 namespace theory {
 namespace bv {
 
-BBProof::BBProof(TheoryState* state) : d_bb(new BBSimple(state)) {}
+std::unordered_map<Kind, PfRule, kind::KindHashFunction>
+    BBProof::s_kindToPfRule = {
+        {kind::CONST_BITVECTOR, PfRule::BV_BITBLAST_CONST},
+        {kind::EQUAL, PfRule::BV_BITBLAST_EQUAL},
+        {kind::BITVECTOR_ULT, PfRule::BV_BITBLAST_ULT},
+        {kind::BITVECTOR_ULE, PfRule::BV_BITBLAST_ULE},
+        {kind::BITVECTOR_UGT, PfRule::BV_BITBLAST_UGT},
+        {kind::BITVECTOR_UGE, PfRule::BV_BITBLAST_UGE},
+        {kind::BITVECTOR_SLT, PfRule::BV_BITBLAST_SLT},
+        {kind::BITVECTOR_SLE, PfRule::BV_BITBLAST_SLE},
+        {kind::BITVECTOR_SGT, PfRule::BV_BITBLAST_SGT},
+        {kind::BITVECTOR_SGE, PfRule::BV_BITBLAST_SGE},
+        {kind::BITVECTOR_NOT, PfRule::BV_BITBLAST_NOT},
+        {kind::BITVECTOR_CONCAT, PfRule::BV_BITBLAST_CONCAT},
+        {kind::BITVECTOR_AND, PfRule::BV_BITBLAST_AND},
+        {kind::BITVECTOR_OR, PfRule::BV_BITBLAST_OR},
+        {kind::BITVECTOR_XOR, PfRule::BV_BITBLAST_XOR},
+        {kind::BITVECTOR_XNOR, PfRule::BV_BITBLAST_XNOR},
+        {kind::BITVECTOR_NAND, PfRule::BV_BITBLAST_NAND},
+        {kind::BITVECTOR_NOR, PfRule::BV_BITBLAST_NOR},
+        {kind::BITVECTOR_COMP, PfRule::BV_BITBLAST_COMP},
+        {kind::BITVECTOR_MULT, PfRule::BV_BITBLAST_MULT},
+        {kind::BITVECTOR_PLUS, PfRule::BV_BITBLAST_PLUS},
+        {kind::BITVECTOR_SUB, PfRule::BV_BITBLAST_SUB},
+        {kind::BITVECTOR_NEG, PfRule::BV_BITBLAST_NEG},
+        {kind::BITVECTOR_UDIV, PfRule::BV_BITBLAST_UDIV},
+        {kind::BITVECTOR_UREM, PfRule::BV_BITBLAST_UREM},
+        {kind::BITVECTOR_SDIV, PfRule::BV_BITBLAST_SDIV},
+        {kind::BITVECTOR_SREM, PfRule::BV_BITBLAST_SREM},
+        {kind::BITVECTOR_SMOD, PfRule::BV_BITBLAST_SMOD},
+        {kind::BITVECTOR_SHL, PfRule::BV_BITBLAST_SHL},
+        {kind::BITVECTOR_LSHR, PfRule::BV_BITBLAST_LSHR},
+        {kind::BITVECTOR_ASHR, PfRule::BV_BITBLAST_ASHR},
+        {kind::BITVECTOR_ULTBV, PfRule::BV_BITBLAST_ULTBV},
+        {kind::BITVECTOR_SLTBV, PfRule::BV_BITBLAST_SLTBV},
+        {kind::BITVECTOR_ITE, PfRule::BV_BITBLAST_ITE},
+        {kind::BITVECTOR_EXTRACT, PfRule::BV_BITBLAST_EXTRACT},
+        {kind::BITVECTOR_REPEAT, PfRule::BV_BITBLAST_REPEAT},
+        {kind::BITVECTOR_ZERO_EXTEND, PfRule::BV_BITBLAST_ZERO_EXTEND},
+        {kind::BITVECTOR_SIGN_EXTEND, PfRule::BV_BITBLAST_SIGN_EXTEND},
+        {kind::BITVECTOR_ROTATE_RIGHT, PfRule::BV_BITBLAST_ROTATE_RIGHT},
+        {kind::BITVECTOR_ROTATE_LEFT, PfRule::BV_BITBLAST_ROTATE_LEFT},
+};
+
+BBProof::BBProof(TheoryState* state,
+                 ProofNodeManager* pnm,
+                 TConvProofGenerator* tcpg)
+    : d_bb(new BBSimple(state)), d_pnm(pnm), d_tcpg(tcpg)
+{
+}
+
+BBProof::~BBProof() {}
 
 void BBProof::bbAtom(TNode node)
 {
   std::vector<TNode> visit;
   visit.push_back(node);
   std::unordered_set<TNode, TNodeHashFunction> visited;
+
+  bool fproofs =
+      options::proofGranularityMode() != options::ProofGranularityMode::OFF;
+  bool fpenabled = isProofsEnabled() && fproofs;
+
+  NodeManager* nm = NodeManager::currentNM();
+
   while (!visit.empty())
   {
     TNode n = visit.back();
@@ -50,22 +110,89 @@ void BBProof::bbAtom(TNode node)
     {
       if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
       {
-        // unused for now, will be needed for proof logging
         Bits bits;
         d_bb->makeVariable(n, bits);
+        if (fpenabled)
+        {
+          Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
+          d_bbMap.emplace(n, n_tobv);
+          d_tcpg->addRewriteStep(n,
+                                 n_tobv,
+                                 PfRule::BV_BITBLAST_VAR,
+                                 {},
+                                 {n.eqNode(n_tobv)},
+                                 false);
+        }
       }
       else if (n.getType().isBitVector())
       {
         Bits bits;
         d_bb->bbTerm(n, bits);
+        Kind kind = n.getKind();
+        if (fpenabled)
+        {
+          Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
+          d_bbMap.emplace(n, n_tobv);
+          Node c_tobv;
+          if (n.isConst())
+          {
+            c_tobv = n;
+          }
+          else
+          {
+            std::vector<Node> children_tobv;
+            if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+            {
+              children_tobv.push_back(n.getOperator());
+            }
+
+            for (const auto& child : n)
+            {
+              children_tobv.push_back(d_bbMap.at(child));
+            }
+            c_tobv = nm->mkNode(kind, children_tobv);
+          }
+          d_tcpg->addRewriteStep(c_tobv,
+                                 n_tobv,
+                                 s_kindToPfRule.at(kind),
+                                 {},
+                                 {c_tobv.eqNode(n_tobv)},
+                                 false);
+        }
       }
       else
       {
         d_bb->bbAtom(n);
+        if (fpenabled)
+        {
+          Node n_tobv = getStoredBBAtom(n);
+          std::vector<Node> children_tobv;
+          for (const auto& child : n)
+          {
+            children_tobv.push_back(d_bbMap.at(child));
+          }
+          Node c_tobv = nm->mkNode(n.getKind(), children_tobv);
+          d_tcpg->addRewriteStep(c_tobv,
+                                 n_tobv,
+                                 s_kindToPfRule.at(n.getKind()),
+                                 {},
+                                 {c_tobv.eqNode(n_tobv)},
+                                 false);
+        }
       }
       visit.pop_back();
     }
   }
+  if (isProofsEnabled() && !fproofs)
+  {
+    Node node_tobv = getStoredBBAtom(node);
+    d_tcpg->addRewriteStep(node,
+                           node_tobv,
+                           PfRule::BV_BITBLAST,
+                           {},
+                           {node.eqNode(node_tobv)},
+                           false);
+  }
 }
 
 bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
@@ -83,6 +210,8 @@ bool BBProof::collectModelValues(TheoryModel* m,
   return d_bb->collectModelValues(m, relevantTerms);
 }
 
+bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
+
 }  // namespace bv
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
index bd5232a76..6cd4960fb 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.h
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -20,6 +20,9 @@
 #include "theory/bv/bitblast/simple_bitblaster.h"
 
 namespace cvc5 {
+
+class TConvProofGenerator;
+
 namespace theory {
 namespace bv {
 
@@ -28,8 +31,8 @@ class BBProof
   using Bits = std::vector<Node>;
 
  public:
-  BBProof(TheoryState* state);
-  ~BBProof() = default;
+  BBProof(TheoryState* state, ProofNodeManager* pnm, TConvProofGenerator* tcpg);
+  ~BBProof();
 
   /** Bit-blast atom 'node'. */
   void bbAtom(TNode node);
@@ -43,7 +46,21 @@ class BBProof
   bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
 
  private:
+  /** Map node kinds to proof rules. */
+  static std::unordered_map<Kind, PfRule, kind::KindHashFunction>
+      s_kindToPfRule;
+
+  /** Return true if proofs are enabled. */
+  bool isProofsEnabled() const;
+
+  /** The associated simple bit-blaster. */
   std::unique_ptr<BBSimple> d_bb;
+  /** The associated proof node manager. */
+  ProofNodeManager* d_pnm;
+  /** The associated term conversion proof generator. */
+  TConvProofGenerator* d_tcpg;
+  /** Map bit-vector nodes to bit-blasted nodes. */
+  std::unordered_map<Node, Node, NodeHashFunction> d_bbMap;
 };
 
 }  // namespace bv
diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index b3abd6269..52f5d52ac 100644
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/bv/bv_solver_simple.h"
 
+#include "expr/term_conversion_proof_generator.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
@@ -69,9 +70,20 @@ BVSolverSimple::BVSolverSimple(TheoryState* s,
                                TheoryInferenceManager& inferMgr,
                                ProofNodeManager* pnm)
     : BVSolver(*s, inferMgr),
-      d_bitblaster(new BBProof(s)),
-      d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
-                : nullptr)
+      d_tcpg(pnm ? new TConvProofGenerator(
+                 pnm,
+                 nullptr,
+                 /* ONCE to visit each term only once, post-order.  FIXPOINT
+                  * could lead to infinite loops due to terms being rewritten
+                  * to terms that contain themselves */
+                 TConvPolicy::ONCE,
+                 /* STATIC to get the same ProofNode for a shared subterm. */
+                 TConvCachePolicy::STATIC,
+                 "BVSolverSimple::TConvProofGenerator",
+                 nullptr,
+                 false)
+                 : nullptr),
+      d_bitblaster(new BBProof(s, pnm, d_tcpg.get()))
 {
 }
 
@@ -86,13 +98,13 @@ void BVSolverSimple::addBBLemma(TNode fact)
   Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
   Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
 
-  if (d_epg == nullptr)
+  if (d_tcpg == nullptr)
   {
     d_im.lemma(lemma, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
   }
   else
   {
-    TrustNode tlem = d_epg->mkTrustNode(lemma, PfRule::BV_BITBLAST, {}, {fact});
+    TrustNode tlem = TrustNode::mkTrustLemma(lemma, d_tcpg.get());
     d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
   }
 }
@@ -116,14 +128,13 @@ bool BVSolverSimple::preNotifyFact(
     NodeManager* nm = NodeManager::currentNM();
     Node lemma = nm->mkNode(kind::EQUAL, fact, n);
 
-    if (d_epg == nullptr)
+    if (d_tcpg == nullptr)
     {
       d_im.lemma(lemma, InferenceId::BV_SIMPLE_LEMMA);
     }
     else
     {
-      TrustNode tlem =
-          d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
+      TrustNode tlem = TrustNode::mkTrustLemma(lemma, d_tcpg.get());
       d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA);
     }
 
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index 6994d755d..106a473d9 100644
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -21,9 +21,11 @@
 #include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/bv/bv_solver.h"
 #include "theory/bv/proof_checker.h"
-#include "theory/eager_proof_generator.h"
 
 namespace cvc5 {
+
+class TConvProofGenerator;
+
 namespace theory {
 namespace bv {
 
@@ -71,11 +73,10 @@ class BVSolverSimple : public BVSolver
    */
   void addBBLemma(TNode fact);
 
+  /** Proof generator. */
+  std::unique_ptr<TConvProofGenerator> d_tcpg;
   /** Bit-blaster used to bit-blast atoms/terms. */
   std::unique_ptr<BBProof> d_bitblaster;
-
-  /** Proof generator that manages proofs for lemmas generated by this class. */
-  std::unique_ptr<EagerProofGenerator> d_epg;
   /** Proof rule checker */
   BVProofRuleChecker d_checker;
 };
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 3a1032bc3..c9999d39b 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -38,6 +38,9 @@ well-founded BITVECTOR_TYPE \
 
 ### non-parameterized operator kinds ------------------------------------------
 
+## conversion to bit-vector from vector of Booleans kind
+operator BITVECTOR_BB_TERM 1: "create bit-vector from vector of Booleans"
+
 ## concatentation kind
 operator BITVECTOR_CONCAT 2: "concatenation of two or more bit-vectors"
 
@@ -61,7 +64,6 @@ operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bi
 operator BITVECTOR_SDIV 2 "2's complement signed division"
 operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)"
 operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)"
-# total division kinds
 
 ## shift kinds
 operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)"
@@ -158,6 +160,9 @@ parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-
 
 typerule CONST_BITVECTOR ::cvc5::theory::bv::BitVectorConstantTypeRule
 
+## conversion to bit-vector from vector of Booleans kind
+typerule BITVECTOR_BB_TERM ::cvc5::theory::bv::BitVectorToBVTypeRule
+
 ## concatentation kind
 typerule BITVECTOR_CONCAT ::cvc5::theory::bv::BitVectorConcatTypeRule
 
diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp
index 57244d9b4..b8ede6386 100644
--- a/src/theory/bv/proof_checker.cpp
+++ b/src/theory/bv/proof_checker.cpp
@@ -22,6 +22,47 @@ namespace bv {
 void BVProofRuleChecker::registerTo(ProofChecker* pc)
 {
   pc->registerChecker(PfRule::BV_BITBLAST, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_CONST, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_VAR, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_EQUAL, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_ULT, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_ULE, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_UGT, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_UGE, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SLT, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SLE, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SGT, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SGE, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_NOT, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_CONCAT, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_AND, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_OR, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_XOR, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_XNOR, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_NAND, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_NOR, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_COMP, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_MULT, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_PLUS, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SUB, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_NEG, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_UDIV, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_UREM, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SDIV, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SREM, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SMOD, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SHL, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_LSHR, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_ASHR, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_ULTBV, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SLTBV, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_ITE, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_EXTRACT, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_REPEAT, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_ZERO_EXTEND, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_SIGN_EXTEND, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_ROTATE_RIGHT, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_ROTATE_LEFT, this);
   pc->registerChecker(PfRule::BV_EAGER_ATOM, this);
 }
 
@@ -38,6 +79,32 @@ Node BVProofRuleChecker::checkInternal(PfRule id,
     Node n = bb.getStoredBBAtom(args[0]);
     return args[0].eqNode(n);
   }
+  else if (id == PfRule::BV_BITBLAST_CONST || id == PfRule::BV_BITBLAST_VAR
+           || id == PfRule::BV_BITBLAST_EQUAL || id == PfRule::BV_BITBLAST_ULT
+           || id == PfRule::BV_BITBLAST_ULE || id == PfRule::BV_BITBLAST_UGT
+           || id == PfRule::BV_BITBLAST_UGE || id == PfRule::BV_BITBLAST_SLT
+           || id == PfRule::BV_BITBLAST_SLE || id == PfRule::BV_BITBLAST_SGT
+           || id == PfRule::BV_BITBLAST_SGE || id == PfRule::BV_BITBLAST_NOT
+           || id == PfRule::BV_BITBLAST_CONCAT || id == PfRule::BV_BITBLAST_AND
+           || id == PfRule::BV_BITBLAST_OR || id == PfRule::BV_BITBLAST_XOR
+           || id == PfRule::BV_BITBLAST_XNOR || id == PfRule::BV_BITBLAST_NAND
+           || id == PfRule::BV_BITBLAST_NOR || id == PfRule::BV_BITBLAST_COMP
+           || id == PfRule::BV_BITBLAST_MULT || id == PfRule::BV_BITBLAST_PLUS
+           || id == PfRule::BV_BITBLAST_SUB || id == PfRule::BV_BITBLAST_NEG
+           || id == PfRule::BV_BITBLAST_UDIV || id == PfRule::BV_BITBLAST_UREM
+           || id == PfRule::BV_BITBLAST_SDIV || id == PfRule::BV_BITBLAST_SREM
+           || id == PfRule::BV_BITBLAST_SMOD || id == PfRule::BV_BITBLAST_SHL
+           || id == PfRule::BV_BITBLAST_LSHR || id == PfRule::BV_BITBLAST_ASHR
+           || id == PfRule::BV_BITBLAST_ULTBV || id == PfRule::BV_BITBLAST_SLTBV
+           || id == PfRule::BV_BITBLAST_ITE || id == PfRule::BV_BITBLAST_EXTRACT
+           || id == PfRule::BV_BITBLAST_REPEAT
+           || id == PfRule::BV_BITBLAST_ZERO_EXTEND
+           || id == PfRule::BV_BITBLAST_SIGN_EXTEND
+           || id == PfRule::BV_BITBLAST_ROTATE_RIGHT
+           || id == PfRule::BV_BITBLAST_ROTATE_LEFT)
+  {
+    return args[0];
+  }
   else if (id == PfRule::BV_EAGER_ATOM)
   {
     Assert(children.empty());
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 6594e9fa7..763617d25 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -81,6 +81,25 @@ class BitVectorConcatTypeRule
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+class BitVectorToBVTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    for (const auto& child : n)
+    {
+      TypeNode t = child.getType(check);
+      if (!t.isBoolean())
+      {
+        throw TypeCheckingExceptionPrivate(n, "expecting Boolean terms");
+      }
+    }
+    return nodeManager->mkBitVectorType(n.getNumChildren());
+  }
+};
+
 class BitVectorITETypeRule
 {
  public: