Major Section: SWITCHES-PARAMETERS-AND-MODES
Examples: (set-splitter-output t) ; enable reports of ``splitter'' rules (default) (set-splitter-output nil) ; disable reports of ``splitter'' rules
After evaluation of the form (set-splitter-output t) (the default), then
whenever prove output is not inhibited (see set-inhibit-output-lst),
ACL2 will report rewrite and definition rules that may have reduced
a goal to more than one subgoal. See splitter for how to interpret such
reports. We call such rules ``splitter rules'' for the goal that is being
split. This information can be useful in deciding how to eliminate large
splits, for example of Goal into Subgoal 1000 through Subgoal 1, by disabling
some splitter rules. If you want to avoid the printing of such information,
you can put the form (set-splitter-output t) in your customization file;
see acl2-customization.
Note that this command does not change the ACL2 world; it only modifies
the state. More precisely, it sets a state global to the indicated
value. (See state for discussion of the ``global-table'' of the state.)
When prove output is enabled (see set-inhibit-output-lst), the value of
that state global is the value of the form (splitter-output);
otherwise the value of that form is nil.
Again, see splitter for the effects of turning on the reporting of splitter rules.
