Add necessary BV macro rewrites and their elaboration

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

Hide file tree

Showing 8 changed files with 655 additions and 1 deletion.
diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h
@@ -3011,6 +3011,136 @@ enum ENUM(ProofRewriteRule)
    * \endverbatim
    */
   EVALUE(DT_MATCH_ELIM),
+  /**
+   * \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),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Bitvectors -- Extract negations from multiplicands**

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -654,6 +654,8 @@ libcvc5_add_sources(
   theory/bv/bv_solver_bitblast_internal.h
   theory/bv/int_blaster.cpp
   theory/bv/int_blaster.h
+  theory/bv/macro_rewrite_elaborator.cpp
+  theory/bv/macro_rewrite_elaborator.h
   theory/bv/proof_checker.cpp
   theory/bv/proof_checker.h
   theory/bv/theory_bv.cpp

diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp
@@ -285,6 +285,25 @@ const char* toString(cvc5::ProofRewriteRule rule)
     case ProofRewriteRule::DT_COLLAPSE_UPDATER: return "dt-collapse-updater";
     case ProofRewriteRule::DT_UPDATER_ELIM: return "dt-updater-elim";
     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:
+      return "macro-bv-concat-extract-merge";
+    case ProofRewriteRule::MACRO_BV_CONCAT_CONSTANT_MERGE:
+      return "macro-bv-concat-constant-merge";
     case ProofRewriteRule::MACRO_BV_EQ_SOLVE: return "macro-bv-eq-solve";
     case ProofRewriteRule::BV_UMULO_ELIMINATE: return "bv-umulo-eliminate";
     case ProofRewriteRule::BV_SMULO_ELIMINATE: return "bv-smulo-eliminate";

diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp
@@ -59,7 +59,8 @@ std::ostream& operator<<(std::ostream& os, TheoryRewriteMode tm)
   return os;
 }
 
-BasicRewriteRCons::BasicRewriteRCons(Env& env) : EnvObj(env)
+BasicRewriteRCons::BasicRewriteRCons(Env& env) : EnvObj(env),
+      d_bvRewElab(env)
 {
 
 }
@@ -297,6 +298,18 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite(CDProof* cdp,
         handledMacro = true;
       }
       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:
+      handledMacro = d_bvRewElab.ensureProofFor(cdp, id, eq);
+      break;
     default: break;
   }
   if (handledMacro)

diff --git a/src/rewriter/basic_rewrite_rcons.h b/src/rewriter/basic_rewrite_rcons.h
@@ -27,6 +27,7 @@
 #include "smt/env_obj.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
+#include "theory/bv/macro_rewrite_elaborator.h"
 
 namespace cvc5::internal {
 namespace rewriter {
@@ -357,6 +358,8 @@ class BasicRewriteRCons : protected EnvObj
   bool tryTheoryRewrite(CDProof* cdp,
                         const Node& eq,
                         theory::TheoryRewriteCtx ctx);
+  /** The BV rewrite elaborator */
+  theory::bv::MacroRewriteElaborator d_bvRewElab;
 };
 
 }  // namespace rewriter