#!/usr/bin/python3

import os
from GoL_SAT_utils import *

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 (cell_is_true(coords_to_var(grid, VAR_FALSE, r, c, H, W),
                                             get_neighbours(grid, VAR_FALSE, r, c, H, W)))
            else:
                s.add_clauses (cell_is_false(coords_to_var(grid, VAR_FALSE, r, c, H, W),
                                              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 (cell_is_false(coords_to_var(grid, VAR_FALSE, r, c, H, W),
                                          get_neighbours(grid, VAR_FALSE, r, c, H, W)))
    for c in [-1,W]:
        for r in range(-1, H+1):
            s.add_clauses (cell_is_false(coords_to_var(grid, VAR_FALSE, r, c, H, W),
                                          get_neighbours(grid, VAR_FALSE, r, c, H, W)))

    assert s.solve()

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

    print_grid(tmp)
    write_RLE(tmp)

    return tmp

while True:
    try_again()
    if s.fetch_next_solution()==False:
        break
    print ("")