SET-CASE-SPLIT-LIMITATIONS

set the case-split-limitations 
Major Section:  EVENTS




Examples:
(set-case-split-limitations '(500 100))
(set-case-split-limitations 'nil)
(set-case-split-limitations '(500 nil))
The first of these prevents clausify 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.

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 acl2-defaults-table, and hence its effect is local to the book or encapsulate form containing it; see acl2-defaults-table. 

General Form:
(set-case-split-limitations lst)
where lst is either nil (denoting a list of two nils), or a list of length two, each element of which is either nil or a natural number. When nil is used as an element, it is treated as positive infinity. The default setting is (500 100).

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)            [1]
and another is 
(implies (and p (not q) r) s)      [2]
then the subsumption/replacement loop would produce the single subgoal 
(implies (and p r) s)              [3]
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.

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 nest of 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 different contexts.

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.