		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

4vmask-to-a4vec-varcount

Signature
(4vmask-to-a4vec-varcount mask boolmask) → count
Arguments: mask — Guard (4vmask-p mask).; boolmask — Guard (integerp boolmask).
Returns: count — Type (natp count).

Definitions and Theorems

Function: 4vmask-to-a4vec-varcount

(defun 4vmask-to-a4vec-varcount (mask boolmask)
 (declare (xargs :guard (and (4vmask-p mask)
                             (integerp boolmask))))
 (declare (xargs :guard (not (sparseint-< mask 0))))
 (let ((__function__ '4vmask-to-a4vec-varcount))
  (declare (ignorable __function__))
  (b* ((mask (sparseint-nfix (4vmask-fix mask))))
    (- (* 2 (sparseint-bitcount mask))
       (sparseint-bitcount
            (sparseint-bitand mask (int-to-sparseint boolmask)))))))

Theorem: natp-of-4vmask-to-a4vec-varcount

(defthm natp-of-4vmask-to-a4vec-varcount
  (b* ((count (4vmask-to-a4vec-varcount mask boolmask)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: 4vmask-to-a4vec-varcount-of-4vmask-fix-mask

(defthm 4vmask-to-a4vec-varcount-of-4vmask-fix-mask
  (equal (4vmask-to-a4vec-varcount (4vmask-fix mask)
                                   boolmask)
         (4vmask-to-a4vec-varcount mask boolmask)))

Theorem: 4vmask-to-a4vec-varcount-4vmask-equiv-congruence-on-mask

(defthm 4vmask-to-a4vec-varcount-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (4vmask-to-a4vec-varcount mask boolmask)
                  (4vmask-to-a4vec-varcount mask-equiv boolmask)))
  :rule-classes :congruence)

Theorem: 4vmask-to-a4vec-varcount-of-ifix-boolmask

(defthm 4vmask-to-a4vec-varcount-of-ifix-boolmask
  (equal (4vmask-to-a4vec-varcount mask (ifix boolmask))
         (4vmask-to-a4vec-varcount mask boolmask)))

Theorem: 4vmask-to-a4vec-varcount-int-equiv-congruence-on-boolmask

(defthm 4vmask-to-a4vec-varcount-int-equiv-congruence-on-boolmask
  (implies (int-equiv boolmask boolmask-equiv)
           (equal (4vmask-to-a4vec-varcount mask boolmask)
                  (4vmask-to-a4vec-varcount mask boolmask-equiv)))
  :rule-classes :congruence)