		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-bitcount-rec

Signature
(sparseint$-bitcount-rec offset negbit x) → count
Arguments: offset — Guard (natp offset).; x — Guard (sparseint$-p x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: sparseint$-bitcount-rec

(defun sparseint$-bitcount-rec (offset negbit x)
 (declare (xargs :guard (and (natp offset) (sparseint$-p x))))
 (declare
      (xargs :guard (equal negbit
                           (bool->bit (< (sparseint$-val x) 0)))))
 (let ((__function__ 'sparseint$-bitcount-rec))
  (declare (ignorable __function__))
  (sparseint$-case
    x
    :leaf (logcount (logtail offset x.val))
    :concat
    (b*
     ((offset (lnfix offset))
      (negbit
           (mbe :logic (bool->bit (eql (sparseint$-compare x 0) -1))
                :exec negbit))
      ((when (<= x.width offset))
       (sparseint$-bitcount-rec (- offset x.width)
                                negbit x.msbs))
      (width1 (- x.width offset)))
     (+ (sparseint$-bitcount-width width1 offset negbit x.lsbs)
        (sparseint$-bitcount-rec 0 negbit x.msbs))))))

Theorem: natp-of-sparseint$-bitcount-rec

(defthm natp-of-sparseint$-bitcount-rec
  (b* ((count (sparseint$-bitcount-rec offset negbit x)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: sparseint$-bitcount-rec-correct

(defthm sparseint$-bitcount-rec-correct
  (b*
   ((common-lisp::?count (sparseint$-bitcount-rec offset negbit x)))
   (equal count
          (logcount (logtail offset (sparseint$-val x))))))

Theorem: sparseint$-bitcount-rec-of-nfix-offset

(defthm sparseint$-bitcount-rec-of-nfix-offset
  (equal (sparseint$-bitcount-rec (nfix offset)
                                  negbit x)
         (sparseint$-bitcount-rec offset negbit x)))

Theorem: sparseint$-bitcount-rec-nat-equiv-congruence-on-offset

(defthm sparseint$-bitcount-rec-nat-equiv-congruence-on-offset
  (implies (nat-equiv offset offset-equiv)
           (equal (sparseint$-bitcount-rec offset negbit x)
                  (sparseint$-bitcount-rec offset-equiv negbit x)))
  :rule-classes :congruence)

Theorem: sparseint$-bitcount-rec-of-sparseint$-fix-x

(defthm sparseint$-bitcount-rec-of-sparseint$-fix-x
  (equal (sparseint$-bitcount-rec offset negbit (sparseint$-fix x))
         (sparseint$-bitcount-rec offset negbit x)))

Theorem: sparseint$-bitcount-rec-sparseint$-equiv-congruence-on-x

(defthm sparseint$-bitcount-rec-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-bitcount-rec offset negbit x)
                  (sparseint$-bitcount-rec offset negbit x-equiv)))
  :rule-classes :congruence)