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

3 files changed, 106 insertions, 0 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();