Skip to main content

prove_shifted

sirius::solver::t0

Function prove_shifted 

Source 
pub fn prove_shifted(
    cmp: Cmp,
    lhs: &Poly,
    rhs: &Poly,
    lower: &dyn Fn(Var) -> Option<i128>,
) -> bool
Expand description

prove given a constant lower bound per variable rather than a non-negative set. A variable with v >= c is rewritten as c + v' for a non-negative v', so 2*n - 2 >= 0 follows from n >= 1; a bound of 0 is the plain non-negative case.