#!/usr/bin/python3

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

#"""
final_state=[
" * ",
"* *",
" * "]
#"""

"""
final_state=[
"      ",
"      ",
" **** ",
"      ",
"      "]
"""

"""
final_state=[
"             ",
"   *     *   ",
"    *   *    ",
"   *******   ",
"  ** *** **  ",
" *********** ",
" * ******* * ",
" * *     * * ",
"    ** **    ",
"             "]
"""

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]=="*":
                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

while True:
    solution=try_again()
    if solution==None:
        break

    s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(solution, grid, VAR_FALSE, H, W)))
    s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(my_utils.reflect_vertically(solution), grid, VAR_FALSE, H, W)))
    s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(my_utils.reflect_horizontally(solution), grid, VAR_FALSE, H, W)))
    # is this square?
    if W==H:
        s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(my_utils.rotate_rect_array(solution,1), grid, VAR_FALSE, H, W)))
        s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(my_utils.rotate_rect_array(solution,2), grid, VAR_FALSE, H, W)))
        s.add_clause(SAT_lib.negate_clause(GoL_SAT_utils.grid_to_clause(my_utils.rotate_rect_array(solution,3), grid, VAR_FALSE, H, W)))
    print ("")