From 9a9f5c41b83828de8448c56d1ca8799f9334f86e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 15 Jul 2026 10:21:23 -0700 Subject: [PATCH 1/2] Recognize rational roots in closest-root isolation, guarded by algebraic.isolate_rational_roots Co-Authored-By: Claude Fable 5 --- src/math/polynomial/algebraic_numbers.cpp | 95 +++++++++++++++++++++++ src/math/polynomial/algebraic_params.pyg | 1 + 2 files changed, 96 insertions(+) diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 945b9023dce..32b2d632abf 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -88,6 +88,7 @@ namespace algebraic_numbers { // configuration int m_min_magnitude; bool m_factor; + bool m_isolate_rational_roots; polynomial::factor_params m_factor_params; int m_zero_accuracy; @@ -152,6 +153,7 @@ namespace algebraic_numbers { algebraic_params p(_p); m_min_magnitude = -static_cast(p.min_mag()); m_factor = p.factor(); + m_isolate_rational_roots = p.isolate_rational_roots(); m_factor_params.m_max_p = p.factor_max_prime(); m_factor_params.m_p_trials = p.factor_num_primes(); m_factor_params.m_max_search_size = p.factor_search_size(); @@ -831,11 +833,104 @@ namespace algebraic_numbers { return; } + // At this point [a, b] is an *isolating* and *refinable* interval for p: + // it contains exactly one real root of the square-free polynomial p, and + // neither endpoint is itself that root. That root could still be a + // *rational* number: unlike the general isolate_roots(), this closest-root + // path does NOT factor p, so a reducible polynomial (e.g. a product of + // linear factors) is handled whole and keeps its rational roots instead of + // exposing them as degree-1 factors. If we blindly built an algebraic_cell + // here we would create a "root object" that is really just a rational, which + // is both wasteful and, downstream, error-prone (algebraic-number comparison + // must special-case such cells). So first try to recognize a rational root + // and, if found, return it as a plain rational (basic numeral). + if (m_isolate_rational_roots && rational_root_in_interval(sz, p, a, b, r)) + return; + del(r); r = mk_algebraic_cell(sz, p, a, b, false /* minimal */); SASSERT(acell_inv(*r.to_algebraic())); } + // Decide whether the unique real root of the square-free integer polynomial p + // that lies in the isolating interval [l, u] is a rational number and, if so, + // store it in r as a basic (rational) numeral and return true. Otherwise return + // false (the root is irrational and must be represented as a root object). + // + // Notation: p(x) = a_n*x^n + ... + a_1*x + a_0 with a_i integers (mpz), a_n != 0. + // mpbq = dyadic rational (denominator is a power of two); + // mpq = arbitrary rational; mpz = integer. + // + // Preconditions (guaranteed by the caller, isolate_kth_root): + // * p is square-free, so all its roots are simple (no repeated roots). + // * [l, u] is an isolating interval: it contains EXACTLY ONE real root of p. + // This is why we may speak of "the root" in the interval. + // + // The mathematics used: + // + // 1. Rational Root Theorem. If a polynomial with integer coefficients has a + // rational root num/den, where den > 0 does not divide num, + // then den divides the leading coefficient a_n. In + // particular every rational root can be written with denominator |a_n|, + // i.e. as m/|a_n| for some integer m. We can represent the root as that m/|a_n| + // for some integer m. + // + // 2. Two distinct rationals m1/|a_n| and m2/|a_n| differ by at least 1/|a_n|. Hence if we + // first shrink [l, u] to have width < 1/|a_n|, the interval can contain at + // most one rational of the form m/|a_n| => if the + // root is rational it must equal that single candidate. + bool rational_root_in_interval(unsigned sz, mpz const * p, mpbq & l, mpbq & u, numeral & r) { + // a_n is the leading coefficient; work with its absolute value |a_n|. + mpz const & a_n = p[sz - 1]; + scoped_mpz abs_a_n(qm()); + qm().set(abs_a_n, a_n); + qm().abs(abs_a_n); + + // We need the interval width to be strictly less than 1/|a_n| + // refine() shrinks by halving, i.e. it reaches width <= 1/2^k. Choosing + // k = floor(log2(|a_n|)) + 1 + // gives 2^k > |a_n|, hence 1/2^k < 1/|a_n|, which is what we want. + unsigned k = qm().log2(abs_a_n); + k++; + + // Refine [l, u] to precision k. refine() returns false in the lucky case + // where the bisection lands *exactly* on a dyadic rational that is a root + // of p; in that case the exact root has been stored in the lower endpoint l, + // so we can return it directly as a basic rational. + if (!upm().refine(sz, p, bqm(), l, u, k)) { + scoped_mpq q(qm()); + to_mpq(qm(), l, q); + set(r, q); + return true; + } + // Otherwise refine() succeeded and [l, u] now has width < 1/|a_n|. + + // Build the unique candidate rational m/|a_n| that could lie in [l, u]. + // Scale the interval by |a_n|: [l*|a_n|, u*|a_n|] has width < 1, so it + // contains at most one integer. That integer, if any, is m = floor(u*|a_n|), + // and the candidate rational is m/|a_n|. + scoped_mpbq a_n_upper(bqm()); + bqm().mul(u, abs_a_n, a_n_upper); // a_n_upper = u * |a_n| + scoped_mpz zcandidate(qm()); + bqm().floor(qm(), a_n_upper, zcandidate); // m = floor(u * |a_n|) + scoped_mpq candidate(qm()); + qm().set(candidate, zcandidate, abs_a_n); // candidate = m / |a_n| + + // By construction candidate <= u. We still must confirm two things: + // (a) candidate is actually inside the interval, i.e. l < candidate + // (if candidate <= l then there is no rational m/|a_n| inside [l,u]); + // (b) candidate is genuinely a root, i.e. p(candidate) == 0. + // If both hold, then since the interval isolates exactly one root, that + // root equals candidate and is rational. If p(candidate) != 0, then by the + // Rational Root Theorem no rational (which would have to be m/|a_n|) is a + // root here, so the single root in the interval is irrational. + if (bqm().lt(l, candidate) && upm().eval_sign_at(sz, p, candidate) == sign_zero) { + set(r, candidate); + return true; + } + return false; + } + // Closest-root isolation for an (integer) univariate polynomial. void isolate_roots_closest_univariate(polynomial_ref const & p, mpq const & s, numeral_vector & roots, svector & indices) { SASSERT(is_univariate(p)); diff --git a/src/math/polynomial/algebraic_params.pyg b/src/math/polynomial/algebraic_params.pyg index 0e53a40b836..5adc23aac9c 100644 --- a/src/math/polynomial/algebraic_params.pyg +++ b/src/math/polynomial/algebraic_params.pyg @@ -4,6 +4,7 @@ def_module_params('algebraic', params=(('zero_accuracy', UINT, 0, 'one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k)'), ('min_mag', UINT, 16, 'Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16'), ('factor', BOOL, True, 'use polynomial factorization to simplify polynomials representing algebraic numbers'), + ('isolate_rational_roots', BOOL, True, 'in closest-root isolation, detect when the isolated root is rational and represent it as a rational instead of an algebraic cell'), ('factor_max_prime', UINT, 31, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step'), ('factor_num_primes', UINT, 1, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)\'s. This parameter specify the maximum number of finite factorizations to be considered, before lifting and searching'), ('factor_search_size', UINT, 5000, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space'))) From 0bf29be6a8ffef074fec145b18870deb18af0e18 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 15 Jul 2026 11:39:45 -0700 Subject: [PATCH 2/2] Remove algebraic.isolate_rational_roots parameter; rational root recognition is always on Co-Authored-By: Claude Fable 5 --- src/math/polynomial/algebraic_numbers.cpp | 4 +--- src/math/polynomial/algebraic_params.pyg | 1 - 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 32b2d632abf..101115ab319 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -88,7 +88,6 @@ namespace algebraic_numbers { // configuration int m_min_magnitude; bool m_factor; - bool m_isolate_rational_roots; polynomial::factor_params m_factor_params; int m_zero_accuracy; @@ -153,7 +152,6 @@ namespace algebraic_numbers { algebraic_params p(_p); m_min_magnitude = -static_cast(p.min_mag()); m_factor = p.factor(); - m_isolate_rational_roots = p.isolate_rational_roots(); m_factor_params.m_max_p = p.factor_max_prime(); m_factor_params.m_p_trials = p.factor_num_primes(); m_factor_params.m_max_search_size = p.factor_search_size(); @@ -844,7 +842,7 @@ namespace algebraic_numbers { // is both wasteful and, downstream, error-prone (algebraic-number comparison // must special-case such cells). So first try to recognize a rational root // and, if found, return it as a plain rational (basic numeral). - if (m_isolate_rational_roots && rational_root_in_interval(sz, p, a, b, r)) + if (rational_root_in_interval(sz, p, a, b, r)) return; del(r); diff --git a/src/math/polynomial/algebraic_params.pyg b/src/math/polynomial/algebraic_params.pyg index 5adc23aac9c..0e53a40b836 100644 --- a/src/math/polynomial/algebraic_params.pyg +++ b/src/math/polynomial/algebraic_params.pyg @@ -4,7 +4,6 @@ def_module_params('algebraic', params=(('zero_accuracy', UINT, 0, 'one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k)'), ('min_mag', UINT, 16, 'Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16'), ('factor', BOOL, True, 'use polynomial factorization to simplify polynomials representing algebraic numbers'), - ('isolate_rational_roots', BOOL, True, 'in closest-root isolation, detect when the isolated root is rational and represent it as a rational instead of an algebraic cell'), ('factor_max_prime', UINT, 31, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step'), ('factor_num_primes', UINT, 1, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)\'s. This parameter specify the maximum number of finite factorizations to be considered, before lifting and searching'), ('factor_search_size', UINT, 5000, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space')))