from z3 import *
import base64
import os

solver = Solver()

input = []
for i in range(0x24):
    input.append(BitVec('b%i' % i, 8))


for i in range(0x24):
    solver.add(input[i] >= 48)
    solver.add(input[i] <= 122)

solver.add(input[0] == 0x63)

solver.add(input[2] == ord("V"))

# solver.add(input[0xa] == ord('V'))

solver.add(input[0xa] == input[2])

solver.add(input[1] == 0x32)

solver.add(input[3] == 0x6a)

solver.add(input[0] + 1 == input[4])

solver.add(input[0xc] == input[4] - 1)
solver.add(input[4] - 1 == input[0x16])
solver.add(input[4] - 1 == input[0x18])

solver.add(input[0x23] == input[0xb] + 9)  # maybe 22

solver.add(input[3] - 0x20 == input[6])

solver.add(input[0xb] == 0x30)
solver.add(input[0x17] == 0x30)

solver.add(input[0] - 1 == input[8])

solver.add(input[4] + 2 == input[0x1b])
solver.add(input[4] + 2 == input[0x1f])

solver.add(input[0x1b] + 7 == input[9])
solver.add(input[0x1b] + 7 == input[0x19])

solver.add(input[1] + 1 == input[0xd])
solver.add(input[1] + 1 == input[0x11])
solver.add(input[1] + 1 == input[0x15])

solver.add(input[7] == 0x70)

solver.add(input[0xf] == input[7] + 3)

solver.add(input[0xf] + 1 == input[0xe])

solver.add(input[0x13] == 0x7a)
solver.add(input[0] - 0x21 == input[0x22])


solver.add(input[5] == ord('X'))
solver.add(input[0x14] == ord('X'))
solver.add(input[0x1d] == ord('X'))
solver.add(input[0x21] == ord('X'))

# solver.add(0x58 ^ input[5] ^ input[0x14] ^ input[0x1d] ^ input[0x21] == 0x58)


solver.add(input[0x1a] == 0x31)
solver.add(input[9] - 0x20 == input[0x10])
solver.add(input[0x10] == input[0x1c])

solver.add(input[1] == 0x32)

solver.add(input[0x7] - 0x1e == input[0x12])

solver.add(input[0x12] == input[0x1e])

solver.add(input[0x4] == input[0x20])


print("Solving...")
# Solve the equations

print(solver.check())
modl = solver.model()
# Create an ASCII string from the resulting bytes
res = ""
for obj in input:
    try:
        c = modl[obj].as_long()
        print('b%i: %x' % (i, c))
        res = res + chr(c)
    except:
        pass
print("Result: " + res)
print(base64.b64decode(res))