Major Section: OTHER

Logically, `(with-prover-step-limit expr form)`

is equivalent to `form`

,
except that if the number of ``prover steps'' executed during evaluation of
`form`

exceeds a bound specified by the value of `expr`

, then that proof
will abort. See set-prover-step-limit for a related utility that sets the
limit on prover steps globally instead of setting it for just one form, and
for a discussion of the notion of ``prover steps'', which could change in
future ACL2 releases. For a related utility based on time instead of prover
steps, see with-prover-time-limit; but as discussed in the
documentation for `set-prover-step-limit`

, there is at best a loose
connection between the counting of steps and `with-prover-time-limit`

.

The arguments of `(with-prover-step-limit expr form)`

are evaluated.
However, the (optional) argument `flg`

is not evaluated in
`(with-prover-step-limit expr flg form)`

.

Depending on the machine you are using, you may have less than a half-hour of
time before the number of prover steps exceeds the maximum limit on prover
steps that may be imposed, which is one less than the value of
`*default-step-limit*`

. But there is no limit unless you explicitly call
`with-prover-step-limit`

or `set-prover-step-limit`

.

For examples of how step-limits work besides those presented below, see the
community book `books/misc/misc2/step-limits.lisp`

.

For a utility that returns an indicator of the number of prover steps most recently taken, see last-prover-steps.

Note that `with-prover-step-limit`

may not be called inside definitions,
and that it is simply the identity macro in raw Lisp. However,
`with-prover-step-limit!`

may be called in place of
`with-prover-step-limit`

, with the effect described here even in raw Lisp.

Examples: ; Limit (mini-proveall) to 100,000 prover steps (which happens to suffice) (with-prover-step-limit 100000 (mini-proveall)) ; Same as above for the inner call of with-prover-step-limit; so the ; mini-proveall call completes, but then we get an error because the second ; argument of the outer with-prover-step-limit call took more than 200 ; steps. (with-prover-step-limit 200 (with-prover-step-limit 100000 (mini-proveall))) ; Same as preceding form just above, except that this time there is no error, ; because the inner call of with-prover-step-limit has an extra argument ; of t inserted into the second argument position, which specifies that this ; entire inner call is treated as though it uses no prover steps. (with-prover-step-limit 200 (with-prover-step-limit 100000 t (mini-proveall))) ; The inner call limits (mini-proveall) to 200 prover steps, which fails ; almost immediately. (with-prover-step-limit 100000 (with-prover-step-limit 200 (mini-proveall))) ; Do not limit the number of prover steps, regardless of such a limit imposed ; globally or by the surrounding context. (with-prover-step-limit nil (mini-proveall)) ; Same as just above (indeed, nil above is converted to ; *default-step-limit*): (with-prover-step-limit *default-step-limit* (mini-proveall)) ; Advanced example: Limit the indicated theorem to 100 steps, and when the ; proof does not complete, then put down a label instead. (mv-let (erp val state) (with-prover-step-limit 100 (thm (equal (append (append x x) x) (append x x x)))) (if erp (deflabel foo :doc "Attempt failed.") (value (list :succeeded-with val)))) ; Use extra argument of t to avoid ``charging'' steps for the indicated ; form. (with-prover-step-limit 500 (encapsulate () (with-prover-step-limit 500 t ; Don't charge prover steps for this first defthm. (defthm test1 (equal (append x (append y z)) (append (append x y) z)) :rule-classes nil)) (defthm test2 (equal (append x (append y z)) (append (append x y) z)) :rule-classes nil))) General Forms: (with-prover-step-limit expr form) (with-prover-step-limit expr flg form)where

`form`

is an arbitrary form to evaluate, and `expr`

evaluates to
one of the following: `nil`

; a natural number not exceeding the value of
`*default-step-limit*`

; or the special value, `:START`

. The optional
extra argument in the second position, `flg`

, must be Boolean if supplied.If the value of `expr`

is a natural number less than the value of
`*default-step-limit*`

, then that value is the maximum number of prover
steps permitted during evaluation of `form`

before an error occurs. If
however the value of `expr`

is `nil`

or is the value of
`*default-step-limit*`

, then no limit is placed on the number of prover
steps during processing of `form`

. Otherwise, the value of `expr`

should
be the keyword `:START`

, which is intended for use by the ACL2
implementation and may have semantics that change with new ACL2 versions.

Finally we describe the optional extra Boolean argument, `flg`

. If `flg`

is `nil`

or omitted, then a running count of prover steps is maintained
after `form`

is evaluated; otherwise, that count is not affected by
evaluation of `form`

. To see how this works when `flg`

is nil or
omitted, consider an event of shape `(progn form1 form2)`

, where we are
tracking prover steps (say, because of a superior call of
`with-prover-step-limit`

). If `n`

is the number of prover steps
available when the `progn`

form is entered, and if `s`

prover steps are
executed while evaluating `form1`

, then `n-s`

steps are available for
evaluation of `form2`

provided `s`

does not exceed `n`

; otherwise, an
error occurs. In particular, this is the case if `form1`

is an event
`(with-prover-step-limit k form1')`

. However, if `form1`

is an event
`(with-prover-step-limit k t form1')`

, then because of the extra argument
of `t`

, no steps are ``charged'' to `form`

; that is, all `n`

steps,
rather than `n-s`

steps, are available for evaluation of `form2`

.