mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-04 17:35:17 +00:00
Code Activity

Deprecate injectivity_tactic.cpp: forward mk_injectivity_tactic to simplifier-based impl

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-12 05:32:32 +00:00
parent c303b56f04
commit 995e0e1f14
2 changed files with 1 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/core/CMakeLists.txt
View file

@ -6,7 +6,6 @@ z3_add_component(core_tactics
ctx_simplify_tactic.cpp ctx_simplify_tactic.cpp
elim_term_ite_tactic.cpp elim_term_ite_tactic.cpp
elim_uncnstr_tactic.cpp elim_uncnstr_tactic.cpp
injectivity_tactic.cpp
nnf_tactic.cpp nnf_tactic.cpp
occf_tactic.cpp occf_tactic.cpp
pb_preprocess_tactic.cpp pb_preprocess_tactic.cpp

5
src/tactic/core/injectivity_tactic.h
View file

@ -50,9 +50,7 @@ Tactic Documentation:
class ast_manager; class ast_manager;
class tactic; class tactic;
tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p = params_ref()); inline 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()) {
return alloc(dependent_expr_state_tactic, m, p, return alloc(dependent_expr_state_tactic, m, p,
[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
return alloc(injectivity_simplifier, m, p, s); 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("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)") ADD_SIMPLIFIER("injectivity", "Identifies and applies injectivity axioms.", "alloc(injectivity_simplifier, m, p, s)")
*/ */