Major Section: SWITCHES-PARAMETERS-AND-MODES-OH-MY
The first of these prevents
Examples: (set-case-split-limitations '(500 100)) (set-case-split-limitations 'nil) (set-case-split-limitations '(500 nil))
clausifyfrom 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.
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so
recorded. Moreover, its effect is to set the
hence its effect is
local to the book or
containing it; see acl2-defaults-table.
General Form: (set-case-split-limitations lst)where
nil(denoting a list of two
nils), or a list of length two, each element of which is either
nilor a natural number. When
nilis used as an element, it is treated as positive infinity. The default setting is
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.
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
(implies (and p q r) s) and another is
(implies (and p (not q) r) s) then the subsumption/replacement loop would produce the single subgoal
(implies (and p r) s) 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  and  are likely to duplicate much work, which is only done once in proving . 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.
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!
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
IFs, 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
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.
IFs 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.
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.
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.
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
IFs 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.
If the second ``number'' is
nil 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.