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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
<html>
<head><title>SET-CASE-SPLIT-LIMITATIONS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SET-CASE-SPLIT-LIMITATIONS</h2>set the case-split-limitations
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre><p>
Examples:
(set-case-split-limitations '(500 100))
(set-case-split-limitations 'nil)
(set-case-split-limitations '(500 nil))
</pre>
The first of these prevents <code>clausify</code> from trying the
subsumption/replacement (see below) loop if more than 500 clauses
are involved. It also discourages the clause simplifier from
splitting into more than 100 cases at once.<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. Moreover, its effect is to set the <code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code>, and
hence its effect is <code><a href="LOCAL.html">local</a></code> to the book or <code><a href="ENCAPSULATE.html">encapsulate</a></code> form
containing it; see <a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a>.
<p>
<pre>
General Form:
(set-case-split-limitations lst)
</pre>
where <code>lst</code> is either <code>nil</code> (denoting a list of two <code>nil</code>s), or a
list of length two, each element of which is either <code>nil</code> or a natural
number. When <code>nil</code> is used as an element, it is treated as positive
infinity. The default setting is <code>(500 100)</code>.<p>
The first number specifies the maximum number of clauses that may
participate in the ``subsumption/replacement'' loop. Because of the
expensive nature of that loop (which compares every clause to every
other in a way that is quadratic in the number of literals in the
clauses), when the number of clauses exceeds about 1000, the system
tends to ``go into a black hole,'' printing nothing and not even
doing many garbage collections (because the subsumption/replacement
loop does not create new clauses so much as it just tries to delete
old ones). The initial setting is lower than the threshold at which
we see noticeably bad performance, so you probably will not see this
behavior unless you have raised or disabled the limit.<p>
Why raise the subsumption/replacement limit? The
subsumption/replacement loop cleans up the set of subgoals produced
by the simplifier. For example, if one subgoal is
<pre>
(implies (and p q r) s) [1]
</pre>
and another is
<pre>
(implies (and p (not q) r) s) [2]
</pre>
then the subsumption/replacement loop would produce the single
subgoal
<pre>
(implies (and p r) s) [3]
</pre>
instead. This cleanup process is simply skipped when the number of
subgoals exceeds the subsumption/replacement limit. But each subgoal
must nonetheless be proved. The proofs of [1] and [2] are likely to
duplicate much work, which is only done once in proving [3]. So
with a low limit, you may find the system quickly produces a set of
subgoals but then takes a long time to prove that set. With a higher
limit, you may find the set of subgoals to be ``cleaner'' and faster
to prove. <p>
Why lower the subsumption/replacement limit? If you see the system
go into a ``black hole'' of the sort described above (no output, and
few garbage collections), it could due to the
subsumption/replacement loop working on a large set of large
subgoals. You might temporarily lower the limit so that
it begins to print the uncleaned set of subgoals. Perhaps by
looking at the output you will realize that some function can be
disabled so as to prevent the case explosion. Then raise or disable
the limit again!<p>
The second number in the case-split-limitations specifies how many
case splits the simplifier will allow before it begins to shut down
case splitting. In normal operation, when a literal rewrites to a
nest of <code>IF</code>s, the system simplifies all subsequent literals in
all the contexts generated by walking through the nest in all
possible ways. This can also cause the system to ``go into a black
hole'' printing nothing except garbage collection messages. This
``black hole'' behavior is different from than mentioned above
because space is typically being consumed at a prodigious rate,
since the system is rewriting the literals over and over in many
different contexts.<p>
As the simplifier sweeps across the clause, it keeps track of the
number of cases that have been generated. When that number exceeds
the second number in case-split-limitations, the simplifier stops
rewriting literals. The remaining, unrewritten, literals are copied
over into the output clauses. <code>IF</code>s in those literals are split
out, but the literals themselves are not rewritten. Each output
clause is then attacked again, by subsequent simplification, and
eventually the unrewritten literals in the tail of the clause will
be rewritten because the earlier literals will stabilize and stop
producing case splits.<p>
The default setting of 100 is fairly low. We have seen successful
proofs in which thousands of subgoals were created by a
simplification. By setting the second number to small values, you
can force the system to case split slowly. For example, a setting
of 5 will cause it to generate ``about 5'' subgoals per
simplification.<p>
You can read about how the simplifier works in the book
Computer-Aided Reasoning: An Approach (Kaufmann, Manolios, Moore).
If you think about it, you will see that with a low case limit, the
initial literals of a goal are repeatedly simplified, because each time
a subgoal is simplified we start at the left-most subterm. So when
case splitting prevents the later subterms from being fully split out,
we revisit the earlier terms before getting to the later ones. This
can be good. Perhaps it takes several rounds of rewriting before
the earlier terms are in normal form and then the later terms rewrite
quickly. But it could happen that the earlier terms are expensive to
rewrite and do not change, making the strategy of delayed case splits
less efficient. It is up to you.<p>
Sometimes the simplifier produces more clauses than you might
expect, even with case-split-limitations in effect. As noted above,
once the limit has been exceeded, the simplifier does not rewrite
subsequent literals. But <code>IF</code>s in those literals are split out
nonetheless. Furthermore, the enforcement of the limit is -- as
described above -- all or nothing: if the limit allows us to rewrite
a literal then we rewrite the literal fully, without regard for
limitations, and get as many cases as ``naturally'' are produced.
It quite often happens that a single literal, when expanded, may
grossly exceed the specified limits.<p>
If the second ``number'' is <code>nil</code> and the simplifier is going to
produce more than 1000 clauses, a ``helpful little message'' to
this effect is printed out. This output is printed to the
system's ``comment window'' not the standard proofs output.
<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>
|
