• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
        • Bv
          • Byte-to-bits
          • Bits-to-byte-little
          • Bits-to-byte
          • Byte-to-bits-little
          • Bvchop
          • Bvuminus
          • Bvplus
          • Bvminus
          • Ihs
          • Rtl
        • Algebra
      • Testing-utilities
    • Bv

    Bvminus

    Bit-vector difference.

    ;; Compute the (modular) difference of X and Y.
    ;; TODO: Consider defining this in terms of bvplus and bvuminus.
    (defund bvminus (size x y)
      (declare (type (integer 0 *) size))
      (bvchop size (- (ifix x) (ifix y))))