		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-binary-bittest-int

Signature
(sparseint$-binary-bittest-int op offset x y) → test
Arguments: op — Guard (integerp op).; offset — Guard (natp offset).; x — Guard (sparseint$-p x).; y — Guard (integerp y).
Returns: test — Type (booleanp test).

Definitions and Theorems

Function: sparseint$-binary-bittest-int

(defun sparseint$-binary-bittest-int (op offset x y)
 (declare (type (unsigned-byte 4) op))
 (declare (xargs :guard (and (integerp op)
                             (natp offset)
                             (sparseint$-p x)
                             (integerp y))))
 (let ((__function__ 'sparseint$-binary-bittest-int))
   (declare (ignorable __function__))
   (b* ((y (lifix y))
        (offset (lnfix offset))
        ((when (or (eql y 0) (eql y -1)))
         (b* ((cofactor (binary-bitop-cofactor2 op (- y))))
           (sparseint$-unary-bittest-offset cofactor offset x))))
     (sparseint$-case
          x :leaf
          (binary-bittest op (logtail offset x.val)
                          y)
          :concat
          (b* (((when (<= x.width offset))
                (sparseint$-binary-bittest-int op (- offset x.width)
                                               x.msbs y))
               (width1 (- x.width offset)))
            (or (sparseint$-binary-bittest-int-width
                     op width1
                     offset x.lsbs (bignum-logext width1 y))
                (sparseint$-binary-bittest-int
                     op 0 x.msbs (logtail width1 y))))))))

Theorem: booleanp-of-sparseint$-binary-bittest-int

(defthm booleanp-of-sparseint$-binary-bittest-int
  (b* ((test (sparseint$-binary-bittest-int op offset x y)))
    (booleanp test))
  :rule-classes :type-prescription)

Theorem: sparseint$-val-of-sparseint$-binary-bittest-int

(defthm sparseint$-val-of-sparseint$-binary-bittest-int
  (b* ((?test (sparseint$-binary-bittest-int op offset x y)))
    (equal test
           (binary-bittest op (logtail offset (sparseint$-val x))
                           y))))

Theorem: sparseint$-binary-bittest-int-of-ifix-op

(defthm sparseint$-binary-bittest-int-of-ifix-op
  (equal (sparseint$-binary-bittest-int (ifix op)
                                        offset x y)
         (sparseint$-binary-bittest-int op offset x y)))

Theorem: sparseint$-binary-bittest-int-int-equiv-congruence-on-op

(defthm sparseint$-binary-bittest-int-int-equiv-congruence-on-op
  (implies
       (int-equiv op op-equiv)
       (equal (sparseint$-binary-bittest-int op offset x y)
              (sparseint$-binary-bittest-int op-equiv offset x y)))
  :rule-classes :congruence)

Theorem: sparseint$-binary-bittest-int-of-nfix-offset

(defthm sparseint$-binary-bittest-int-of-nfix-offset
  (equal (sparseint$-binary-bittest-int op (nfix offset)
                                        x y)
         (sparseint$-binary-bittest-int op offset x y)))

Theorem: sparseint$-binary-bittest-int-nat-equiv-congruence-on-offset

(defthm sparseint$-binary-bittest-int-nat-equiv-congruence-on-offset
  (implies
       (nat-equiv offset offset-equiv)
       (equal (sparseint$-binary-bittest-int op offset x y)
              (sparseint$-binary-bittest-int op offset-equiv x y)))
  :rule-classes :congruence)

Theorem: sparseint$-binary-bittest-int-of-sparseint$-fix-x

(defthm sparseint$-binary-bittest-int-of-sparseint$-fix-x
  (equal (sparseint$-binary-bittest-int op offset (sparseint$-fix x)
                                        y)
         (sparseint$-binary-bittest-int op offset x y)))

Theorem: sparseint$-binary-bittest-int-sparseint$-equiv-congruence-on-x

(defthm
     sparseint$-binary-bittest-int-sparseint$-equiv-congruence-on-x
  (implies
       (sparseint$-equiv x x-equiv)
       (equal (sparseint$-binary-bittest-int op offset x y)
              (sparseint$-binary-bittest-int op offset x-equiv y)))
  :rule-classes :congruence)

Theorem: sparseint$-binary-bittest-int-of-ifix-y

(defthm sparseint$-binary-bittest-int-of-ifix-y
  (equal (sparseint$-binary-bittest-int op offset x (ifix y))
         (sparseint$-binary-bittest-int op offset x y)))

Theorem: sparseint$-binary-bittest-int-int-equiv-congruence-on-y

(defthm sparseint$-binary-bittest-int-int-equiv-congruence-on-y
  (implies
       (int-equiv y y-equiv)
       (equal (sparseint$-binary-bittest-int op offset x y)
              (sparseint$-binary-bittest-int op offset x y-equiv)))
  :rule-classes :congruence)