Enum WitnessRule 

pub enum WitnessRule {
    SolverAcceptance,
    DeclaredRowRelative,
}

Which accepting test the witness-refutation gate uses to decide that a sampled point satisfies a row.

The two forms exist because the question the witness answers is not always the same question. Both are accepting tests, so both must fail closed — when in doubt, accept the point, withdraw the verdict, keep the proof unclaimed.

Variants

SolverAcceptance

Default, and the only rule for any path where the solve can run.

Accepts a row when the residual is negligible at the row’s live magnitude through the clamped form tol * max(scale, 1) — i.e. exactly what the solver’s own acceptance test would wave through. This is the #380 rule: never certify what the solver itself would accept as feasible, or the same model reports “proved infeasible” with presolve on and Solve_Succeeded with it off.

DeclaredRowRelative

Only for paths where the solve provably cannot run, so no Solve_Succeeded counterfactual exists to contradict (today: the too-few-degrees-of-freedom gate, gh#391).

Accepts a row when the residual is negligible relative to the row’s declared magnitude, max(|g_l|, |g_u|) over its finite bounds, with no absolute clamp. Declared, not live: the live value moves with the sampled point, while the bounds are the magnitude the modeller wrote the row in — the same “declared, not live” pattern fbbt_infeasibility_survives_margin uses for its per-row margin.

Why the clamp has to go here: tol * max(scale, 1) reinstates an absolute floor once the row’s magnitude drops below 1, so multiplying every row of an infeasible model by 1e-12 — which changes the feasible set not at all — makes every point of the box “satisfy” every row and withdraws a scale-free bound-propagation proof. That is the whole of gh#391: s*x == 0.2*s with s*x == 0.8*s crosses by 0.6 at every s, yet the verdict flipped at s <= ~3e-8.

Why it is still safe: the clamp’s job is to not demand more precision than the solver promised, because a solver converges to absolute residuals. On this path the solver never produces a point at all, so there is no converged residual to be compatible with — the alternative to the proof is a structural error, not a solution.

The b = 0 hazard is handled explicitly and fails closed: a homogeneous row (g_l = g_u = 0, or a row with no finite bound at all) has no declared magnitude, which would make the relative test unsatisfiable by construction — viol == scale for any nonzero float noise — and a genuinely feasible point would fail to refute. Such a row keeps WitnessRule::SolverAcceptance’s clamped form, i.e. the absolute floor.

Trait Implementations

impl Clone for WitnessRule

fn clone(&self) -> WitnessRule

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for WitnessRule

impl Debug for WitnessRule

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for WitnessRule

fn default() -> WitnessRule

Returns the “default value” for a type.

impl Eq for WitnessRule

impl PartialEq for WitnessRule

fn eq(&self, other: &WitnessRule) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for WitnessRule