Set the case-split-limitations

Also see case-split-limitations for an example of how this utility inhibits case splitting.

Examples: (set-case-split-limitations '(500 100)) (set-case-split-limitations 'nil) (set-case-split-limitations '(500 nil))

The first of these prevents

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.

See hints for discussion of a related hint,

General Form: (set-case-split-limitations lst)

where

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

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.

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); also see introduction-to-the-theorem-prover for a detailed tutorial on using the ACL2 prover. 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

If the second ``number'' is