import z3


targets = {
    (0x00091F53, 0x68FBA45D): None,
    (0x00000C0E, 0x3E98F88A): None,
    (0x0001A660, 0x04B58623): b'NOCHEAT',
    (0x000066DB, 0xA208CA35): b'CHEATOFF',
    (0x00009A12, 0xC7037294): None,
    (0x0006C1D2, 0xB6327AD8): None,
    (0x00005B9B, 0x4054633A): None,
    (0x00011F18, 0xBD67C5D2): None,
    (0x000369A7, 0x90FFC99D): None,
    (0x0005DFC2, 0xC3A3D0C1): None,
    (0x0012AEA6, 0xD6EDD572): None,
    (0x00007C51, 0x348501F8): None,
    (0x000B0354, 0x6692C49D): None,
    (0x000B2974, 0x030792AE): None,
    (0x0003D73D, 0x1645EBE3): None,
    (0x00174E57, 0x3432E939): None,
    (0x000A004D, 0x9071ECD6): None,
    (0x000057AA, 0x17A7A13A): None,
    (0x00003E9B, 0xC9DF00BF): None,
    (0x000081FC, 0x15293D85): None,
    (0x0003BDE6, 0xAD523686): None,
    (0x0000CF49, 0x6BA41039): None,
    (0x00006C6F, 0x4CB9D0FE): None,
    (0x0011D757, 0xD026D5C2): None,
    (0x0000B94C, 0x4C37F1FC): None,
    (0x0000899C, 0xDAEA8887): None,
    (0x000067F7, 0x5D5E8746): None,
    (0x000192C7, 0x23FCE135): None,
    (0x0000009A, 0x00033E70): None,
    (0x000002CE, 0x00346D5B): None,
    (0x00000148, 0x00033F84): None,
}


def hash_it(s, name):
    # Initialize variables
    x = z3.BitVecVal(0, 32)
    iVar6 = z3.BitVecVal(0, 32)
    multiplier_7 = z3.BitVecVal(1, 32)  # iVar5
    multiplier_6 = z3.BitVecVal(1, 32)  # iVar4

    # Process each input byte
    for c in name:
        # Shift values
        c = z3.If(c > 0x40, c - 0x40, c - 0x15)
        c = z3.ZeroExt(24, c)

        # Calculate hash components
        iVar6 += z3.URem(c, 7) * multiplier_7
        x += z3.URem(c, 6) * multiplier_6

        multiplier_6 *= 6
        multiplier_7 *= 7

    # Calculate final hash value
    z = iVar6 * (x * 2 + 1)
    return x, z


def solve_hash(t1, t2, length=8):
    s = z3.Solver()

    # Name character array, constrained to printable ASCII
    name = [z3.BitVec(f'n_{i}', 8) for i in range(length)]
    for c in name:
        # s.add(c >= 32, c <= 126)  # any printable ASCII character
        # s.add(c >= ord('A'), c <= ord('Z'))  # uppercase alpha
        s.add(z3.Or(
            z3.And(c >= ord('A'), c <= ord('Z')),  # uppercase alpha
            z3.And(c >= ord('0'), c <= ord('9'))   # or numeric
        ))

    # Compute the hash
    x, z = hash_it(s, name)
    s.add(
        z3.Or(
            x == t1,  # player 1
            x | (1 << 0x1A) == t1  # player 2
        ),
        z == t2
    )

    if s.check() == z3.sat:
        m = s.model()
        return bytes([m[b].as_long() for b in name]).decode()

    return None


for length in range(4, 12):
    print('Considering names of length', length)
    for (t1, t2), known in targets.items():
        if known is not None:
            continue

        answer = solve_hash(t1, t2, length)
        if answer is None:
            continue

        print(f"h'(0x{t1:08x}, 0x{t2:08x}) = '{answer}'")
        targets[(t1, t2)] = answer


# Pretty print the array again
print('targets = {')
for (t1, t2), known in targets.items():
    print(f'    (0x{t1:08x}, 0x{t2:08x}): {known!r},')
print('}')