Major Section: OTHER

Examples:where; Limit (mini-proveall) to about 1/4 second: (with-prover-time-limit 1/4 (mini-proveall))

; Limit (mini-proveall) to about 1/4 second, even if surrounding call of ; with-prover-time-limit provides for a more restrictive bound: (with-prover-time-limit '(1/4) (mini-proveall))

; Limit the indicated theorem to about 1/50 second, and if the proof does not ; complete or it fails, then put down a label instead. (mv-let (erp val state) (with-prover-time-limit 1/50 (thm (equal (append (append x x) x) (append x x x)))) (if erp (deflabel foo :doc "Attempt failed.") (value (list :succeeded-with val))))

General Form: (with-prover-time-limit time form)

`time`

evaluates to a positive rational number or to a list
containing such, and `form`

is arbitrary. Logically,
`(with-prover-time-limit time form)`

is equivalent to `form`

. However,
if the runtime for evaluation of `form`

exceeds the value specified by
`time`

, and if ACL2 notices this fact during a proof, then that proof will
abort, for example like this:
ACL2 Error in ( DEFTHM PERM-REFLEXIVE ...): Out of time in the rewriter.If there is already a surrounding call of

`with-prover-time-limit`

that has
set up an expiration time, the inner `with-prover-time-limit`

call is not
allowed to push that time further into the future unless the inner time is
specified as a list containing a rational, rather than as a rational.
Although `with-prover-time-limit`

is an ACL2 function -- in particular it
evaluates both its arguments -- nevertheless, it is not a standard function
in some respects. (1) The value of its first (time limit) argument affects
the evaluation of its second argument (by causing an error during that
evaluation if the time for completion is insufficient). (2) The second
argument can return multiple values (see mv), which are then returned by the
call of `with-prover-time-limit`

. (3) Thus, there is not a fixed number of
values returned by `with-prover-time-limit`

.

If you find that the time limit appears to be implemented too loosely, you are encouraged to email an example to the ACL2 implementors with instructions on how to observe the undesirable behavior. This information can probably be used to improve ACL2 by the insertion of more checks for expiration of the time limit.

The rest of this documentation topic explains the rather subtle logical
story, and is not necessary for understanding how to use
`with-prover-time-limit`

. The ACL2 `state`

object logically contains a
field called the `acl2-oracle`

, which is an arbitrary true list of objects.
This field can be read by a function called `read-acl2-oracle`

, which
however is untouchable (see push-untouchable), meaning that it is cannot be
called by ACL2 users. The `acl2-oracle`

field is thus ``secret''. Our
claim is that any ACL2 session makes sense for **some** value of
`acl2-oracle`

in the initial `state`

for that session. Logically,
`with-prover-time-limit`

is a no-op, just returning its second value. But
under the hood, it provides a ``hint'' for the `acl2-oracle`

, so that
(logically speaking) when its first element (`car`

) is consulted by
ACL2's prover to see if the time limit has expired, it gets the ``right''
answer (specifically, either nil if all is well or else a message to print if
the time limit has expired). Logically, the `acl2-oracle`

is then
`cdr`

'ed -- that is, its first element is popped off -- so that
future results from `read-acl2-oracle`

are independent of the one just
obtained.