Bitwise operators
&
pact
(& x y) pact
(& x y)- takes
x:integer - takes
y:integer - produces
integer
Bitwise and
Supported in either invariants or properties.
|
pact
(| x y) pact
(| x y)- takes
x:integer - takes
y:integer - produces
integer
Bitwise or
Supported in either invariants or properties.
xor
pact
(xor x y) pact
(xor x y)- takes
x:integer - takes
y:integer - produces
integer
Bitwise exclusive-or
Supported in either invariants or properties.
shift
pact
(shift x y) pact
(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.
~
pact
(~ x) pact
(~ x)- takes
x:integer - produces
integer
Reverse all bits in x
Supported in either invariants or properties.