• 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
        • 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-difference

(sbitset-difference X Y) constructs the set X - Y.

Signature

(sbitset-difference x y) → sbitset

Arguments

x — Guard (sbitsetp x).

y — Guard (sbitsetp y).

Definitions and Theorems

Function: sbitset-difference-exec

(defun sbitset-difference-exec (x y)
 (declare (xargs :guard (and (sbitsetp x) (sbitsetp y))))
 (let ((__function__ 'sbitset-difference-exec))
  (declare (ignorable __function__))
  (b*
   (((when (atom x)) nil)
    ((when (atom y)) x)
    (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))
     (cons (car x)
           (sbitset-difference-exec (cdr x) y)))
    ((unless (eql x1.offset y1.offset))
     (sbitset-difference-exec x (cdr y)))
    (x1.block (sbitset-pair-block x1))
    (y1.block (sbitset-pair-block y1))
    (new-block
        (the-sbitset-block (logandc2 (the-sbitset-block x1.block)
                                     (the-sbitset-block y1.block))))
    ((when (eql 0 (the-sbitset-block new-block)))
     (sbitset-difference-exec (cdr x)
                              (cdr y)))
    (new-pair (sbitset-pair x1.offset new-block)))
   (cons new-pair
         (sbitset-difference-exec (cdr x)
                                  (cdr y))))))

Function: sbitset-difference$inline

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

Theorem: sbitsetp-of-sbitset-difference-exec

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

Theorem: sbitset-of-sbitset-difference

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

Theorem: sbitset-members-of-sbitset-difference

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