from z3 import *
set_param("parallel.enable", True)
n = 64
m = 2
flags = BitVec('flags', n)
check = BitVec('check', m)

# // `flags` is a 32bit integer. It can store 16 flags of 2bit size each.
# // `check` is a 2 bit flag ( integer with only 2 bits set )
# // We have to find if `check` flag is set anywhere in 16 slots of `flags`

# the mask is 1 repeated every m bits
const = BitVecVal(0, n)
for i in range(0, n, m):
    const |= (1 << i)

print(hex(simplify(const).as_long()))

def f(flags, check):
    mask = (ZeroExt(n-m, check)) * const
    diff = flags ^ mask
    # cascade the result and check if it is 0
    half = diff | (diff >> 1)
    half = half & const
    flip = ~half & const
    return simplify((flip != 0))

def g(flags, check):
    return simplify(Or([Extract(i+(m-1), i, flags) == check for i in range(0, n, m)]))

# print(simplify(f(flags, check)))
# print(simplify(g(flags, check)))

s = Solver()
s.add(f(flags, check) != g(flags, check))
# assert(s.check() == unsat)
if s.check() == sat:
    print(s.model())
else:
    print("unsat")