pub fn verify(
path: &str,
rules: &[Rule],
model: &Model,
solver: &Solver,
) -> Result<Report, Vec<Error>>Expand description
Ask about every rule.
A rule that the solver settles at its own width is discharged and that is the end of it. A
rule it gives up on is asked again at BOUNDED_WIDTHS, but only if the rule carries a
written reason for taking narrow widths as enough, because a bounded proof is a judgement
somebody makes and not a fallback a tool takes on its own. A rule carrying such a reason gets
ten seconds at its real width rather than the whole budget, because what it is being asked
there is whether the reason has stopped being true.
ยงErrors
Anything the model cannot write out, and anything that stops the solver from running.