fast-alists are used inefficiently
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.
Obtaining hash-table performance from hons-get requires one to follow
a certain discipline. If this discipline is violated, you may see a "slow
alist warning". This warning means that the alist you are extending or
accessing does not have a valid hash table associated with it, and hence any
accesses must be carried out with hons-assoc-equal instead of
gethash.
You can control whether or not you get a warning and, if so, whether or not a break (an error from which you can continue) ensues. For instance:
(set-slow-alist-action :warning) ; warn on slow access (default) (set-slow-alist-action :break) ; warn and also call break$ (set-slow-alist-action nil) ; do not warn or break
The above forms expand to table events, so they can be embedded in
encapsulates and books, wrapped in local, and so on.
