Limiting the number of immediate subgoals
Examples: ACL2 !>(case-split-limitations (w state)) (500 100)
With the setting above, which is the default,
The following example illustrates how the latter restriction — specifically, not rewriting subsequent literals to avoid further case splits — can work. We define a (rather nonsensical) function whose body introduces several cases.
(defun f1 (a b c) (if a (if b (equal c 0) (equal c 1)) (if b (equal c 2) (equal c 3)))) (set-case-split-limitations '(500 10)) (set-gag-mode nil) (thm (or (equal (f1 a b c) xxx) (equal (f1 d e f) yyy) (equal (f1 g h i) zzz)) :hints (("Goal" :in-theory (disable f1)) ("Goal'" :in-theory (enable f1))) :otf-flg t)
We show the output below. The simplification of the original goal to Goal' replaces the original goal, which is the clause (i.e., disjunction) consisting of the single literal (i.e., term) shown above, to the clause consisting of three literals, namely, the list:
; Goal', as a clause (disjunction of three literals) ((EQUAL (F1 A B C) XXX) (EQUAL (F1 D E F) YYY) (EQUAL (F1 G H I) ZZZ))
That simplification is reflected in the value printed (as an implication)
for Goal' in the output, below. If we omit the call of set-case-split-limitations above, then we get 64 cases, from opening up the
[Note: A hint was supplied of the goal above. Thanks!] This simplifies, using trivial observations, to [Note: A hint was supplied of the goal below. Thanks!] Goal' (IMPLIES (AND (NOT (EQUAL (F1 A B C) XXX)) (NOT (EQUAL (F1 D E F) YYY))) (EQUAL (F1 G H I) ZZZ)). This simplifies, using the :definition F1 (if-intro), to the following thirteen conjectures. Subgoal 13 (IMPLIES (AND A B (NOT (EQUAL (EQUAL C 0) XXX)) (NOT (EQUAL (F1 D E F) YYY))) (EQUAL (F1 G H I) ZZZ)).
Why, though, are there 13 cases, even though the limit was specified as 10?
Initially, the first literal
In short: the first time a literal splits into enough cases so that the accumulated number of cases exceeds the limit, rewriting stops — but that last split can put us significantly past the limit specified.
See set-case-split-limitations for a more general discussion.