• 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
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
          • Vl-expr-widthsfixed-p
          • Vl-make-idexpr-list
          • Vl-exprlist-resolved->vals
          • Vl-idexprlist->names
          • Vl-expr-names
          • Vl-expr-count
          • Vl-idexpr
          • Vl-exprlist-to-plainarglist
          • Vl-expr-atoms
          • Vl-expr-ops
          • Vl-expr-count-noatts
          • Vl-make-index
          • Vl-expr-selects
          • Vl-bitlist-from-nat
          • Vl-pps-expr
          • Vl-expr-add-atts
          • Vl-idexprlist-p
          • Vl-expr-resolved-p
          • Vl-pps-origexpr
          • Vl-expr-funnames
          • Vl-idexpr->name
          • Vl-idexpr-p
          • Vl-exprlist-funnames
          • Vl-resolved->val
          • Vl-exprlist-resolved-p
          • Vl-expr->atts
          • Vl-obviously-true-expr-p
          • Vl-obviously-false-expr-p
          • Vl-exprlist-has-funcalls
          • Vl-expr-has-funcalls
          • Vl-zbitlist-p
          • Vl-zatom-p
          • Vl-exprlist-has-ops
          • Vl-expr-has-ops
          • Vl-expr-varnames
          • Vl-one-bit-constants
        • 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

• Mlib

Expr-tools

Basic functions for working with expressions.

Subtopics

Vl-expr-widthsfixed-p

Determines if all of the finalwidth fields throughout an expression are natural numbers.

Vl-make-idexpr-list

(vl-make-idexpr-list x finalwidth finaltype) maps vl-idexpr across a list.

Vl-exprlist-resolved->vals

(vl-exprlist-resolved->vals x) maps vl-resolved->val across a list.

Vl-idexprlist->names

(vl-idexprlist->names x) maps vl-idexpr->name across a list.

Vl-expr-names

Gather the names of all vl-id-p atoms throughout an expression.

Vl-expr-count

A measure for recurring over expressions.

Vl-idexpr

Construct an vl-idexpr-p.

Vl-exprlist-to-plainarglist

Convert expressions into vl-plainarg-ps.

Vl-expr-atoms

Gather all of the atoms throughout an expression.

Vl-expr-ops

Gather all of the operators used throughout an expression.

Vl-expr-count-noatts

A measure for recurring over expressions but ignoring attributes.

Vl-make-index

Safely create a constant integer atom whose value is n.

Vl-expr-selects

Collects up all the selection expressions (bit-selects, part-selects, array indexing, and unresolved indexing) and returns them as a flat list of expressions.

Vl-bitlist-from-nat

Turn a natural number into a vl-bitlist-p of the given width.

Vl-pps-expr

Pretty-print an expression into a string.

Vl-expr-add-atts

Vl-idexprlist-p

(vl-idexprlist-p x) recognizes lists where every element satisfies vl-idexpr-p.

Vl-expr-resolved-p

Recognizes plain constant integer expressions.

Vl-pps-origexpr

Pretty-print the "original," un-transformed version of an expression into a string.

Vl-expr-funnames

Collect the names of all functions that occur in a vl-expr-p and return them as a string list.

Vl-idexpr->name

Get the name from a vl-idexpr-p.

Vl-idexpr-p

Recognize plain identifier expressions.

Vl-exprlist-funnames

Collect the names of all functions that occur in a vl-exprlist-p and return them as a string list.

Vl-resolved->val

Get the value from a resolved expression.

Vl-exprlist-resolved-p

(vl-exprlist-resolved-p x) recognizes lists where every element satisfies vl-expr-resolved-p.

Vl-expr->atts

Vl-obviously-true-expr-p

Vl-obviously-false-expr-p

Vl-exprlist-has-funcalls

Vl-expr-has-funcalls

Vl-zbitlist-p

Vl-zatom-p

Vl-exprlist-has-ops

Vl-expr-has-ops

Vl-expr-varnames

Extract all the variable names from a VL expression.

Vl-one-bit-constants

Already-sized, one-bit constants.