bv: Simplify BV_BITBLAST_* proof rules. (#6871)

Introduces BV_BITBLAST_STEP rule, which replaces BV_BITBLAST_X rules.

3 files changed, 8 insertions, 115 deletions

diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index a1b856d88..9d4de1387 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -23,50 +23,6 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-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_ADD, PfRule::BV_BITBLAST_ADD},
-        {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, bool fineGrained)
     : d_bb(new BBSimple(state)),
       d_pnm(pnm),
@@ -129,7 +85,7 @@ void BBProof::bbAtom(TNode node)
           d_bbMap.emplace(n, n_tobv);
           d_tcpg->addRewriteStep(n,
                                  n_tobv,
-                                 PfRule::BV_BITBLAST_VAR,
+                                 PfRule::BV_BITBLAST_STEP,
                                  {},
                                  {n.eqNode(n_tobv)},
                                  false);
@@ -165,7 +121,7 @@ void BBProof::bbAtom(TNode node)
           }
           d_tcpg->addRewriteStep(c_tobv,
                                  n_tobv,
-                                 s_kindToPfRule.at(kind),
+                                 PfRule::BV_BITBLAST_STEP,
                                  {},
                                  {c_tobv.eqNode(n_tobv)},
                                  false);
@@ -185,7 +141,7 @@ void BBProof::bbAtom(TNode node)
           Node c_tobv = nm->mkNode(n.getKind(), children_tobv);
           d_tcpg->addRewriteStep(c_tobv,
                                  n_tobv,
-                                 s_kindToPfRule.at(n.getKind()),
+                                 PfRule::BV_BITBLAST_STEP,
                                  {},
                                  {c_tobv.eqNode(n_tobv)},
                                  false);
diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
index 428581fe0..17be4204c 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.h
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -49,10 +49,6 @@ class BBProof
   TConvProofGenerator* getProofGenerator();
 
  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;
 
diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp
index 711e9798c..cbaec7ca6 100644
--- a/src/theory/bv/proof_checker.cpp
+++ b/src/theory/bv/proof_checker.cpp
@@ -22,47 +22,7 @@ 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_ADD, 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_BITBLAST_STEP, this);
   pc->registerChecker(PfRule::BV_EAGER_ATOM, this);
 }
 
@@ -77,30 +37,11 @@ Node BVProofRuleChecker::checkInternal(PfRule id,
     Assert(args[0].getKind() == kind::EQUAL);
     return args[0];
   }
-  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_ADD
-           || 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)
+  else if (id == PfRule::BV_BITBLAST_STEP)
   {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    Assert(args[0].getKind() == kind::EQUAL);
     return args[0];
   }
   else if (id == PfRule::BV_EAGER_ATOM)