WITH-PROVER-STEP-LIMIT

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. The optional extra argument, discussed below, is not evaluated.

Depending on the machine you are using, you may have only (very roughly) 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 besdies those presented below, see the distributed 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 same effect as described here.

Examples:

; Limit (mini-proveall) to 100,000 prover steps (which is enough to complete)
(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 limit (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))

; 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 either, nil, or to a natural number not exceeding the value of *default-step-limit*, or to the special value, :START. The extra argument, flg, should be Boolean if supplied.

If the value of expr is a non-negative integer 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, that value is the keyword :START, which is treated as follows.

- If a preceding call of set-prover-step-limit is in force, then this call provides the new limit or establishes that there is no limit. See set-prover-step-limit for a discussion of how this works.

- Otherwise, if there is a superior call of with-prover-step-limit, then if the immediately superior such call did not establish a limit, then there is no limit.

- Otherwise, if there is a superior call of with-prover-step-limit, then the limit is the current limit, i.e., the difference between the limit established by that superior call and the number of prover steps already recorded since the point of entering that call.

- Otherwise there is no limit.

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 form is an event (with-prover-step-limit k form1'). However, if form 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.