mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-08 10:00:56 +00:00
Code Activity

Remove old cofactor_term_ite_tactic.cpp, use simplifier-based implementation

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-22 00:45:44 +00:00
parent c18db6080a
commit b6e63f06fd
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

@ -2,7 +2,6 @@ z3_add_component(core_tactics
SOURCES SOURCES
blast_term_ite_tactic.cpp blast_term_ite_tactic.cpp
cofactor_elim_term_ite.cpp cofactor_elim_term_ite.cpp
cofactor_term_ite_tactic.cpp
collect_statistics_tactic.cpp collect_statistics_tactic.cpp
ctx_simplify_tactic.cpp ctx_simplify_tactic.cpp
der_tactic.cpp der_tactic.cpp

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

@ -71,15 +71,12 @@ inline dependent_expr_simplifier* mk_cofactor_term_ite_simplifier(
return alloc(cofactor_term_ite_simplifier, m, p, 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()) { 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); 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-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)") ADD_SIMPLIFIER("cofactor-term-ite", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite_simplifier(m, p, s)")
*/ */