• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
      • Bitsets
        • Bitset-members
        • Bitset-insert
        • Bitset-delete
        • Bitset-intersectp
        • Bitset-intersect
        • Bitset-difference
        • Bitset-subsetp
        • Bitset-union
        • Bitset-memberp
        • Bitset-singleton
        • Bitset-list
        • Bitset-cardinality
        • Bitset-list*
        • Utilities
      • Sbitsets
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bitsets

Bitset-cardinality

(bitset-cardinality x) determines the cardinality of the set X.

Signature

(bitset-cardinality x) → *

Arguments

x — Guard (natp x).

We prefer to reason about (set::cardinality (bitset-members X)). We could have used this as the :logic definition, but the logcount-based definition should be better for symbolic simulation with ACL2::gl.

Definitions and Theorems

Function: bitset-cardinality$inline

(defun acl2::bitset-cardinality$inline (x)
  (declare (type unsigned-byte x))
  (declare (xargs :guard (natp x)))
  (declare (xargs :split-types t))
  (let ((__function__ 'bitset-cardinality))
    (declare (ignorable __function__))
    (the unsigned-byte
         (logcount (the unsigned-byte (lnfix x))))))

Theorem: bitset-cardinality-removal

(defthm bitset-cardinality-removal
  (equal (bitset-cardinality x)
         (cardinality (bitset-members x))))