		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-i2v-aux

Signature
(sv::aig-i2v-aux x idx length) → bitlist
Arguments: x — Guard (integerp x).; idx — Guard (natp idx).; length — Guard (eql length (integer-length x)).

Definitions and Theorems

Function: aig-i2v-aux

(defun sv::aig-i2v-aux (x idx length)
  (declare (xargs :guard (and (integerp x)
                              (natp idx)
                              (eql length (integer-length x)))))
  (declare (xargs :guard (<= idx (integer-length x))))
  (let ((__function__ 'sv::aig-i2v-aux))
    (declare (ignorable __function__))
    (b* ((x (lifix x))
         (idx (lnfix idx))
         (length (mbe :logic (integer-length x)
                      :exec length))
         ((when (mbe :logic (>= idx length)
                     :exec (eql idx length)))
          (sv::aig-sterm (logbitp idx x))))
      (sv::aig-scons (logbitp idx x)
                     (sv::aig-i2v-aux x (1+ idx) length)))))

Theorem: aig-list->s-of-bfr-snorm

(defthm aig-list->s-of-bfr-snorm
  (equal (sv::aig-list->s (bfr-snorm x) env)
         (sv::aig-list->s x env)))

Theorem: aig-i2v-aux-correct

(defthm aig-i2v-aux-correct
  (b* ((?bitlist (sv::aig-i2v-aux x idx length)))
    (equal (sv::aig-list->s bitlist env)
           (logtail idx x))))