# coding: utf-8
import os, sys
from z3 import *

# get the playground information
if len(sys.argv) != 2:
    print("Usage: python3 square.py <test-file>")
    sys.exit(0)

with open(sys.argv[1]) as f:
    playground = f.read()
rows = playground.strip().split("\n")
playground = [[None if x == "_" else int(x) for x in r.split()] for r in rows]

# get the playground size
size_y = len(playground)
assert(size_y != 0)
size_x = len(playground[0])
assert(size_x != 0)
assert(size_x == size_y)

#################################### Square ####################################

# create the solver
solver = Solver()

# hint: when creating Int(...) variables for the cells, use something like the coordinates as part of the variable name
numbers = [[None for _j in range(size_x)] for _j in range(size_y)]



# call the solver and check satisfiability
res = solver.check()
if res != sat:
    print("unsat")
    sys.exit(1)

# print the model
m = solver.model()
for i in range(size_y):
    results = []
    for j in range(size_x):
        num = numbers[i][j]
        results.append("_" if num is None else m[num].as_long())
    print(("%4s" * len(results)) % tuple(results))

################################################################################