Setup

src/CMakeLists.txt

@@ -656,6 +656,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

src/rewriter/basic_rewrite_rcons.cpp

@@ -68,7 +68,8 @@ BasicRewriteRCons::BasicRewriteRCons(Env& env)
     : EnvObj(env),
       d_theoryRewriteMacroExpand(
           statisticsRegistry().registerHistogram<ProofRewriteRule>(
-              "BasicRewriteRCons::macroExpandCount"))
+              "BasicRewriteRCons::macroExpandCount")),
+              d_bvRewElab(env)
 {
 
 }
@@ -354,6 +355,19 @@ 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:
+    case ProofRewriteRule::MACRO_BV_FLATTEN_ASSOC_COMMUT:
+      handledMacro = d_bvRewElab.ensureProofFor(cdp, id, eq);
+      break;
     default: break;
   }
   if (handledMacro)

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 {
@@ -451,6 +452,8 @@ class BasicRewriteRCons : protected EnvObj
    * expanded in macro elimination by this class.
    */
   HistogramStat<ProofRewriteRule> d_theoryRewriteMacroExpand;
+  /** The BV rewrite elaborator */
+  theory::bv::MacroRewriteElaborator d_bvRewElab;
 };
 
 }  // namespace rewriter

src/theory/bv/macro_rewrite_elaborator.cpp

@@ -0,0 +1,50 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Methods for elaborating MACRO_BV_* proof rewrites.
+ */
+
+#include "theory/bv/macro_rewrite_elaborator.h"
+
+namespace cvc5::internal {
+namespace theory {
+namespace bv {
+
+MacroRewriteElaborator::MacroRewriteElaborator(Env& env) : EnvObj(env){}
+MacroRewriteElaborator::~MacroRewriteElaborator() {}
+bool MacroRewriteElaborator::ensureProofFor(CDProof* cdp,
+                                  ProofRewriteRule id,
+                                  const Node& eq)
+{
+  switch (id)
+  {
+    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:
+    case ProofRewriteRule::MACRO_BV_FLATTEN_ASSOC_COMMUT:
+      break;
+    default:
+      break;
+  }
+  return false;
+}
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace cvc5::internal

src/theory/bv/macro_rewrite_elaborator.h

@@ -0,0 +1,55 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Methods for elaborating MACRO_BV_* proof rewrites.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__BV__MACRO_REWRITE_ELABORATOR_H
+#define CVC5__THEORY__BV__MACRO_REWRITE_ELABORATOR_H
+
+#include "proof/proof.h"
+#include "smt/env_obj.h"
+
+namespace cvc5::internal {
+namespace theory {
+namespace bv {
+
+/**
+ * Methods for elaborating MACRO_BV_* proof rewrites. This class is called during
+ * RARE proof reconstruction.
+ */
+class MacroRewriteElaborator : protected EnvObj
+{
+ public:
+  /** Constructor */
+  MacroRewriteElaborator(Env& env);
+  ~MacroRewriteElaborator();
+  /**
+   * Elaborate a rewrite eq that was proven by a macro rewrite rule.
+   *
+   * @param cdp The proof to add to.
+   * @param id The (macro) rewrite id that proved the rewrite.
+   * @param eq The rewrite proven.
+   * @return true if added a closed proof of eq to cdp.
+   */
+  bool ensureProofFor(CDProof* cdp,
+                                   ProofRewriteRule id,
+                                   const Node& eq);
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace cvc5::internal
+
+#endif /* CVC5__THEORY__BV__MACRO_REWRITE_ELABORATOR_H */