• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
          • Vl-keep-modinsts-by-modname
          • Vl-keep-modinsts-by-instname
          • Vl-delete-modinsts-by-instname
          • Vl-keep-imports-by-package
          • Vl-delete-modinsts-by-modname
          • Vl-delete-imports-by-package
          • Vl-keep-descriptions
          • Vl-delete-descriptions
          • Vl-keep-paramdecls
          • Vl-keep-interfaces
          • Vl-delete-paramdecls
          • Vl-delete-interfaces
          • Vl-keep-vardecls
          • Vl-keep-typedefs
          • Vl-keep-taskdecls
          • Vl-keep-programs
            • Vl-fast-keep-programs
            • Vl-slow-keep-programs
          • Vl-keep-portdecls
          • Vl-keep-packages
          • Vl-keep-fundecls
          • Vl-delete-taskdecls
          • Vl-delete-portdecls
          • Vl-keep-modules
          • Vl-keep-configs
          • Vl-keep-classes
          • Vl-delete-vardecls
          • Vl-delete-typedefs
          • Vl-delete-programs
          • Vl-delete-packages
          • Vl-delete-fundecls
          • Vl-delete-modules
          • Vl-delete-configs
          • Vl-delete-classes
          • Vl-keep-udps
          • Vl-delete-udps
          • Vl-filter-modinsts-by-modname+
          • Vl-filter-modinsts-by-modname
          • Vl-filter-modinsts-by-instname
          • Vl-filter-imports-by-package
          • Vl-filter-descriptions
          • Vl-filter-vardecls
          • Vl-filter-typedefs
          • Vl-filter-taskdecls
          • Vl-filter-programs
          • Vl-filter-portdecls
          • Vl-filter-paramdecls
          • Vl-filter-packages
          • Vl-filter-modules
          • Vl-filter-interfaces
          • Vl-filter-fundecls
          • Vl-filter-configs
          • Vl-filter-udps
          • Vl-filter-classes
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Filtering-by-name

Vl-keep-programs

Keep vl-program-ps by name.

Signature

(vl-keep-programs names x) → filtered-x

Arguments

names — Names of vl-programs to keep.
    Guard (string-listp names).

x — List to filter.
    Guard (vl-programlist-p x).

Returns

filtered-x — Type (vl-programlist-p filtered-x).

Definitions and Theorems

Function: vl-keep-programs

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

Theorem: vl-programlist-p-of-vl-keep-programs

(defthm vl-programlist-p-of-vl-keep-programs
  (b* ((filtered-x (vl-keep-programs names x)))
    (vl-programlist-p filtered-x))
  :rule-classes :rewrite)

Theorem: vl-keep-programs-when-atom

(defthm vl-keep-programs-when-atom
  (implies (atom x)
           (equal (vl-keep-programs names x) nil)))

Theorem: vl-keep-programs-of-cons

(defthm vl-keep-programs-of-cons
  (equal (vl-keep-programs names (cons a x))
         (if (member-equal (vl-program->name a)
                           (string-list-fix names))
             (cons (vl-program-fix a)
                   (vl-keep-programs names x))
           (vl-keep-programs names x))))

Theorem: member-equal-of-vl-keep-programs

(defthm member-equal-of-vl-keep-programs
  (iff (member-equal a (vl-keep-programs names x))
       (and (member-equal a (vl-programlist-fix x))
            (member-equal (vl-program->name a)
                          (string-list-fix names)))))

Theorem: subsetp-equal-of-vl-keep-programs

(defthm subsetp-equal-of-vl-keep-programs
  (subsetp-equal (vl-keep-programs names x)
                 (vl-programlist-fix x)))

Theorem: vl-keep-programs-when-atom-of-names

(defthm vl-keep-programs-when-atom-of-names
  (implies (atom names)
           (equal (vl-keep-programs names x) nil)))

Theorem: vl-slow-keep-programs-removal

(defthm vl-slow-keep-programs-removal
  (equal (vl-slow-keep-programs names x)
         (vl-keep-programs names x)))

Theorem: vl-fast-keep-programs-removal

(defthm vl-fast-keep-programs-removal
  (equal (vl-fast-keep-programs names fal x nrev)
         (append nrev (vl-keep-programs names x))))

Theorem: vl-keep-programs-of-string-list-fix-names

(defthm vl-keep-programs-of-string-list-fix-names
  (equal (vl-keep-programs (string-list-fix names)
                           x)
         (vl-keep-programs names x)))

Theorem: vl-keep-programs-string-list-equiv-congruence-on-names

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

Theorem: vl-keep-programs-of-vl-programlist-fix-x

(defthm vl-keep-programs-of-vl-programlist-fix-x
  (equal (vl-keep-programs names (vl-programlist-fix x))
         (vl-keep-programs names x)))

Theorem: vl-keep-programs-vl-programlist-equiv-congruence-on-x

(defthm vl-keep-programs-vl-programlist-equiv-congruence-on-x
  (implies (vl-programlist-equiv x x-equiv)
           (equal (vl-keep-programs names x)
                  (vl-keep-programs names x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-fast-keep-programs

Vl-slow-keep-programs