Rewrite-stack-limit
Limiting the stack depth of the ACL2 rewriter
ACL2 users can create rules of class :rewrite (see
rule-classes) that have the potential of causing an infinite loop in
the ACL2 rewriter. This could lead to Lisp stack overflows and even
segmentation faults. For this reason, the depth of certain calls of functions
in the ACL2 rewriter is limited by default using the value of the form
(rewrite-stack-limit (w state)). To see the limit in action, execute the
following forms.
(defthm app-assoc-1
(equal (append (append x y) z)
(append x y z)))
(defthm app-assoc-2
(equal (append x y z)
(append (append x y) z)))
(thm (equal (append a b c) xxx)
; try without these hints to see a slightly different error message
:hints (("Goal" :do-not '(preprocess))))
The ensuing error message shows a stack of one greater than the value of
(rewrite-stack-limit (w state)), which by default is the value of the
constant *default-rewrite-stack-limit*. The error message also explains
how to use :brr t and (cw-gstack) to find
looping rewrite rules.
This limit can be changed; see set-rewrite-stack-limit.
For a related limit, see backchain-limit.
Subtopics
- Set-rewrite-stack-limit
- Sets the rewrite stack depth used by the rewriter
