The number of prover steps most recently taken
For discussions of prover step limits, See set-prover-step-limit and see with-prover-step-limit.
The summary printed for an event typically includes a line showing the prover steps counted, for example as follows.
Prover steps counted: 7240
The value of the form
The value of
nil, if no prover steps were taken, e.g., with (thm (equal x x)); else,
the (positive) number of steps taken, if the number of steps did not exceed the starting limit; else,
the negative of the starting limit.
Note that the ``most recently completed event'' in this sense includes compound events. Consider the following example.
(progn (thm (equal (append (append x y) z) (append x y z))) (thm (equal (car (cons x y)) x)))
The summaries show (in some ACL2 versions, at least) 435 steps for the
first call of
Prover steps counted: 435 Prover steps counted: More than 5 Prover steps counted: More than 440
Since the most recently completed event is the
We conclude with two remarks for advanced users who wish to invoke
Remark 1. Suppose that you want to write a utility that takes some action
based on the number of prover steps performed by the first event that is
generated within a sequence of events, for example the number of prover steps
taken to admit
(progn (defun f1 ...) (defun f2 ...))
A solution is to record the steps taken by the first defun before executing subsequent events, as follows (see make-event).
(progn (defun f1 ...) (make-event (pprogn (f-put-global 'my-step-count (last-prover-steps state) state) (value '(value-triple nil)))) (defun f2 ...))
Remark 2. It is possible to write utilities that are treated as events for purposes of the discussion above; that is, their calls can be
followed by evaluating