1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
<html>
<head><title>SET-REWRITE-STACK-LIMIT.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SET-REWRITE-STACK-LIMIT</h2>Sets the rewrite stack depth used by the rewriter
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical <a href="WORLD.html">world</a> and is so
recorded.<p>
<pre>
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 limit
</pre>
This event sets the maximum stack depth for calls of certain functions that
implement the ACL2 rewriter; see <a href="REWRITE-STACK-LIMIT.html">rewrite-stack-limit</a>. It must be a
non-negative integer less than 2^28. A call
<code>(set-rewrite-stack-limit limit)</code> is equivalent to:
<pre>
(table acl2-defaults-table :rewrite-stack-limit limit).
</pre>
The use of <code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code> ensures that this event's effect is
implicitly <code><a href="LOCAL.html">local</a></code> to the book or <code><a href="ENCAPSULATE.html">encapsulate</a></code> form in which it
occurs.
<p>
For a different but somewhat related concept, see <a href="BACKCHAIN-LIMIT.html">backchain-limit</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
