From 995e0e1f145fcf19384b08b437905a12cafc8a2c Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Mar 2026 05:32:32 +0000 Subject: [PATCH] Deprecate injectivity_tactic.cpp: forward mk_injectivity_tactic to simplifier-based impl Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/core/CMakeLists.txt | 1 - src/tactic/core/injectivity_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 69c60bc7d..8ab41f155 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -6,7 +6,6 @@ z3_add_component(core_tactics ctx_simplify_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp - injectivity_tactic.cpp nnf_tactic.cpp occf_tactic.cpp pb_preprocess_tactic.cpp diff --git a/src/tactic/core/injectivity_tactic.h b/src/tactic/core/injectivity_tactic.h index d0bdfa283..06a841fe6 100644 --- a/src/tactic/core/injectivity_tactic.h +++ b/src/tactic/core/injectivity_tactic.h @@ -50,9 +50,7 @@ Tactic Documentation: class ast_manager; class tactic; -tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p = params_ref()); - -inline tactic* mk_injectivity2_tactic(ast_manager& m, params_ref const& p = params_ref()) { +inline tactic* mk_injectivity_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(injectivity_simplifier, m, p, s); @@ -61,7 +59,6 @@ inline tactic* mk_injectivity2_tactic(ast_manager& m, params_ref const& p = para /* ADD_TACTIC("injectivity", "Identifies and applies injectivity axioms.", "mk_injectivity_tactic(m, p)") - ADD_TACTIC("injectivity2", "Identifies and applies injectivity axioms.", "mk_injectivity2_tactic(m, p)") ADD_SIMPLIFIER("injectivity", "Identifies and applies injectivity axioms.", "alloc(injectivity_simplifier, m, p, s)") */