• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
          • Substitution
          • Allexprs
          • Hid-tools
            • Following-hids
            • Vl-hidexpr-traverse-datatype
            • Abstract-hids
              • Vl-hidexpr-p
              • Vl-hidindex-p
              • Vl-hidexpr-collect-indices
              • Vl-hidindex->indices
              • Vl-hidexpr->rest
              • Vl-indexexpr->indices
                • Vl-indexexpr->indices-exec
              • Vl-hidexpr->first
              • Vl-indexexpr->scopeexpr
              • Vl-scopeexpr->scopes
              • Vl-hidname-p
              • Vl-hidexpr->endp
              • Vl-scopeexpr->hid
              • Vl-hidname->name
              • Vl-hidindex->name
              • Vl-hidindex-count-indices
              • Vl-scopeexpr-p
              • Vl-scopeatom->name
              • Vl-scopename-p
              • Vl-scopename-fix
              • Vl-indexexpr-p
              • Vl-fast-keyguts-p
              • Vl-scopeatom-p
              • Vl-scopenamelist
            • Vl-hidexpr-find-type
          • 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
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Abstract-hids

Vl-indexexpr->indices

Signature
(vl-indexexpr->indices x) → indices
Arguments
x — Guard (vl-expr-p x).
Returns
indices — Type (vl-exprlist-p indices).

Definitions and Theorems

Function: vl-indexexpr->indices$inline

(defun vl-indexexpr->indices$inline (x)
  (declare (xargs :guard (vl-expr-p x)))
  (declare (xargs :guard (vl-indexexpr-p x)))
  (let ((__function__ 'vl-indexexpr->indices))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((when (vl-atom-p x)) nil)
              ((vl-nonatom x))
              ((when (or (vl-op-equiv x.op :vl-index)
                         (vl-op-equiv x.op :vl-bitselect)))
               (append (vl-indexexpr->indices (first x.args))
                       (list (second x.args)))))
           nil)
         :exec (vl-indexexpr->indices-exec x nil))))

Theorem: vl-exprlist-p-of-vl-indexexpr->indices

(defthm vl-exprlist-p-of-vl-indexexpr->indices
  (b* ((indices (vl-indexexpr->indices$inline x)))
    (vl-exprlist-p indices))
  :rule-classes :rewrite)

Theorem: vl-indexexpr->indices-exec-removal

(defthm vl-indexexpr->indices-exec-removal
  (equal (vl-indexexpr->indices-exec x acc)
         (append (vl-indexexpr->indices x)
                 (vl-exprlist-fix acc))))

Theorem: vl-indexexpr->indices$inline-of-vl-expr-fix-x

(defthm vl-indexexpr->indices$inline-of-vl-expr-fix-x
  (equal (vl-indexexpr->indices$inline (vl-expr-fix x))
         (vl-indexexpr->indices$inline x)))

Theorem: vl-indexexpr->indices$inline-vl-expr-equiv-congruence-on-x

(defthm vl-indexexpr->indices$inline-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-indexexpr->indices$inline x)
                  (vl-indexexpr->indices$inline x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-indexexpr->indices-exec