(hons-wash) is like gc$ but can also garbage collect normed
objects (CCL Only).
Major Section: HONS-AND-MEMOIZATION
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.
