		Search-engine friendly clone of the ACL2 documentation.

Limited-shifts

Logcollapse

OR together all the bits of x at position or above, collapsing them into the single bit at position.

Signature
(logcollapse position x) → *
Arguments: position — Guard (natp position).; x — Guard (natp x).

This operation helps avoid catastrophically large shifts in computing, e.g., concatenations with symbolic widths. When there is a care-mask of width w, then we can collapse all the bits at w and above into the bit at w, because the presence of those upper bits means that the shift is longer than we care about.

There is a large potential for off-by-one errors when thinking about this function. It may help to start with the fact that (logcollapse 0 x) collapses all bits of x into a single bit. In general, (logcollapse n x) results in at most n+1 bits.

Definitions and Theorems

Function: logcollapse

(defun logcollapse (position x)
  (declare (xargs :guard (and (natp position) (natp x))))
  (let ((__function__ 'logcollapse))
    (declare (ignorable __function__))
    (b* ((position (lnfix position)))
      (logior (loghead position x)
              (ash (b-not (bool->bit (eql 0 (logtail position x))))
                   position)))))

Subtopics

Aig-logcollapse-ns