(hons-clear gc) is a drastic garbage collection mechanism that clears out
the underlying Hons Space.
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-clear just returns nil; we leave it enabled and would think
it odd to ever prove a theorem about it.
Under the hood, hons-clear brutally (1) clears all the tables that govern
which conses are normed, then (2) optionally garbage collects, per the
gc argument, then finally (3) re-norms the keys of fast-alists and
persistently normed conses; see hons-copy-persistent.
Note. The hash tables making up the Hons Space retain their sizes after being
cleared. If you want to shrink them, see hons-resize.
Note. CCL users might prefer hons-wash, which is relatively efficient
and allows for the garbage collection of normed conses without impacting their
normed status.
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.
