• 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
      • Sbitsets
        • Sbitset-members
        • Sbitset-pairp
          • Sbitset-pair-members
          • Sbitset-blockp
          • *sbitset-block-size*
          • Sbitset-pair
          • Sbitset-pair-offset
          • Sbitset-pair-block
        • 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

• Sbitsets

Sbitset-pairp

(sbitset-pairp x) recognizes a valid (offset . block) pair for sparse bitsets.

Signature

(sbitset-pairp x) → pairp

Returns

pairp — Type (booleanp pairp).

Definitions and Theorems

Function: sbitset-pairp$inline

(defun sbitset-pairp$inline (x)
  (declare (xargs :guard t))
  (let ((__function__ 'sbitset-pairp))
    (declare (ignorable __function__))
    (and (consp x)
         (natp (car x))
         (sbitset-blockp (cdr x)))))

Theorem: booleanp-of-sbitset-pairp

(defthm booleanp-of-sbitset-pairp
  (b* ((pairp (sbitset-pairp$inline x)))
    (booleanp pairp))
  :rule-classes :type-prescription)

Theorem: consp-when-sbitset-pairp

(defthm consp-when-sbitset-pairp
  (implies (sbitset-pairp x) (consp x))
  :rule-classes :compound-recognizer)

Theorem: sbitset-pair-offset-of-sbitset-pair

(defthm sbitset-pair-offset-of-sbitset-pair
  (equal (sbitset-pair-offset (sbitset-pair offset block))
         offset))

Theorem: sbitset-pair-block-of-sbitset-pair

(defthm sbitset-pair-block-of-sbitset-pair
  (equal (sbitset-pair-block (sbitset-pair offset block))
         block))

Theorem: sbitset-pair-offset-type

(defthm sbitset-pair-offset-type
  (implies (force (sbitset-pairp x))
           (natp (sbitset-pair-offset x)))
  :rule-classes :type-prescription)

Theorem: sbitset-pair-block-type

(defthm sbitset-pair-block-type
  (implies (force (sbitset-pairp x))
           (and (integerp (sbitset-pair-block x))
                (< 0 (sbitset-pair-block x))))
  :rule-classes :type-prescription)

Theorem: sbitset-pair-block-upper-bound

(defthm sbitset-pair-block-upper-bound
  (implies (force (sbitset-pairp x))
           (< (sbitset-pair-block x)
              (expt 2 *sbitset-block-size*)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: sbitset-pairp-of-sbitset-pair

(defthm sbitset-pairp-of-sbitset-pair
  (implies (and (force (natp offset))
                (force (sbitset-blockp block)))
           (sbitset-pairp (sbitset-pair offset block))))

Theorem: sbitset-blockp-of-sbitset-pair-block

(defthm sbitset-blockp-of-sbitset-pair-block
  (implies (force (sbitset-pairp x))
           (sbitset-blockp (sbitset-pair-block x))))

Subtopics

Sbitset-pair-members

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

Sbitset-blockp

(sbitset-blockp x) recognizes numbers that are valid as the block component of an sbitset-pairp.

*sbitset-block-size*

Size of each block in an sparse bitset.

Sbitset-pair

(sbitset-pair offset block) constructs a (offset . block) pair.

Sbitset-pair-offset

(sbitset-pair-offset x) gets the offset from an (offset . block) pair.

Sbitset-pair-block

(sbitset-pair-block x) gets the block from an (offset . block) pair.