		Search-engine friendly clone of the ACL2 documentation.

Sbitsets

Sbitset-members

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

In the logic, we just call sbitset-pair-members on each block to get the members.

However, this function should typically be left disabled and you should not reason about the underlying representation of sparse bitsets.

For faster execution, when the block size is 32 or 60 we use a partially unrolled inner loop for extracting the bits from each block. This optimization is not performed for other block sizes.

Definitions and Theorems

Function: sbitset-members-exec

(defun sbitset-members-exec (x acc)
  (declare (xargs :guard (sbitsetp x)))
  (if (atom x)
      acc
    (let* ((pair1 (car x))
           (offset1 (sbitset-pair-offset pair1))
           (block1 (sbitset-pair-block pair1)))
      (60bits-0-59 (* offset1 60)
                   block1
                   (sbitset-members-exec (cdr x) acc)))))

Function: sbitset-members-aux$inline

(defun sbitset-members-aux$inline (x)
  (declare (xargs :guard (sbitsetp x)))
  (mbe :logic
       (if (not (sbitsetp x))
           nil
         (if (atom x)
             nil
           (append (sbitset-pair-members (car x))
                   (sbitset-members-aux (cdr x)))))
       :exec (sbitset-members-exec x nil)))

Theorem: sbitset-members-exec-removal

(defthm sbitset-members-exec-removal
  (implies (force (sbitsetp x))
           (equal (sbitset-members-exec x acc)
                  (append (sbitset-members-aux x) acc))))

Function: sbitset-members$inline

(defun acl2::sbitset-members$inline (x)
  (declare (xargs :guard (sbitsetp x)))
  (let ((__function__ 'sbitset-members))
    (declare (ignorable __function__))
    (mbe :logic
         (if (or (not (sbitsetp x)) (atom x))
             nil
           (union (sbitset-pair-members (car x))
                  (sbitset-members (cdr x))))
         :exec (sbitset-members-exec x nil))))

Theorem: sbitset-members-aux-removal

(defthm sbitset-members-aux-removal
  (equal (sbitset-members-aux x)
         (sbitset-members x)))

Theorem: sbitset-members-default

(defthm sbitset-members-default
  (implies (not (sbitsetp a))
           (equal (sbitset-members a) nil)))

Theorem: sbitset-members-when-atom

(defthm sbitset-members-when-atom
  (implies (atom x)
           (equal (sbitset-members x) nil)))

Theorem: sbitset-members-of-cons

(defthm sbitset-members-of-cons
  (implies (force (sbitsetp (cons a x)))
           (equal (sbitset-members (cons a x))
                  (union (sbitset-pair-members a)
                         (sbitset-members x)))))

Theorem: sbitset-members-of-sbitset-fix

(defthm sbitset-members-of-sbitset-fix
  (equal (sbitset-members (sbitset-fix b))
         (sbitset-members b)))

Theorem: true-listp-of-sbitset-members

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

Theorem: setp-of-sbitset-members

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

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

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

Subtopics

Sbitset-pair-members: (sbitset-pair-members x) extracts the members of a single sbitset-pairp.
In-of-sbitset-members: Low-level lemma to rewrite (in a (sbitset-members x)) into a more structural form.