		Search-engine friendly clone of the ACL2 documentation.

Aig-random-sim

Logbitp-env60

Given an ALST binding variables to 60-bit integers as in aig-vecsim60, we extract an ordinary, Boolean-valued alist by using the Ith bit of each variable.

Signature
(logbitp-env60 i alst) → *

Definitions and Theorems

Function: logbitp-env60

(defun logbitp-env60 (i alst)
  (declare (xargs :guard t))
  (let ((__function__ 'logbitp-env60))
    (declare (ignorable __function__))
    (cond ((atom alst) nil)
          ((atom (car alst))
           (logbitp-env60 i (cdr alst)))
          (t (cons (cons (caar alst)
                         (if (natp i)
                             (if (< i 60)
                                 (logbitp i (cdar alst))
                               nil)
                           (logbitp 0 (cdar alst))))
                   (logbitp-env60 i (cdr alst)))))))