#!/usr/bin/python3

import os
import GoL_SAT_utils, SAT_lib

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):
            v=GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W)
            n=GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W)
            if final_state[r][c]=="*":
                s.add_clauses (GoL_SAT_utils.cell_is_true(v, n))
            else:
                s.add_clauses (GoL_SAT_utils.cell_is_false(v, n))

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

    for c in [-1,W]:
        for r in range(-1, H+1):
            v=GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W)
            n=GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W)
            s.add_clauses (GoL_SAT_utils.cell_is_false(v, n))

    assert s.solve()

    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:
    try_again()
    if s.fetch_next_solution()==False:
        break
    print ("")