• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
      • Bitsets
        • Bitset-members
          • Ttag-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-members

(bitset-members x) converts a bitset into an ordinary, ordered set.

Signature

(bitset-members x) → *

Arguments

x — Guard (natp x).

Reasoning note: bitset-members is fundamental to reasoning about bitsets; see Reasoning with Bitsets in bitsets. Its definition and the theorem in-of-bitset-members should generally be left disabled since they expose the underlying representation of bitsets.

Performance note: bitset-members is inherently expensive: no matter how it is implemented, it must create at least |X| conses. You may sometimes be able to avoid this cost using functions like bitset-memberp, bitset-intersectp, or bitset-subsetp instead.

It is simple enough to convert a bitset into an ordered set: since the integer-length of x gives us an upper bound on its elements, we just need to walk up to this bound and collect all i such that (logbitp i x).

The definition below uses bits-between to do just this. However, note that when the bignum-extract-opt book is loaded (which requires a ttag), a more efficient implementation is used; see ttag-bitset-members and bignum-extract for details.

Definitions and Theorems

Function: bitset-members

(defun bitset-members (x)
  (declare (xargs :guard (natp x)))
  (let ((__function__ 'bitset-members))
    (declare (ignorable __function__))
    (mbe :logic
         (let ((x (nfix x)))
           (bits-between 0 (integer-length x) x))
         :exec (bits-between 0 (integer-length x) x))))

Theorem: bitset-members-default

(defthm bitset-members-default
  (implies (not (natp a))
           (equal (bitset-members a) nil)))

Theorem: bitset-members-of-nfix

(defthm bitset-members-of-nfix
  (equal (bitset-members (nfix b))
         (bitset-members b)))

Theorem: true-listp-of-bitset-members

(defthm true-listp-of-bitset-members
  (true-listp (bitset-members x))
  :rule-classes :type-prescription)

Theorem: nat-listp-of-bitset-members

(defthm nat-listp-of-bitset-members
  (nat-listp (bitset-members x)))

Theorem: no-duplicatesp-equal-of-bitset-members

(defthm no-duplicatesp-equal-of-bitset-members
  (no-duplicatesp-equal (bitset-members x)))

Theorem: setp-of-bitset-members

(defthm setp-of-bitset-members
  (setp (bitset-members x)))

Theorem: in-of-bitset-members

(defthm in-of-bitset-members
  (equal (in a (bitset-members x))
         (and (natp a) (logbitp a (nfix x)))))

Theorem: bitset-members-under-iff

(defthm bitset-members-under-iff
  (iff (bitset-members x) (posp x)))

Subtopics

Ttag-bitset-members

Notes about the optimization of bitset-members.