mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-05 01:45:15 +00:00
Code Activity

Remove old mk_factor_tactic, rename factor2 to factor

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:12 +00:00
parent 42d3a13ddf
commit 4f6c0637fc
3 changed files with 3 additions and 328 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/tactic/arith/factor_tactic.h
View file

@ -37,17 +37,12 @@ Factor polynomials in equalities and inequalities.
#include "tactic/dependent_expr_state_tactic.h"
#include "ast/simplifiers/factor_simplifier.h"
class ast_manager;
tactic * mk_factor_tactic(ast_manager & m, params_ref const & p = params_ref());
inline tactic * mk_factor2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
inline tactic * mk_factor_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(factor_simplifier, m, p, s); });
}
/*
ADD_TACTIC("factor", "polynomial factorization.", "mk_factor_tactic(m, p)")
ADD_TACTIC("factor2", "polynomial factorization.", "mk_factor2_tactic(m, p)")
ADD_SIMPLIFIER("factor", "polynomial factorization.", "mk_factor_simplifier(m, p, s)")
*/