from z3 import *

NUM_BITS = 8

INT_MAX = 2**(NUM_BITS - 1) - 1
INT_MIN = - (2**(NUM_BITS-1))

"""
https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax
Compute the minimum (min) or maximum (max) of two integers without branching:
int x;  // we want to find the minimum of x and y
int y;   
int r;  // the result goes here 

r = y ^ ((x ^ y) & -(x < y)); // min(x, y)
"""
x = BitVec("x", NUM_BITS)
y = BitVec("y", NUM_BITS)
zero = BitVecVal(0, NUM_BITS)
one = BitVecVal(1, NUM_BITS)

print("variant 1, signed")
r_s = y ^ ((x ^ y) & (zero -(If(x < y, one, zero))))
min_s = If(x<y, x, y)
solve(r_s != min_s)

#print("variant 1, unsigned")
#r_u = y ^ ((x ^ y) & (zero -(If(ULT(x, y), one, zero))))
#m_u = If(ULT(x,y), x, y)
#solve(r_u != m_u)

"""
Other websites report different versions (https://github.com/keon/awesome-bits):
Get the min of two [32-bit integer] values

a & ((a-b) >> 31) | b & (~(a-b) >> 31);
"""

print("variant 2, signed")
r2_s = (x & ((x-y) >> (NUM_BITS - 1))) | (y & (~(x-y) >> (NUM_BITS - 1)))
solve(r2_s != min_s)

print("variant 2, unsigned")
min_u = If(ULT(x, y), x, y)
r2_u = (x & (LShR(x-y, (NUM_BITS - 1)))) | (y & LShR(~(x-y), (NUM_BITS - 1)))
solve(r2_u != min_u)





"""
https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax
If you know that INT_MIN <= x - y <= INT_MAX, then you can use the following,
 which are faster because (x - y) only needs to be evaluated once.
r = y + ((x - y) & ((x - y) >> (sizeof(int) * CHAR_BIT - 1))); // min(x, y)
"""

print("variant 3, signed")
r3 = y + ((x - y) & ((x - y) >> (NUM_BITS - 1)))
overflow = If(y < 0, x > INT_MAX + y, x < INT_MIN + y)
solve(And(Not(overflow), r3 != min_s))