limit the number of steps for proofs
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.


; 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 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 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)
         (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.
   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.