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

• Bitsets

Bitset-intersectp

(bitset-intersectp x y) efficiently determines if X and Y have any common members.

Signature

(bitset-intersectp x y) → intersectp

Arguments

x — Guard (natp x).

y — Guard (natp y).

Returns

intersectp — Type (booleanp intersectp).

This is efficient because, unlike bitset-intersect, we don't actually construct the intersection.

Definitions and Theorems

Function: bitset-intersectp$inline

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

Theorem: booleanp-of-bitset-intersectp

(defthm acl2::booleanp-of-bitset-intersectp
        (b* ((intersectp (acl2::bitset-intersectp$inline x y)))
            (booleanp intersectp))
        :rule-classes :type-prescription)

Theorem: bitset-intersectp-when-not-natp-left

(defthm bitset-intersectp-when-not-natp-left
        (implies (not (natp x))
                 (equal (bitset-intersectp x y) nil)))

Theorem: bitset-intersectp-when-not-natp-right

(defthm bitset-intersectp-when-not-natp-right
        (implies (not (natp y))
                 (equal (bitset-intersectp x y) nil)))

Theorem: bitset-intersectp-of-nfix-left

(defthm bitset-intersectp-of-nfix-left
        (equal (bitset-intersectp (nfix x) y)
               (bitset-intersectp x y)))

Theorem: bitset-intersectp-of-nfix-right

(defthm bitset-intersectp-of-nfix-right
        (equal (bitset-intersectp x (nfix y))
               (bitset-intersectp x y)))

Theorem: bitset-intersectp-removal

(defthm bitset-intersectp-removal
        (implies (bitset-intersectp x y)
                 (intersect (bitset-members x)
                            (bitset-members y))))