		Search-engine friendly clone of the ACL2 documentation.

Debugging

Splitter

Reporting of rules whose application may have caused case splits

When the ACL2 rewriter applies a rule to a term, a goal might simplify to more than one subgoal. A rule with such an application is called a ``splitter''. Here, we explain the output produced for splitters when proof output is enabled (see set-inhibit-output-lst) and such reporting is turned on (as it is by default) — that is, when the value of (splitter-output) is true.

See set-splitter-output for how to turn off, or on, the reporting of splitters. Also see set-case-split-limitations for information on how to control case splits. Note that since splitters are rule applications, splitter output is not generated for case splits that are caused by other than rules, such as the mere presence of calls of the function symbol, if, in the goal.

We begin by describing three types of splitters.

if-intro: The rule application may have introduced a call of IF, in the sense discussed at the end below.

case-split: For the application of a rule with hypothesis of the form (case-split <hyp>), <hyp> did not simplify to true or false.

immed-forced: For the application of a rule with hypothesis of the form (force <hyp>), <hyp> did not simplify to true or false, where immediate-force-modep is enabled (see immediate-force-modep).

These three annotations — if-intro, case-split, and immed-forced — may be used in proof output and summaries for describing rule applications, as discussed below. A fourth annotation, forced, may also be used in proof output to indicate the application of a rule with hypothesis of the form (force <hyp>) when <hyp> did not simplify to true or false, where immediate-force-modep is disabled (see immediate-force-modep). We don't consider such uses of force to be splitters, because they do not cause case splits (though they do produce goals to prove after lower-case ``q.e.d.'' is printed); see force.

There are three kinds of output affected by splitters, illustrated in turn below using examples.

(a) During the proof, gag-mode and raw proof format (see set-raw-proof-format) off

(b) During the proof, gag-mode or raw proof format on

(c) Summary

Of course, (a) and (b) are skipped if proof output is inhibited, and (c) is skipped if summary output is inhibited; see set-inhibit-output-lst.

(a) During the proof, gag-mode and raw proof format (see set-raw-proof-format) off

With gag-mode off (or when using :pso, :psof, or :psog) one normally gets an English commentary. The following output indicates that at least one application of each rule F and G is of type if-intro, at least one application of rules G and R1 are of type case-split, and at least one application of rule R3 is of type immed-forced. If immediate-force-modep is off then ``immed-forced'' would be replaced by ``forced''.

This simplifies, using the :definitions F (if-intro), G (case-split and
if-intro) and H and the :rewrite rules R1, R2 (case-split), and
R3 (immed-forced), to the following two conjectures.

Note that any such printing of ``forced'' is done even if (splitter-output) is false.

(b) During the proof, gag-mode or raw proof format on

With gag-mode or raw proof format (see set-raw-proof-format) on, the proof output is abbreviated. However, in these cases ``Splitter Notes'' are printed so that one can still get important information to help control large case splits (by disabling splitter rules as appropriate). These are printed at the point when a goal splits into subgoals. Here, for example, is the Splitter Note that corresponds to the output shown in (a) above. It shows the goal whose simplification has produced a split into more than one subgoal, and it shows how many subgoals have been created.

Splitter note (see :DOC splitter) for Subgoal *1/2.2.1' (2 subgoals).
  case-split: ((:DEFINITION G) (:REWRITE R2))
  immed-forced: ((:REWRITE R3))
  if-intro: ((:DEFINITION G) (:DEFINITION F))

No such splitter notes are printed for the use of force (when immediate-force-modep is off).

Here is a possible summary corresponding to our running example. In the summary, ``Splitter rules'' is omitted if there are no splitter rules, and a splitter type is only mentioned if there is at least one corresponding splitter rule.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION F)
        (:DEFINITION G)
        (:DEFINITION H)
        (:REWRITE R1)
        (:REWRITE R2)
        (:REWRITE R3))
Splitter rules (see :DOC splitter):
  case-split: ((:DEFINITION G) (:REWRITE R2))
  immed-forced: ((:REWRITE R3))
  if-intro: ((:DEFINITION G) (:DEFINITION F))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  145

No indication for ``forced'' is given for ``Splitter rules''. (As discussed earlier above, the forced hypotheses are not considered relevant for determining splitter rule applications unless immediate-force-modep is on.)

We conclude by giving the criteria for a rewrite or definition rule application to be a splitter of type if-intro.

Reporting of splitter rules is on, i.e., the value of (splitter-output) is true.
At least two subgoals are created, even before considering subgoals generated by hypotheses that are calls of case-split or force.
The term to which the rule is applied is at the top level, rather than being encountered when trying to establish the hypothesis of a rule.
The rule is a rewrite rule, a definition rule, or a meta rule.
There is a call of the function symbol IF in the right-hand side of the rewrite rule; or, in the case of a definition rule, in the body of the definition; or, in the case of a meta rule, in the result of applying the metafunction.
There is a call of the function symbol IF in the result of rewriting: the right-hand side (for a rewrite rule), the definition body (for a definition rule), or the metafunction application (for a meta rule).

Any rule application meeting the above criteria will be considered a splitter of type if-intro, even if the call does not actually cause a case split. For example, if you are proving (implies (hyp x) (conc x)) and rule R rewrites (hyp x) to (if (h1 x) (h2 x) nil), which is really the term (and (h1 x) (h2 x)), then R may be labeled as a splitter rule. If you want to find the causes of case-splitting, the list of if-intro splitters can help you narrow your search, but may include irrelevant rules as well.

Finally, note that you may see splits not attributed to splitters. We believe that this will be uncommon during simplification, though it can occur for example when a call of IF is in the body of a let expression, i.e., in a call of a lambda expression. But splits caused by other processes, notably destructor elimination (see elim), will typically not be attributed to splitters.

Subtopics

Set-splitter-output: Turn on or off reporting of rules that may have caused case splits
Splitter-output: Status for reporting of splitter rules