• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
          • Vl-namefactory-p
            • Vl-namefactory-plain-names
            • Vl-namefactory-indexed-name
            • Vl-namefactory-plain-name
            • Vl-namefactory-maybe-initialize
            • Vl-namefactory-namedb-fix
            • Vl-namefactory-allnames
            • Vl-starting-namefactory
            • Vl-namefactory-namedb-okp
            • Vl-empty-namefactory
            • Vl-free-namefactory
          • Vl-namefactory-fix
          • Vl-namefactory-equiv
          • Make-vl-namefactory
          • Vl-namefactory->namedb
          • Vl-namefactory->mod
          • Change-vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-namefactory-p

Vl-namefactory-allnames

(vl-namefactory-p x) returns a list of all names that are considered to be used by the name factory.

Signature

(vl-namefactory-allnames factory) → names

Arguments

factory — Guard (vl-namefactory-p factory).

Returns

names — Type (string-listp names).

This function is not particularly efficient, and probably should not ordinarily be executed in real programs. Its main purpose is to establish the freshness guarantee for name factories, described in vl-namefactory-p.

Definitions and Theorems

Function: vl-namefactory-allnames

(defun vl-namefactory-allnames (factory)
  (declare (xargs :guard (vl-namefactory-p factory)))
  (let ((__function__ 'vl-namefactory-allnames))
    (declare (ignorable __function__))
    (mbe :logic
         (vl-namedb-allnames
              (vl-namefactory->namedb
                   (vl-namefactory-maybe-initialize factory)))
         :exec
         (let ((mod (vl-namefactory->mod factory))
               (namedb (vl-namefactory->namedb factory)))
           (cond ((vl-namedb->names namedb)
                  (vl-namedb-allnames namedb))
                 (mod (vl-module->modnamespace mod))
                 (t nil))))))

Theorem: string-listp-of-vl-namefactory-allnames

(defthm string-listp-of-vl-namefactory-allnames
  (b* ((names (vl-namefactory-allnames factory)))
    (string-listp names))
  :rule-classes :rewrite)

Theorem: vl-namefactory-allnames-of-vl-namefactory-maybe-initialize

(defthm vl-namefactory-allnames-of-vl-namefactory-maybe-initialize
  (equal (vl-namefactory-allnames
              (vl-namefactory-maybe-initialize factory))
         (vl-namefactory-allnames factory)))

Theorem: vl-namefactory-allnames-of-vl-namefactory-fix-factory

(defthm vl-namefactory-allnames-of-vl-namefactory-fix-factory
  (equal (vl-namefactory-allnames (vl-namefactory-fix factory))
         (vl-namefactory-allnames factory)))

Theorem: vl-namefactory-allnames-vl-namefactory-equiv-congruence-on-factory

(defthm
 vl-namefactory-allnames-vl-namefactory-equiv-congruence-on-factory
 (implies (vl-namefactory-equiv factory factory-equiv)
          (equal (vl-namefactory-allnames factory)
                 (vl-namefactory-allnames factory-equiv)))
 :rule-classes :congruence)