Bitwise operators
&
(& x y)(& x y)- takes
x:integer - takes
y:integer - produces
integer
Bitwise and
Supported in either invariants or properties.
|
(| x y)(| x y)- takes
x:integer - takes
y:integer - produces
integer
Bitwise or
Supported in either invariants or properties.
xor
(xor x y)(xor x y)- takes
x:integer - takes
y:integer - produces
integer
Bitwise exclusive-or
Supported in either invariants or properties.
shift
(shift x y)(shift x y)- takes
x:integer - takes
y:integer - produces
integer
Shift x y bits left if y is positive, or right by -y bits otherwise.
Supported in either invariants or properties.
~
(~ x)(~ x)- takes
x:integer - produces
integer
Reverse all bits in x
Supported in either invariants or properties.