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

Introduces BV_BITBLAST_STEP rule, which replaces BV_BITBLAST_X rules.

diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index 676fa6a63e377265f2e504630b4f11e0626dfc94..def57532d10b4021978e9ff0847c662deea7da9f 100644 (file)
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -121,47 +121,7 @@ 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_ADD: return "BV_BITBLAST_ADD";
-    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_BITBLAST_STEP: return "BV_BITBLAST_STEP";
     case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM";
     //================================================= Datatype rules
     case PfRule::DT_UNIF: return "DT_UNIF";

diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index c1cf0338afb40247a019620e1cfcea46a5ab7d4f..d20c3ecc06d5ccc099636bb58634c860639ccc3b 100644 (file)
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -730,63 +730,18 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (= t bitblast(t))
   BV_BITBLAST,
-  // ======== Bitblast Bit-Vector Constant
+  // ======== Bitblast Bit-Vector Constant, Variable
   // 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_ADD,
-  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,
+  BV_BITBLAST_STEP,
+
   // ======== Eager Atom
   // Children: none
   // Arguments: (F)

diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index a1b856d88b25f50a124652bf012c470c72214798..9d4de13870ed3489377261d10d5f67930b7992b6 100644 (file)
--- 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 428581fe083a7ae1f40229ced762305035fa1e1e..17be4204c834f171433a99eca0320f96d1d72d46 100644 (file)
--- 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 711e9798caa49b7f3644cc6fc387a15883fb3d47..cbaec7ca6e7464fa2fa7ab0c31325d0ed0c993e7 100644 (file)
--- 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)