• 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
      • Sbitsets
        • Sbitset-members
          • Sbitset-pair-members
          • In-of-sbitset-members
        • Sbitset-pairp
        • Sbitsetp
        • Sbitset-intersect
        • Sbitset-difference
        • Sbitset-union
        • Sbitset-singleton
        • Sbitset-fix
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Sbitset-members
• Sbitset-pairp

Sbitset-pair-members

(sbitset-pair-members x) extracts the members of a single sbitset-pairp.

Signature

(sbitset-pair-members x) → set

Arguments

x — Guard (sbitset-pairp x).

For instance, if the pair is (0 . 7), we produce the set {0, 1, 2}; if the set is (1 . 7), we produce {60, 61, 62}.

This serves as the logical definition we use to reason about member extraction.

Normally this function isn't executed. When the block size is 32 or 60, we can instead use the optimized bits-0-31 or 60bits-0-59 routines instead. But, if you change the block size to something else, this function will be executed and its performance will probably be bad. In this case, you might want to write a custom bits-0-32 style routine for your block size.

Definitions and Theorems

Function: sbitset-pair-members

(defun sbitset-pair-members (x)
  (declare (xargs :guard (sbitset-pairp x)))
  (let ((__function__ 'sbitset-pair-members))
    (declare (ignorable __function__))
    (add-to-each (* (sbitset-pair-offset x)
                    *sbitset-block-size*)
                 (bits-between 0 *sbitset-block-size*
                               (sbitset-pair-block x)))))

Theorem: sbitset-pair-members-of-nil

(defthm sbitset-pair-members-of-nil
  (equal (sbitset-pair-members nil) nil))

Theorem: true-listp-of-sbitset-pair-members

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

Theorem: integer-listp-of-sbitset-pair-members

(defthm integer-listp-of-sbitset-pair-members
  (implies (force (sbitset-pairp x))
           (integer-listp (sbitset-pair-members x))))

Theorem: member-equal-sbitset-pair-members

(defthm member-equal-sbitset-pair-members
  (implies (force (sbitset-pairp x))
           (iff (member-equal a (sbitset-pair-members x))
                (and (natp a)
                     (equal (floor a *sbitset-block-size*)
                            (sbitset-pair-offset x))
                     (logbitp (mod a *sbitset-block-size*)
                              (sbitset-pair-block x))))))

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

(defthm no-duplicatesp-equal-of-sbitset-pair-members
  (implies (force (sbitset-pairp x))
           (no-duplicatesp-equal (sbitset-pair-members x))))

Theorem: offsets-must-agree-when-sbitset-pair-members-intersect

(defthm offsets-must-agree-when-sbitset-pair-members-intersect
  (implies (and (force (sbitset-pairp x))
                (force (sbitset-pairp y))
                (intersectp-equal (sbitset-pair-members x)
                                  (sbitset-pair-members y))
                (syntaxp (term-order y x)))
           (equal (sbitset-pair-offset x)
                  (sbitset-pair-offset y))))

Theorem: consp-of-sbitset-pair-members

(defthm consp-of-sbitset-pair-members
  (implies (force (sbitset-pairp x))
           (and (true-listp (sbitset-pair-members x))
                (consp (sbitset-pair-members x))))
  :rule-classes :type-prescription)

Theorem: setp-of-sbitset-pair-members

(defthm setp-of-sbitset-pair-members
  (implies (force (sbitset-pairp a))
           (setp (sbitset-pair-members a))))

Theorem: in-of-sbitset-pair-members

(defthm in-of-sbitset-pair-members
  (implies (force (sbitset-pairp x))
           (equal (in a (sbitset-pair-members x))
                  (and (natp a)
                       (equal (floor a *sbitset-block-size*)
                              (sbitset-pair-offset x))
                       (logbitp (mod a *sbitset-block-size*)
                                (sbitset-pair-block x))))))

Theorem: emptyp-of-sbitset-pair-members

(defthm emptyp-of-sbitset-pair-members
  (implies (force (sbitset-pairp x))
           (not (emptyp (sbitset-pair-members x)))))