		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-design-remove-unnecessary-modules

Signature
(vl-design-remove-unnecessary-modules keep design) → new-design
Arguments: keep — Guard (string-listp keep).; design — Guard (vl-design-p design).
Returns: new-design — Type (vl-design-p new-design).

Definitions and Theorems

Function: vl-design-remove-unnecessary-modules

(defun vl-design-remove-unnecessary-modules (keep design)
  (declare (xargs :guard (and (string-listp keep)
                              (vl-design-p design))))
  (let ((__function__ 'vl-design-remove-unnecessary-modules))
    (declare (ignorable __function__))
    (b* ((design (vl-design-fix design))
         ((unless keep) design)
         (keep1 (mergesort (string-list-fix keep)))
         (keep2 (mergesort (vl-collect-new-names-from-orignames
                                keep1 (vl-design->mods design))))
         (keep (union keep1 keep2)))
      (vl-remove-unnecessary-elements keep design))))

Theorem: vl-design-p-of-vl-design-remove-unnecessary-modules

(defthm vl-design-p-of-vl-design-remove-unnecessary-modules
  (b*
   ((new-design (vl-design-remove-unnecessary-modules keep design)))
   (vl-design-p new-design))
  :rule-classes :rewrite)