		Search-engine friendly clone of the ACL2 documentation.

Miscellaneous

Case-split-limitations

Limiting the number of immediate subgoals

Examples:
ACL2 !>(case-split-limitations (w state))
(500 100)

With the setting above, which is the default, clausify will not try subsumption/replacement if more than 500 clauses are involved. Furthermore, the simplifier, as it sweeps over a clause, will inhibit further case splits when it has accumulated 100 subgoals. To implement this inhibition, ACL2 refuses to rewrite subsequent literals, although it continues to split on any IF calls in those literals.

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 calls of f1 and splitting on the variables a, b, d, e, g, and h. But with the limit of 10 provided by set-case-split-limitations above, fewer cases are generated because rewriting of literals is inhibited, as explained below. Here is the first part of the output for that limit of 10.

[Note:  A hint was supplied for the goal above.  Thanks!]

This simplifies, using trivial observations, to

[Note:  A hint was supplied for 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 (EQUAL (F1 A B C) XXX) was rewritten, splitting into four cases; and for each of those cases, the second literal was rewritten, splitting further; and so on. However, the first time more than 10 cases were generated was when there were 10 cases generated so far and a literal generated four cases — then since that one literal generated four cases, 4-1 = 3 cases were added to the 10 already generated. From that point on, further rewriting of literals did not take place.

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.