From 886361006f8bbb2b0cfee3d6def0dfd1cee296dc Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 21 Feb 2026 23:25:05 +0000 Subject: [PATCH 1/4] Initial plan From 42d3a13ddff9373631aa46c9c9cbbd0c0969f851 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 21 Feb 2026 23:45:51 +0000 Subject: [PATCH 2/4] Add factor_simplifier and factor2 tactic wrapping the simplifier Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/simplifiers/CMakeLists.txt | 1 + src/ast/simplifiers/factor_simplifier.cpp | 267 ++++++++++++++++++++++ src/ast/simplifiers/factor_simplifier.h | 38 +++ src/tactic/arith/factor_tactic.h | 13 +- 4 files changed, 318 insertions(+), 1 deletion(-) create mode 100644 src/ast/simplifiers/factor_simplifier.cpp create mode 100644 src/ast/simplifiers/factor_simplifier.h diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index d947011ae..988c1ba3b 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -15,6 +15,7 @@ z3_add_component(simplifiers eliminate_predicates.cpp euf_completion.cpp extract_eqs.cpp + factor_simplifier.cpp linear_equation.cpp max_bv_sharing.cpp model_reconstruction_trail.cpp diff --git a/src/ast/simplifiers/factor_simplifier.cpp b/src/ast/simplifiers/factor_simplifier.cpp new file mode 100644 index 000000000..f803ccb3f --- /dev/null +++ b/src/ast/simplifiers/factor_simplifier.cpp @@ -0,0 +1,267 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + factor_simplifier.cpp + +Abstract: + + Polynomial factorization simplifier. + Ported from factor_tactic.cpp by Leonardo de Moura (leonardo) 2012-02-03. + +--*/ + +#include "ast/simplifiers/factor_simplifier.h" +#include "ast/expr2polynomial.h" +#include "ast/arith_decl_plugin.h" +#include "ast/rewriter/rewriter_def.h" +#include "math/polynomial/polynomial.h" + +struct factor_simplifier::rw_cfg : public default_rewriter_cfg { + ast_manager & m; + arith_util m_util; + unsynch_mpq_manager m_qm; + polynomial::manager m_pm; + default_expr2polynomial m_expr2poly; + polynomial::factor_params m_fparams; + bool m_split_factors; + + rw_cfg(ast_manager & _m, params_ref const & p): + m(_m), + m_util(_m), + m_pm(m.limit(), m_qm), + m_expr2poly(m, m_pm) { + updt_params(p); + } + + void updt_params(params_ref const & p) { + m_split_factors = p.get_bool("split_factors", true); + m_fparams.updt_params(p); + } + + expr * mk_mul(unsigned sz, expr * const * args) { + SASSERT(sz > 0); + if (sz == 1) + return args[0]; + return m_util.mk_mul(sz, args); + } + + expr * mk_zero_for(expr * arg) { + return m_util.mk_numeral(rational(0), m_util.is_int(arg)); + } + + // p1^k1 * p2^k2 = 0 --> p1*p2 = 0 + void mk_eq(polynomial::factors const & fs, expr_ref & result) { + expr_ref_buffer args(m); + expr_ref arg(m); + for (unsigned i = 0; i < fs.distinct_factors(); ++i) { + m_expr2poly.to_expr(fs[i], true, arg); + args.push_back(arg); + } + result = m.mk_eq(mk_mul(args.size(), args.data()), mk_zero_for(arg)); + } + + // p1^k1 * p2^k2 = 0 --> p1 = 0 or p2 = 0 + void mk_split_eq(polynomial::factors const & fs, expr_ref & result) { + expr_ref_buffer args(m); + expr_ref arg(m); + for (unsigned i = 0; i < fs.distinct_factors(); ++i) { + m_expr2poly.to_expr(fs[i], true, arg); + args.push_back(m.mk_eq(arg, mk_zero_for(arg))); + } + if (args.size() == 1) + result = args[0]; + else + result = m.mk_or(args); + } + + decl_kind flip(decl_kind k) { + SASSERT(k == OP_LT || k == OP_GT || k == OP_LE || k == OP_GE); + switch (k) { + case OP_LT: return OP_GT; + case OP_LE: return OP_GE; + case OP_GT: return OP_LT; + case OP_GE: return OP_LE; + default: + UNREACHABLE(); + return k; + } + } + + // p1^{2*k1} * p2^{2*k2 + 1} >=< 0 + // --> + // (p1^2)*p2 >=<0 + void mk_comp(decl_kind k, polynomial::factors const & fs, expr_ref & result) { + SASSERT(k == OP_LT || k == OP_GT || k == OP_LE || k == OP_GE); + expr_ref_buffer args(m); + expr_ref arg(m); + for (unsigned i = 0; i < fs.distinct_factors(); ++i) { + m_expr2poly.to_expr(fs[i], true, arg); + if (fs.get_degree(i) % 2 == 0) + arg = m_util.mk_power(arg, m_util.mk_numeral(rational(2), m_util.is_int(arg))); + args.push_back(arg); + } + expr * lhs = mk_mul(args.size(), args.data()); + result = m.mk_app(m_util.get_family_id(), k, lhs, mk_zero_for(lhs)); + } + + // See mk_split_strict_comp and mk_split_nonstrict_comp + void split_even_odd(bool strict, polynomial::factors const & fs, expr_ref_buffer & even_eqs, expr_ref_buffer & odd_factors) { + expr_ref arg(m); + for (unsigned i = 0; i < fs.distinct_factors(); ++i) { + m_expr2poly.to_expr(fs[i], true, arg); + if (fs.get_degree(i) % 2 == 0) { + expr * eq = m.mk_eq(arg, mk_zero_for(arg)); + if (strict) + even_eqs.push_back(m.mk_not(eq)); + else + even_eqs.push_back(eq); + } + else { + odd_factors.push_back(arg); + } + } + } + + // Strict case + // p1^{2*k1} * p2^{2*k2 + 1} >< 0 + // --> + // p1 != 0 and p2 >< 0 + // + // Nonstrict + // p1^{2*k1} * p2^{2*k2 + 1} >=< 0 + // --> + // p1 = 0 or p2 >=< 0 + // + void mk_split_comp(decl_kind k, polynomial::factors const & fs, expr_ref & result) { + SASSERT(k == OP_LT || k == OP_GT || k == OP_LE || k == OP_GE); + bool strict = (k == OP_LT) || (k == OP_GT); + expr_ref_buffer args(m); + expr_ref_buffer odd_factors(m); + split_even_odd(strict, fs, args, odd_factors); + if (odd_factors.empty()) { + if (k == OP_LT) { + result = m.mk_false(); + return; + } + if (k == OP_GE) { + result = m.mk_true(); + return; + } + } + else { + args.push_back(m.mk_app(m_util.get_family_id(), k, mk_mul(odd_factors.size(), odd_factors.data()), mk_zero_for(odd_factors[0]))); + } + SASSERT(!args.empty()); + if (args.size() == 1) + result = args[0]; + else if (strict) + result = m.mk_and(args); + else + result = m.mk_or(args); + } + + br_status factor(func_decl * f, expr * lhs, expr * rhs, expr_ref & result) { + polynomial_ref p1(m_pm); + polynomial_ref p2(m_pm); + scoped_mpz d1(m_qm); + scoped_mpz d2(m_qm); + m_expr2poly.to_polynomial(lhs, p1, d1); + m_expr2poly.to_polynomial(rhs, p2, d2); + TRACE(factor_tactic_bug, + tout << "lhs: " << mk_ismt2_pp(lhs, m) << "\n"; + tout << "p1: " << p1 << "\n"; + tout << "d1: " << d1 << "\n"; + tout << "rhs: " << mk_ismt2_pp(rhs, m) << "\n"; + tout << "p2: " << p2 << "\n"; + tout << "d2: " << d2 << "\n";); + scoped_mpz lcm(m_qm); + m_qm.lcm(d1, d2, lcm); + m_qm.div(lcm, d1, d1); + m_qm.div(lcm, d2, d2); + m_qm.neg(d2); + polynomial_ref p(m_pm); + p = m_pm.addmul(d1, m_pm.mk_unit(), p1, d2, m_pm.mk_unit(), p2); + if (is_const(p)) + return BR_FAILED; + polynomial::factors fs(m_pm); + TRACE(factor_tactic_bug, tout << "p: " << p << "\n";); + m_pm.factor(p, fs, m_fparams); + SASSERT(fs.distinct_factors() > 0); + TRACE(factor_tactic_bug, tout << "factors:\n"; fs.display(tout); tout << "\n";); + if (fs.distinct_factors() == 1 && fs.get_degree(0) == 1) + return BR_FAILED; + if (m.is_eq(f)) { + if (m_split_factors) + mk_split_eq(fs, result); + else + mk_eq(fs, result); + } + else { + decl_kind k = f->get_decl_kind(); + if (m_qm.is_neg(fs.get_constant())) + k = flip(k); + + if (m_split_factors) + mk_split_comp(k, fs, result); + else + mk_comp(k, fs, result); + } + return BR_DONE; + } + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + if (num != 2) + return BR_FAILED; + if (m.is_eq(f) && (m_util.is_arith_expr(args[0]) || m_util.is_arith_expr(args[1])) && (!m.is_bool(args[0]))) + return factor(f, args[0], args[1], result); + if (f->get_family_id() != m_util.get_family_id()) + return BR_FAILED; + switch (f->get_decl_kind()) { + case OP_LT: + case OP_GT: + case OP_LE: + case OP_GE: + return factor(f, args[0], args[1], result); + } + return BR_FAILED; + } +}; + +struct factor_simplifier::rw : public rewriter_tpl { + rw_cfg m_cfg; + rw(ast_manager & m, params_ref const & p): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, p) { + } +}; + +factor_simplifier::factor_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s) + : dependent_expr_simplifier(m, s), m_params(p), m_rw(alloc(rw, m, p)) {} + +void factor_simplifier::updt_params(params_ref const& p) { + m_params.append(p); + m_rw->cfg().updt_params(m_params); +} + +void factor_simplifier::collect_param_descrs(param_descrs& r) { + r.insert("split_factors", CPK_BOOL, + "apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).", "true"); + polynomial::factor_params::get_param_descrs(r); +} + +void factor_simplifier::reduce() { + expr_ref new_curr(m); + proof_ref new_pr(m); + for (unsigned idx : indices()) { + auto const& d = m_fmls[idx]; + m_rw->operator()(d.fml(), new_curr, new_pr); + if (new_curr != d.fml()) + m_fmls.update(idx, dependent_expr(m, new_curr, mp(d.pr(), new_pr), d.dep())); + } +} + +dependent_expr_simplifier* mk_factor_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s) { + return alloc(factor_simplifier, m, p, s); +} diff --git a/src/ast/simplifiers/factor_simplifier.h b/src/ast/simplifiers/factor_simplifier.h new file mode 100644 index 000000000..c26186e7f --- /dev/null +++ b/src/ast/simplifiers/factor_simplifier.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + factor_simplifier.h + +Abstract: + + Polynomial factorization simplifier. + +Author: + + Leonardo de Moura (leonardo) 2012-02-03 + +--*/ +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "util/params.h" + +class factor_simplifier : public dependent_expr_simplifier { + struct rw_cfg; + struct rw; + params_ref m_params; + scoped_ptr m_rw; + +public: + factor_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s); + + char const* name() const override { return "factor"; } + + void updt_params(params_ref const& p) override; + void collect_param_descrs(param_descrs& r) override; + void reduce() override; +}; + +dependent_expr_simplifier* mk_factor_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s); diff --git a/src/tactic/arith/factor_tactic.h b/src/tactic/arith/factor_tactic.h index 7be5c5df6..61b8d9f12 100644 --- a/src/tactic/arith/factor_tactic.h +++ b/src/tactic/arith/factor_tactic.h @@ -33,10 +33,21 @@ Factor polynomials in equalities and inequalities. #pragma once #include "util/params.h" +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/factor_simplifier.h" + class ast_manager; -class tactic; 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()) { + 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)") */ From 4f6c0637fc876f754214b2a1d408801897e1a081 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:12 +0000 Subject: [PATCH 3/4] Remove old mk_factor_tactic, rename factor2 to factor Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/arith/CMakeLists.txt | 1 - src/tactic/arith/factor_tactic.cpp | 323 +---------------------------- src/tactic/arith/factor_tactic.h | 7 +- 3 files changed, 3 insertions(+), 328 deletions(-) diff --git a/src/tactic/arith/CMakeLists.txt b/src/tactic/arith/CMakeLists.txt index 4eabef4a6..611e373b0 100644 --- a/src/tactic/arith/CMakeLists.txt +++ b/src/tactic/arith/CMakeLists.txt @@ -7,7 +7,6 @@ z3_add_component(arith_tactics degree_shift_tactic.cpp diff_neq_tactic.cpp eq2bv_tactic.cpp - factor_tactic.cpp fix_dl_var_tactic.cpp fm_tactic.cpp lia2card_tactic.cpp diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 4416517ff..dadb11214 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -8,330 +8,11 @@ Module Name: Abstract: Polynomial factorization tactic. + The implementation has been moved to ast/simplifiers/factor_simplifier.cpp. + The tactic is now a thin wrapper around factor_simplifier via dependent_expr_state_tactic. Author: Leonardo de Moura (leonardo) 2012-02-03 -Revision History: - --*/ -#include "tactic/tactical.h" -#include "ast/expr2polynomial.h" -#include "ast/rewriter/rewriter_def.h" - -class factor_tactic : public tactic { - - struct rw_cfg : public default_rewriter_cfg { - ast_manager & m; - arith_util m_util; - unsynch_mpq_manager m_qm; - polynomial::manager m_pm; - default_expr2polynomial m_expr2poly; - polynomial::factor_params m_fparams; - bool m_split_factors; - - rw_cfg(ast_manager & _m, params_ref const & p): - m(_m), - m_util(_m), - m_pm(m.limit(), m_qm), - m_expr2poly(m, m_pm) { - updt_params(p); - } - - void updt_params(params_ref const & p) { - m_split_factors = p.get_bool("split_factors", true); - m_fparams.updt_params(p); - } - - expr * mk_mul(unsigned sz, expr * const * args) { - SASSERT(sz > 0); - if (sz == 1) - return args[0]; - return m_util.mk_mul(sz, args); - } - - expr * mk_zero_for(expr * arg) { - return m_util.mk_numeral(rational(0), m_util.is_int(arg)); - } - - // p1^k1 * p2^k2 = 0 --> p1*p2 = 0 - void mk_eq(polynomial::factors const & fs, expr_ref & result) { - expr_ref_buffer args(m); - expr_ref arg(m); - for (unsigned i = 0; i < fs.distinct_factors(); ++i) { - m_expr2poly.to_expr(fs[i], true, arg); - args.push_back(arg); - } - result = m.mk_eq(mk_mul(args.size(), args.data()), mk_zero_for(arg)); - } - - // p1^k1 * p2^k2 = 0 --> p1 = 0 or p2 = 0 - void mk_split_eq(polynomial::factors const & fs, expr_ref & result) { - expr_ref_buffer args(m); - expr_ref arg(m); - for (unsigned i = 0; i < fs.distinct_factors(); ++i) { - m_expr2poly.to_expr(fs[i], true, arg); - args.push_back(m.mk_eq(arg, mk_zero_for(arg))); - } - if (args.size() == 1) - result = args[0]; - else - result = m.mk_or(args); - } - - decl_kind flip(decl_kind k) { - SASSERT(k == OP_LT || k == OP_GT || k == OP_LE || k == OP_GE); - switch (k) { - case OP_LT: return OP_GT; - case OP_LE: return OP_GE; - case OP_GT: return OP_LT; - case OP_GE: return OP_LE; - default: - UNREACHABLE(); - return k; - } - } - - // p1^{2*k1} * p2^{2*k2 + 1} >=< 0 - // --> - // (p1^2)*p2 >=<0 - void mk_comp(decl_kind k, polynomial::factors const & fs, expr_ref & result) { - SASSERT(k == OP_LT || k == OP_GT || k == OP_LE || k == OP_GE); - expr_ref_buffer args(m); - expr_ref arg(m); - for (unsigned i = 0; i < fs.distinct_factors(); ++i) { - m_expr2poly.to_expr(fs[i], true, arg); - if (fs.get_degree(i) % 2 == 0) - arg = m_util.mk_power(arg, m_util.mk_numeral(rational(2), m_util.is_int(arg))); - args.push_back(arg); - } - expr * lhs = mk_mul(args.size(), args.data()); - result = m.mk_app(m_util.get_family_id(), k, lhs, mk_zero_for(lhs)); - } - - // See mk_split_strict_comp and mk_split_nonstrict_comp - void split_even_odd(bool strict, polynomial::factors const & fs, expr_ref_buffer & even_eqs, expr_ref_buffer & odd_factors) { - expr_ref arg(m); - for (unsigned i = 0; i < fs.distinct_factors(); ++i) { - m_expr2poly.to_expr(fs[i], true, arg); - if (fs.get_degree(i) % 2 == 0) { - expr * eq = m.mk_eq(arg, mk_zero_for(arg)); - if (strict) - even_eqs.push_back(m.mk_not(eq)); - else - even_eqs.push_back(eq); - } - else { - odd_factors.push_back(arg); - } - } - } - - // Strict case - // p1^{2*k1} * p2^{2*k2 + 1} >< 0 - // --> - // p1 != 0 and p2 >< 0 - // - // Nonstrict - // p1^{2*k1} * p2^{2*k2 + 1} >=< 0 - // --> - // p1 = 0 or p2 >=< 0 - // - void mk_split_comp(decl_kind k, polynomial::factors const & fs, expr_ref & result) { - SASSERT(k == OP_LT || k == OP_GT || k == OP_LE || k == OP_GE); - bool strict = (k == OP_LT) || (k == OP_GT); - expr_ref_buffer args(m); - expr_ref_buffer odd_factors(m); - split_even_odd(strict, fs, args, odd_factors); - if (odd_factors.empty()) { - if (k == OP_LT) { - result = m.mk_false(); - return; - } - if (k == OP_GE) { - result = m.mk_true(); - return; - } - } - else { - args.push_back(m.mk_app(m_util.get_family_id(), k, mk_mul(odd_factors.size(), odd_factors.data()), mk_zero_for(odd_factors[0]))); - } - SASSERT(!args.empty()); - if (args.size() == 1) - result = args[0]; - else if (strict) - result = m.mk_and(args); - else - result = m.mk_or(args); - } - - br_status factor(func_decl * f, expr * lhs, expr * rhs, expr_ref & result) { - polynomial_ref p1(m_pm); - polynomial_ref p2(m_pm); - scoped_mpz d1(m_qm); - scoped_mpz d2(m_qm); - m_expr2poly.to_polynomial(lhs, p1, d1); - m_expr2poly.to_polynomial(rhs, p2, d2); - TRACE(factor_tactic_bug, - tout << "lhs: " << mk_ismt2_pp(lhs, m) << "\n"; - tout << "p1: " << p1 << "\n"; - tout << "d1: " << d1 << "\n"; - tout << "rhs: " << mk_ismt2_pp(rhs, m) << "\n"; - tout << "p2: " << p2 << "\n"; - tout << "d2: " << d2 << "\n";); - scoped_mpz lcm(m_qm); - m_qm.lcm(d1, d2, lcm); - m_qm.div(lcm, d1, d1); - m_qm.div(lcm, d2, d2); - m_qm.neg(d2); - polynomial_ref p(m_pm); - p = m_pm.addmul(d1, m_pm.mk_unit(), p1, d2, m_pm.mk_unit(), p2); - if (is_const(p)) - return BR_FAILED; - polynomial::factors fs(m_pm); - TRACE(factor_tactic_bug, tout << "p: " << p << "\n";); - m_pm.factor(p, fs, m_fparams); - SASSERT(fs.distinct_factors() > 0); - TRACE(factor_tactic_bug, tout << "factors:\n"; fs.display(tout); tout << "\n";); - if (fs.distinct_factors() == 1 && fs.get_degree(0) == 1) - return BR_FAILED; - if (m.is_eq(f)) { - if (m_split_factors) - mk_split_eq(fs, result); - else - mk_eq(fs, result); - } - else { - decl_kind k = f->get_decl_kind(); - if (m_qm.is_neg(fs.get_constant())) - k = flip(k); - - if (m_split_factors) - mk_split_comp(k, fs, result); - else - mk_comp(k, fs, result); - } - return BR_DONE; - } - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - if (num != 2) - return BR_FAILED; - if (m.is_eq(f) && (m_util.is_arith_expr(args[0]) || m_util.is_arith_expr(args[1])) && (!m.is_bool(args[0]))) - return factor(f, args[0], args[1], result); - if (f->get_family_id() != m_util.get_family_id()) - return BR_FAILED; - switch (f->get_decl_kind()) { - case OP_LT: - case OP_GT: - case OP_LE: - case OP_GE: - return factor(f, args[0], args[1], result); - } - return BR_FAILED; - } - }; - - struct rw : public rewriter_tpl { - rw_cfg m_cfg; - - rw(ast_manager & m, params_ref const & p): - rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m, p) { - } - }; - - struct imp { - ast_manager & m; - rw m_rw; - - imp(ast_manager & _m, params_ref const & p): - m(_m), - m_rw(m, p) { - } - - - void updt_params(params_ref const & p) { - m_rw.cfg().updt_params(p); - } - - void operator()(goal_ref const & g, - goal_ref_buffer & result) { - tactic_report report("factor", *g); - bool produce_proofs = g->proofs_enabled(); - - expr_ref new_curr(m); - proof_ref new_pr(m); - unsigned size = g->size(); - for (unsigned idx = 0; !g->inconsistent() && idx < size; ++idx) { - expr * curr = g->form(idx); - m_rw(curr, new_curr, new_pr); - if (produce_proofs) { - proof * pr = g->pr(idx); - new_pr = m.mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); - } - g->inc_depth(); - result.push_back(g.get()); - } - }; - - imp * m_imp; - params_ref m_params; -public: - factor_tactic(ast_manager & m, params_ref const & p): - m_params(p) { - m_imp = alloc(imp, m, p); - } - - tactic * translate(ast_manager & m) override { - return alloc(factor_tactic, m, m_params); - } - - ~factor_tactic() override { - dealloc(m_imp); - } - - char const* name() const override { return "factor"; } - - void updt_params(params_ref const & p) override { - m_params.append(p); - m_imp->m_rw.cfg().updt_params(m_params); - } - - void collect_param_descrs(param_descrs & r) override { - r.insert("split_factors", CPK_BOOL, - "apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).", "true"); - polynomial::factor_params::get_param_descrs(r); - } - - void operator()(goal_ref const & in, - goal_ref_buffer & result) override { - try { - (*m_imp)(in, result); - } - catch (z3_error & ex) { - throw ex; - } - catch (z3_exception & ex) { - throw tactic_exception(ex.what()); - } - } - - void cleanup() override { - imp * d = alloc(imp, m_imp->m, m_params); - std::swap(d, m_imp); - dealloc(d); - } - - -}; - -tactic * mk_factor_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(factor_tactic, m, p)); -} - - - diff --git a/src/tactic/arith/factor_tactic.h b/src/tactic/arith/factor_tactic.h index 61b8d9f12..4f884dafa 100644 --- a/src/tactic/arith/factor_tactic.h +++ b/src/tactic/arith/factor_tactic.h @@ -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)") */ From fd424c7afd1be991f0a138ca1ec2cf215bd591e2 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 23 Feb 2026 04:01:34 +0000 Subject: [PATCH 4/4] Delete factor_tactic.cpp (implementation moved to factor_simplifier.cpp) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/arith/factor_tactic.cpp | 18 ------------------ 1 file changed, 18 deletions(-) delete mode 100644 src/tactic/arith/factor_tactic.cpp diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp deleted file mode 100644 index dadb11214..000000000 --- a/src/tactic/arith/factor_tactic.cpp +++ /dev/null @@ -1,18 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - factor_tactic.cpp - -Abstract: - - Polynomial factorization tactic. - The implementation has been moved to ast/simplifiers/factor_simplifier.cpp. - The tactic is now a thin wrapper around factor_simplifier via dependent_expr_state_tactic. - -Author: - - Leonardo de Moura (leonardo) 2012-02-03 - ---*/