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] 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)") */