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.
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.
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.
