(hons-clear gc) is a drastic garbage collection mechanism that clears out the underlying Hons Space.

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.