From ff7cc0f59ea1b86264e2e667eeb174454d81c273 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 26 Feb 2026 20:07:42 +0000 Subject: [PATCH] Remove old blast-term-ite tactic class, rename blast-term-ite2 to blast-term-ite Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- .../simplifiers/blast_term_ite_simplifier.h | 19 ++ src/tactic/core/blast_term_ite_tactic.cpp | 200 +----------------- src/tactic/core/blast_term_ite_tactic.h | 6 +- 3 files changed, 23 insertions(+), 202 deletions(-) diff --git a/src/ast/simplifiers/blast_term_ite_simplifier.h b/src/ast/simplifiers/blast_term_ite_simplifier.h index 682523038..977b6c586 100644 --- a/src/ast/simplifiers/blast_term_ite_simplifier.h +++ b/src/ast/simplifiers/blast_term_ite_simplifier.h @@ -15,6 +15,7 @@ Author: #include "ast/simplifiers/dependent_expr_state.h" #include "ast/rewriter/rewriter_def.h" +#include "ast/scoped_proof.h" #include "params/tactic_params.hpp" @@ -116,4 +117,22 @@ public: m_fmls.update(idx, dependent_expr(m, new_fml, mp(d.pr(), new_pr), d.dep())); } } + + static void blast_term_ite(expr_ref& fml, unsigned max_inflation) { + ast_manager& m = fml.get_manager(); + scoped_no_proof _sp(m); + params_ref p; + rw ite_rw(m, p); + ite_rw.m_cfg.m_max_inflation = max_inflation; + if (max_inflation < UINT_MAX) + ite_rw.m_cfg.m_init_term_size = get_num_exprs(fml); + try { + expr_ref tmp(m); + ite_rw(fml, tmp); + fml = tmp; + } + catch (z3_exception &) { + // max steps exceeded. + } + } }; diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index 45ea00045..f35a12668 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -14,203 +14,9 @@ Author: Nikolaj Bjorner (nbjorner) 2013-11-4 --*/ -#include "ast/normal_forms/defined_names.h" -#include "ast/rewriter/rewriter_def.h" -#include "ast/scoped_proof.h" -#include "tactic/tactical.h" -#include "params/tactic_params.hpp" - - - -// -// (f (if c1 (if c2 e1 e2) e3) b c) -> -// (if c1 (if c2 (f e1 b c) -// - - -class blast_term_ite_tactic : public tactic { - - struct rw_cfg : public default_rewriter_cfg { - ast_manager& m; - unsigned long long m_max_memory; // in bytes - unsigned m_num_fresh; // number of expansions - 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_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - 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()); // multiplicative factor of initial term size. - } - - - - bool max_steps_exceeded(unsigned num_steps) const { - // if (memory::get_allocation_size() > m_max_memory) - // throw tactic_exception(TACTIC_MAX_MEMORY_MSG); - 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) { - } - }; - - struct imp { - ast_manager & m; - rw m_rw; - - imp(ast_manager & _m, params_ref const & p): - m(_m), - m_rw(m, p) { - } - - void updt_params(params_ref const & p) { - m_rw.m_cfg.updt_params(p); - } - - void operator()(goal_ref const & g, goal_ref_buffer & result) { - tactic_report report("blast-term-ite", *g); - expr_ref new_curr(m); - proof_ref new_pr(m); - unsigned num_fresh = 0; - unsigned idx = 0; - for (auto [curr, dep, pr] : *g) { - if (m_rw.m_cfg.m_max_inflation < UINT_MAX) { - m_rw.m_cfg.m_init_term_size = get_num_exprs(curr); - num_fresh += m_rw.m_cfg.m_num_fresh; - m_rw.m_cfg.m_num_fresh = 0; - } - m_rw(curr, new_curr, new_pr); - new_pr = m.mk_modus_ponens(pr, new_pr); - g->update(idx++, new_curr, new_pr, dep); - } - - report_tactic_progress(":blast-term-ite-consts", m_rw.m_cfg.m_num_fresh + num_fresh); - g->inc_depth(); - result.push_back(g.get()); - } - }; - - imp * m_imp; - params_ref m_params; -public: - blast_term_ite_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(blast_term_ite_tactic, m, m_params); - } - - ~blast_term_ite_tactic() override { - dealloc(m_imp); - } - - char const* name() const override { return "blast_term_ite"; } - - void updt_params(params_ref const & p) override { - m_params.append(p); - m_imp->m_rw.m_cfg.updt_params(m_params); - } - - void collect_param_descrs(param_descrs & r) override { - insert_max_memory(r); - insert_max_steps(r); - r.insert("max_inflation", CPK_UINT, "(default: infinity) multiplicative factor of initial term size.", "4294967295"); - } - - void operator()(goal_ref const & in, goal_ref_buffer & result) override { - (*m_imp)(in, result); - } - - void cleanup() override { - ast_manager & m = m_imp->m; - dealloc(m_imp); - m_imp = alloc(imp, m, m_params); - } - - static void blast_term_ite(expr_ref& fml, unsigned max_inflation) { - ast_manager& m = fml.get_manager(); - scoped_no_proof _sp(m); - params_ref p; - rw ite_rw(m, p); - ite_rw.m_cfg.m_max_inflation = max_inflation; - if (max_inflation < UINT_MAX) { - ite_rw.m_cfg.m_init_term_size = get_num_exprs(fml); - } - try { - expr_ref tmp(m); - ite_rw(fml, tmp); - fml = tmp; - } - catch (z3_exception &) { - // max steps exceeded. - } - } -}; - -tactic * mk_blast_term_ite_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(blast_term_ite_tactic, m, p)); -} +#include "tactic/core/blast_term_ite_tactic.h" void blast_term_ite(expr_ref& fml, unsigned max_inflation) { - blast_term_ite_tactic::blast_term_ite(fml, max_inflation); + blast_term_ite_simplifier::blast_term_ite(fml, max_inflation); } + diff --git a/src/tactic/core/blast_term_ite_tactic.h b/src/tactic/core/blast_term_ite_tactic.h index cb0ec259f..c1233953a 100644 --- a/src/tactic/core/blast_term_ite_tactic.h +++ b/src/tactic/core/blast_term_ite_tactic.h @@ -48,11 +48,8 @@ Use `elim-term-ite` elsewhere when possible. #include "tactic/tactic.h" #include "tactic/dependent_expr_state_tactic.h" #include "ast/simplifiers/blast_term_ite_simplifier.h" -class ast_manager; -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()) { +inline tactic * mk_blast_term_ite_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); @@ -61,7 +58,6 @@ inline tactic * mk_blast_term_ite2_tactic(ast_manager & m, params_ref const & p /* 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)") */