• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Vl-loadstate
        • Lexer
        • Parser
        • Vl-load-merge-descriptions
        • Vl-find-basename/extension
        • Vl-load-file
        • Vl-loadresult
        • Scope-of-defines
        • Vl-find-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-read-file
        • Vl-includeskips-report-gather
        • Vl-load-main
        • Extended-characters
          • Vl-location
          • Vl-echar-p
          • Vl-echarlist->chars
          • Vl-echarlist-from-chars
          • Vl-echarlist-from-str
          • Vl-echarlist-unsigned-value
            • Vl-echarlist-unsigned-value-aux
          • Vl-change-echarlist-locations
          • Vl-echar-digit-value
          • Vl-echarlist->string
        • Vl-load
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-preprocess-debug
        • Vl-write-preprocessor-debug-file
        • Vl-read-file-report-gather
        • Vl-load-descriptions
        • Vl-load-files
        • Translate-off
        • Vl-load-read-file-hook
        • Vl-read-file-report
        • Vl-loadstate-pad
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-loadstate->warnings
        • Vl-iskips-report
        • Vl-descriptionlist
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Extended-characters

Vl-echarlist-unsigned-value

(vl-echarlist-unsigned-value x radix) interprets the extended character list x as a base-radix number, or returns nil if x is invalid.

Signature

(vl-echarlist-unsigned-value x radix) → *

Arguments

x — Guard (vl-echarlist-p x).

radix — Guard (natp radix).

We see if X is made up entirely of base RADIX digits. If so, we return the number represented by X, treating the digits as if they are written with the most significant digit first. For instance, an echarlist whose string is "987" has, in base 10, an unsigned-value of 987. Otherwise, if there are any invalid digits, we return NIL.

Definitions and Theorems

Function: vl-echarlist-unsigned-value

(defun vl-echarlist-unsigned-value (x radix)
  (declare (xargs :guard (and (vl-echarlist-p x) (natp radix))))
  (declare (xargs :guard (and (<= 2 radix) (<= radix 36))))
  (let ((__function__ 'vl-echarlist-unsigned-value))
    (declare (ignorable __function__))
    (if (not (consp x))
        nil
      (vl-echarlist-unsigned-value-aux x (lnfix radix)
                                       (len x)))))

Theorem: natp-of-vl-echarlist-unsigned-value-aux

(defthm natp-of-vl-echarlist-unsigned-value-aux
  (implies (vl-echarlist-unsigned-value x radix)
           (and (natp (vl-echarlist-unsigned-value x radix))
                (integerp (vl-echarlist-unsigned-value x radix))
                (<= 0
                    (vl-echarlist-unsigned-value x radix))))
  :rule-classes
  ((:rewrite)
   (:type-prescription
        :corollary
        (or (not (vl-echarlist-unsigned-value x radix))
            (and (integerp (vl-echarlist-unsigned-value x radix))
                 (<= 0
                     (vl-echarlist-unsigned-value x radix)))))))

Theorem: vl-echarlist-unsigned-value-when-not-consp

(defthm vl-echarlist-unsigned-value-when-not-consp
  (implies (not (consp x))
           (equal (vl-echarlist-unsigned-value x radix)
                  nil)))

Theorem: type-of-vl-echarlist-unsigned-value

(defthm type-of-vl-echarlist-unsigned-value
  (or (not (vl-echarlist-unsigned-value x radix))
      (natp (vl-echarlist-unsigned-value x radix)))
  :rule-classes :type-prescription)

Theorem: vl-echarlist-unsigned-value-of-vl-echarlist-fix-x

(defthm vl-echarlist-unsigned-value-of-vl-echarlist-fix-x
  (equal (vl-echarlist-unsigned-value (vl-echarlist-fix x)
                                      radix)
         (vl-echarlist-unsigned-value x radix)))

Theorem: vl-echarlist-unsigned-value-vl-echarlist-equiv-congruence-on-x

(defthm
     vl-echarlist-unsigned-value-vl-echarlist-equiv-congruence-on-x
  (implies (vl-echarlist-equiv x x-equiv)
           (equal (vl-echarlist-unsigned-value x radix)
                  (vl-echarlist-unsigned-value x-equiv radix)))
  :rule-classes :congruence)

Theorem: vl-echarlist-unsigned-value-of-nfix-radix

(defthm vl-echarlist-unsigned-value-of-nfix-radix
  (equal (vl-echarlist-unsigned-value x (nfix radix))
         (vl-echarlist-unsigned-value x radix)))

Theorem: vl-echarlist-unsigned-value-nat-equiv-congruence-on-radix

(defthm vl-echarlist-unsigned-value-nat-equiv-congruence-on-radix
  (implies (acl2::nat-equiv radix radix-equiv)
           (equal (vl-echarlist-unsigned-value x radix)
                  (vl-echarlist-unsigned-value x radix-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-echarlist-unsigned-value-aux