Skip to main content

pounce_presolve/fbbt/
interval.rs

1//! Rounded interval arithmetic for FBBT.
2//!
3//! Each operator returns an *outward-rounded* over-approximation: the
4//! result is guaranteed to contain the exact mathematical range, even
5//! after `f64` rounding errors in the underlying operation. This is
6//! the soundness property FBBT needs — over-approximation may produce
7//! a looser tightening than ideal, but it can never over-tighten and
8//! drop a feasible point.
9//!
10//! Rounding policy: every finite floating-point result is widened by
11//! one ULP outward (`next_down` on `lo`, `next_up` on `hi`) before
12//! returning. This costs one ULP of accuracy per operation but
13//! requires no FPU rounding-mode changes and works identically on
14//! every target. The accumulated padding is `O(ULP × depth)` for a
15//! DAG of depth `depth`, well within what FBBT tolerates.
16//!
17//! Function semantics on the empty interval propagate: any operation
18//! involving `EMPTY` returns `EMPTY`. The orchestrator interprets a
19//! leaf interval of `EMPTY` as "FBBT detected infeasibility" (the
20//! constraint's reverse propagation produced an empty variable
21//! interval).
22
23use pounce_common::types::Number;
24
25/// Closed interval `[lo, hi]` with outward rounding on operations.
26///
27/// `EMPTY` is encoded as `lo > hi` (specifically `lo = +∞`,
28/// `hi = -∞`). `ENTIRE` is `(-∞, +∞)`. Construction helpers normalize
29/// these for you.
30#[derive(Debug, Clone, Copy, PartialEq)]
31pub struct Interval {
32    pub lo: Number,
33    pub hi: Number,
34}
35
36impl Interval {
37    /// `[-∞, +∞]` — represents "no information".
38    pub const ENTIRE: Interval = Interval {
39        lo: Number::NEG_INFINITY,
40        hi: Number::INFINITY,
41    };
42
43    /// `∅` — empty set; sentinel for infeasibility.
44    pub const EMPTY: Interval = Interval {
45        lo: Number::INFINITY,
46        hi: Number::NEG_INFINITY,
47    };
48
49    /// Closed interval `[lo, hi]`. NaN endpoints or `lo > hi` collapse
50    /// to [`Self::EMPTY`] so downstream rules don't have to special-
51    /// case malformed input.
52    pub fn new(lo: Number, hi: Number) -> Self {
53        if lo.is_nan() || hi.is_nan() || lo > hi {
54            return Self::EMPTY;
55        }
56        Self { lo, hi }
57    }
58
59    /// Degenerate interval `[x, x]`. NaN collapses to `EMPTY`.
60    pub fn point(x: Number) -> Self {
61        if x.is_nan() {
62            return Self::EMPTY;
63        }
64        Self { lo: x, hi: x }
65    }
66
67    pub fn is_empty(&self) -> bool {
68        self.lo > self.hi || self.lo.is_nan() || self.hi.is_nan()
69    }
70
71    pub fn is_entire(&self) -> bool {
72        self.lo == Number::NEG_INFINITY && self.hi == Number::INFINITY
73    }
74
75    /// `true` iff `x ∈ [lo, hi]`.
76    pub fn contains(&self, x: Number) -> bool {
77        !self.is_empty() && self.lo <= x && x <= self.hi
78    }
79
80    pub fn contains_zero(&self) -> bool {
81        self.contains(0.0)
82    }
83
84    /// `hi - lo`, or 0 for empty. May be `+∞`.
85    pub fn width(&self) -> Number {
86        if self.is_empty() {
87            0.0
88        } else {
89            self.hi - self.lo
90        }
91    }
92
93    /// `[max(self.lo, other.lo), min(self.hi, other.hi)]`. Empty if
94    /// the result is malformed — this is the right semantics for
95    /// FBBT's "narrow against the constraint" step.
96    pub fn intersect(self, other: Self) -> Self {
97        if self.is_empty() || other.is_empty() {
98            return Self::EMPTY;
99        }
100        Self::new(self.lo.max(other.lo), self.hi.min(other.hi))
101    }
102
103    /// Convex hull `[min(lo, lo), max(hi, hi)]`. Empty if both inputs
104    /// are empty.
105    pub fn hull(self, other: Self) -> Self {
106        if self.is_empty() {
107            return other;
108        }
109        if other.is_empty() {
110            return self;
111        }
112        Self::new(self.lo.min(other.lo), self.hi.max(other.hi))
113    }
114
115    // -------- Arithmetic (outward-rounded) --------
116
117    pub fn add(self, rhs: Self) -> Self {
118        if self.is_empty() || rhs.is_empty() {
119            return Self::EMPTY;
120        }
121        Self {
122            lo: round_down(self.lo + rhs.lo),
123            hi: round_up(self.hi + rhs.hi),
124        }
125    }
126
127    pub fn sub(self, rhs: Self) -> Self {
128        if self.is_empty() || rhs.is_empty() {
129            return Self::EMPTY;
130        }
131        Self {
132            lo: round_down(self.lo - rhs.hi),
133            hi: round_up(self.hi - rhs.lo),
134        }
135    }
136
137    pub fn neg(self) -> Self {
138        if self.is_empty() {
139            return Self::EMPTY;
140        }
141        Self {
142            lo: -self.hi,
143            hi: -self.lo,
144        }
145    }
146
147    /// Interval multiplication — the classic four-corner formula.
148    pub fn mul(self, rhs: Self) -> Self {
149        if self.is_empty() || rhs.is_empty() {
150            return Self::EMPTY;
151        }
152        let p1 = self.lo * rhs.lo;
153        let p2 = self.lo * rhs.hi;
154        let p3 = self.hi * rhs.lo;
155        let p4 = self.hi * rhs.hi;
156        let lo = round_down(p1.min(p2).min(p3.min(p4)));
157        let hi = round_up(p1.max(p2).max(p3.max(p4)));
158        Self { lo, hi }
159    }
160
161    /// Division — returns `ENTIRE` (rather than a split / extended
162    /// interval) when `0 ∈ rhs`, since FBBT's reverse rules elsewhere
163    /// can recover useful information without the union-of-intervals
164    /// complexity here.
165    pub fn div(self, rhs: Self) -> Self {
166        if self.is_empty() || rhs.is_empty() {
167            return Self::EMPTY;
168        }
169        if rhs.contains_zero() {
170            // Conservative: any value is possible.
171            return Self::ENTIRE;
172        }
173        // Reciprocal endpoints must be outward-rounded before
174        // entering `mul`: `mul` rounds its four corner products by 1
175        // ULP, but that ±1 ULP does not compensate for an inward-
176        // rounded reciprocal (e.g. `1.0 / 3.0` evaluates one ULP
177        // below true 1/3 under IEEE round-to-nearest, so using it as
178        // the upper bound would exclude `1/3 + ε`).
179        self.mul(Self {
180            lo: round_down(1.0 / rhs.hi),
181            hi: round_up(1.0 / rhs.lo),
182        })
183    }
184
185    /// `[lo, hi]^n` for non-negative integer `n`. Handles the
186    /// non-monotone case `n` even, `0 ∈ self` correctly.
187    pub fn pow_uint(self, n: u32) -> Self {
188        if self.is_empty() {
189            return Self::EMPTY;
190        }
191        if n == 0 {
192            return Self::point(1.0);
193        }
194        if n == 1 {
195            return self;
196        }
197        let (a, b) = (self.lo, self.hi);
198        if n % 2 == 1 {
199            // Odd → monotone increasing.
200            Self {
201                lo: round_down(powi(a, n as i32)),
202                hi: round_up(powi(b, n as i32)),
203            }
204        } else if a >= 0.0 {
205            // Even, fully non-negative → monotone increasing.
206            Self {
207                lo: round_down(powi(a, n as i32)),
208                hi: round_up(powi(b, n as i32)),
209            }
210        } else if b <= 0.0 {
211            // Even, fully non-positive → monotone decreasing in
212            // magnitude; powers are non-negative with the smaller
213            // |.| inside the interval.
214            Self {
215                lo: round_down(powi(b, n as i32)),
216                hi: round_up(powi(a, n as i32)),
217            }
218        } else {
219            // Even, straddles zero → minimum is at 0, max at the
220            // extreme with larger |.|.
221            let ha = powi(a, n as i32);
222            let hb = powi(b, n as i32);
223            Self {
224                lo: 0.0,
225                hi: round_up(ha.max(hb)),
226            }
227        }
228    }
229
230    /// `√[lo, hi]`. Negative `lo` clipped to 0 (matches mathematical
231    /// domain). Empty input or fully-negative interval → `EMPTY`.
232    pub fn sqrt(self) -> Self {
233        if self.is_empty() || self.hi < 0.0 {
234            return Self::EMPTY;
235        }
236        let lo = self.lo.max(0.0).sqrt();
237        let hi = self.hi.sqrt();
238        Self {
239            lo: round_down(lo),
240            hi: round_up(hi),
241        }
242    }
243
244    /// `exp([lo, hi])` — monotone increasing.
245    pub fn exp(self) -> Self {
246        if self.is_empty() {
247            return Self::EMPTY;
248        }
249        Self {
250            lo: round_down(self.lo.exp()),
251            hi: round_up(self.hi.exp()),
252        }
253    }
254
255    /// `ln([lo, hi])` — monotone increasing on `x > 0`. `lo ≤ 0` is
256    /// clipped to the smallest positive finite (return `-∞` on the
257    /// low side). Fully-non-positive intervals → `EMPTY`.
258    pub fn ln(self) -> Self {
259        if self.is_empty() || self.hi <= 0.0 {
260            return Self::EMPTY;
261        }
262        let lo = if self.lo <= 0.0 {
263            Number::NEG_INFINITY
264        } else {
265            round_down(self.lo.ln())
266        };
267        Self {
268            lo,
269            hi: round_up(self.hi.ln()),
270        }
271    }
272
273    /// `|[lo, hi]|`.
274    pub fn abs(self) -> Self {
275        if self.is_empty() {
276            return Self::EMPTY;
277        }
278        if self.lo >= 0.0 {
279            self
280        } else if self.hi <= 0.0 {
281            self.neg()
282        } else {
283            // Straddles zero.
284            Self {
285                lo: 0.0,
286                hi: self.lo.abs().max(self.hi),
287            }
288        }
289    }
290
291    /// `sin([lo, hi])`. When the interval is wider than 2π or wraps
292    /// over both a peak and a trough we return `[-1, 1]`; otherwise
293    /// we test against the local extrema. A loose-but-sound choice.
294    pub fn sin(self) -> Self {
295        if self.is_empty() {
296            return Self::EMPTY;
297        }
298        trig_image(self.lo, self.hi, |x| x.sin(), SIN_PEAKS, SIN_TROUGHS)
299    }
300
301    /// `cos([lo, hi])`.
302    pub fn cos(self) -> Self {
303        if self.is_empty() {
304            return Self::EMPTY;
305        }
306        trig_image(self.lo, self.hi, |x| x.cos(), COS_PEAKS, COS_TROUGHS)
307    }
308
309    /// Element-wise `min(self, other)`.
310    pub fn min(self, other: Self) -> Self {
311        if self.is_empty() {
312            return Self::EMPTY;
313        }
314        if other.is_empty() {
315            return Self::EMPTY;
316        }
317        Self::new(self.lo.min(other.lo), self.hi.min(other.hi))
318    }
319
320    /// Element-wise `max(self, other)`.
321    pub fn max(self, other: Self) -> Self {
322        if self.is_empty() {
323            return Self::EMPTY;
324        }
325        if other.is_empty() {
326            return Self::EMPTY;
327        }
328        Self::new(self.lo.max(other.lo), self.hi.max(other.hi))
329    }
330}
331
332// -------- Rounding helpers --------
333
334/// Outward round on the low end: nudge `x` one ULP toward `-∞`.
335/// Identity on infinities and NaN.
336fn round_down(x: Number) -> Number {
337    if x.is_finite() {
338        x.next_down()
339    } else {
340        x
341    }
342}
343
344/// Outward round on the high end: nudge `x` one ULP toward `+∞`.
345fn round_up(x: Number) -> Number {
346    if x.is_finite() {
347        x.next_up()
348    } else {
349        x
350    }
351}
352
353/// `x^n` for non-negative `n`, with `0^0 = 1` (Rust's `f64::powi`
354/// convention).
355fn powi(x: Number, n: i32) -> Number {
356    x.powi(n)
357}
358
359// -------- Trigonometric image bounds --------
360//
361// For `sin([a,b])` we check whether the interval crosses any
362// peak (`x` where sin x = 1, i.e. π/2 + 2πk) or trough
363// (`x` where sin x = -1, i.e. -π/2 + 2πk). If it does, the global
364// max / min is locked. Otherwise the image is between the endpoint
365// values. Same for cos.
366
367const TWO_PI: Number = 2.0 * std::f64::consts::PI;
368const SIN_PEAKS: Number = std::f64::consts::FRAC_PI_2; // π/2 + 2πk
369const SIN_TROUGHS: Number = -std::f64::consts::FRAC_PI_2;
370const COS_PEAKS: Number = 0.0; // 0 + 2πk
371const COS_TROUGHS: Number = std::f64::consts::PI; // π + 2πk
372
373fn trig_image<F>(
374    lo: Number,
375    hi: Number,
376    f: F,
377    peak_offset: Number,
378    trough_offset: Number,
379) -> Interval
380where
381    F: Fn(Number) -> Number,
382{
383    if !lo.is_finite() || !hi.is_finite() {
384        // Unbounded → can hit any value in [-1, 1].
385        return Interval::new(-1.0, 1.0);
386    }
387    if hi - lo >= TWO_PI {
388        return Interval::new(-1.0, 1.0);
389    }
390    // Reference k such that the closest peak ≥ lo is at peak_offset
391    // + 2πk.
392    let crosses = |offset: Number| -> bool {
393        let k = ((lo - offset) / TWO_PI).ceil();
394        let x = offset + TWO_PI * k;
395        x <= hi
396    };
397    let endpoint_lo = f(lo);
398    let endpoint_hi = f(hi);
399    let mut local_min = endpoint_lo.min(endpoint_hi);
400    let mut local_max = endpoint_lo.max(endpoint_hi);
401    if crosses(peak_offset) {
402        local_max = 1.0;
403    }
404    if crosses(trough_offset) {
405        local_min = -1.0;
406    }
407    Interval {
408        lo: round_down(local_min),
409        hi: round_up(local_max),
410    }
411}
412
413#[cfg(test)]
414mod tests {
415    use super::*;
416
417    fn approx_eq(a: Number, b: Number, eps: Number) -> bool {
418        (a - b).abs() <= eps + eps * b.abs()
419    }
420
421    #[test]
422    fn empty_propagates() {
423        let e = Interval::EMPTY;
424        let a = Interval::new(0.0, 1.0);
425        assert!(e.add(a).is_empty());
426        assert!(a.add(e).is_empty());
427        assert!(e.mul(a).is_empty());
428        assert!(e.sqrt().is_empty());
429        assert!(e.exp().is_empty());
430    }
431
432    #[test]
433    fn new_normalizes_malformed() {
434        assert!(Interval::new(1.0, 0.0).is_empty());
435        assert!(Interval::new(Number::NAN, 1.0).is_empty());
436        assert!(Interval::new(1.0, Number::NAN).is_empty());
437    }
438
439    #[test]
440    fn entire_is_entire() {
441        assert!(Interval::ENTIRE.is_entire());
442        assert!(Interval::ENTIRE.contains_zero());
443        assert!(!Interval::EMPTY.is_entire());
444    }
445
446    #[test]
447    fn add_widens_outward() {
448        // [1, 2] + [3, 4] = [4, 6] (outward-rounded).
449        let r = Interval::new(1.0, 2.0).add(Interval::new(3.0, 4.0));
450        assert!(r.lo <= 4.0 && 4.0 - r.lo < 1e-15);
451        assert!(r.hi >= 6.0 && r.hi - 6.0 < 1e-15);
452    }
453
454    #[test]
455    fn sub_uses_cross_endpoints() {
456        // [1, 2] - [3, 4] = [-3, -1].
457        let r = Interval::new(1.0, 2.0).sub(Interval::new(3.0, 4.0));
458        assert!(r.lo <= -3.0 && -3.0 - r.lo < 1e-15);
459        assert!(r.hi >= -1.0 && r.hi - (-1.0) < 1e-15);
460    }
461
462    #[test]
463    fn mul_handles_sign_crossings() {
464        // [-2, 3] * [-1, 4] — must consider all four corners.
465        // Min is (-2)*4 = -8; max is 3*4 = 12.
466        let r = Interval::new(-2.0, 3.0).mul(Interval::new(-1.0, 4.0));
467        assert!(r.contains(-8.0));
468        assert!(r.contains(12.0));
469        assert!(r.lo <= -8.0);
470        assert!(r.hi >= 12.0);
471    }
472
473    #[test]
474    fn div_by_zero_crossing_yields_entire() {
475        let r = Interval::new(1.0, 2.0).div(Interval::new(-1.0, 1.0));
476        assert!(r.is_entire());
477    }
478
479    #[test]
480    fn div_disjoint_from_zero_inverts_correctly() {
481        // [1, 4] / [2, 4] ⊆ [1/4, 2] = [0.25, 2].
482        let r = Interval::new(1.0, 4.0).div(Interval::new(2.0, 4.0));
483        assert!(r.contains(0.25));
484        assert!(r.contains(2.0));
485        assert!(r.lo <= 0.25);
486        assert!(r.hi >= 2.0);
487    }
488
489    #[test]
490    fn pow_uint_even_straddles_zero() {
491        // [-2, 3]^2 = [0, 9].
492        let r = Interval::new(-2.0, 3.0).pow_uint(2);
493        assert_eq!(r.lo, 0.0);
494        assert!(r.hi >= 9.0);
495    }
496
497    #[test]
498    fn pow_uint_even_negative() {
499        // [-4, -2]^2 = [4, 16].
500        let r = Interval::new(-4.0, -2.0).pow_uint(2);
501        assert!(r.lo <= 4.0);
502        assert!(r.hi >= 16.0);
503    }
504
505    #[test]
506    fn pow_uint_odd() {
507        // [-2, 3]^3 = [-8, 27].
508        let r = Interval::new(-2.0, 3.0).pow_uint(3);
509        assert!(r.lo <= -8.0);
510        assert!(r.hi >= 27.0);
511    }
512
513    #[test]
514    fn pow_zero_and_one() {
515        let i = Interval::new(2.0, 5.0);
516        let z = i.pow_uint(0);
517        assert_eq!(z.lo, 1.0);
518        assert_eq!(z.hi, 1.0);
519        let o = i.pow_uint(1);
520        assert_eq!(o, i);
521    }
522
523    #[test]
524    fn sqrt_clips_negative_lo() {
525        // Domain clip: sqrt([-1, 4]) takes the positive part of the
526        // domain. The mathematical lower bound is 0; outward rounding
527        // is allowed to nudge it one ULP below zero (still a valid
528        // over-approximation).
529        let r = Interval::new(-1.0, 4.0).sqrt();
530        assert!(r.lo <= 0.0);
531        assert!(r.lo >= -1e-300, "outward bump should be at most ~1 ULP");
532        assert!(r.hi >= 2.0);
533    }
534
535    #[test]
536    fn sqrt_of_fully_negative_is_empty() {
537        assert!(Interval::new(-4.0, -1.0).sqrt().is_empty());
538    }
539
540    #[test]
541    fn exp_is_monotone() {
542        let r = Interval::new(0.0, 1.0).exp();
543        assert!(r.contains(1.0));
544        assert!(r.contains(std::f64::consts::E));
545    }
546
547    #[test]
548    fn ln_of_non_positive_is_empty() {
549        assert!(Interval::new(-2.0, -1.0).ln().is_empty());
550        assert!(Interval::new(-2.0, 0.0).ln().is_empty());
551    }
552
553    #[test]
554    fn ln_with_zero_lower_yields_neg_inf() {
555        let r = Interval::new(0.0, 1.0).ln();
556        assert_eq!(r.lo, Number::NEG_INFINITY);
557        assert!(r.contains(0.0));
558    }
559
560    #[test]
561    fn ln_strict_positive() {
562        // ln([1, e]) ⊆ [0, 1].
563        let r = Interval::new(1.0, std::f64::consts::E).ln();
564        assert!(r.contains(0.0));
565        assert!(r.contains(1.0));
566    }
567
568    #[test]
569    fn abs_negative_interval() {
570        let r = Interval::new(-3.0, -1.0).abs();
571        assert!(r.contains(1.0));
572        assert!(r.contains(3.0));
573    }
574
575    #[test]
576    fn abs_straddling_interval() {
577        let r = Interval::new(-2.0, 3.0).abs();
578        assert_eq!(r.lo, 0.0);
579        assert!(r.hi >= 3.0);
580    }
581
582    #[test]
583    fn sin_full_range() {
584        // sin([0, 2π]) = [-1, 1].
585        let r = Interval::new(0.0, TWO_PI).sin();
586        assert!(approx_eq(r.lo, -1.0, 1e-15));
587        assert!(approx_eq(r.hi, 1.0, 1e-15));
588    }
589
590    #[test]
591    fn sin_within_one_branch() {
592        // sin([0, π/2]) = [0, 1].
593        let r = Interval::new(0.0, std::f64::consts::FRAC_PI_2).sin();
594        assert!(r.contains(0.0));
595        assert!(r.contains(1.0));
596    }
597
598    #[test]
599    fn cos_at_zero() {
600        // cos([-ε, ε]) ⊆ [1-O(ε²), 1].
601        let r = Interval::new(-0.1, 0.1).cos();
602        assert!(r.contains(1.0));
603        assert!(r.lo < 1.0);
604    }
605
606    #[test]
607    fn intersect_disjoint_is_empty() {
608        assert!(Interval::new(0.0, 1.0)
609            .intersect(Interval::new(2.0, 3.0))
610            .is_empty());
611    }
612
613    #[test]
614    fn intersect_overlap() {
615        let r = Interval::new(0.0, 5.0).intersect(Interval::new(3.0, 10.0));
616        assert_eq!(r, Interval::new(3.0, 5.0));
617    }
618
619    #[test]
620    fn hull_combines() {
621        let r = Interval::new(0.0, 1.0).hull(Interval::new(5.0, 6.0));
622        assert_eq!(r, Interval::new(0.0, 6.0));
623    }
624
625    #[test]
626    fn min_max_pairs() {
627        let a = Interval::new(1.0, 5.0);
628        let b = Interval::new(2.0, 7.0);
629        let mn = a.min(b);
630        assert!(mn.contains(1.0));
631        assert!(mn.contains(5.0));
632        let mx = a.max(b);
633        assert!(mx.contains(2.0));
634        assert!(mx.contains(7.0));
635    }
636
637    /// Soundness fuzz: for random `[a, b]` and random `x ∈ [a, b]`,
638    /// the operation's result must contain `f(x)` exactly.
639    #[test]
640    fn fuzz_add_contains_pointwise() {
641        let cases = [
642            ((0.5, 2.5), (1.0, 1.5), 1.5, 2.0),
643            ((-3.0, 1.0), (-1.0, 4.0), 0.5, 2.5),
644            ((1.0e-10, 1.0e10), (1.0, 1.0), 100.0, 1.0),
645        ];
646        for &((a, b), (c, d), x, y) in &cases {
647            let i = Interval::new(a, b).add(Interval::new(c, d));
648            assert!(i.contains(x + y), "{a},{b} + {c},{d} ∌ {x}+{y}");
649        }
650    }
651
652    #[test]
653    fn fuzz_mul_contains_pointwise() {
654        let cases = [
655            ((-2.0, 3.0), (-1.0, 4.0), 0.5, 2.0),
656            ((1.0, 10.0), (0.1, 0.2), 5.0, 0.15),
657            ((-5.0, -1.0), (-3.0, -1.0), -3.0, -2.0),
658        ];
659        for &((a, b), (c, d), x, y) in &cases {
660            let i = Interval::new(a, b).mul(Interval::new(c, d));
661            assert!(i.contains(x * y), "{a},{b} × {c},{d} ∌ {x}×{y}");
662        }
663    }
664
665    #[test]
666    fn fuzz_div_contains_pointwise() {
667        // Reciprocal endpoints round inward under IEEE round-to-
668        // nearest, so `div` must explicitly outward-round them
669        // before entering `mul`. The `(0.1, 0.2) / (3.0, 4.0)` case
670        // hits a reciprocal-of-3 boundary; the second is a sanity
671        // check that the result still contains the exact midpoint.
672        let cases = [
673            ((0.1, 0.2), (3.0, 4.0), 0.15, 3.5),
674            ((1.0, 1.0), (3.0, 3.0), 1.0, 3.0),
675            ((-2.0, 5.0), (1.0, 7.0), 1.5, 3.0),
676        ];
677        for &((a, b), (c, d), x, y) in &cases {
678            let i = Interval::new(a, b).div(Interval::new(c, d));
679            assert!(i.contains(x / y), "{a},{b} / {c},{d} ∌ {x}/{y}");
680        }
681    }
682
683    /// Outward rounding is observable: `(a + b) - b` may not be
684    /// exactly `a`, but the resulting interval must still contain
685    /// `a`.
686    #[test]
687    fn rounding_does_not_shrink_below_truth() {
688        let one = Interval::point(0.1);
689        let two = Interval::point(0.2);
690        let sum = one.add(two);
691        assert!(sum.contains(0.3));
692    }
693}