Hons-clear
(hons-clear gc) is a drastic garbage collection mechanism that
clears out the underlying Hons Space.
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.
Notes.
- The hash tables making up the Hons Space retain their sizes after being
cleared. If you want to shrink them, see hons-resize.
- CCL and GCL users might prefer hons-wash, which is relatively
efficient and allows for the garbage collection of normed conses without
impacting their normed status.
- 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.
- (For ACL2(p) users only; see parallelism) If parallel execution is
enabled (see set-parallel-execution), as it is by default in ACL2(p),
then hons-clear may be a no-op (other than to print a warning), in order
to avoid thread-unsafe behavior. (However, In CCL you are unlikely to see
this restriction unless you are running more than one thread.) To get around
this restriction, you can instead use hons-clear!, which however
requires a trust-tag.
Function: hons-clear
(defun hons-clear (gc)
(declare (xargs :guard t))
(declare (ignore gc))
nil)
