Major Section: EVENTS
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
Example Forms: (set-rewrite-stack-limit 30) ; set to small limit :set-rewrite-stack-limit 30 ; same as above (set-rewrite-stack-limit *default-rewrite-stack-limit*) ; the default :set-rewrite-stack-limit (1- (expt 2 28)) ; maximum legal limit :set-rewrite-stack-limit nil ; same as above -- essentially, no limitThis event sets the maximum stack depth for calls of certain functions that implement the ACL2 rewriter; see rewrite-stack-limit. It must be a non-negative integer less than 2^28. A call
(set-rewrite-stack-limit limit)is equivalent to:
(table acl2-defaults-table :rewrite-stack-limit limit).The use of
acl2-defaults-tableensures that this event's effect is implicitly
localto the book or
encapsulateform in which it occurs.
For a different but somewhat related concept, see backchain-limit.