#!/usr/bin/env python3

import sys
from z3 import *

"""
coordinates:
------------------------------
00 01 02 | 03 04 05 | 06 07 08
10 11 12 | 13 14 15 | 16 17 18
20 21 22 | 23 24 25 | 26 27 28
------------------------------
30 31 32 | 33 34 35 | 36 37 38
40 41 42 | 43 44 45 | 46 47 48
50 51 52 | 53 54 55 | 56 57 58
------------------------------
60 61 62 | 63 64 65 | 66 67 68
70 71 72 | 73 74 75 | 76 77 78
80 81 82 | 83 84 85 | 86 87 88
------------------------------
"""

s=Solver()

# using Python list comprehension, construct array of arrays of BitVec instances:
cells=[[BitVec('cell%d%d' % (r, c), 16) for c in range(9)] for r in range(9)]

# http://www.norvig.com/sudoku.html
# http://www.mirror.co.uk/news/weird-news/worlds-hardest-sudoku-can-you-242294
puzzle=""
puzzle+="..53....."
puzzle+="8......2."
puzzle+=".7..1.5.."
puzzle+="4....53.."
puzzle+=".1..7...6"
puzzle+="..32...8."
puzzle+=".6.5....9"
puzzle+="..4....3."
puzzle+=".....97.."

# process text line:
current_column=0
current_row=0
for i in puzzle:
    if i!='.':
        s.add(cells[current_row][current_column]==BitVecVal(int(i),16))
    current_column=current_column+1
    if current_column==9:
        current_column=0
        current_row=current_row+1

one=BitVecVal(1,16)
mask=BitVecVal(0b1111111110,16)

# for all 9 rows
for r in range(9):
    s.add(((one<<cells[r][0]) |
        (one<<cells[r][1]) |
        (one<<cells[r][2]) |
        (one<<cells[r][3]) |
        (one<<cells[r][4]) |
        (one<<cells[r][5]) |
        (one<<cells[r][6]) |
        (one<<cells[r][7]) |
        (one<<cells[r][8]))==mask)

# for all 9 columns
for c in range(9):
    s.add(((one<<cells[0][c]) |
        (one<<cells[1][c]) |
        (one<<cells[2][c]) |
        (one<<cells[3][c]) |
        (one<<cells[4][c]) |
        (one<<cells[5][c]) |
        (one<<cells[6][c]) |
        (one<<cells[7][c]) |
        (one<<cells[8][c]))==mask)

# enumerate all 9 squares
for r in range(0, 9, 3):
    for c in range(0, 9, 3):
        # add constraints for each 3*3 square:
            s.add(one<<cells[r+0][c+0] |
                one<<cells[r+0][c+1] |
                one<<cells[r+0][c+2] |
                one<<cells[r+1][c+0] |
                one<<cells[r+1][c+1] |
                one<<cells[r+1][c+2] |
                one<<cells[r+2][c+0] |
                one<<cells[r+2][c+1] |
                one<<cells[r+2][c+2]==mask)

print (s.check())
#print (s.model())
m=s.model()

for r in range(9):
    for c in range(9):
        sys.stdout.write (str(m[cells[r][c]])+" ")
    print ("")