		Search-engine friendly clone of the ACL2 documentation.

Std/alists

Worth-hashing

Heuristic for deciding when to use fast-alists.

Signature
(worth-hashing x) → bool

When alists are very short, it may be better for performance and memory usage to use naive alist algorithms instead of constructing hash tables.

(worth-hashing x) is a rough heuristic that is used in various fast-alist operations (e.g., fal-all-boundp) to decide when alists are long enough or will be used heavily enough to justify constructing hash tables.

It currently just decides whether x is longer than 18 elements long. This particular choice is just a historical oddity that probably has no empirical justification.

Definitions and Theorems

Function: worth-hashing$inline

(defun worth-hashing$inline (x)
  (declare (xargs :guard t))
  (let ((__function__ 'worth-hashing))
    (declare (ignorable __function__))
    (mbe :logic (>= (len x) 18)
         :exec (and (consp x)
                    (worth-hashing1 (cdr x) 17)))))