More

ajreynol · Feb 24, 2025 · f161b06 · f161b06
1 parent 81525a7
commit f161b06
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 1 deletion.
diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h
@@ -3149,69 +3149,129 @@ enum ENUM(ProofRewriteRule)
    * \verbatim embed:rst:leading-asterisk
    * **Bitvectors -- Macro extract and concat **
    *
+   * .. math::
+   *    a = b
+   *
+   * where :math:`a` is rewritten to :math:`b` by the internal rewrite
+   * rule ExtractConcat.
+   *
    * \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 **
    *
+   * .. math::
+   *    a = b
+   *
+   * where :math:`a` is rewritten to :math:`b` by the internal rewrite
+   * rule OrSimplify.
+   *
    * \endverbatim
    */
   EVALUE(MACRO_BV_OR_SIMPLIFY),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Bitvectors -- Macro and simplify **
    *
+   * .. math::
+   *    a = b
+   *
+   * where :math:`a` is rewritten to :math:`b` by the internal rewrite
+   * rule AndSimplify.
+   *
    * \endverbatim
    */
   EVALUE(MACRO_BV_AND_SIMPLIFY),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Bitvectors -- Macro xor simplify **
    *
+   * .. math::
+   *    a = b
+   *
+   * where :math:`a` is rewritten to :math:`b` by the internal rewrite
+   * rule XorSimplify.
+   *
    * \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 **
    *
+   * .. math::
+   *    a = b
+   *
+   * where :math:`a` is rewritten to :math:`b` by the internal rewrite
+   * rule MultSltMult.
+   *
    * \endverbatim
    */
   EVALUE(MACRO_BV_MULT_SLT_MULT),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Bitvectors -- Macro concat extract merge **
    *
+   * .. math::
+   *    a = b
+   *
+   * where :math:`a` is rewritten to :math:`b` by the internal rewrite
+   * rule ConcatExtractMerge.
+   *
    * \endverbatim
    */
   EVALUE(MACRO_BV_CONCAT_EXTRACT_MERGE),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Bitvectors -- Macro concat constant merge **
    *
+   * .. math::
+   *    a = b
+   *
+   * where :math:`a` is rewritten to :math:`b` by the internal rewrite
+   * rule ConcatConstantMerge.
+   *
    * \endverbatim
    */
   EVALUE(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;