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. 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 less than 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, as well as for 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. A call of
`set-prover-step-limit`

applies to each subsequent form unless the call of
`set-prover-step-limit`

is within a summary context, in which case its
effect disappears when exiting that summary context.

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-1The 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 120The summary for the

`encapsulate`

event then indicates that the
available steps for that event have also been exceeded:
Prover steps counted: More than 500The 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.