		Search-engine friendly clone of the ACL2 documentation.

Hex-digit-string-p

Recognizer for strings whose characters are hexadecimal digits.

Signature
(hex-digit-string-p x) → bool

Corner case: this accepts the empty string since all of its characters are hex digits.

Logically this is defined in terms of hex-digit-char-list*p. But in the execution, we use a char-based function that avoids exploding the string. This provides much better performance, e.g., on an AMD FX-8350 with CCL:

;; 0.97 seconds, no garbage
(let ((x "deadbeef"))
  (time$ (loop for i fixnum from 1 to 10000000 do
               (str::hex-digit-string-p x))))

;; 1.74 seconds, 1.28 GB allocated
(let ((x "deadbeef"))
  (time$ (loop for i fixnum from 1 to 10000000 do
               (str::hex-digit-char-list*p (explode x)))))

Definitions and Theorems

Function: hex-digit-string-p$inline

(defun hex-digit-string-p$inline (x)
  (declare (type string x))
  (let ((acl2::__function__ 'hex-digit-string-p))
    (declare (ignorable acl2::__function__))
    (mbe :logic (hex-digit-char-list*p (explode x))
         :exec (hex-digit-string-p-aux x 0 (length x)))))

Theorem: istreqv-implies-equal-hex-digit-string-p-1

(defthm istreqv-implies-equal-hex-digit-string-p-1
  (implies (istreqv x x-equiv)
           (equal (hex-digit-string-p x)
                  (hex-digit-string-p x-equiv)))
  :rule-classes (:congruence))

Subtopics

Hex-digit-string-p-aux