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)
ACL2 Error in ( DEFTHM PERM-REFLEXIVE ...): Out of time in the rewriter.
If there is already a surrounding call of
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.
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