sirius/solver/
t0.rs

1//! Try to prove a goal given only a non-negative variable list.
2
3use crate::solver::Cmp;
4use crate::solver::poly::{Poly, Var, poly};
5
6/// Try to prove a goal given only a non-negative variable list.
7pub fn prove(cmp: Cmp, lhs: &Poly, rhs: &Poly, nonneg: &dyn Fn(Var) -> bool) -> bool {
8    match cmp {
9        Cmp::Eq => lhs == rhs,
10        Cmp::Ne => (lhs.sub(rhs)).as_constant().is_some_and(|c| !c.is_zero()),
11        Cmp::Le => less_or_eq(lhs, rhs, nonneg),
12        Cmp::Lt => less_or_eq(&(lhs.add(&poly!(1))), rhs, nonneg),
13        Cmp::Ge => less_or_eq(rhs, lhs, nonneg),
14        Cmp::Gt => less_or_eq(&(rhs.add(&poly!(1))), lhs, nonneg),
15    }
16}
17
18/// [`prove`] given a constant lower bound per variable rather than a non-negative set. A variable
19/// with `v >= c` is rewritten as `c + v'` for a non-negative `v'`, so `2*n - 2 >= 0` follows from
20/// `n >= 1`; a bound of `0` is the plain non-negative case.
21pub fn prove_shifted(
22    cmp: Cmp,
23    lhs: &Poly,
24    rhs: &Poly,
25    lower: &dyn Fn(Var) -> Option<i128>,
26) -> bool {
27    let shift = |p: &Poly| {
28        p.map_vars(|v| match lower(v) {
29            Some(c) if c != 0 => Poly::var(v, 1).add(&Poly::constant(c)),
30            _ => Poly::var(v, 1),
31        })
32    };
33    prove(cmp, &shift(lhs), &shift(rhs), &|v| lower(v).is_some())
34}
35
36fn less_or_eq(lhs: &Poly, rhs: &Poly, nonneg: &dyn Fn(Var) -> bool) -> bool {
37    lhs == rhs || rhs.sub(lhs).always_nonneg(nonneg)
38}
39
40#[cfg(test)]
41mod tests {
42    use super::{Cmp, Var, poly, prove};
43
44    fn all_but_a(v: Var) -> bool {
45        v != 'a' as Var
46    }
47
48    #[test]
49    fn nonnegative_differences_prove_leq() {
50        assert!(prove(Cmp::Le, &poly!(n), &poly!(n + 1), &all_but_a));
51        assert!(prove(Cmp::Le, &poly!(0), &poly!(n), &all_but_a));
52        assert!(prove(Cmp::Le, &poly!(n), &poly!(2 * n), &all_but_a));
53
54        assert!(!prove(Cmp::Lt, &poly!(0), &poly!(n), &all_but_a));
55        assert!(!prove(Cmp::Le, &poly!(1), &poly!(n), &all_but_a));
56    }
57
58    #[test]
59    fn rigid_sizes_not_nonneg() {
60        assert!(!prove(Cmp::Le, &poly!(0), &poly!(a), &all_but_a));
61    }
62
63    #[test]
64    fn lower_bounds_shift() {
65        use super::prove_shifted;
66
67        // n >= 1, a >= -2, nothing known about b
68        let lower = |v: Var| match v {
69            _ if v == 'n' as Var => Some(1),
70            _ if v == 'a' as Var => Some(-2),
71            _ => None,
72        };
73        assert!(prove_shifted(Cmp::Ge, &poly!(2 * n - 2), &poly!(0), &lower));
74        assert!(prove_shifted(
75            Cmp::Lt,
76            &poly!(n ^ 2 - 2 * n + 1),
77            &poly!(n ^ 2),
78            &lower
79        ));
80        assert!(prove_shifted(Cmp::Ge, &poly!(a + 2), &poly!(0), &lower));
81        assert!(prove_shifted(
82            Cmp::Ge,
83            &poly!(a * n + 2 * n),
84            &poly!(0),
85            &lower
86        ));
87        // a shifted variable is not itself non-negative
88        assert!(!prove_shifted(Cmp::Ge, &poly!(a), &poly!(0), &lower));
89        assert!(!prove_shifted(
90            Cmp::Ge,
91            &poly!(2 * n - 3),
92            &poly!(0),
93            &lower
94        ));
95        assert!(!prove_shifted(Cmp::Ge, &poly!(b), &poly!(0), &lower));
96        // equalities are unaffected by the change of variables
97        assert!(prove_shifted(
98            Cmp::Eq,
99            &poly!(n ^ 2 - 1),
100            &poly!(n ^ 2 - 1),
101            &lower
102        ));
103        assert!(!prove_shifted(
104            Cmp::Eq,
105            &poly!(n ^ 2 - 1),
106            &poly!(n ^ 2),
107            &lower
108        ));
109        assert!(prove_shifted(
110            Cmp::Ne,
111            &poly!(n ^ 2 - 1),
112            &poly!(n ^ 2),
113            &lower
114        ));
115    }
116}
sirius/solver/t0.rs

sirius/solver/
t0.rs
