Optimized duplicate expression gatherer for leftright checking.
(vl-leftright-exprlist-duplicates x) → *
Originally I just used duplicated-members to check for duplicates. Profiling revealed that this was expensive. To speed it up, I made a benchmark out of some real calls of duplicated-members for leftright checking. Out of 396,966 calls, 396,945 of them (99.99+%) had no duplicated members. Furthermore, short lists are extremely common:
However, there are occasionally very long lists with over 600+ members. This function is just an optimized alternative to duplicated-members that seems to perform well on this kind of data set. We gain significant performance out of this function by memoizing vl-expr-strip.
Function:
(defun vl-leftright-exprlist-duplicates (x) (declare (xargs :guard (vl-exprlist-p x))) (declare (xargs :guard (true-listp x))) (let ((__function__ 'vl-leftright-exprlist-duplicates)) (declare (ignorable __function__)) (mbe :logic (hons-duplicated-members (vl-exprlist-fix x)) :exec (b* (((when (longer-than-p 25 x)) (hons-duplicated-members x)) ((when (no-duplicatesp-equal x)) nil)) (hons-duplicated-members x)))))
Theorem:
(defthm vl-leftright-exprlist-duplicates-of-vl-exprlist-fix-x (equal (vl-leftright-exprlist-duplicates (vl-exprlist-fix x)) (vl-leftright-exprlist-duplicates x)))
Theorem:
(defthm vl-leftright-exprlist-duplicates-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-leftright-exprlist-duplicates x) (vl-leftright-exprlist-duplicates x-equiv))) :rule-classes :congruence)