		Search-engine friendly clone of the ACL2 documentation.

Filtering-by-name

Vl-keep-modinsts-by-instname

Keep vl-modinst-ps by instname.

Signature
(vl-keep-modinsts-by-instname names x) → filtered-x
Arguments: names — Names of vl-modinsts to keep.
Guard (string-listp names).; x — List to filter.
Guard (vl-modinstlist-p x).
Returns: filtered-x — Type (vl-modinstlist-p filtered-x).

Definitions and Theorems

Function: vl-keep-modinsts-by-instname

(defun vl-keep-modinsts-by-instname (names x)
 (declare (xargs :guard (and (string-listp names)
                             (vl-modinstlist-p x))))
 (let ((__function__ 'vl-keep-modinsts-by-instname))
  (declare (ignorable __function__))
  (mbe
   :logic
   (cond ((atom x) nil)
         ((member-equal (vl-modinst->instname (car x))
                        (string-list-fix names))
          (cons (vl-modinst-fix (car x))
                (vl-keep-modinsts-by-instname names (cdr x))))
         (t (vl-keep-modinsts-by-instname names (cdr x))))
   :exec
   (b*
    (((when (or (atom names) (atom x))) nil)
     ((unless (longer-than-p 10 names))
      (vl-slow-keep-modinsts-by-instname names x))
     (fal (make-lookup-alist names))
     (ans
         (with-local-nrev
              (vl-fast-keep-modinsts-by-instname names fal x nrev)))
     (- (fast-alist-free fal)))
    ans))))

Theorem: vl-modinstlist-p-of-vl-keep-modinsts-by-instname

(defthm vl-modinstlist-p-of-vl-keep-modinsts-by-instname
  (b* ((filtered-x (vl-keep-modinsts-by-instname names x)))
    (vl-modinstlist-p filtered-x))
  :rule-classes :rewrite)

Theorem: vl-keep-modinsts-by-instname-when-atom

(defthm vl-keep-modinsts-by-instname-when-atom
  (implies (atom x)
           (equal (vl-keep-modinsts-by-instname names x)
                  nil)))

Theorem: vl-keep-modinsts-by-instname-of-cons

(defthm vl-keep-modinsts-by-instname-of-cons
  (equal (vl-keep-modinsts-by-instname names (cons a x))
         (if (member-equal (vl-modinst->instname a)
                           (string-list-fix names))
             (cons (vl-modinst-fix a)
                   (vl-keep-modinsts-by-instname names x))
           (vl-keep-modinsts-by-instname names x))))

Theorem: member-equal-of-vl-keep-modinsts-by-instname

(defthm member-equal-of-vl-keep-modinsts-by-instname
  (iff (member-equal a
                     (vl-keep-modinsts-by-instname names x))
       (and (member-equal a (vl-modinstlist-fix x))
            (member-equal (vl-modinst->instname a)
                          (string-list-fix names)))))

Theorem: subsetp-equal-of-vl-keep-modinsts-by-instname

(defthm subsetp-equal-of-vl-keep-modinsts-by-instname
  (subsetp-equal (vl-keep-modinsts-by-instname names x)
                 (vl-modinstlist-fix x)))

Theorem: vl-keep-modinsts-by-instname-when-atom-of-names

(defthm vl-keep-modinsts-by-instname-when-atom-of-names
  (implies (atom names)
           (equal (vl-keep-modinsts-by-instname names x)
                  nil)))

Theorem: vl-slow-keep-modinsts-by-instname-removal

(defthm vl-slow-keep-modinsts-by-instname-removal
  (equal (vl-slow-keep-modinsts-by-instname names x)
         (vl-keep-modinsts-by-instname names x)))

Theorem: vl-fast-keep-modinsts-by-instname-removal

(defthm vl-fast-keep-modinsts-by-instname-removal
  (equal (vl-fast-keep-modinsts-by-instname names fal x nrev)
         (append nrev
                 (vl-keep-modinsts-by-instname names x))))

Theorem: vl-keep-modinsts-by-instname-of-string-list-fix-names

(defthm vl-keep-modinsts-by-instname-of-string-list-fix-names
  (equal (vl-keep-modinsts-by-instname (string-list-fix names)
                                       x)
         (vl-keep-modinsts-by-instname names x)))

Theorem: vl-keep-modinsts-by-instname-string-list-equiv-congruence-on-names

(defthm
 vl-keep-modinsts-by-instname-string-list-equiv-congruence-on-names
 (implies (str::string-list-equiv names names-equiv)
          (equal (vl-keep-modinsts-by-instname names x)
                 (vl-keep-modinsts-by-instname names-equiv x)))
 :rule-classes :congruence)

Theorem: vl-keep-modinsts-by-instname-of-vl-modinstlist-fix-x

(defthm vl-keep-modinsts-by-instname-of-vl-modinstlist-fix-x
  (equal (vl-keep-modinsts-by-instname names (vl-modinstlist-fix x))
         (vl-keep-modinsts-by-instname names x)))

Theorem: vl-keep-modinsts-by-instname-vl-modinstlist-equiv-congruence-on-x

(defthm
  vl-keep-modinsts-by-instname-vl-modinstlist-equiv-congruence-on-x
  (implies (vl-modinstlist-equiv x x-equiv)
           (equal (vl-keep-modinsts-by-instname names x)
                  (vl-keep-modinsts-by-instname names x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-fast-keep-modinsts-by-instname
Vl-slow-keep-modinsts-by-instname