Skip to main content

oxiz_math/algebraic/
isolate.rs

1//! Root Isolation for Algebraic Numbers.
2//!
3//! Algorithms for isolating real roots of polynomials into disjoint intervals.
4//! Each interval contains exactly one root, enabling construction of algebraic numbers.
5//!
6//! ## Algorithms
7//!
8//! - **Sturm Sequences**: Count roots in intervals
9//! - **Bisection**: Refine intervals containing roots
10//! - **Descartes' Rule**: Upper bound on positive roots
11//!
12//! ## References
13//!
14//! - "Algorithms in Real Algebraic Geometry" (Basu et al., 2006)
15//! - Z3's `math/polynomial/algebraic_numbers.cpp`
16
17use crate::polynomial::root_counting::Polynomial;
18#[allow(unused_imports)]
19use crate::prelude::*;
20use num_bigint::BigInt;
21use num_rational::BigRational;
22use num_traits::{Signed, Zero};
23
24/// Isolating interval for a root.
25#[derive(Debug, Clone)]
26pub struct IsolatingInterval {
27    /// Lower bound.
28    pub lower: BigRational,
29    /// Upper bound.
30    pub upper: BigRational,
31    /// Sign at lower bound.
32    pub sign_lower: i32,
33    /// Sign at upper bound.
34    pub sign_upper: i32,
35}
36
37impl IsolatingInterval {
38    /// Create a new isolating interval.
39    pub fn new(lower: BigRational, upper: BigRational, sign_lower: i32, sign_upper: i32) -> Self {
40        Self {
41            lower,
42            upper,
43            sign_lower,
44            sign_upper,
45        }
46    }
47
48    /// Get interval width.
49    pub fn width(&self) -> BigRational {
50        &self.upper - &self.lower
51    }
52
53    /// Get midpoint.
54    pub fn midpoint(&self) -> BigRational {
55        (&self.lower + &self.upper) / BigRational::from(BigInt::from(2))
56    }
57}
58
59/// Safety-net bisection-depth ceiling for [`RootIsolator::isolate_in_interval`].
60///
61/// This is independent of [`IsolationConfig::max_iterations`] (which bounds
62/// the *refinement* of an already-isolated single-root interval, not the
63/// isolation search itself). See [`IsolationStats::incomplete`] for why this
64/// is a pure safety net rather than a correctness-affecting parameter.
65const MAX_ROOT_ISOLATION_DEPTH: u32 = 4096;
66
67/// Configuration for root isolation.
68#[derive(Debug, Clone)]
69pub struct IsolationConfig {
70    /// Use Sturm sequences for root counting.
71    pub use_sturm: bool,
72    /// Use Descartes' rule for optimization.
73    pub use_descartes: bool,
74    /// Maximum refinement iterations.
75    pub max_iterations: usize,
76    /// Precision threshold.
77    pub precision: BigRational,
78}
79
80impl Default for IsolationConfig {
81    fn default() -> Self {
82        Self {
83            use_sturm: true,
84            use_descartes: true,
85            max_iterations: 1000,
86            precision: BigRational::new(BigInt::from(1), BigInt::from(1_000_000)),
87        }
88    }
89}
90
91/// Statistics for root isolation.
92#[derive(Debug, Clone, Default)]
93pub struct IsolationStats {
94    /// Sturm sequence computations.
95    pub sturm_computations: u64,
96    /// Bisection steps.
97    pub bisection_steps: u64,
98    /// Sign evaluations.
99    pub sign_evaluations: u64,
100    /// Roots isolated.
101    pub roots_isolated: u64,
102    /// Set to `true` if bisection ever hit `MAX_ROOT_ISOLATION_DEPTH`
103    /// before narrowing a sub-interval down to exactly one root.
104    ///
105    /// With a correct Sturm sequence and exact rational bisection this
106    /// should never happen for any well-formed polynomial: distinct real
107    /// roots always have a positive minimum pairwise separation, so repeated
108    /// bisection is mathematically guaranteed to isolate each one eventually.
109    /// A `true` value therefore indicates a pathological input or an
110    /// upstream bug (e.g. an incorrect Sturm sequence), and it also means
111    /// [`RootIsolator::isolate_roots`]'s returned list may be missing one or
112    /// more roots for the affected sub-interval -- this flag is what makes
113    /// that condition visible instead of it being a silently-incomplete
114    /// result.
115    pub incomplete: bool,
116}
117
118/// Interval refinement method.
119#[derive(Debug, Clone, Copy, PartialEq, Eq)]
120pub enum IntervalRefinement {
121    /// Bisection method.
122    Bisection,
123    /// Newton's method.
124    Newton,
125    /// Hybrid (bisection + Newton).
126    Hybrid,
127}
128
129/// Root isolator using interval arithmetic.
130pub struct RootIsolator {
131    /// Polynomial to isolate roots for (univariate over Q).
132    poly: Polynomial,
133    /// Configuration.
134    config: IsolationConfig,
135    /// Statistics.
136    stats: IsolationStats,
137    /// Cached Sturm sequence.
138    sturm_sequence: Option<Vec<Polynomial>>,
139}
140
141impl RootIsolator {
142    /// Create a new root isolator.
143    pub fn new(poly: Polynomial, config: IsolationConfig) -> Self {
144        Self {
145            poly,
146            config,
147            stats: IsolationStats::default(),
148            sturm_sequence: None,
149        }
150    }
151
152    /// Create with default configuration.
153    pub fn default_config(poly: Polynomial) -> Self {
154        Self::new(poly, IsolationConfig::default())
155    }
156
157    /// Isolate all real roots of the polynomial.
158    pub fn isolate_roots(&mut self) -> Vec<IsolatingInterval> {
159        // Handle trivial cases: zero polynomial or non-zero constant
160        let is_zero = self.poly.degree() == 0 && self.poly.coeffs.first().is_none_or(Zero::is_zero);
161        if is_zero || self.poly.degree() == 0 {
162            return Vec::new();
163        }
164
165        // Compute Sturm sequence if enabled
166        if self.config.use_sturm {
167            self.compute_sturm_sequence();
168        }
169
170        // Find bounds for all real roots
171        let (lower_bound, upper_bound) = self.root_bounds();
172
173        // Isolate roots in [lower_bound, upper_bound]
174        self.isolate_in_interval(lower_bound, upper_bound)
175    }
176
177    /// Compute Sturm sequence for the polynomial.
178    fn compute_sturm_sequence(&mut self) {
179        let mut seq = vec![self.poly.clone(), self.poly.derivative()];
180
181        loop {
182            let len = seq.len();
183            if len < 2 {
184                break;
185            }
186
187            let last = &seq[len - 1];
188            // Stop when the tail is degree-0 (zero or non-zero constant): any polynomial
189            // mod a constant is 0, so the next negated remainder would be 0 anyway.
190            if last.degree() == 0 {
191                break;
192            }
193
194            let remainder = seq[len - 2].remainder(&seq[len - 1]);
195
196            // Negate remainder (Sturm sequence convention: p_{k+1} = -rem(p_{k-1}, p_k))
197            let negated = Polynomial::new(remainder.coeffs.iter().map(|c| -c).collect());
198
199            if negated.degree() == 0 && negated.coeffs.first().is_none_or(Zero::is_zero) {
200                break;
201            }
202
203            seq.push(negated);
204
205            // Guard against degenerate polynomials
206            if seq.len() > 1000 {
207                break;
208            }
209        }
210
211        self.sturm_sequence = Some(seq);
212        self.stats.sturm_computations += 1;
213    }
214
215    /// Count roots in an interval using Sturm's theorem.
216    fn count_roots(&mut self, lower: &BigRational, upper: &BigRational) -> usize {
217        if self.sturm_sequence.is_none() {
218            self.compute_sturm_sequence();
219        }
220
221        // Clone to avoid simultaneous immutable+mutable borrow of self.
222        let seq: Vec<Polynomial> = self.sturm_sequence.as_ref().cloned().unwrap_or_default();
223
224        let sign_changes_lower = self.count_sign_changes(&seq, lower);
225        let sign_changes_upper = self.count_sign_changes(&seq, upper);
226
227        (sign_changes_lower as isize - sign_changes_upper as isize).unsigned_abs()
228    }
229
230    /// Count sign changes in Sturm sequence at a point.
231    fn count_sign_changes(&mut self, seq: &[Polynomial], point: &BigRational) -> usize {
232        self.stats.sign_evaluations += seq.len() as u64;
233
234        let signs: Vec<i32> = seq
235            .iter()
236            .map(|p| {
237                let val = p.eval(point);
238                if val.is_positive() {
239                    1
240                } else if val.is_negative() {
241                    -1
242                } else {
243                    0
244                }
245            })
246            .filter(|&s| s != 0) // Skip zeros per Sturm's theorem
247            .collect();
248
249        // Count sign changes
250        let mut changes = 0;
251        for i in 0..signs.len().saturating_sub(1) {
252            if signs[i] != signs[i + 1] {
253                changes += 1;
254            }
255        }
256
257        changes
258    }
259
260    /// Compute bounds containing all real roots (Cauchy bound).
261    ///
262    /// Cauchy bound: |roots| <= 1 + max(|a_i| / |a_n|)
263    pub(crate) fn root_bounds(&self) -> (BigRational, BigRational) {
264        let coeffs = &self.poly.coeffs;
265        if coeffs.is_empty() {
266            return (BigRational::zero(), BigRational::zero());
267        }
268
269        let leading = match coeffs.last() {
270            Some(c) => c.abs(),
271            None => return (BigRational::zero(), BigRational::zero()),
272        };
273
274        if leading.is_zero() {
275            return (BigRational::zero(), BigRational::zero());
276        }
277
278        let mut max_ratio = BigRational::zero();
279        for coeff in coeffs.iter().take(coeffs.len() - 1) {
280            let ratio = coeff.abs() / &leading;
281            if ratio > max_ratio {
282                max_ratio = ratio;
283            }
284        }
285
286        let bound = BigRational::from(BigInt::from(1)) + max_ratio;
287
288        (-bound.clone(), bound)
289    }
290
291    /// Isolate roots in a given interval.
292    ///
293    /// Iterative (explicit work-stack) rather than recursive, with
294    /// [`MAX_ROOT_ISOLATION_DEPTH`] as a defensive bisection-depth ceiling:
295    /// see [`IsolationStats::incomplete`] for why this bound should never
296    /// actually be hit for a well-formed polynomial, and
297    /// [`crate::polynomial::root_isolation`]'s sibling implementation of the
298    /// same algorithm, or `oxiz-nlsat`'s `SturmSequence::isolate_in_interval_bounded`
299    /// (same algorithm again, over a different `Polynomial` type), for the
300    /// same defensive pattern applied elsewhere in this workspace.
301    fn isolate_in_interval(
302        &mut self,
303        lower: BigRational,
304        upper: BigRational,
305    ) -> Vec<IsolatingInterval> {
306        self.isolate_in_interval_bounded(lower, upper, MAX_ROOT_ISOLATION_DEPTH)
307    }
308
309    /// [`Self::isolate_in_interval`] with an explicit depth ceiling, so
310    /// tests can force the [`IsolationStats::incomplete`] path
311    /// deterministically without needing a pathological polynomial that
312    /// requires thousands of bisection levels.
313    fn isolate_in_interval_bounded(
314        &mut self,
315        lower: BigRational,
316        upper: BigRational,
317        max_depth: u32,
318    ) -> Vec<IsolatingInterval> {
319        let mut results = Vec::new();
320        // Each work item is a sub-interval still to resolve, paired with
321        // its remaining bisection-depth budget (decremented per level, like
322        // a recursion-depth parameter would be, but living on the heap
323        // instead of the native call stack).
324        let mut work: Vec<(BigRational, BigRational, u32)> = vec![(lower, upper, max_depth)];
325
326        while let Some((lo, hi, depth)) = work.pop() {
327            let num_roots = self.count_roots(&lo, &hi);
328
329            if num_roots == 0 {
330                continue;
331            }
332
333            if num_roots == 1 {
334                // Single root in interval
335                let sign_lower = self.eval_sign(&lo);
336                let sign_upper = self.eval_sign(&hi);
337
338                self.stats.roots_isolated += 1;
339
340                results.push(IsolatingInterval::new(lo, hi, sign_lower, sign_upper));
341                continue;
342            }
343
344            if depth == 0 {
345                // Defensive-only fallback (see `IsolationStats::incomplete`):
346                // dropping this sub-range rather than recursing forever or
347                // fabricating a single interval that falsely claims to
348                // isolate multiple roots. Recorded so callers can detect it.
349                self.stats.incomplete = true;
350                continue;
351            }
352
353            // Multiple roots: bisect. Push the right half first so the
354            // left half (pushed last) is popped -- and fully drained,
355            // including everything it in turn pushes -- before the right
356            // half is touched, reproducing the original recursion's
357            // left-to-right result order.
358            self.stats.bisection_steps += 1;
359
360            let mid = (&lo + &hi) / BigRational::from(BigInt::from(2));
361            work.push((mid.clone(), hi, depth - 1));
362            work.push((lo, mid, depth - 1));
363        }
364
365        results
366    }
367
368    /// Evaluate sign of polynomial at a point (-1, 0, or 1).
369    fn eval_sign(&mut self, point: &BigRational) -> i32 {
370        self.stats.sign_evaluations += 1;
371
372        let val = self.poly.eval(point);
373
374        if val.is_positive() {
375            1
376        } else if val.is_negative() {
377            -1
378        } else {
379            0
380        }
381    }
382
383    /// Refine an isolating interval.
384    pub fn refine_interval(
385        &mut self,
386        interval: &IsolatingInterval,
387        method: IntervalRefinement,
388    ) -> IsolatingInterval {
389        match method {
390            IntervalRefinement::Bisection => self.refine_bisection(interval),
391            IntervalRefinement::Newton => self.refine_newton(interval),
392            IntervalRefinement::Hybrid => {
393                // Try Newton first, fall back to bisection if not contracting fast enough
394                let newton_result = self.refine_newton(interval);
395                if newton_result.width()
396                    < interval.width() * BigRational::new(BigInt::from(9), BigInt::from(10))
397                {
398                    newton_result
399                } else {
400                    self.refine_bisection(interval)
401                }
402            }
403        }
404    }
405
406    /// Refine interval using bisection.
407    fn refine_bisection(&mut self, interval: &IsolatingInterval) -> IsolatingInterval {
408        self.stats.bisection_steps += 1;
409
410        let mid = interval.midpoint();
411        let sign_mid = self.eval_sign(&mid);
412
413        if sign_mid == 0 {
414            // Exact root
415            return IsolatingInterval::new(mid.clone(), mid, 0, 0);
416        }
417
418        if sign_mid != interval.sign_lower {
419            // Root in [lower, mid]
420            IsolatingInterval::new(interval.lower.clone(), mid, interval.sign_lower, sign_mid)
421        } else {
422            // Root in [mid, upper]
423            IsolatingInterval::new(mid, interval.upper.clone(), sign_mid, interval.sign_upper)
424        }
425    }
426
427    /// Refine interval using Newton's method.
428    fn refine_newton(&mut self, interval: &IsolatingInterval) -> IsolatingInterval {
429        let mid = interval.midpoint();
430        let f_mid = self.poly.eval(&mid);
431        let df_mid = self.poly.derivative().eval(&mid);
432
433        if df_mid.is_zero() {
434            // Derivative is zero - fall back to bisection
435            return self.refine_bisection(interval);
436        }
437
438        // Newton step: x_new = x - f(x)/f'(x)
439        let x_new = &mid - (&f_mid / &df_mid);
440
441        // Ensure new point is strictly inside interval
442        if x_new > interval.lower && x_new < interval.upper {
443            let sign_new = self.eval_sign(&x_new);
444
445            if sign_new == 0 {
446                return IsolatingInterval::new(x_new.clone(), x_new, 0, 0);
447            }
448
449            if sign_new != interval.sign_lower {
450                IsolatingInterval::new(interval.lower.clone(), x_new, interval.sign_lower, sign_new)
451            } else {
452                IsolatingInterval::new(x_new, interval.upper.clone(), sign_new, interval.sign_upper)
453            }
454        } else {
455            // Newton step escaped the interval - use bisection
456            self.refine_bisection(interval)
457        }
458    }
459
460    /// Get statistics.
461    pub fn stats(&self) -> &IsolationStats {
462        &self.stats
463    }
464
465    /// Reset statistics.
466    pub fn reset_stats(&mut self) {
467        self.stats = IsolationStats::default();
468    }
469}
470
471#[cfg(test)]
472mod tests {
473    use super::*;
474
475    fn rat(n: i64) -> BigRational {
476        BigRational::from(BigInt::from(n))
477    }
478
479    #[test]
480    fn test_isolator_creation() {
481        let poly = Polynomial::new(vec![rat(-2), rat(0), rat(1)]);
482
483        let isolator = RootIsolator::default_config(poly);
484        assert_eq!(isolator.stats().roots_isolated, 0);
485    }
486
487    #[test]
488    fn test_root_bounds() {
489        let poly = Polynomial::new(vec![rat(-6), rat(5), rat(1)]); // x^2 + 5x - 6
490
491        let isolator = RootIsolator::default_config(poly);
492        let (lower, upper) = isolator.root_bounds();
493
494        // Roots are -6 and 1, so bounds should contain both
495        assert!(lower < rat(-6));
496        assert!(upper > rat(1));
497    }
498
499    #[test]
500    fn test_isolate_linear() {
501        let poly = Polynomial::new(vec![rat(-5), rat(1)]); // x - 5
502
503        let mut isolator = RootIsolator::default_config(poly);
504        let intervals = isolator.isolate_roots();
505
506        assert_eq!(intervals.len(), 1);
507        assert!(intervals[0].lower <= rat(5));
508        assert!(intervals[0].upper >= rat(5));
509    }
510
511    #[test]
512    fn test_refine_bisection() {
513        let poly = Polynomial::new(vec![rat(-2), rat(0), rat(1)]); // x^2 - 2
514
515        let mut isolator = RootIsolator::default_config(poly);
516
517        let interval = IsolatingInterval::new(rat(1), rat(2), -1, 1);
518
519        let refined = isolator.refine_interval(&interval, IntervalRefinement::Bisection);
520
521        assert!(refined.width() < interval.width());
522    }
523
524    #[test]
525    fn test_stats() {
526        let poly = Polynomial::new(vec![rat(-5), rat(1)]);
527
528        let mut isolator = RootIsolator::default_config(poly);
529        isolator.isolate_roots();
530
531        assert!(isolator.stats().roots_isolated > 0);
532        assert!(isolator.stats().sign_evaluations > 0);
533    }
534
535    // -----------------------------------------------------------------------
536    // `isolate_in_interval` bisection-depth regression tests (audit: no
537    // bound at all on the bisection recursion; `oxiz-nlsat`'s sibling
538    // implementation of the same algorithm already carries a 4096-level
539    // safety net).
540    // -----------------------------------------------------------------------
541
542    #[test]
543    fn test_isolate_roots_multiple_roots_via_bisection_behaviour_preserved() {
544        // x^2 - 2 has two real roots (Âħsqrt(2)); the Cauchy bound brackets
545        // both in one interval, so isolate_roots must bisect to separate
546        // them. This exact path (isolate_in_interval's num_roots > 1
547        // branch) had no prior test coverage in this file.
548        let poly = Polynomial::new(vec![rat(-2), rat(0), rat(1)]);
549        let mut isolator = RootIsolator::default_config(poly);
550        let intervals = isolator.isolate_roots();
551
552        assert_eq!(intervals.len(), 2, "x^2 - 2 has exactly two real roots");
553        assert!(intervals[0].lower <= intervals[0].upper);
554        assert!(intervals[1].lower <= intervals[1].upper);
555        // The two isolating intervals must be disjoint (one entirely below
556        // the other), in either order.
557        assert!(
558            intervals[0].upper <= intervals[1].lower || intervals[1].upper <= intervals[0].lower,
559            "isolating intervals must not overlap: {:?}",
560            intervals
561        );
562        assert!(
563            !isolator.stats().incomplete,
564            "a normal, well-separated polynomial must never hit the depth cap"
565        );
566        assert_eq!(isolator.stats().roots_isolated, 2);
567    }
568
569    #[test]
570    fn test_isolate_in_interval_bounded_depth_cap_is_visible_not_silent() {
571        // x^3 - x = x(x-1)(x+1) has three real roots. With a bisection
572        // budget too small to separate all three, the search must stop and
573        // record `stats.incomplete = true` -- never hang, never fabricate a
574        // merged interval that falsely claims to isolate multiple roots.
575        let poly = Polynomial::new(vec![rat(0), rat(-1), rat(0), rat(1)]);
576        let mut isolator = RootIsolator::default_config(poly);
577        let (lower, upper) = isolator.root_bounds();
578
579        let results = isolator.isolate_in_interval_bounded(lower, upper, 1);
580
581        assert!(
582            isolator.stats().incomplete,
583            "an insufficient depth budget must be recorded as incomplete"
584        );
585        assert!(
586            results.len() < 3,
587            "a truncated search must not fabricate all three roots, got {results:?}"
588        );
589    }
590
591    #[test]
592    fn test_isolate_in_interval_bounded_sufficient_depth_never_marks_incomplete() {
593        // The same cubic with a depth budget known to be sufficient (the
594        // default MAX_ROOT_ISOLATION_DEPTH) must isolate all three roots
595        // and never set `incomplete`.
596        let poly = Polynomial::new(vec![rat(0), rat(-1), rat(0), rat(1)]);
597        let mut isolator = RootIsolator::default_config(poly);
598        let intervals = isolator.isolate_roots();
599
600        assert_eq!(intervals.len(), 3);
601        assert!(!isolator.stats().incomplete);
602    }
603
604    #[test]
605    fn test_isolate_roots_deep_bisection_small_stack() {
606        // Two real roots 2^-2000 apart force many bisection levels (well
607        // under MAX_ROOT_ISOLATION_DEPTH, so this is a *deep-but-finite*
608        // case, not the depth-cap path) from inside a thread with a
609        // deliberately small (1 MiB) stack. A stack overflow aborts the
610        // whole process, so "the thread returned at all" is itself part of
611        // the assertion.
612        let handle = std::thread::Builder::new()
613            .stack_size(1 << 20)
614            .spawn(|| {
615                let mut den = BigInt::from(1u32);
616                for _ in 0..2000 {
617                    den *= 2;
618                }
619                let eps = BigRational::new(BigInt::from(1), den);
620                // p(x) = x*(x - eps) = x^2 - eps*x
621                let poly = Polynomial::new(vec![rat(0), -eps, rat(1)]);
622                let mut isolator = RootIsolator::default_config(poly);
623                let intervals = isolator.isolate_roots();
624                assert_eq!(intervals.len(), 2);
625                assert!(!isolator.stats().incomplete);
626            })
627            .expect("spawning a thread with an explicit stack size must succeed");
628        handle
629            .join()
630            .expect("a deep-but-finite bisection must not overflow a 1 MiB stack");
631    }
632}