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

• Sbitsets

Sbitset-intersect

(sbitset-intersect X Y ...) constructs the set X \intersect Y \intersect ....

Macro: sbitset-intersect

(defmacro sbitset-intersect (&rest args)
          (cond ((atom args) nil)
                ((atom (cdr args)) (car args))
                (t (xxxjoin 'sbitset-binary-intersect
                            args))))

Definitions and Theorems

Function: sbitset-intersect-exec

(defun
 sbitset-intersect-exec (x y)
 (declare (xargs :guard (and (sbitsetp x) (sbitsetp y))))
 (let
  ((__function__ 'sbitset-intersect-exec))
  (declare (ignorable __function__))
  (b*
    (((when (atom x)) nil)
     ((when (atom y)) nil)
     (x1 (car x))
     (y1 (car y))
     ((the unsigned-byte x1.offset)
      (sbitset-pair-offset x1))
     ((the unsigned-byte y1.offset)
      (sbitset-pair-offset y1))
     ((when (< x1.offset y1.offset))
      (sbitset-intersect-exec (cdr x) y))
     ((unless (eql x1.offset y1.offset))
      (sbitset-intersect-exec x (cdr y)))
     (x1.block (sbitset-pair-block x1))
     (y1.block (sbitset-pair-block y1))
     (new-block
          (the-sbitset-block (logand (the-sbitset-block x1.block)
                                     (the-sbitset-block y1.block))))
     ((when (eql 0 (the-sbitset-block new-block)))
      (sbitset-intersect-exec (cdr x)
                              (cdr y)))
     (new-pair (sbitset-pair x1.offset new-block)))
    (cons new-pair
          (sbitset-intersect-exec (cdr x)
                                  (cdr y))))))

Function: sbitset-binary-intersect$inline

(defun sbitset-binary-intersect$inline (x y)
       (declare (xargs :guard (and (sbitsetp x) (sbitsetp y))))
       (let ((__function__ 'sbitset-binary-intersect))
            (declare (ignorable __function__))
            (mbe :logic (sbitset-intersect-exec (sbitset-fix x)
                                                (sbitset-fix y))
                 :exec (sbitset-intersect-exec x y))))

Theorem: sbitsetp-of-sbitset-intersect-exec

(defthm sbitsetp-of-sbitset-intersect-exec
        (implies (and (sbitsetp x) (sbitsetp y))
                 (sbitsetp (sbitset-intersect-exec x y))))

Theorem: sbitset-of-sbitset-intersect

(defthm sbitset-of-sbitset-intersect
        (sbitsetp (sbitset-intersect x y)))

Theorem: sbitset-members-of-sbitset-intersect

(defthm sbitset-members-of-sbitset-intersect
        (equal (sbitset-members (sbitset-intersect x y))
               (intersect (sbitset-members x)
                          (sbitset-members y))))