		Search-engine friendly clone of the ACL2 documentation.

Leftright-check

Vl-leftright-exprlist-duplicates

Optimized duplicate expression gatherer for leftright checking.

Signature
(vl-leftright-exprlist-duplicates x) → *
Arguments: x — Guard (vl-exprlist-p 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:

150,302 of them have only 2 elements (37%)
45,301 of them have only 3 elements (11%)
31,930 of them have only 4 elements (8%)
25,516 of them have only 5 elements (6%)

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.

Definitions and Theorems

Function: vl-leftright-exprlist-duplicates

(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: vl-leftright-exprlist-duplicates-of-vl-exprlist-fix-x

(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: vl-leftright-exprlist-duplicates-vl-exprlist-equiv-congruence-on-x

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