From 7390a9b856d160111775bc1cd729fe75669cdd95 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 26 Feb 2026 03:51:42 +0000 Subject: [PATCH] Convert blast-term-ite tactic to also expose as a simplifier Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/simplifiers/CMakeLists.txt | 1 + .../simplifiers/blast_term_ite_simplifier.h | 119 ++++++++++++++++++ src/tactic/core/blast_term_ite_tactic.h | 13 +- 3 files changed, 132 insertions(+), 1 deletion(-) create mode 100644 src/ast/simplifiers/blast_term_ite_simplifier.h diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index 988c1ba3b..356944281 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -33,6 +33,7 @@ z3_add_component(simplifiers TACTIC_HEADERS bit_blaster.h bit2int.h + blast_term_ite_simplifier.h elim_bounds.h elim_term_ite.h pull_nested_quantifiers.h diff --git a/src/ast/simplifiers/blast_term_ite_simplifier.h b/src/ast/simplifiers/blast_term_ite_simplifier.h new file mode 100644 index 000000000..682523038 --- /dev/null +++ b/src/ast/simplifiers/blast_term_ite_simplifier.h @@ -0,0 +1,119 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + blast_term_ite_simplifier.h + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-4 + +--*/ + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/rewriter/rewriter_def.h" +#include "params/tactic_params.hpp" + + +class blast_term_ite_simplifier : public dependent_expr_simplifier { + + struct rw_cfg : public default_rewriter_cfg { + ast_manager& m; + unsigned m_num_fresh; + unsigned m_max_steps; + unsigned m_max_inflation; + unsigned m_init_term_size; + + rw_cfg(ast_manager& _m, params_ref const& p): + m(_m), + m_num_fresh(0), + m_max_steps(UINT_MAX), + m_max_inflation(UINT_MAX), + m_init_term_size(0) { + updt_params(p); + } + + void updt_params(params_ref const& p) { + tactic_params tp(p); + m_max_steps = p.get_uint("max_steps", tp.blast_term_ite_max_steps()); + m_max_inflation = p.get_uint("max_inflation", tp.blast_term_ite_max_inflation()); + } + + bool max_steps_exceeded(unsigned num_steps) const { + return num_steps >= m_max_steps; + } + + br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { + if (m.is_ite(f)) + return BR_FAILED; + if (m_max_inflation < UINT_MAX && + m_init_term_size > 0 && + m_max_inflation * m_init_term_size < m_num_fresh) + return BR_FAILED; + + for (unsigned i = 0; i < num_args; ++i) { + expr* c, *t, *e; + if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) { + TRACE(blast_term_ite, result = m.mk_app(f, num_args, args); tout << result << "\n";); + expr_ref e1(m), e2(m); + ptr_vector args1(num_args, args); + args1[i] = t; + e1 = m.mk_app(f, num_args, args1.data()); + if (m.are_equal(t, e)) { + result = e1; + return BR_REWRITE1; + } + else { + args1[i] = e; + e2 = m.mk_app(f, num_args, args1.data()); + result = m.mk_ite(c, e1, e2); + ++m_num_fresh; + return BR_REWRITE3; + } + } + } + return BR_FAILED; + } + + bool rewrite_patterns() const { return false; } + + br_status reduce_app(func_decl* f, unsigned num, expr* const* args, expr_ref& result, proof_ref& result_pr) { + return mk_app_core(f, num, args, result); + } + }; + + struct rw : public rewriter_tpl { + rw_cfg m_cfg; + + rw(ast_manager& m, params_ref const& p): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, p) { + } + }; + + rw m_rw; + +public: + blast_term_ite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s): + dependent_expr_simplifier(m, s), m_rw(m, p) {} + + char const* name() const override { return "blast-term-ite"; } + + void reduce() override { + expr_ref new_fml(m); + proof_ref new_pr(m); + for (unsigned idx : indices()) { + auto const& d = m_fmls[idx]; + if (m_rw.m_cfg.m_max_inflation < UINT_MAX) { + m_rw.m_cfg.m_init_term_size = get_num_exprs(d.fml()); + m_rw.m_cfg.m_num_fresh = 0; + } + m_rw(d.fml(), new_fml, new_pr); + if (d.fml() != new_fml) + m_fmls.update(idx, dependent_expr(m, new_fml, mp(d.pr(), new_pr), d.dep())); + } + } +}; diff --git a/src/tactic/core/blast_term_ite_tactic.h b/src/tactic/core/blast_term_ite_tactic.h index a322b8e11..cb0ec259f 100644 --- a/src/tactic/core/blast_term_ite_tactic.h +++ b/src/tactic/core/blast_term_ite_tactic.h @@ -45,13 +45,24 @@ Use `elim-term-ite` elsewhere when possible. #pragma once #include "util/params.h" +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/blast_term_ite_simplifier.h" class ast_manager; -class tactic; tactic * mk_blast_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref()); +inline tactic * mk_blast_term_ite2_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(blast_term_ite_simplifier, m, p, s); + }); +} + /* ADD_TACTIC("blast-term-ite", "blast term if-then-else by hoisting them.", "mk_blast_term_ite_tactic(m, p)") + ADD_TACTIC("blast-term-ite2", "blast term if-then-else by hoisting them.", "mk_blast_term_ite2_tactic(m, p)") + ADD_SIMPLIFIER("blast-term-ite", "blast term if-then-else by hoisting them.", "alloc(blast_term_ite_simplifier, m, p, s)") */ void blast_term_ite(expr_ref& fml, unsigned max_inflation);