		Search-engine friendly clone of the ACL2 documentation.

Aig-random-sim

Aig-vecsim60

Do a 60-bit wide evaluation of an AIG.

Signature
(aig-vecsim60 aig alst) → *
Arguments: aig — The AIG to simulate.; alst — An alist that should bind the variables of aig to 60-bit naturals. If there are any missing or invalid bindings, we just 60-bit-fix them.

Definitions and Theorems

Function: aig-vecsim60

(defun aig-vecsim60 (aig alst)
 (declare (xargs :guard t))
 (let ((__function__ 'aig-vecsim60))
  (declare (ignorable __function__))
  (aig-cases
   aig :true -1 :false 0 :var
   (let ((look (hons-get aig alst)))
     (if look (60-bit-fix (cdr look)) -1))
   :inv
   (the (signed-byte 61)
        (lognot (the (signed-byte 61)
                     (aig-vecsim60 (car aig) alst))))
   :and
   (let ((a (aig-vecsim60 (car aig) alst)))
     (mbe :logic
          (logand a (aig-vecsim60 (cdr aig) alst))
          :exec
          (if (= (the (signed-byte 61) a) 0)
              0
            (the (signed-byte 61)
                 (logand (the (signed-byte 61) a)
                         (the (signed-byte 61)
                              (aig-vecsim60 (cdr aig) alst))))))))))

Theorem: aig-vecsim60-60-bits

(defthm aig-vecsim60-60-bits
  (signed-byte-p 61 (aig-vecsim60 aig alst)))

Function: aig-vecsim60-memoize-condition

(defun aig-vecsim60-memoize-condition (aig alst)
  (declare (ignorable aig alst)
           (xargs :guard 't))
  (and (consp aig) (cdr aig)))