		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-i2v

Like i2v but for AIGs only.

Signature
(sv::aig-i2v x) → aig
Arguments: x — Guard (integerp x).

Definitions and Theorems

Function: aig-i2v

(defun sv::aig-i2v (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'sv::aig-i2v))
    (declare (ignorable __function__))
    (sv::aig-i2v-aux x 0 (integer-length x))))

Theorem: aig-i2v-correct

(defthm aig-i2v-correct
  (equal (sv::aig-list->s (sv::aig-i2v x) env)
         (ifix x)))