#!/usr/bin/python3

from typing import List
import os, SAT_lib, GoL_SAT_utils, my_utils

# https://www.conwaylife.com/wiki/Garden_of_Eden#Records
# https://conwaylife.com/patterns/gardenofeden1.cells
# 1971, Roger Banks et al., 33 × 9 = 297
"""
final_state=[
"OOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOO",
"OO.O.OOO.OOO.OO.O.O.O.O.O.O.O.O.O",
"O.O.OOO.OOO.OOOO.OOO.O.O.O.O.O.O.",
"OOOOO.OOO.OOO.OOOO.OOOOOOOOOOOOOO",
"O.O.OO.OOO.OOO.O.OOO.O.O.O.O.O.O.",
"OOOO.OOO.OOO.OOOOO.OO.O.O.O.O.O.O",
".OO.OOO.OOO.OOO.O.O.OOOOOOOOOOOOO",
"OO.OO.OOO.OOO.OO.OOOO.O.O.O.O.O.O",
"OOOOOOOOOOOOOOOOOO.OOOOOOOOOOOOOO"]
"""

# https://www.conwaylife.com/wiki/Garden_of_Eden#Records
# https://conwaylife.com/patterns/gardenofeden5x45.cells
# 2016, Steven Eker, 45 × 5 = 225
"""
final_state=[
"OO.O.O..O.OOO.O..OOO.OOOOOOO..OOOOOO..O.O.O.O",
".OO.O.OO.O.O.O.O.O.OOO.O.O.O.O.O.O.OOO.O.O.O.",
"..OO.OO..OOOO..OOOOOO..OOOOOO..OOOOO.OOOOO.O.",
".OO.O.OO.O.O.O.O.O.OOO.O.O.O.O.O.O.OOO.O.O.O.",
"OO.O.O..O.OOO.O..OOO.OOOOOOO..OOOOOO..O.O.O.O"]
"""
# https://www.conwaylife.com/wiki/Garden_of_Eden#Records
# https://www.conwaylife.com/patterns/gardenofeden11.cells
# 2017, Steven Eker, 9 × 11 = 99
final_state=[
"..OO.OOO.O.",
".O..O.O.O..",
"O.OOO..OOO.",
".O.O.O..O.O",
".OOO..OO..O",
"OO...OO..O.",
"O.O.O.OOO..",
"O..O.O..O..",
".OOO..OOOO."]

H=len(final_state) # HEIGHT
W=len(final_state[0]) # WIDTH

print ("HEIGHT=", H, "WIDTH=", W)

s=SAT_lib.SAT_lib(maxsat=False)
VAR_FALSE=s.const_false
grid=[[s.create_var() for w in range(W)] for h in range(H)]

def try_again ():
    # rules for the main part of grid
    for r in range(H):
        for c in range(W):
            if final_state[r][c]=="O":
                s.add_clauses (GoL_SAT_utils.cell_is_true(GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W),
                                             GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W)))
            else:
                s.add_clauses (GoL_SAT_utils.cell_is_false(GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W),
                                              GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W)))

    # cells behind visible grid must always be false:
    for c in range(-1, W+1):
        for r in [-1,H]:
            s.add_clauses (GoL_SAT_utils.cell_is_false(GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W),
                                          GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W)))
    for c in [-1,W]:
        for r in range(-1, H+1):
            s.add_clauses (GoL_SAT_utils.cell_is_false(GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W),
                                          GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W)))

    if s.solve()==False:
        return None

    tmp=GoL_SAT_utils.SAT_solution_to_grid(grid, VAR_FALSE, s.solution, H, W)

    GoL_SAT_utils.print_grid(tmp)
    GoL_SAT_utils.write_RLE(tmp)

    return tmp

solution=try_again()
if solution==None:
    print ("Eden (UNSAT)")
else:
    print ("not Eden (SAT)")