From 0cc4afa09729e47dc12fd4b514fd7979d681b9cb Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 21 Feb 2026 23:50:32 +0000
Subject: [PATCH] Add bvarray2uf_simplifier: convert tactic to simplifier

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/tactic/bv/bvarray2uf_simplifier.h | 66 +++++++++++++++++++++++++++
 src/tactic/bv/bvarray2uf_tactic.h     | 13 ++++++
 2 files changed, 79 insertions(+)
 create mode 100644 src/tactic/bv/bvarray2uf_simplifier.h

diff --git a/src/tactic/bv/bvarray2uf_simplifier.h b/src/tactic/bv/bvarray2uf_simplifier.h
new file mode 100644
index 000000000..df837bc5c
--- /dev/null
+++ b/src/tactic/bv/bvarray2uf_simplifier.h
@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    bvarray2uf_simplifier.h
+
+Abstract:
+
+    Simplifier that rewrites bit-vector arrays into bit-vector
+    (uninterpreted) functions.
+
+Author:
+
+    Christoph (cwinter) 2015-11-04
+
+--*/
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/converters/generic_model_converter.h"
+#include "tactic/bv/bvarray2uf_rewriter.h"
+
+class bvarray2uf_simplifier : public dependent_expr_simplifier {
+    bvarray2uf_rewriter         m_rw;
+    generic_model_converter_ref m_fmc;
+
+public:
+    bvarray2uf_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls)
+        : dependent_expr_simplifier(m, fmls),
+          m_rw(m, p),
+          m_fmc(alloc(generic_model_converter, m, "bvarray2uf")) {
+        m_rw.set_mcs(m_fmc.get());
+    }
+
+    char const* name() const override { return "bvarray2uf"; }
+
+    // bvarray2uf_rewriter does not support proofs
+    bool supports_proofs() const override { return false; }
+
+    void reduce() override {
+        m_rw.reset();
+        m_fmc = alloc(generic_model_converter, m, "bvarray2uf");
+        m_rw.set_mcs(m_fmc.get());
+
+        expr_ref  new_curr(m);
+        proof_ref new_pr(m);
+        for (unsigned idx : indices()) {
+            auto const& d = m_fmls[idx];
+            m_rw(d.fml(), new_curr, new_pr);
+            m_fmls.update(idx, dependent_expr(m, new_curr, nullptr, d.dep()));
+        }
+
+        // Add extra assertions generated by the rewriter (e.g., injectivity lemmas)
+        for (expr* a : m_rw.m_cfg.extra_assertions)
+            m_fmls.add(dependent_expr(m, a, nullptr, nullptr));
+
+        // Register model converter entries for array-to-UF model reconstruction
+        for (auto const& entry : m_fmc->entries()) {
+            if (entry.m_instruction == generic_model_converter::instruction::HIDE)
+                m_fmls.model_trail().hide(entry.m_f);
+            else if (entry.m_instruction == generic_model_converter::instruction::ADD)
+                m_fmls.model_trail().push(entry.m_f, entry.m_def, nullptr, {});
+        }
+    }
+};
diff --git a/src/tactic/bv/bvarray2uf_tactic.h b/src/tactic/bv/bvarray2uf_tactic.h
index 393ab164c..c5d4d3a03 100644
--- a/src/tactic/bv/bvarray2uf_tactic.h
+++ b/src/tactic/bv/bvarray2uf_tactic.h
@@ -32,12 +32,25 @@ Tactic that rewrites bit-vector arrays into bit-vector
 #pragma once
 
 #include "util/params.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "tactic/bv/bvarray2uf_simplifier.h"
+
 class ast_manager;
 class tactic;
 
 tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+inline tactic * mk_bvarray2uf2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p,
+        [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
+            return alloc(bvarray2uf_simplifier, m, p, s);
+        });
+}
+
 /*
     ADD_TACTIC("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf_tactic(m, p)")
+    ADD_TACTIC("bvarray2uf2", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf2_tactic(m, p)")
+    ADD_SIMPLIFIER("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "alloc(bvarray2uf_simplifier, m, p, s)")
 */