#!/usr/bin/python3

import os, SAT_lib, GoL_SAT_utils, SL_common, my_utils

W=20 # WIDTH
H=20 # HEIGHT

s=SAT_lib.SAT_lib()
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)
            s.add_clauses (SL_common.gen_SL(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))

    # each row must contain at least one cell!
    for r in range(H):
        v=[GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W) for c in range(W)]
        s.fix_OR_list (v)

    # each column must contain at least one cell!
    for c in range(W):
        v=[GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W) for r in range(H)]
        s.fix_OR_list (v)

    # make result denser:
    lst=[]
    for r in range(H):
        for c in range(W):
            lst.append(GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W))
    # divide them all by chunks and add to clauses:
    CHUNK_LEN=3
    for c in my_utils.partition(lst,int(len(lst)/CHUNK_LEN)):
        s.add_clause(c)

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

    t=GoL_SAT_utils.SAT_solution_to_grid(grid, VAR_FALSE, s.solution, H, W)
    GoL_SAT_utils.print_grid(t)
    GoL_SAT_utils.write_RLE(t)

    return t

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

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