(hons-resize ...)can be used to manually adjust the sizes of the hash
tables that govern which ACL2 Objects are considered normed.
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.
(hons-resize [:str-ht size] [:nil-ht size] [:cdr-ht size] [:cdr-ht-eql size] [:addr-ht size] [:other-ht size] [:sbits size] [:fal-ht size] [:persist-ht size])
(hons-resize :str-ht 100000 :addr-ht (expt 2 27))
hons-resize just returns nil; we leave it enabled and would
think it odd to ever prove a theorem about it.
Under the hood,
hons-resize can be used to change the sizes of certain hash
tables in the Hons Space.
All arguments are optional. The size given to each argument should either be nil (the default) or a natural number. A natural number indicates the newly desired size for the hash table, whereas nil means "don't resize this table." Any non-natural argument is regarded as nil.
You may wish to call this function for two reasons.
1. Improving Performance by Resizing Up
Since the hash tables in the Hons Space automatically grow as new objects are
hons-resize is unnecessary. But automatic growth can be slow
because it is incremental: a particular hash table might be grown dozens of
times over the course of your application. Using
hons-resize to pick a
more appropriate initial size may help to reduce this overhead.
2. Reducing Memory Usage by Resizing Down
Resizing can also be used to shrink the hash tables. This might possibly be
useful immediately after a
hons-clear to free up memory taken by the hash
tables themselves. (Of course, the tables will grow again as you create new
Advice for using
Note that hash tables that are already close to the desired size, or which have too many elements to fit into the desired size, will not actually be resized. This makes resizing relatively "safe."
Note that the
hons-summary function can be used to see how large and how
full your hash tables are. This may be useful in deciding what sizes you want
to give to
hons-resize operates by (1) allocating new hash tables, then (2)
copying everything from the old hash table into the new table. Because of
this, for best performance you should ideally call it when the hash tables
involved are minimally populated, i.e., at the start of your application, or
soon after a