Bitops/extra-defs
Additional bitwise operations.
This is just an ad-hoc collection of low-level bit operations,
mostly developed in support of specifying various integer and packed-integer
instructions.
Subtopics
- Abs-diff
- (abs-diff a b) is just (abs (- (ifix a) (ifix b))), but
optimized for ACL2::gl.
- Nth-slice512
- Extract the nth 512-bit slice of the integer x.
- Nth-slice128
- Extract the nth 128-bit slice of the integer x.
- Nth-slice8
- Extract the nth 8-bit slice of the integer x.
- Nth-slice64
- Extract the nth 64-bit slice of the integer x.
- Nth-slice4
- Extract the nth 4-bit slice of the integer x.
- Nth-slice32
- Extract the nth 32-bit slice of the integer x.
- Nth-slice256
- Extract the nth 256-bit slice of the integer x.
- Nth-slice2
- Extract the nth 2-bit slice of the integer x.
- Nth-slice16
- Extract the nth 16-bit slice of the integer x.
- Negate-slice8
- (negate-slice8 x) computes the 8-bit two's complement negation of
x and returns it as an 8-bit natural.
- Copybit
- Set To[n] := From[n]
- Negate-slice32
- (negate-slice32 x) computes the 32-bit two's complement negation
of x and returns it as an 32-bit natural.
- Negate-slice16
- (negate-slice16 x) computes the 16-bit two's complement negation
of x and returns it as an 16-bit natural.
- Negate-slice64
- (negate-slice64 x) computes the 64-bit two's complement negation
of x and returns it as an 64-bit natural.
- Bitscan-rev
- (bitscan-rev src) returns the bit position of the most significant
bit in src that is set, or 0 when src is zero (and hence has no such
bit).
- Bitscan-fwd
- (bitscan-fwd src) returns the bit position of the least significant
bit in src that is set, or 0 when src is zero (and hence has no such
bit).
- Setbit
- Set X[n] := 1
- Notbit
- Set X[n] := ~X[n]
- Clearbit
- Set X[n] := 0
