		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-string->bits

Signature
(vl-string->bits x n) → val
Arguments: x — Guard (stringp x).; n — Guard (natp n).
Returns: val — Type (natp val).

Definitions and Theorems

Function: vl-string->bits

(defun vl-string->bits (x n)
  (declare (xargs :guard (and (stringp x) (natp n))))
  (declare (xargs :guard (<= (nfix n) (length x))))
  (let ((__function__ 'vl-string->bits))
    (declare (ignorable __function__))
    (b* (((when (zp n)) 0)
         (charval (char-code (char x (1- n))))
         (rest (vl-string->bits x (1- n))))
      (logior (ash rest 8) charval))))

Theorem: natp-of-vl-string->bits

(defthm natp-of-vl-string->bits
  (b* ((val (vl-string->bits x n)))
    (natp val))
  :rule-classes :rewrite)

Theorem: vl-string->bits-of-str-fix-x

(defthm vl-string->bits-of-str-fix-x
  (equal (vl-string->bits (str-fix x) n)
         (vl-string->bits x n)))

Theorem: vl-string->bits-streqv-congruence-on-x

(defthm vl-string->bits-streqv-congruence-on-x
  (implies (streqv x x-equiv)
           (equal (vl-string->bits x n)
                  (vl-string->bits x-equiv n)))
  :rule-classes :congruence)

Theorem: vl-string->bits-of-nfix-n

(defthm vl-string->bits-of-nfix-n
  (equal (vl-string->bits x (nfix n))
         (vl-string->bits x n)))

Theorem: vl-string->bits-nat-equiv-congruence-on-n

(defthm vl-string->bits-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (vl-string->bits x n)
                  (vl-string->bits x n-equiv)))
  :rule-classes :congruence)