import re
f = open("./sakura_de.c", "r").read()
idx = re.findall("v[0-9]* = \(__int64 \*\)nothing_[0-9]*\(\(__int64\)\&v([0-9]*)\)", f)
loop_n = re.findall("v[0-9]* = plus_([0-9]*)", f)
con = re.findall("\( v[0-9]* \!= ([0-9]*) \)", f)
f = open("./variables", "r").read()
equ = re.findall("v([0-9]*) = ([0-9]*);", f)
stack = [0]*1944
for ( x , y ) in equ:
stack[int(x)] = int(y)
get_stack = lambda a,b: (stack[int(idx[a])+b*2] + (stack[int(idx[a])+1+b*2] <<32))
z3_code = """
#! /usr/bin/env python
# -*- coding: utf-8 -*-
from z3 import *
s = Solver()
"""
for row in range(20):
for col in range(20):
name = chr(ord('A')+row) + str(col)
z3_code += "{} = Int('{}')\n".format(name,name)
z3_code += "s.add( 0 < {} , {} < 10)\n".format(name,name)
for j in range(150):
loop = int(int(loop_n[j])/8)
this_loop = []
for i in range(loop):
xx = get_stack(j,i)
row = xx&0xffffffff
col = xx>>32
this_loop.append((row, col))
for i in range(0,len(this_loop)-1):
(row, col) = this_loop[i]
a = chr(ord('A')+row) + str(col)
for k in range(i+1,len(this_loop)):
(row, col) = this_loop[k]
b = chr(ord('A')+row) + str(col)
z3_code += "s.add( {} != {})\n".format(a, b)
z3_code += "s.add("
for i in range(len(this_loop)):
(row, col) = this_loop[i]
a = chr(ord('A')+row) + str(col)
z3_code += " {} + ".format(a)
z3_code += " 0 == {})\n".format(con[j])
z3_code += """
s.check()
m = s.model()
sakura = [0]*400
for i in m:
row = ord(str(i)[0]) - ord('A')
col = int(str(i)[1:])
sakura[ 20*row + col ] = str(m[i])
print ''.join(sakura)
"""
exec z3_code
