import string
import z3

def is_char_allowed(current_char):
    current_char = ord(current_char)
    if (current_char & 128) != 0 or not ((current_char >> 6) & 1) or (current_char >> 4) & 1 and (current_char >> 3) & 1 and ((current_char >> 2) & 1 or (current_char >> 1) & 1 and current_char & 1) or not ((current_char >> 4) & 1) and not ((current_char >> 3) & 1) and not ((current_char >> 2) & 1) and not ((current_char >> 1) & 1) and not (current_char & 1):
        return False
    return True

# (((chr >> 5) & 1) << 15) | ((((chr >> 5) & 1) << 14) | ((((chr >> 5) & 1) << 13) | ((((chr >> 5) & 1) << 10) | ((((chr >> 4) & 1) << 9) | ((((chr >> 3) & 1) << 8) | (((chr >> 5) & 1) << 7) | ((((chr >> 5) & 1) << 6) | ((unsigned __int8)(32 * ((chr >> 5) & 1)) | ((unsigned __int8)(4 * ((chr >> 2) & 1)) | ((unsigned __int8)(2 * ((chr >> 1) & 1)) | chr & 1) & 0xFB) & 0xDF) & 0xBF) & 0x7F) & 0xFDFF) & 0xFBFF) & 0xDFFF) & 0xBFFF) & 0x7FFF;

out = []
for ch in string.printable:
    if is_char_allowed(ch):
        out.append(ch)


def get_char(ch):
    return (((ch >> 5) & 1) << 15) | ((((ch >> 5) & 1) << 14) | ((((ch >> 5) & 1) << 13) | ((((ch >> 5) & 1) << 10) | ((((ch >> 4) & 1) << 9) | ((((ch >> 3) & 1) << 8) | (((ch >> 5) & 1) << 7) | ((((ch >> 5) & 1) << 6) | ((0xff&(32 * ((ch >> 5) & 1))) | ((0xff&(4 * ((ch >> 2) & 1))) | ((0xff&(2 * ((ch >> 1) & 1))) | ch & 1) & 0xFB) & 0xDF) & 0xBF) & 0x7F) & 0xFDFF) & 0xFBFF) & 0xDFFF) & 0xBFFF) & 0x7FFF


rzeczy = []
for o in out:
    rzeczy.append(get_char(ord(o)))

x = z3.BitVec('x', 64)
y = z3.BitVec('y', 64)
s = z3.Solver()

s.add((y + (x + (1 + 0xf4a30cd491608469 * x) * 0x80884058088405 + 0x44424E) * 0x80884058088405)+7644228357687976132 == 0)
v = []
for ch in rzeczy:
    v.append(f"(x&0xffff == {ch})")
v = " or ".join(v)
s.add(eval(v))

v = []
for ch in rzeczy:
    v.append(f"(y&0xffff == {ch})")
v = " or ".join(v)
s.add(eval(v))

print(s.check())
print(s.model())
print(out)