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

1 files changed, 62 insertions, 0 deletions

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)