SET-PROVER-STEP-LIMIT

sets the step-limit used by the ACL2 prover at the top level only
Major Section:  SWITCHES-PARAMETERS-AND-MODES

This event provides a way to limit the number of so-called ``prover steps'' permitted for an event. See with-prover-step-limit for a way to specify the limit on prover steps for a single event, rather than globally (and without the restriction mentioned above, pertaining to the top level). For a related utility based on time instead of prover steps, see with-prover-time-limit. For examples of how step limits work, see the community book books/misc/misc2/step-limits.lisp.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. Moreover, its effect is to set the acl2-defaults-table, and hence its effect is local to the book or encapsulate form containing it; see acl2-defaults-table.

Example Forms:
(set-prover-step-limit *default-step-limit*) ; no limit on prover steps
(set-prover-step-limit nil)   ; abbreviation for the form just above
(set-prover-step-limit 10000) ; allow at most 10,000 prover steps per event

General Form:
(set-prover-step-limit expr)
where expr evaluates either to nil or else to a natural number not exceeding the value of *default-step-limit*. If that value is nil or the value of *default-step-limit*, then no default limit is placed on the number of prover ``steps'' (see below) during processing of an event. Otherwise, that value is the maximum number of prover steps permitted before an error occurs.

This event specifies the limit on the number of ``steps'' counted by the ACL2 prover during processing of an event. Currently, a step is counted for each call of the system functions rewrite and expand-abbreviations. However, the steps counted may change in future releases of ACL2, so users would probably be well served by avoiding the assumption that only the above two calls are counted as prover steps.

Depending on the computer you are using, you may have only (very roughly) a half-hour of time before the number of prover steps exceeds the maximum step-limit, which is one less than the value of *default-step-limit*. Note however the exception stated above: if the ``limit'' is nil or is the value of *default-step-limit*, then no limit is imposed.

The limit is relevant for every event, to calls of thm and certify-book, and more generally, to any form that creates a ``summary context'' to print the usual event summary. The limit is also put in force when entering the proof-checker. Below, at the end of this documentation topic, we explain in detail when a call of set-prover-step-limit is in force: in brief, it applies to all forms that are either at the top level or are inside the same summary contexts.

Note that the limit applies to each event, not just ``atomic'' events. Consider the following example.

(set-prover-step-limit 500)

(encapsulate
  ()
  (defthm lemma-1 ; takes 380 steps
    (equal (append (append x y) z) (append x y z))
    :rule-classes nil)
  (defthm lemma-2 ; would take 319 steps
    (equal (len (append x y)) (+ (len x) (len y)))
    :rule-classes nil))
The first defthm event, lemma-1 takes 380 steps (as of this writing), as shown in the summary:
Prover steps counted:  380
LEMMA-1
The second defthm event, lemma-2, takes 319 steps (as of this writing) when evaluated at the top level. However, in the context above, 380 steps of the available 500 steps (from the set-prover-step-limit event above) have already been taken under the above encapsulate event. Thus, when the number of steps would exceed 120, the proof of lemma-2 is aborted:
ACL2 Error in STEP-LIMIT:  The prover step-limit, which is 120 in the
current context, has been exceeded.  See :DOC set-prover-step-limit.
The summary for lemma-2 reflects that situation:
Prover steps counted:  More than 120
The summary for the encapsulate events then indicates that the available steps for that event have also been exceeded:
Prover steps counted:  More than 500
The discussion above applies to any event that contains other events, hence applies similarly to progn events.

For those who use make-event, we note that prover steps in the expansion phase similarly contribute to the total number of steps counted. For example, suppose that the limit is 500 prover steps as above, and you submit (make-event EXPR), where 300 prover steps take place during evaluation of EXPR, producing event EV. Then evaluation of EV will cause an error if it takes more than 200 prover steps. This observation actually can be used to count prover steps for sequences of forms that are not all legal events (see embedded-event-form), such as calls of thm. For example, a small built-in ACL2 test suite that includes thm forms can be run by evaluating the form (mini-proveall), and the steps can be counted as shown below. (Here we assume a fresh ACL2 session; an error would occur if first, we evaluate the event (set-prover-step-limit 500) displayed above.)

ACL2 !>(make-event (er-progn (mini-proveall) (value '(value-triple nil))))
[[... output omitted here ...]]
Summary
Form:  ( MAKE-EVENT (ER-PROGN ...))
Rules: NIL
Warnings:  Double-rewrite, Equiv, Subsume and Non-rec
Time:  0.38 seconds (prove: 0.04, print: 0.29, other: 0.05)
Prover steps counted:  41090
 NIL
ACL2 !>

Technical Remark. For a call of mfc-rw or any mfc- function (see extended-metafunctions), the steps taken during that call are forgotten when returning from that call.

Finally, we discuss in some detail with a set-prover-step-limit event is in force: it applies to a subsequent form that is either at the top level or at the same level as the set-prover-step-limit form, in the following sense. Let us say that a ``summary context'' is any context for which the usual ACL2 summary will ultimately be printed (if summary printing is not inhibited). Every event -- a call of defun or defthm, or more generally, every embedded event form (see embedded-event-form) -- establishes a summary context, as do certain other top-level forms such as calls of thm and certify-book. (But a call of ld does not establish a summary context.) Here, we consider two forms to be at the same level if they are in the same summary contexts. Thus, if set-prover-step-limit is called at the top level, then this call is not in force for events under a call of certify-book, encapsulate, progn, make-event, or (more generally) under any form that establishes a summary context. Also, if set-prover-step-limit is called inside a summary context, then it does not apply above that summary context except, if it is not local to some event, at the very top level.