Type Alias BoxOutcome 

pub type BoxOutcome = Outcome<BoxCertificate, BoxUnknown>;

Result of prove_nonnegative_on_box: an Outcome with a BoxCertificate or a BoxUnknown.

Aliased Type

pub enum BoxOutcome {
    Proved(BoxCertificate),
    #[non_exhaustive]
    Refuted {
        point: Vec<(Expr<Numeric>, Ratio<BigInt>)>,
        value: Ratio<BigInt>,
        param_value: Option<Ratio<BigInt>>,
    },
    Unknown(BoxUnknown),
}

Variants

Proved(BoxCertificate)

A certificate, re-verified with exact arithmetic before it was returned: the goal is non-negative on the set.

#[non_exhaustive]

Refuted

The goal is negative at this exact point of the set — the claim is false.

Fields

Non-exhaustive enum variants could have additional fields added in future. Therefore, non-exhaustive enum variants cannot be constructed in external crates and cannot be matched against.

point: Vec<(Expr<Numeric>, Ratio<BigInt>)>

(variable, value) pairs in the prover’s generator order; for a parametric set the parameter is the last entry.

value: Ratio<BigInt>

The (negative) value of the goal at point.

param_value: Option<Ratio<BigInt>>

The parameter value at which the counterexample lives, when the set depends on a parameter.

Unknown(BoxUnknown)

Neither a certificate nor a counterexample was found within the search; U says how far the search went. Never a wrong Proved.