From e8db5204c028bb9c05bbca34aecb4bd3e216b97b 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:15 +0000 Subject: [PATCH 1/4] Initial plan From c18db6080a8e62800aab17f163957822c8007010 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 21 Feb 2026 23:52:01 +0000 Subject: [PATCH 2/4] Convert cofactor-term-ite tactic to also expose as a simplifier Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/core/cofactor_term_ite_tactic.h | 52 ++++++++++++++++++++-- 1 file changed, 49 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/cofactor_term_ite_tactic.h b/src/tactic/core/cofactor_term_ite_tactic.h index 68568c8ce..0cb9f9142 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.h +++ b/src/tactic/core/cofactor_term_ite_tactic.h @@ -29,11 +29,57 @@ It hoists nested if-then-else expressions inside terms into the top level of the #pragma once #include "util/params.h" -class ast_manager; -class tactic; +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/dependent_expr_state.h" +#include "tactic/core/cofactor_elim_term_ite.h" + +class cofactor_term_ite_simplifier : public dependent_expr_simplifier { + params_ref m_params; + cofactor_elim_term_ite m_elim_ite; + +public: + cofactor_term_ite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s) + : dependent_expr_simplifier(m, s), m_params(p), m_elim_ite(m, p) {} + + char const* name() const override { return "cofactor-term-ite"; } + + void updt_params(params_ref const& p) override { + m_params.append(p); + m_elim_ite.updt_params(m_params); + } + + void collect_param_descrs(param_descrs& r) override { + m_elim_ite.collect_param_descrs(r); + } + + bool supports_proofs() const override { return false; } + + void reduce() override { + expr_ref new_fml(m); + for (unsigned idx : indices()) { + auto const& d = m_fmls[idx]; + m_elim_ite(d.fml(), new_fml); + if (new_fml != d.fml()) + m_fmls.update(idx, dependent_expr(m, new_fml, nullptr, d.dep())); + } + } +}; + +inline dependent_expr_simplifier* mk_cofactor_term_ite_simplifier( + ast_manager& m, params_ref const& p, dependent_expr_state& s) { + return alloc(cofactor_term_ite_simplifier, m, p, s); +} + +inline tactic* mk_cofactor_term_ite2_tactic(ast_manager& m, params_ref const& p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, mk_cofactor_term_ite_simplifier); +} tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref()); + /* - ADD_TACTIC("cofactor-term-ite", "eliminate term if-the-else using cofactors.", "mk_cofactor_term_ite_tactic(m, p)") + ADD_TACTIC("cofactor-term-ite", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite_tactic(m, p)") + ADD_TACTIC("cofactor-term-ite2", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite2_tactic(m, p)") + ADD_SIMPLIFIER("cofactor-term-ite", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite_simplifier(m, p, s)") */ From b6e63f06fdfecb8ab3f9e768928995830b8b530a Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 22 Feb 2026 00:45:44 +0000 Subject: [PATCH 3/4] Remove old cofactor_term_ite_tactic.cpp, use simplifier-based implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/core/CMakeLists.txt | 1 - src/tactic/core/cofactor_term_ite_tactic.h | 5 +---- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index a191b6251..8f57e5bbf 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(core_tactics SOURCES blast_term_ite_tactic.cpp cofactor_elim_term_ite.cpp - cofactor_term_ite_tactic.cpp collect_statistics_tactic.cpp ctx_simplify_tactic.cpp der_tactic.cpp diff --git a/src/tactic/core/cofactor_term_ite_tactic.h b/src/tactic/core/cofactor_term_ite_tactic.h index 0cb9f9142..a22edb087 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.h +++ b/src/tactic/core/cofactor_term_ite_tactic.h @@ -71,15 +71,12 @@ inline dependent_expr_simplifier* mk_cofactor_term_ite_simplifier( return alloc(cofactor_term_ite_simplifier, m, p, s); } -inline tactic* mk_cofactor_term_ite2_tactic(ast_manager& m, params_ref const& p = params_ref()) { +inline tactic* mk_cofactor_term_ite_tactic(ast_manager& m, params_ref const& p = params_ref()) { return alloc(dependent_expr_state_tactic, m, p, mk_cofactor_term_ite_simplifier); } -tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref()); - /* ADD_TACTIC("cofactor-term-ite", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite_tactic(m, p)") - ADD_TACTIC("cofactor-term-ite2", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite2_tactic(m, p)") ADD_SIMPLIFIER("cofactor-term-ite", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite_simplifier(m, p, s)") */ From afbd038924143a06722f905c80b6552fd6d0e253 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 23 Feb 2026 03:57:37 +0000 Subject: [PATCH 4/4] Delete cofactor_term_ite_tactic.cpp Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/core/cofactor_term_ite_tactic.cpp | 71 -------------------- 1 file changed, 71 deletions(-) delete mode 100644 src/tactic/core/cofactor_term_ite_tactic.cpp diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp deleted file mode 100644 index c46e5d9f2..000000000 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ /dev/null @@ -1,71 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - cofactor_term_ite_tactic.cpp - -Abstract: - - Wrap cofactor_elim_term_ite as a tactic. - Eliminate (ground) term if-then-else's using cofactors. - -Author: - - Leonardo de Moura (leonardo) 2012-02-20. - -Revision History: - ---*/ -#include "tactic/tactical.h" -#include "tactic/core/cofactor_elim_term_ite.h" - -/** - \brief Wrapper for applying cofactor_elim_term_ite in an assertion set. - */ -class cofactor_term_ite_tactic : public tactic { - params_ref m_params; - cofactor_elim_term_ite m_elim_ite; - - void process(goal & g) { - ast_manager & m = g.m(); - unsigned idx = 0; - for (const auto& [f, dep, pr] : g) { - if (g.inconsistent()) - break; - expr_ref new_f(m); - m_elim_ite(f, new_f); - g.update(idx++, new_f, nullptr, dep); - } - } - -public: - cofactor_term_ite_tactic(ast_manager & m, params_ref const & p): - m_params(p), - m_elim_ite(m, p) { - } - - tactic * translate(ast_manager & m) override { - return alloc(cofactor_term_ite_tactic, m, m_params); - } - - char const* name() const override { return "cofactor"; } - void updt_params(params_ref const & p) override { m_params.append(p); m_elim_ite.updt_params(m_params); } - void collect_param_descrs(param_descrs & r) override { m_elim_ite.collect_param_descrs(r); } - - void operator()(goal_ref const & g, goal_ref_buffer& result) override { - fail_if_proof_generation("cofactor-term-ite", g); - fail_if_unsat_core_generation("cofactor-term-ite", g); - tactic_report report("cofactor-term-ite", *g); - process(*(g.get())); - g->inc_depth(); - result.push_back(g.get()); - } - - void cleanup() override { return m_elim_ite.cleanup(); } - -}; - -tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(cofactor_term_ite_tactic, m, p)); -}