functions that are invisible to the loop-stopper algorithm

ACL2 !>(invisible-fns-table (w state))
((binary-+ unary--)
 (binary-* unary-/)
 (unary-- unary--)
 (unary-/ unary-/))
Among other things, the setting above has the effect of making unary-- ``invisible'' for the purposes of applying permutative :rewrite rules to binary-+ trees. Also see add-invisible-fns, see remove-invisible-fns, and see set-invisible-fns-table.

See table for a general discussion of tables.

The ``invisible functions table'' is an alist with elements of the following form, where fn is a function symbol and the ufni are unary function symbols in the current ACL2 world, and k is at least 1.

(fn ufn1 ufn2 ... ufnk)

This table thus associates with certain function symbols, e.g., fn above, a set of unary functions, e.g., the ufni above. The ufni associated with fn in the invisible functions table are said to be ``invisible with respect to fn.'' If fn is not the car of any pair in the alist, then no function is invisible for it. Thus for example, setting the invisible functions alist to nil completely eliminates the consideration of invisibility.

The notion of invisibility is involved in the use of the :loop-stopper field of :rewrite rules to prevent the indefinite application of permutative rewrite rules. Roughly speaking, if rewrite rules are being used to permute arg and (ufni arg) inside of a nest of fn calls, and ufni is invisible with respect to fn, then arg and (ufni arg) are considered to have the same ``weight'' and will be permuted so as to end up as adjacent tips in the fn nest. See loop-stopper.