		Search-engine friendly clone of the ACL2 documentation.

Filtering-by-name

Vl-filter-modinsts-by-modname

Partition a list of vl-modinsts by modname.

Signature
(vl-filter-modinsts-by-modname names x) → (mv named unnamed)
Arguments: names — Names to filter with.
Guard (string-listp names).; x — List to filter.
Guard (vl-modinstlist-p x).

The only reason to use this function is efficiency. Logically, named is equal to vl-keep-modinsts-by-modname and unnamed is equal to vl-delete-modinsts-by-modname. We leave this function enabled and would think it odd to ever prove a theorem about it.

Definitions and Theorems

Function: vl-filter-modinsts-by-modname

(defun vl-filter-modinsts-by-modname (names x)
 (declare (xargs :guard (and (string-listp names)
                             (vl-modinstlist-p x))))
 (let ((__function__ 'vl-filter-modinsts-by-modname))
  (declare (ignorable __function__))
  (mbe
    :logic
    (mv (vl-keep-modinsts-by-modname names x)
        (vl-delete-modinsts-by-modname names x))
    :exec
    (b*
      (((when (atom names))
        (mv nil (list-fix x)))
       ((when (atom x)) (mv nil nil))
       (fal (make-lookup-alist names))
       ((local-stobjs nrev nrev2)
        (mv yes no nrev nrev2))
       ((mv nrev nrev2)
        (vl-fast-filter-modinsts-by-modname names fal x nrev nrev2))
       (- (fast-alist-free fal))
       ((mv yes nrev) (nrev-finish nrev))
       ((mv no nrev2) (nrev-finish nrev2)))
      (mv yes no nrev nrev2)))))

Theorem: vl-fast-filter-modinsts-by-modname-removal-0

(defthm vl-fast-filter-modinsts-by-modname-removal-0
 (equal
   (mv-nth
        0
        (vl-fast-filter-modinsts-by-modname names fal x nrev nrev2))
   (append nrev
           (vl-keep-modinsts-by-modname names x))))

Theorem: vl-fast-filter-modinsts-by-modname-removal-1

(defthm vl-fast-filter-modinsts-by-modname-removal-1
 (equal
   (mv-nth
        1
        (vl-fast-filter-modinsts-by-modname names fal x nrev nrev2))
   (append nrev2
           (vl-delete-modinsts-by-modname names x))))

Subtopics

Vl-filter-modinsts-by-modname+: Same as vl-filter-modinsts-by-modname, but requires that the fast alist of names be provided instead of recomputing it.