Fast list membership using make-lookup-alist.
(fast-memberp a x alist) → *
- alist — Guard (set-equiv (alist-keys alist) (list-fix x)).
In the logic, (fast-memberp a x alist) is just a list membership check;
we leave fast-memberp enabled and always reason about member-equal
However, our guard requires that alist is the result of running make-lookup-alist on x. Because of this, in the execution, the call of
member-equal call is instead carried out using hons-get on the
alist, and hence is a hash table lookup.
Definitions and Theorems
(defun fast-memberp$inline (a x alist)
(declare (xargs :guard (set-equiv (alist-keys alist)
(let ((__function__ 'fast-memberp))
(declare (ignorable __function__))
(mbe :logic (if (member-equal a x) t nil)
:exec (if (hons-get a alist) t nil))))