(hons-wash) is like gc$ but can also garbage collect normed objects (CCL Only).

This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see hons-and-memoization.

Logically, hons-wash just returns nil; we leave it enabled and would think it odd to ever prove a theorem about it.

Under the hood, in CCL, hons-wash runs a garbage collection after taking special measures to allow normed conses to be collected. In Lisps other than CCL, hons-wash does nothing. This is because the efficient implementation of hons-wash is specific to the "static honsing" scheme which requires CCL-specific features.

Why is this function needed? Ordinarily, it is not possible to garbage collect any normed conses. This is because the Hons Space includes pointers to any normed conses, and hence Lisp's garbage collector thinks these objects are live. To correct for this, hons-wash (1) clears out these pointers, (2) runs a garbage collection, then (3) re-norms any previously-normed conses which have survived the garbage collection.

Note. It is not recommended to interrupt this function. Doing so may cause persistently normed conses and fast alist keys to become un-normed, which might lead to less efficient re-norming and/or violations of the fast-alist discipline.