SET-NU-REWRITER-MODE

to turn on and off the nu-rewriter
Major Section:  EVENTS

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

This event sets a flag that controls whether the ACL2 rewriter uses the special-purpose nth/update-nth rewriter (nu-rewriter). The flag may have one of three values: nil, t, or :literals.

:set-nu-rewriter-mode nil       ; do not use nu-rewriter
:set-nu-rewriter-mode t         ; use nu-rewriter in rewriting
:set-nu-rewriter-mode :literals ; use nu-rewriter in rewriting after
                                ;  a pre-pass through every literal

The value nil prevents the use of the nu-rewriter. The other two values allow the use of the nu-rewriter.

When the flag is non-nil and the rewriter encounters a term that ``begins with an nth'', the nu-rewriter is applied. By ``begins with an nth'' here we mean either the term is an application of nth or is an application of some nonrecursive function or lambda expression whose body contains an expression that begins with an nth.

Note that the use of the nu-rewriter here described above is driven by the rewriter, i.e., the nu-rewriter is applied only to terms visited by the rewriter in its inside-out sweep. When the flag is set to :literals the system makes a pre-pass through every goal clause and applies the nu-rewriter to every subterm. The rewriter is then used on the output of that pre-pass.

We expect to write more documentation as we gain experience with the nu-rewriter.