More

ajreynol · Feb 24, 2025 · c6226e9 · c6226e9
1 parent 86dc0d5
commit c6226e9
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 49 deletions.
diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h
@@ -3024,32 +3024,6 @@ enum ENUM(ProofRewriteRule)
    * \endverbatim
    */
   EVALUE(MACRO_BV_EXTRACT_CONCAT),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Bitvectors -- Macro extract sign extend **
-   *
-   * .. math::
-   *    a = b
-   *
-   * where :math:`a` is rewritten to :math:`b` by the internal rewrite
-   * rule ExtractSignExtend.
-   *
-   * \endverbatim
-   */
-  EVALUE(MACRO_BV_EXTRACT_SIGN_EXTEND),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Bitvectors -- Macro arithmetic shift right by constant **
-   *
-   * .. math::
-   *    a = b
-   *
-   * where :math:`a` is rewritten to :math:`b` by the internal rewrite
-   * rule AshrByConst.
-   *
-   * \endverbatim
-   */
-  EVALUE(MACRO_BV_ASHR_BY_CONST),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Bitvectors -- Macro or simplify **
@@ -3089,19 +3063,6 @@ enum ENUM(ProofRewriteRule)
    * \endverbatim
    */
   EVALUE(MACRO_BV_XOR_SIMPLIFY),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Bitvectors -- Macro and/or/xor concat pullup **
-   *
-   * .. math::
-   *    a = b
-   *
-   * where :math:`a` is rewritten to :math:`b` by the internal rewrite
-   * rule AndOrXorConcatPullup.
-   *
-   * \endverbatim
-   */
-  EVALUE(MACRO_BV_AND_OR_XOR_CONCAT_PULLUP),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Bitvectors -- Macro multiply signed less than multiply **

diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp
@@ -287,17 +287,11 @@ const char* toString(cvc5::ProofRewriteRule rule)
     case ProofRewriteRule::DT_MATCH_ELIM: return "dt-match-elim";
     case ProofRewriteRule::MACRO_BV_EXTRACT_CONCAT:
       return "macro-bv-extract-concat";
-    case ProofRewriteRule::MACRO_BV_EXTRACT_SIGN_EXTEND:
-      return "macro-bv-extract-sign-extend";
-    case ProofRewriteRule::MACRO_BV_ASHR_BY_CONST:
-      return "macro-bv-ashr-by-const";
     case ProofRewriteRule::MACRO_BV_OR_SIMPLIFY: return "macro-bv-or-simplify";
     case ProofRewriteRule::MACRO_BV_AND_SIMPLIFY:
       return "macro-bv-and-simplify";
     case ProofRewriteRule::MACRO_BV_XOR_SIMPLIFY:
       return "macro-bv-xor-simplify";
-    case ProofRewriteRule::MACRO_BV_AND_OR_XOR_CONCAT_PULLUP:
-      return "macro-bv-and-or-xor-concat-pullup";
     case ProofRewriteRule::MACRO_BV_MULT_SLT_MULT:
       return "macro-bv-mult-slt-mult";
     case ProofRewriteRule::MACRO_BV_CONCAT_EXTRACT_MERGE:

diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp
@@ -299,12 +299,9 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite(CDProof* cdp,
       }
       break;
     case ProofRewriteRule::MACRO_BV_EXTRACT_CONCAT:
-    case ProofRewriteRule::MACRO_BV_EXTRACT_SIGN_EXTEND:
-    case ProofRewriteRule::MACRO_BV_ASHR_BY_CONST:
     case ProofRewriteRule::MACRO_BV_OR_SIMPLIFY:
     case ProofRewriteRule::MACRO_BV_AND_SIMPLIFY:
     case ProofRewriteRule::MACRO_BV_XOR_SIMPLIFY:
-    case ProofRewriteRule::MACRO_BV_AND_OR_XOR_CONCAT_PULLUP:
     case ProofRewriteRule::MACRO_BV_MULT_SLT_MULT:
     case ProofRewriteRule::MACRO_BV_CONCAT_EXTRACT_MERGE:
     case ProofRewriteRule::MACRO_BV_CONCAT_CONSTANT_MERGE:

diff --git a/src/theory/bv/macro_rewrite_elaborator.cpp b/src/theory/bv/macro_rewrite_elaborator.cpp
@@ -49,7 +49,6 @@ bool MacroRewriteElaborator::ensureProofFor(CDProof* cdp,
       return ensureProofForExtractConcat(cdp, eq);
     case ProofRewriteRule::MACRO_BV_MULT_SLT_MULT:
       return ensureProofForMultSltMult(cdp, eq);
-    case ProofRewriteRule::MACRO_BV_AND_OR_XOR_CONCAT_PULLUP:break;
     default: break;
   }
   return false;