		Search-engine friendly clone of the ACL2 documentation.

Miscellaneous

With-prover-time-limit

Limit the time for proofs

Examples:

; 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)

where 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 time 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.

Note that by default, the time used is runtime (cpu time); to switch to realtime (elapsed time), see get-internal-time.

For a related utility based on prover steps instead of time, see with-prover-step-limit; also see set-prover-step-limit. Those utilities have the advantage of having platform-independent behavior, unlike time limits, which of course are generally less restrictive for faster processors. But note that the prover steps counted need not correspond closely to prover time. For other utilities that limit time, see with-timeout and oracle-timelimit.

Although with-prover-time-limit behaves like an ACL2 function in the sense that it evaluates both its arguments, it is however actually a macro that behaves as follows. (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, it may be because the prover only checks the time elapsed at certain points during the proof process, for example at entry to the rewriter. For example, if you write your own clause-processor that does an expensive computation, the time is unlikely to be checked during its execution. If however you find the time limit seems to be ignored even during ordinary prover operation, you are encouraged to email an example to the ACL2 implementors with instructions on how to observe the undesirable behavior. This information can perhaps 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; see read-ACL2-oracle. Our claim is that every 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.