from z3 import *

with open('init.lua', 'r') as f:
    data_raw = f.read().split('\\n')

line_ptr = 0
while 'Cutlane' not in data_raw[line_ptr]:
    line_ptr += 1

arr = [0 for _ in range(20000)]

print(line_ptr)

def get_val(l):
    return (int(l.split('_')[1]), int(l.split('_')[2]))

def get_opers_0(l):
    return int(l.split('[')[1].split(']')[0])

def get_opers_2_3(oper_1, oper_1_0):
    if oper_1_0 != 'MOV':
        oper_1_1 = oper_1.split('(')[1].split(')')[0]
        oper_a = oper_1_1.split(', ')
    else:
        oper_a = (oper_1, None)
    
    if 'var_arr' in oper_a[0]:
        oper_2 = ('arr', get_opers_0(oper_a[0]))
    elif 'var' in oper_a[0]:
        oper_2 = ('var', get_val(oper_a[0]))
    else:
        oper_2 = ('const', int(oper_a[0]))
    
    if oper_a[1] == None:
        return (oper_2, None)

    if 'var_arr' in oper_a[1]:
        oper_3 = ('arr', get_opers_0(oper_a[1]))
    elif 'var' in oper_a[1]:
        oper_3 = ('var', get_val(oper_a[1]))
    else:
        oper_3 = ('const', int(oper_a[1]))

    return (oper_2, oper_3)

state = [
    [ BitVec(f'x{i}{j}', 1) for j in range(5) ] for i in range(15)
]

while True:
    if line_ptr >= len(data_raw):
        break
    line = data_raw[line_ptr]
    if 'if var_arr' in line:
        stripped_0 = int(line.split('if var_arr[')[1].split(']')[0])
        stripped_1 = int(line.split(' and ')[0].split('== ')[1])
        if stripped_1 == 0:
            
            line_ptr += 1
            continue
        s = Solver()
        s.add(arr[stripped_0] == stripped_1)
        assert(s.check() == sat)
        m = s.model()
        for i in range(5):
            for j in range(15):
                v = m[BitVec(f'x{j}{i}', 1)].as_long()
                if v == 1:
                    print('#', end='')
                else:
                    print('.', end='')
            print()
        arr = [0 for _ in range(20000)]
    elif 'local var_arr' not in line and 'var_arr' in line:
        
        oper_0 = get_opers_0(line.split(' = ')[0])
        #print(line, end=' ')
        oper_1 = line.split(' = ')[1]
        if 'XOR' in oper_1:
            oper_1 = 'XOR'
        elif 'AND' in oper_1:
            oper_1 = 'AND'
        elif 'OR' in oper_1:
            oper_1 = 'OR'
        else:
            oper_1 = 'MOV'
        
        oper_2, oper_3 = get_opers_2_3(line.split(' = ')[1], oper_1)
        #print(oper_0, oper_1, oper_2, oper_3)

        if oper_2[0] == 'var':
            A = state[oper_2[1][0]][oper_2[1][1]]
        elif oper_2[0] == 'arr':
            A = arr[oper_2[1]]
        elif oper_2[0] == 'const':
            A = oper_2[1]
        else:
            raise NotImplementedError
        
        if oper_3 == None:
            B = None
        elif oper_3[0] == 'var':
            B = state[oper_3[1][0]][oper_3[1][1]]
        elif oper_3[0] == 'arr':
            B = arr[oper_3[1]]
        elif oper_3[0] == 'const':
            B = oper_3[1]
        else:
            raise NotImplementedError
        
        if oper_1 == 'MOV':
            assert(B == None)
            arr[oper_0] = A
        elif oper_1 == 'OR':
            arr[oper_0] = A | B
        elif oper_1 == 'XOR':
            arr[oper_0] = A ^ B
        elif oper_1 == 'AND':
            arr[oper_0] = A & B
        else:
            raise NotImplementedError

    else:
        pass #print(line)

    line_ptr += 1