HONS-RESIZE

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.

General form:

 (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])

Example:

 (hons-resize :str-ht 100000
              :addr-ht (expt 2 27))

Logically, 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 normed, 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 normed objects.)

Advice for using hons-resize.

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.

Note that 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 hons-clear.