Expand description
Interval arithmetic with Poly endpoints. Allows attempted interval tracking, given non-negative variables, for e.g. loop bounds.
| operation | result | requires |
|---|---|---|
| $x + y$ | $[a + c, b + d]$ | |
| $-x$ | $[-b, -a]$ | |
| $px$ | $[pa, pb]$ | $p \geq 0$ |
| $xy$ | $[ac, bd]$ | $a \geq 0, c \geq 0$ |
| $x^n$ | $[a^n, b^n]$ | $n$ odd |
| $x^n$ | $[a^n, b^n]$ | $n$ even, $a \geq 0$ |
| $x^n$ | $[0, a^n + b^n]$ | $n$ even |
use sirius::solver::poly::{poly, Var, interval::Interval};
let nonneg = |_: Var| true;
let i = Interval::new(poly!(0), poly!(a - 1));
let j = Interval::new(poly!(0), poly!(b - 1));
let range = poly!(i*b + j)
.substitute_interval('j' as Var, &j, &nonneg)
.and_then(|r| r.substitute('i' as Var, &i, &nonneg))
.unwrap();
assert_eq!(range, Interval::new(poly!(0), poly!(a*b - 1)));