sets the step-limit used by the ACL2 prover at the top level only

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 distributed book books/misc/misc2/step-limits.lisp.


Example Forms:

General Form:
(set-prover-step-limit expr)


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)

  (defthm lemma-1 ; takes 380 steps
    :rule-classes nil)
  (defthm lemma-2 ; would take 319 steps
    :rule-classes nil))
Prover steps counted:  380
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


Rules: NIL
Prover steps counted:  41090
ACL2 !>


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.