• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • 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-keep-descriptions
            • Vl-delete-imports-by-package
            • Vl-delete-descriptions
            • Vl-delete-paramdecls
            • Vl-delete-interfaces
            • Vl-keep-taskdecls
            • Vl-keep-portdecls
            • Vl-keep-paramdecls
            • Vl-keep-interfaces
            • Vl-keep-vardecls
            • Vl-keep-typedefs
            • Vl-keep-programs
            • 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-modules
            • Vl-delete-fundecls
            • 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-classes
            • Vl-filter-udps
          • Vl-interface-mocktype
          • Stripping-functions
          • Genblob
          • Expr-tools
          • Hierarchy
          • Extract-vl-types
          • 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
    • Testing-utilities
    • Math
  • Mlib

Filtering-by-name

Functions for filtering lists of parsed objects by their names.

We implement functions for keeping and deleting objects by their names, and also for partitioning lists of objects into named and unnamed sub-lists.

These functions are logically simple, but we use MBE to make them fairly efficient. In particular, suppose we want to keep, delete, or filter the list x using some list of names.

  • If there are only a few names, we use naive algorithm that calls member-equal repeatedly, and this is effectively O(|x|).
  • When there are many names, we use make-lookup-alist to construct a temporary, fast alist, and use fast-memberp to perform the lookups. Assuming that hashing operations are constant time, constructing this table is O(|names|), and the subsequent processing of x is O(|x|).

These functions preserve the order of the initial list. The order of names is irrelevant, and any spurious names that aren't among the names of x are simply ignored.

See also finding-by-name for related functions that can also be used to look up objects by their names and to rearrange objects by their names.

Subtopics

Vl-keep-modinsts-by-modname
Keep vl-modinst-ps by modname.
Vl-keep-modinsts-by-instname
Keep vl-modinst-ps by instname.
Vl-delete-modinsts-by-instname
Delete vl-modinsts by instname.
Vl-keep-imports-by-package
Keep vl-import-ps by package.
Vl-delete-modinsts-by-modname
Delete vl-modinsts by modname.
Vl-keep-descriptions
Keep vl-description-ps by name.
Vl-delete-imports-by-package
Delete vl-imports by package.
Vl-delete-descriptions
Delete vl-descriptions by name.
Vl-delete-paramdecls
Delete vl-paramdecls by name.
Vl-delete-interfaces
Delete vl-interfaces by name.
Vl-keep-taskdecls
Keep vl-taskdecl-ps by name.
Vl-keep-portdecls
Keep vl-portdecl-ps by name.
Vl-keep-paramdecls
Keep vl-paramdecl-ps by name.
Vl-keep-interfaces
Keep vl-interface-ps by name.
Vl-keep-vardecls
Keep vl-vardecl-ps by name.
Vl-keep-typedefs
Keep vl-typedef-ps by name.
Vl-keep-programs
Keep vl-program-ps by name.
Vl-keep-packages
Keep vl-package-ps by name.
Vl-keep-fundecls
Keep vl-fundecl-ps by name.
Vl-delete-taskdecls
Delete vl-taskdecls by name.
Vl-delete-portdecls
Delete vl-portdecls by name.
Vl-keep-modules
Keep vl-module-ps by name.
Vl-keep-configs
Keep vl-config-ps by name.
Vl-keep-classes
Keep vl-class-ps by name.
Vl-delete-vardecls
Delete vl-vardecls by name.
Vl-delete-typedefs
Delete vl-typedefs by name.
Vl-delete-programs
Delete vl-programs by name.
Vl-delete-packages
Delete vl-packages by name.
Vl-delete-modules
Delete vl-modules by name.
Vl-delete-fundecls
Delete vl-fundecls by name.
Vl-delete-configs
Delete vl-configs by name.
Vl-delete-classes
Delete vl-classs by name.
Vl-keep-udps
Keep vl-udp-ps by name.
Vl-delete-udps
Delete vl-udps by name.
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.
Vl-filter-modinsts-by-modname
Partition a list of vl-modinsts by modname.
Vl-filter-modinsts-by-instname
Partition a list of vl-modinsts by instname.
Vl-filter-imports-by-package
Partition a list of vl-imports by package.
Vl-filter-descriptions
Partition a list of vl-descriptions by name.
Vl-filter-vardecls
Partition a list of vl-vardecls by name.
Vl-filter-typedefs
Partition a list of vl-typedefs by name.
Vl-filter-taskdecls
Partition a list of vl-taskdecls by name.
Vl-filter-programs
Partition a list of vl-programs by name.
Vl-filter-portdecls
Partition a list of vl-portdecls by name.
Vl-filter-paramdecls
Partition a list of vl-paramdecls by name.
Vl-filter-packages
Partition a list of vl-packages by name.
Vl-filter-modules
Partition a list of vl-modules by name.
Vl-filter-interfaces
Partition a list of vl-interfaces by name.
Vl-filter-fundecls
Partition a list of vl-fundecls by name.
Vl-filter-configs
Partition a list of vl-configs by name.
Vl-filter-classes
Partition a list of vl-classs by name.
Vl-filter-udps
Partition a list of vl-udps by name.