From 6bd009ed6a635d239957e75e1b5c0bc835ff4234 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 21 Feb 2026 23:25:53 +0000 Subject: [PATCH 1/4] Initial plan 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 2/4] 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)") */ From d9d712f1d049de2f3a7b9de279fcb6d7e72117aa Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 22 Feb 2026 00:43:36 +0000 Subject: [PATCH 3/4] Remove old bvarray2uf_tactic implementation; use simplifier as basis Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/bv/CMakeLists.txt | 1 - src/tactic/bv/bvarray2uf_tactic.h | 6 ++---- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt index 9009e6fa5..d5920b88e 100644 --- a/src/tactic/bv/CMakeLists.txt +++ b/src/tactic/bv/CMakeLists.txt @@ -4,7 +4,6 @@ z3_add_component(bv_tactics bit_blaster_tactic.cpp bv1_blaster_tactic.cpp bvarray2uf_rewriter.cpp - bvarray2uf_tactic.cpp bv_bound_chk_tactic.cpp bv_bounds_tactic.cpp bv_size_reduction_tactic.cpp diff --git a/src/tactic/bv/bvarray2uf_tactic.h b/src/tactic/bv/bvarray2uf_tactic.h index c5d4d3a03..d71752853 100644 --- a/src/tactic/bv/bvarray2uf_tactic.h +++ b/src/tactic/bv/bvarray2uf_tactic.h @@ -32,15 +32,14 @@ Tactic that rewrites bit-vector arrays into bit-vector #pragma once #include "util/params.h" +#include "tactic/tactic.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()) { +inline tactic * mk_bvarray2uf_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); @@ -49,7 +48,6 @@ inline tactic * mk_bvarray2uf2_tactic(ast_manager & m, params_ref const & p = pa /* 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)") */ From 1d2a76d27b20d918bc155495de9c31a011182228 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 22 Feb 2026 08:57:39 +0000 Subject: [PATCH 4/4] Delete bvarray2uf_tactic.cpp (removed from CMakeLists.txt) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/bv/bvarray2uf_tactic.cpp | 144 ---------------------------- 1 file changed, 144 deletions(-) delete mode 100644 src/tactic/bv/bvarray2uf_tactic.cpp diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp deleted file mode 100644 index 58a1e6238..000000000 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ /dev/null @@ -1,144 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - - bvarray2uf_tactic.cpp - -Abstract: - - Tactic that rewrites bit-vector arrays into bit-vector - (uninterpreted) functions. - -Author: - - Christoph (cwinter) 2015-11-04 - -Notes: - ---*/ -#include "tactic/tactical.h" -#include "ast/bv_decl_plugin.h" -#include "ast/rewriter/expr_replacer.h" -#include "ast/converters/generic_model_converter.h" -#include "ast/ast_smt2_pp.h" - -#include "tactic/bv/bvarray2uf_tactic.h" -#include "tactic/bv/bvarray2uf_rewriter.h" - -class bvarray2uf_tactic : public tactic { - - struct imp { - ast_manager & m_manager; - bool m_produce_cores; - bvarray2uf_rewriter m_rw; - - ast_manager & m() { return m_manager; } - - imp(ast_manager & m, params_ref const & p) : - m_manager(m), - m_produce_cores(false), - m_rw(m, p) { - updt_params(p); - } - - - void checkpoint() { - if (!m_manager.inc()) - throw tactic_exception(m_manager.limit().get_cancel_msg()); - } - - void operator()(goal_ref const & g, - goal_ref_buffer & result) - { - tactic_report report("bvarray2uf", *g); - result.reset(); - fail_if_unsat_core_generation("bvarray2uf", g); - // bvarray2uf_rewriter does not support proofs (yet). - fail_if_proof_generation("bvarray2uf", g); - - bool produce_models = g->models_enabled(); - bool produce_proofs = g->proofs_enabled(); - model_converter_ref mc; - - if (produce_models) { - generic_model_converter * fmc = alloc(generic_model_converter, m_manager, "bvarray2uf"); - mc = fmc; - m_rw.set_mcs(fmc); - } - - - m_rw.reset(); - expr_ref new_curr(m_manager); - proof_ref new_pr(m_manager); - unsigned size = g->size(); - for (unsigned idx = 0; idx < size; ++idx) { - if (g->inconsistent()) - break; - expr* curr = g->form(idx); - m_rw(curr, new_curr, new_pr); - if (produce_proofs) { - proof * pr = g->pr(idx); - new_pr = m_manager.mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); - } - - for (expr* a : m_rw.m_cfg.extra_assertions) - g->assert_expr(a); - - g->inc_depth(); - g->add(mc.get()); - result.push_back(g.get()); - } - - void updt_params(params_ref const & p) { - } - }; - - imp * m_imp; - params_ref m_params; - -public: - bvarray2uf_tactic(ast_manager & m, params_ref const & p) : - m_params(p) { - m_imp = alloc(imp, m, p); - } - - tactic * translate(ast_manager & m) override { - return alloc(bvarray2uf_tactic, m, m_params); - } - - ~bvarray2uf_tactic() override { - dealloc(m_imp); - } - - char const* name() const override { return "bvarray2uf"; } - - void updt_params(params_ref const & p) override { - m_params.append(p); - m_imp->updt_params(m_params); - } - - void collect_param_descrs(param_descrs & r) override { - insert_produce_models(r); - } - - void operator()(goal_ref const & in, - goal_ref_buffer & result) override { - (*m_imp)(in, result); - } - - void cleanup() override { - ast_manager & m = m_imp->m(); - imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); - dealloc(d); - } - -}; - - -tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(bvarray2uf_tactic, m, p)); -}