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] 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)") */