		Search-engine friendly clone of the ACL2 documentation.

Aig-random-sim

60-bit-fix

Coerce an object to a 60-bit natural.

Signature
(60-bit-fix x) → *

A previous definition for this function was:

(the (signed-byte 61)
  (if (integerp x)
      (logand x (the (signed-byte 61) *60-bit-mask*))
    0))

But the new definition is slightly faster because we avoid the lookup of the *60-bit-mask*.

We could make this almost twice as fast by redefining it under the hood as (if (typep x '(signed-byte 61)) x 0), but I had some trouble getting this to properly inline, and probably it's best to avoid a ttag for such a minor optimization.

Definitions and Theorems

Function: 60-bit-fix$inline

(defun 60-bit-fix$inline (x)
  (declare (xargs :guard t))
  (let ((__function__ '60-bit-fix))
    (declare (ignorable __function__))
    (if (integerp x)
        (the (signed-byte 61)
             (logand x (- (ash 1 60) 1)))
      0)))