From 3125ccbc33caab926c986ef7fd3bd8251408ac81 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Sat, 28 Dec 2019 21:44:18 -0800 Subject: [PATCH] Support for irregular grids --- examples/akari.py | 18 +- examples/araf.py | 44 ++-- examples/battleship.py | 62 ++--- examples/castle_wall.py | 18 +- examples/cave.py | 22 +- examples/fillomino.py | 21 +- examples/gokigen_naname.py | 32 +-- examples/greater_than_killer_sudoku.py | 12 +- examples/halloween_valentines.py | 17 +- examples/heteromino.py | 55 ++--- examples/kuromasu.py | 25 +- examples/lits.py | 49 ++-- examples/masyu.py | 45 ++-- examples/nanro.py | 30 +-- examples/numberlink.py | 35 +-- examples/nurikabe.py | 48 ++-- examples/shape.py | 72 ++++++ examples/skyscraper.py | 16 +- examples/slitherlink.py | 38 ++-- examples/spiral_galaxies.py | 23 +- examples/star_battle.py | 15 +- examples/statue_park_loop.py | 106 +++++++++ examples/sudoku.py | 16 +- examples/tapa.py | 19 +- examples/tutorial.ipynb | 44 ++-- examples/yajilin.py | 23 +- grilops/grids.py | 216 +++++++++++------- grilops/loops.py | 290 +++++++++++------------ grilops/regions.py | 303 +++++++++++++------------ grilops/shapes.py | 253 +++++++++++---------- grilops/sightlines.py | 39 ++-- test/golden/shape.py.txt | 13 ++ test/golden/statue_park_loop.py.txt | 27 +++ 33 files changed, 1214 insertions(+), 832 deletions(-) create mode 100644 examples/shape.py create mode 100644 examples/statue_park_loop.py create mode 100644 test/golden/shape.py.txt create mode 100644 test/golden/statue_park_loop.py.txt diff --git a/examples/akari.py b/examples/akari.py index ade13b7..5aedc46 100644 --- a/examples/akari.py +++ b/examples/akari.py @@ -8,6 +8,7 @@ import grilops import grilops.sightlines +from grilops import Point def main(): @@ -58,21 +59,23 @@ def main(): ("EMPTY", " "), ("LIGHT", "*"), ]) - sg = grilops.SymbolGrid(size, size, sym) + locations = grilops.get_square_locations(size) + sg = grilops.SymbolGrid(locations, sym) for y in range(size): for x in range(size): + p = Point(y, x) if (y, x) in black_cells: - sg.solver.add(sg.cell_is(y, x, sym.BLACK)) - light_count = black_cells[(y, x)] + sg.solver.add(sg.cell_is(p, sym.BLACK)) + light_count = black_cells[p] if light_count is not None: sg.solver.add(PbEq( - [(n.symbol == sym.LIGHT, 1) for n in sg.adjacent_cells(y, x)], + [(n.symbol == sym.LIGHT, 1) for n in sg.adjacent_cells(p)], light_count )) else: # All black cells are given; don't allow this cell to be black. - sg.solver.add(sg.cell_is_one_of(y, x, [sym.EMPTY, sym.LIGHT])) + sg.solver.add(sg.cell_is_one_of(p, [sym.EMPTY, sym.LIGHT])) def is_black(c): return c == sym.BLACK @@ -83,16 +86,17 @@ def count_light(c): for x in range(size): if (y, x) in black_cells: continue + p = Point(y, x) visible_light_count = sum( grilops.sightlines.count_cells( sg, n.location, n.direction, count=count_light, stop=is_black - ) for n in sg.adjacent_cells(y, x) + ) for n in sg.adjacent_cells(p) ) # Ensure that each light cannot see any other lights, and that each cell # is lit by at least one light. sg.solver.add( If( - sg.cell_is(y, x, sym.LIGHT), + sg.cell_is(p, sym.LIGHT), visible_light_count == 0, visible_light_count > 0 ) diff --git a/examples/araf.py b/examples/araf.py index d9e8e73..78fb76a 100644 --- a/examples/araf.py +++ b/examples/araf.py @@ -8,7 +8,7 @@ import grilops import grilops.regions - +from grilops import Point HEIGHT, WIDTH = 7, 7 GIVENS = { @@ -36,6 +36,7 @@ def add_given_pair_constraints(sg, rc): # Each larger (root) given must be paired with a single smaller given in its # same region, and the size of the region must be between the givens' values. for (ly, lx), lv in GIVENS.items(): + lp = Point(ly, lx) partner_terms = [] for (sy, sx), sv in GIVENS.items(): if (ly, lx) == (sy, sx): @@ -43,35 +44,37 @@ def add_given_pair_constraints(sg, rc): if lv <= sv: continue + sp = Point(sy, sx) + # Rule out pairs that can't possibly work, due to the Manhattan distance # between givens being too large. manhattan_distance = abs(ly - sy) + abs(lx - sx) min_region_size = manhattan_distance + 1 if lv < min_region_size: sg.solver.add( - rc.region_id_grid[sy][sx] != rc.location_to_region_id((ly, lx))) + rc.region_id_grid[sp] != rc.location_to_region_id(lp)) continue partner_terms.append( And( # The smaller given must not be a region root. - Not(rc.parent_grid[sy][sx] == grilops.regions.R), + Not(rc.parent_grid[sp] == grilops.regions.R), # The givens must share a region, rooted at the larger given. - rc.region_id_grid[sy][sx] == rc.location_to_region_id((ly, lx)), + rc.region_id_grid[sp] == rc.location_to_region_id(lp), # The region must be larger than the smaller given's value. - sv < rc.region_size_grid[ly][lx] + sv < rc.region_size_grid[lp] ) ) if not partner_terms: - sg.solver.add(rc.parent_grid[ly][lx] != grilops.regions.R) + sg.solver.add(rc.parent_grid[lp] != grilops.regions.R) else: sg.solver.add( Implies( - rc.parent_grid[ly][lx] == grilops.regions.R, + rc.parent_grid[lp] == grilops.regions.R, And( - rc.region_size_grid[ly][lx] < lv, + rc.region_size_grid[lp] < lv, PbEq([(term, 1) for term in partner_terms], 1) ) ) @@ -85,15 +88,17 @@ def main(): # The grid symbols will be the region IDs from the region constrainer. sym = grilops.make_number_range_symbol_set(0, HEIGHT * WIDTH - 1) - sg = grilops.SymbolGrid(HEIGHT, WIDTH, sym) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, sym) rc = grilops.regions.RegionConstrainer( - HEIGHT, WIDTH, sg.solver, + locations, sg.solver, min_region_size=min_given_value + 1, max_region_size=max_given_value - 1 ) for y in range(HEIGHT): for x in range(WIDTH): - sg.solver.add(sg.cell_is(y, x, rc.region_id_grid[y][x])) + p = Point(y, x) + sg.solver.add(sg.cell_is(p, rc.region_id_grid[p])) # Exactly half of the givens must be region roots. As an optimization, add # constraints that the smallest givens must not be region roots, and that the @@ -101,18 +106,19 @@ def main(): undetermined_given_locations = [] num_undetermined_roots = len(GIVENS) // 2 for (y, x), v in GIVENS.items(): + p = Point(y, x) if v == min_given_value: - sg.solver.add(Not(rc.parent_grid[y][x] == grilops.regions.R)) + sg.solver.add(Not(rc.parent_grid[p] == grilops.regions.R)) elif v == max_given_value: - sg.solver.add(rc.parent_grid[y][x] == grilops.regions.R) + sg.solver.add(rc.parent_grid[p] == grilops.regions.R) num_undetermined_roots -= 1 else: - undetermined_given_locations.append((y, x)) + undetermined_given_locations.append(p) sg.solver.add( PbEq( [ - (rc.parent_grid[y][x] == grilops.regions.R, 1) - for (y, x) in undetermined_given_locations + (rc.parent_grid[p] == grilops.regions.R, 1) + for p in undetermined_given_locations ], num_undetermined_roots ) @@ -122,15 +128,15 @@ def main(): for y in range(HEIGHT): for x in range(WIDTH): if (y, x) not in GIVENS: - sg.solver.add(Not(rc.parent_grid[y][x] == grilops.regions.R)) + sg.solver.add(Not(rc.parent_grid[Point(y, x)] == grilops.regions.R)) add_given_pair_constraints(sg, rc) region_id_to_label = { - rc.location_to_region_id((y, x)): chr(65 + i) + rc.location_to_region_id(Point(y, x)): chr(65 + i) for i, (y, x) in enumerate(GIVENS.keys()) } - def show_cell(unused_y, unused_x, region_id): + def show_cell(unused_loc, region_id): return region_id_to_label[region_id] if sg.solve(): diff --git a/examples/battleship.py b/examples/battleship.py index 82feab8..f6770c2 100644 --- a/examples/battleship.py +++ b/examples/battleship.py @@ -4,6 +4,7 @@ import grilops import grilops.shapes +from grilops import Point, Vector SYM = grilops.SymbolSet([ @@ -26,20 +27,20 @@ def main(): """Battleship solver example.""" - sg = grilops.SymbolGrid(HEIGHT, WIDTH, SYM) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, SYM) sc = grilops.shapes.ShapeConstrainer( - HEIGHT, - WIDTH, + locations, [ - [(0, i) for i in range(4)], - [(0, i) for i in range(3)], - [(0, i) for i in range(3)], - [(0, i) for i in range(2)], - [(0, i) for i in range(2)], - [(0, i) for i in range(2)], - [(0, i) for i in range(1)], - [(0, i) for i in range(1)], - [(0, i) for i in range(1)], + [Vector(0, i) for i in range(4)], + [Vector(0, i) for i in range(3)], + [Vector(0, i) for i in range(3)], + [Vector(0, i) for i in range(2)], + [Vector(0, i) for i in range(2)], + [Vector(0, i) for i in range(2)], + [Vector(0, i) for i in range(1)], + [Vector(0, i) for i in range(1)], + [Vector(0, i) for i in range(1)], ], solver=sg.solver, allow_rotations=True @@ -48,29 +49,30 @@ def main(): # Constrain the given ship segment counts and ship segments. for y, count in enumerate(GIVENS_Y): sg.solver.add( - PbEq([(Not(sg.cell_is(y, x, SYM.X)), 1) for x in range(WIDTH)], count) + PbEq([(Not(sg.cell_is(Point(y, x), SYM.X)), 1) for x in range(WIDTH)], count) ) for x, count in enumerate(GIVENS_X): sg.solver.add( - PbEq([(Not(sg.cell_is(y, x, SYM.X)), 1) for y in range(HEIGHT)], count) + PbEq([(Not(sg.cell_is(Point(y, x), SYM.X)), 1) for y in range(HEIGHT)], count) ) for (y, x), s in GIVENS.items(): - sg.solver.add(sg.cell_is(y, x, s)) + sg.solver.add(sg.cell_is(Point(y, x), s)) for y in range(HEIGHT): for x in range(WIDTH): - shape_type = sc.shape_type_grid[y][x] - shape_id = sc.shape_instance_grid[y][x] + p = Point(y, x) + shape_type = sc.shape_type_grid[p] + shape_id = sc.shape_instance_grid[p] touching_types = [ - n.symbol for n in grilops.touching_cells(sc.shape_type_grid, y, x) + n.symbol for n in grilops.touching_cells(sc.shape_type_grid, p) ] touching_ids = [ - n.symbol for n in grilops.touching_cells(sc.shape_instance_grid, y, x) + n.symbol for n in grilops.touching_cells(sc.shape_instance_grid, p) ] # Link the X symbol to the absence of a ship segment. sg.solver.add( - (sc.shape_type_grid[y][x] == -1) == sg.cell_is(y, x, SYM.X)) + (sc.shape_type_grid[p] == -1) == sg.cell_is(p, SYM.X)) # Ship segments of different ships may not touch. and_terms = [] @@ -88,13 +90,13 @@ def main(): sg.solver.add( Implies( And(shape_type >= 0, PbEq(touching_count_terms, 2)), - sg.cell_is(y, x, SYM.B) + sg.cell_is(p, SYM.B) ) ) sg.solver.add( Implies( And(shape_type >= 0, PbEq(touching_count_terms, 0)), - sg.cell_is(y, x, SYM.O) + sg.cell_is(p, SYM.O) ) ) if y > 0: @@ -103,9 +105,9 @@ def main(): And( shape_type >= 0, PbEq(touching_count_terms, 1), - sc.shape_type_grid[y - 1][x] == shape_type + sc.shape_type_grid[Point(y - 1, x)] == shape_type ), - sg.cell_is(y, x, SYM.S) + sg.cell_is(p, SYM.S) ) ) if y < HEIGHT - 1: @@ -114,9 +116,9 @@ def main(): And( shape_type >= 0, PbEq(touching_count_terms, 1), - sc.shape_type_grid[y + 1][x] == shape_type + sc.shape_type_grid[Point(y + 1, x)] == shape_type ), - sg.cell_is(y, x, SYM.N) + sg.cell_is(p, SYM.N) ) ) if x > 0: @@ -125,9 +127,9 @@ def main(): And( shape_type >= 0, PbEq(touching_count_terms, 1), - sc.shape_type_grid[y][x - 1] == shape_type + sc.shape_type_grid[Point(y, x - 1)] == shape_type ), - sg.cell_is(y, x, SYM.E) + sg.cell_is(p, SYM.E) ) ) if x < WIDTH - 1: @@ -136,9 +138,9 @@ def main(): And( shape_type >= 0, PbEq(touching_count_terms, 1), - sc.shape_type_grid[y][x + 1] == shape_type + sc.shape_type_grid[Point(y, x + 1)] == shape_type ), - sg.cell_is(y, x, SYM.W) + sg.cell_is(p, SYM.W) ) ) diff --git a/examples/castle_wall.py b/examples/castle_wall.py index ae22662..c29a2aa 100644 --- a/examples/castle_wall.py +++ b/examples/castle_wall.py @@ -9,6 +9,7 @@ import grilops from grilops.loops import I, O, LoopSymbolSet, LoopConstrainer import grilops.sightlines +from grilops import Point, Vector HEIGHT, WIDTH = 7, 7 @@ -41,28 +42,31 @@ def main(): """Castle Wall solver example.""" - sg = grilops.SymbolGrid(HEIGHT, WIDTH, SYM) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, SYM) lc = LoopConstrainer(sg, single_loop=True) for (y, x), (io, expected_count, direction) in GIVENS.items(): + p = Point(y, x) # Constrain whether the given cell is inside or outside of the loop. This # also prevents these cells from containing loop symbols themselves. - sg.solver.add(lc.inside_outside_grid[y][x] == io) + sg.solver.add(lc.inside_outside_grid[p] == io) if expected_count is not None and direction is not None: # Count and constrain the number of loop segments in the given direction. segment_symbols = DIRECTION_SEGMENT_SYMBOLS[direction] + dy, dx = direction actual_count = grilops.sightlines.count_cells( - sg, (y, x), direction, + sg, p, Vector(dy, dx), lambda c: If(Or(*[c == s for s in segment_symbols]), 1, 0) ) sg.solver.add(actual_count == expected_count) - def show_cell(y, x, _): - if (y, x) in GIVENS: - if GIVENS[(y, x)][0] == I: + def show_cell(p, _): + if (p.y, p.x) in GIVENS: + if GIVENS[(p.y, p.x)][0] == I: return chr(0x25AB) - if GIVENS[(y, x)][0] == O: + if GIVENS[(p.y, p.x)][0] == O: return chr(0x25AA) return None diff --git a/examples/cave.py b/examples/cave.py index 1c09082..e69b20a 100644 --- a/examples/cave.py +++ b/examples/cave.py @@ -9,6 +9,7 @@ import grilops import grilops.regions import grilops.sightlines +from grilops import Point SYM = grilops.SymbolSet([("B", chr(0x2588)), ("W", " ")]) @@ -29,8 +30,9 @@ def main(): """Cave solver example.""" - sg = grilops.SymbolGrid(HEIGHT, WIDTH, SYM) - rc = grilops.regions.RegionConstrainer(HEIGHT, WIDTH, solver=sg.solver) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, SYM) + rc = grilops.regions.RegionConstrainer(locations, solver=sg.solver) # The cave must be a single connected group. We'll define a variable to keep # track of its region ID. @@ -38,10 +40,11 @@ def main(): for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) # Ensure that every cave cell has the same region ID. sg.solver.add( - sg.cell_is(y, x, SYM.W) == - (rc.region_id_grid[y][x] == cave_region_id) + sg.cell_is(p, SYM.W) == + (rc.region_id_grid[p] == cave_region_id) ) # Every shaded region must connect to an edge of the grid. We'll enforce @@ -50,8 +53,8 @@ def main(): if 0 < y < HEIGHT - 1 and 0 < x < WIDTH - 1: sg.solver.add( Implies( - sg.cell_is(y, x, SYM.B), - rc.parent_grid[y][x] != grilops.regions.R + sg.cell_is(p, SYM.B), + rc.parent_grid[p] != grilops.regions.R ) ) @@ -59,17 +62,18 @@ def main(): for x in range(WIDTH): if GIVENS[y][x] == 0: continue - sg.solver.add(sg.cell_is(y, x, SYM.W)) + p = Point(y, x) + sg.solver.add(sg.cell_is(p, SYM.W)) # Count the cells visible along sightlines from the given cell. visible_cell_count = 1 + sum( grilops.sightlines.count_cells( sg, n.location, n.direction, stop=lambda c: c == SYM.B - ) for n in sg.adjacent_cells(y, x) + ) for n in sg.adjacent_cells(p) ) sg.solver.add(visible_cell_count == GIVENS[y][x]) def print_grid(): - sg.print(lambda y, x, _: str(GIVENS[y][x]) if GIVENS[y][x] != 0 else None) + sg.print(lambda p, _: str(GIVENS[p.y][p.x]) if GIVENS[p.y][p.x] != 0 else None) if sg.solve(): print_grid() diff --git a/examples/fillomino.py b/examples/fillomino.py index 5248044..9c74768 100644 --- a/examples/fillomino.py +++ b/examples/fillomino.py @@ -7,6 +7,7 @@ import grilops import grilops.regions +from grilops import Point def main(): @@ -24,35 +25,37 @@ def main(): ] sym = grilops.make_number_range_symbol_set(1, 10) - sg = grilops.SymbolGrid(len(givens), len(givens[0]), sym) + locations = grilops.get_rectangle_locations(len(givens), len(givens[0])) + sg = grilops.SymbolGrid(locations, sym) rc = grilops.regions.RegionConstrainer( - len(givens), - len(givens[0]), + locations, solver=sg.solver ) for y in range(len(givens)): for x in range(len(givens[0])): + p = Point(y, x) + # The filled number must match the size of the region. - sg.solver.add(sg.grid[y][x] == rc.region_size_grid[y][x]) + sg.solver.add(sg.grid[p] == rc.region_size_grid[p]) # The size of the region must match the clue. given = givens[y][x] if given != 0: - sg.solver.add(rc.region_size_grid[y][x] == given) + sg.solver.add(rc.region_size_grid[p] == given) # Different regions of the same size may not be orthogonally adjacent. region_sizes = [ - n.symbol for n in grilops.adjacent_cells(rc.region_size_grid, y, x) + n.symbol for n in grilops.adjacent_cells(rc.region_size_grid, p) ] region_ids = [ - n.symbol for n in grilops.adjacent_cells(rc.region_id_grid, y, x) + n.symbol for n in grilops.adjacent_cells(rc.region_id_grid, p) ] for region_size, region_id in zip(region_sizes, region_ids): sg.solver.add( Implies( - rc.region_size_grid[y][x] == region_size, - rc.region_id_grid[y][x] == region_id + rc.region_size_grid[p] == region_size, + rc.region_id_grid[p] == region_id ) ) diff --git a/examples/gokigen_naname.py b/examples/gokigen_naname.py index d49fb05..0dea6fa 100644 --- a/examples/gokigen_naname.py +++ b/examples/gokigen_naname.py @@ -7,6 +7,7 @@ from z3 import And, BitVec, BitVecVal, If, PbEq import grilops +from grilops import Point HEIGHT = 10 @@ -97,31 +98,31 @@ def add_loop_constraints(sym, sg): or_terms = [] if y - 1 >= 0 and x - 1 >= 0: or_terms.append(If( - And(sg.cell_is(y, x, sym.B), sg.cell_is(y - 1, x - 1, sym.B)), + And(sg.cell_is(Point(y, x), sym.B), sg.cell_is(Point(y - 1, x - 1), sym.B)), north_net_grid[y - 1][x - 1] | location_to_bitvec(y - 1, x - 1), 0 )) if y - 1 >= 0: or_terms.append(If( - sg.grid[y][x] != sg.grid[y - 1][x], + sg.grid[Point(y, x)] != sg.grid[Point(y - 1, x)], north_net_grid[y - 1][x] | location_to_bitvec(y - 1, x), 0 )) if y - 1 >= 0 and x + 1 < WIDTH: or_terms.append(If( - And(sg.cell_is(y, x, sym.F), sg.cell_is(y - 1, x + 1, sym.F)), + And(sg.cell_is(Point(y, x), sym.F), sg.cell_is(Point(y - 1, x + 1), sym.F)), north_net_grid[y - 1][x + 1] | location_to_bitvec(y - 1, x + 1), 0 )) if x - 1 >= 0: or_terms.append(If( - And(sg.cell_is(y, x, sym.B), sg.cell_is(y, x - 1, sym.F)), + And(sg.cell_is(Point(y, x), sym.B), sg.cell_is(Point(y, x - 1), sym.F)), south_net_grid[y][x - 1] | location_to_bitvec(y, x - 1), 0 )) if x + 1 < WIDTH: or_terms.append(If( - And(sg.cell_is(y, x, sym.F), sg.cell_is(y, x + 1, sym.B)), + And(sg.cell_is(Point(y, x), sym.F), sg.cell_is(Point(y, x + 1), sym.B)), south_net_grid[y][x + 1] | location_to_bitvec(y, x + 1), 0 )) @@ -132,31 +133,31 @@ def add_loop_constraints(sym, sg): or_terms = [] if x - 1 >= 0: or_terms.append(If( - And(sg.cell_is(y, x, sym.F), sg.cell_is(y, x - 1, sym.B)), + And(sg.cell_is(Point(y, x), sym.F), sg.cell_is(Point(y, x - 1), sym.B)), north_net_grid[y][x - 1] | location_to_bitvec(y, x - 1), 0 )) if x + 1 < WIDTH: or_terms.append(If( - And(sg.cell_is(y, x, sym.B), sg.cell_is(y, x + 1, sym.F)), + And(sg.cell_is(Point(y, x), sym.B), sg.cell_is(Point(y, x + 1), sym.F)), north_net_grid[y][x + 1] | location_to_bitvec(y, x + 1), 0 )) if y + 1 < HEIGHT and x - 1 >= 0: or_terms.append(If( - And(sg.cell_is(y, x, sym.F), sg.cell_is(y + 1, x - 1, sym.F)), + And(sg.cell_is(Point(y, x), sym.F), sg.cell_is(Point(y + 1, x - 1), sym.F)), south_net_grid[y + 1][x - 1] | location_to_bitvec(y + 1, x - 1), 0 )) if y + 1 < HEIGHT: or_terms.append(If( - sg.grid[y][x] != sg.grid[y + 1][x], + sg.grid[Point(y, x)] != sg.grid[Point(y + 1, x)], south_net_grid[y + 1][x] | location_to_bitvec(y + 1, x), 0 )) if y + 1 < HEIGHT and x + 1 < WIDTH: or_terms.append(If( - And(sg.cell_is(y, x, sym.B), sg.cell_is(y + 1, x + 1, sym.B)), + And(sg.cell_is(Point(y, x), sym.B), sg.cell_is(Point(y + 1, x + 1), sym.B)), south_net_grid[y + 1][x + 1] | location_to_bitvec(y + 1, x + 1), 0 )) @@ -166,21 +167,22 @@ def add_loop_constraints(sym, sg): def main(): """Gokigen Naname solver example.""" sym = grilops.SymbolSet([("F", chr(0x2571)), ("B", chr(0x2572))]) - sg = grilops.SymbolGrid(HEIGHT, WIDTH, sym) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, sym) # Ensure the given number of line segment constraints are met. for (y, x), v in GIVENS.items(): terms = [] if y > 0: if x > 0: - terms.append(sg.cell_is(y - 1, x - 1, sym.B)) + terms.append(sg.cell_is(Point(y - 1, x - 1), sym.B)) if x < WIDTH: - terms.append(sg.cell_is(y - 1, x, sym.F)) + terms.append(sg.cell_is(Point(y - 1, x), sym.F)) if y < HEIGHT: if x > 0: - terms.append(sg.cell_is(y, x - 1, sym.F)) + terms.append(sg.cell_is(Point(y, x - 1), sym.F)) if x < WIDTH: - terms.append(sg.cell_is(y, x, sym.B)) + terms.append(sg.cell_is(Point(y, x), sym.B)) sg.solver.add(PbEq([(term, 1) for term in terms], v)) add_loop_constraints(sym, sg) diff --git a/examples/greater_than_killer_sudoku.py b/examples/greater_than_killer_sudoku.py index 491f82b..c682099 100644 --- a/examples/greater_than_killer_sudoku.py +++ b/examples/greater_than_killer_sudoku.py @@ -8,18 +8,19 @@ from z3 import Distinct, Sum import grilops +from grilops import Point def add_sudoku_constraints(sg): """Add constraints for the normal Sudoku rules.""" for y in range(9): - sg.solver.add(Distinct(*sg.grid[y])) + sg.solver.add(Distinct(*[sg.grid[Point(y, x)] for x in range(9)])) for x in range(9): - sg.solver.add(Distinct(*[r[x] for r in sg.grid])) + sg.solver.add(Distinct(*[sg.grid[Point(y, x)] for y in range(9)])) for z in range(9): top = (z // 3) * 3 left = (z % 3) * 3 - cells = [r[x] for r in sg.grid[top:top + 3] for x in range(left, left + 3)] + cells = [sg.grid[Point(y, x)] for y in range(top, top + 3) for x in range(left, left + 3)] sg.solver.add(Distinct(*cells)) @@ -61,7 +62,8 @@ def main(): } sym = grilops.make_number_range_symbol_set(1, 9) - sg = grilops.SymbolGrid(9, 9, sym) + locations = grilops.get_square_locations(9) + sg = grilops.SymbolGrid(locations, sym) add_sudoku_constraints(sg) @@ -69,7 +71,7 @@ def main(): cage_cells = defaultdict(list) for y in range(9): for x in range(9): - cage_cells[cages[y][x]].append(sg.grid[y][x]) + cage_cells[cages[y][x]].append(sg.grid[Point(y, x)]) # The digits used in each cage must be unique. for cells_in_cage in cage_cells.values(): diff --git a/examples/halloween_valentines.py b/examples/halloween_valentines.py index 224ff55..0ee8169 100644 --- a/examples/halloween_valentines.py +++ b/examples/halloween_valentines.py @@ -8,6 +8,7 @@ import grilops import grilops.loops +from grilops import Point ANSWERS = [ @@ -30,35 +31,37 @@ def extract_answer(sg, loop_order_grid): loop_order_to_yx = {} for y in range(8): for x in range(8): - loop_order_to_yx[model.eval(loop_order_grid[y][x]).as_long()] = (y, x) + loop_order_to_yx[model.eval(loop_order_grid[Point(y, x)]).as_long()] = (y, x) ordered_yx = sorted(list(loop_order_to_yx.items())) solved_grid = sg.solved_grid() answer = "" for _, (y, x) in ordered_yx: - if solved_grid[y][x] in TURN_SYMBOLS and ANSWERS[y][x] != "O": + if solved_grid[Point(y, x)] in TURN_SYMBOLS and ANSWERS[y][x] != "O": answer += ANSWERS[y][x] return answer def main(): """Halloween Town / Valentine's Day Town solver.""" - sg = grilops.SymbolGrid(8, 8, SYM) + locations = grilops.get_square_locations(8) + sg = grilops.SymbolGrid(locations, SYM) lc = grilops.loops.LoopConstrainer(sg, single_loop=True) # Cheat a little bit and force the loop order to start such that the answer # extraction starts at the correct place and proceeds in the correct order. - sg.solver.add(lc.loop_order_grid[5][6] == 0) - sg.solver.add(lc.loop_order_grid[5][5] == 1) + sg.solver.add(lc.loop_order_grid[Point(5, 6)] == 0) + sg.solver.add(lc.loop_order_grid[Point(5, 5)] == 1) turn_count_terms = [] o_count = 0 for y in range(8): for x in range(8): - turn_count_terms.append(If(sg.cell_is_one_of(y, x, TURN_SYMBOLS), 1, 0)) + p = Point(y, x) + turn_count_terms.append(If(sg.cell_is_one_of(p, TURN_SYMBOLS), 1, 0)) if ANSWERS[y][x] == "O": o_count += 1 # Every O must be a turn. - sg.solver.add(sg.cell_is_one_of(y, x, TURN_SYMBOLS)) + sg.solver.add(sg.cell_is_one_of(p, TURN_SYMBOLS)) # There will be exactly twice as many turns as Os. sg.solver.add(Sum(*turn_count_terms) == o_count * 2) diff --git a/examples/heteromino.py b/examples/heteromino.py index 0201131..caaf35b 100644 --- a/examples/heteromino.py +++ b/examples/heteromino.py @@ -8,6 +8,7 @@ import grilops import grilops.regions +from grilops import Point def main(): @@ -29,70 +30,72 @@ def main(): ("SW", chr(0x25FA)), ("NW", chr(0x25F8)), ]) - sg = grilops.SymbolGrid(size, size, sym) + locations = grilops.get_square_locations(size) + sg = grilops.SymbolGrid(locations, sym) rc = grilops.regions.RegionConstrainer( - size, size, solver=sg.solver, complete=False) + locations, solver=sg.solver, complete=False) for y in range(size): for x in range(size): + p = Point(y, x) if (y, x) in black_cells: - sg.solver.add(sg.cell_is(y, x, sym.BL)) + sg.solver.add(sg.cell_is(p, sym.BL)) # Black cells are not part of a region. - sg.solver.add(rc.region_id_grid[y][x] == -1) + sg.solver.add(rc.region_id_grid[p] == -1) else: - sg.solver.add(Not(sg.cell_is(y, x, sym.BL))) + sg.solver.add(Not(sg.cell_is(p, sym.BL))) # All regions have size 3. - sg.solver.add(rc.region_size_grid[y][x] == 3) + sg.solver.add(rc.region_size_grid[p] == 3) # Force the root of each region subtree to be in the middle of the # region, by not allowing non-root cells to have children. sg.solver.add(Implies( - rc.parent_grid[y][x] != grilops.regions.R, - rc.subtree_size_grid[y][x] == 1 + rc.parent_grid[p] != grilops.regions.R, + rc.subtree_size_grid[p] == 1 )) # All cells in the same region must have the same shape symbol. Cells in # different regions must not have the same shape symbol. - shape = sg.grid[y][x] - is_root = rc.parent_grid[y][x] == grilops.regions.R + shape = sg.grid[p] + is_root = rc.parent_grid[p] == grilops.regions.R has_north = False if y > 0: - has_north = rc.parent_grid[y - 1][x] == grilops.regions.S - sg.solver.add(Implies(And(is_root, has_north), sg.grid[y - 1][x] == shape)) + has_north = rc.parent_grid[Point(y - 1, x)] == grilops.regions.S + sg.solver.add(Implies(And(is_root, has_north), sg.grid[Point(y - 1, x)] == shape)) sg.solver.add(Implies( - rc.region_id_grid[y][x] != rc.region_id_grid[y - 1][x], - sg.grid[y - 1][x] != shape + rc.region_id_grid[Point(y, x)] != rc.region_id_grid[Point(y - 1, x)], + sg.grid[Point(y - 1, x)] != shape )) has_south = False if y < size - 1: - has_south = rc.parent_grid[y + 1][x] == grilops.regions.N - sg.solver.add(Implies(And(is_root, has_south), sg.grid[y + 1][x] == shape)) + has_south = rc.parent_grid[Point(y + 1, x)] == grilops.regions.N + sg.solver.add(Implies(And(is_root, has_south), sg.grid[Point(y + 1, x)] == shape)) sg.solver.add(Implies( - rc.region_id_grid[y][x] != rc.region_id_grid[y + 1][x], - sg.grid[y + 1][x] != shape + rc.region_id_grid[Point(y, x)] != rc.region_id_grid[Point(y + 1, x)], + sg.grid[Point(y + 1, x)] != shape )) has_west = False if x > 0: - has_west = rc.parent_grid[y][x - 1] == grilops.regions.E - sg.solver.add(Implies(And(is_root, has_west), sg.grid[y][x - 1] == shape)) + has_west = rc.parent_grid[Point(y, x - 1)] == grilops.regions.E + sg.solver.add(Implies(And(is_root, has_west), sg.grid[Point(y, x - 1)] == shape)) sg.solver.add(Implies( - rc.region_id_grid[y][x] != rc.region_id_grid[y][x - 1], - sg.grid[y][x - 1] != shape + rc.region_id_grid[Point(y, x)] != rc.region_id_grid[Point(y, x - 1)], + sg.grid[Point(y, x - 1)] != shape )) has_east = False if x < size - 1: - has_east = rc.parent_grid[y][x + 1] == grilops.regions.W - sg.solver.add(Implies(And(is_root, has_east), sg.grid[y][x + 1] == shape)) + has_east = rc.parent_grid[Point(y, x + 1)] == grilops.regions.W + sg.solver.add(Implies(And(is_root, has_east), sg.grid[Point(y, x + 1)] == shape)) sg.solver.add(Implies( - rc.region_id_grid[y][x] != rc.region_id_grid[y][x + 1], - sg.grid[y][x + 1] != shape + rc.region_id_grid[Point(y, x)] != rc.region_id_grid[Point(y, x + 1)], + sg.grid[Point(y, x + 1)] != shape )) # Constrain the shape symbol based on adjacent cell relationships. diff --git a/examples/kuromasu.py b/examples/kuromasu.py index 9946e83..6c843d5 100644 --- a/examples/kuromasu.py +++ b/examples/kuromasu.py @@ -8,6 +8,7 @@ import grilops import grilops.regions import grilops.sightlines +from grilops import Point HEIGHT, WIDTH = 11, 11 @@ -36,13 +37,15 @@ def main(): """Kuromasu solver example.""" sym = grilops.SymbolSet([("B", chr(0x2588) * 2), ("W", " ")]) - sg = grilops.SymbolGrid(HEIGHT, WIDTH, sym) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, sym) rc = grilops.regions.RegionConstrainer( - HEIGHT, WIDTH, solver=sg.solver, complete=False) + locations, solver=sg.solver, complete=False) for (y, x), c in GIVENS.items(): + p = Point(y, x) # Numbered cells may not be black. - sg.solver.add(sg.cell_is(y, x, sym.W)) + sg.solver.add(sg.cell_is(p, sym.W)) # Each number on the board represents the number of white cells that can be # seen from that cell, including itself. A cell can be seen from another @@ -51,7 +54,7 @@ def main(): visible_cell_count = 1 + sum( grilops.sightlines.count_cells( sg, n.location, n.direction, stop=lambda c: c == sym.B - ) for n in sg.adjacent_cells(y, x) + ) for n in sg.adjacent_cells(p) ) sg.solver.add(visible_cell_count == c) @@ -64,11 +67,13 @@ def main(): for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) + # No two black cells may be horizontally or vertically adjacent. sg.solver.add( Implies( - sg.cell_is(y, x, sym.B), - And(*[n.symbol == sym.W for n in sg.adjacent_cells(y, x)]) + sg.cell_is(p, sym.B), + And(*[n.symbol == sym.W for n in sg.adjacent_cells(p)]) ) ) @@ -76,15 +81,15 @@ def main(): # be part of a region. sg.solver.add( If( - sg.cell_is(y, x, sym.W), - rc.region_id_grid[y][x] == white_region_id, - rc.region_id_grid[y][x] == -1 + sg.cell_is(p, sym.W), + rc.region_id_grid[p] == white_region_id, + rc.region_id_grid[p] == -1 ) ) def print_grid(): sg.print( - lambda y, x, _: f"{GIVENS[(y, x)]:02}" if (y, x) in GIVENS else None) + lambda p, _: f"{GIVENS[(p.y, p.x)]:02}" if (p.y, p.x) in GIVENS else None) if sg.solve(): print_grid() diff --git a/examples/lits.py b/examples/lits.py index efc24aa..7e5e4cd 100644 --- a/examples/lits.py +++ b/examples/lits.py @@ -8,6 +8,7 @@ import grilops import grilops.regions import grilops.shapes +from grilops import Point, Vector HEIGHT, WIDTH = 10, 10 @@ -29,11 +30,12 @@ def link_symbols_to_shapes(sym, sg, sc): """Add constraints to ensure the symbols match the shapes.""" for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) sg.solver.add( If( - sc.shape_type_grid[y][x] != -1, - sg.cell_is(y, x, sc.shape_type_grid[y][x]), - sg.cell_is(y, x, sym.W) + sc.shape_type_grid[p] != -1, + sg.cell_is(p, sc.shape_type_grid[p]), + sg.cell_is(p, sym.W) ) ) @@ -46,8 +48,9 @@ def add_area_constraints(sc): for y in range(HEIGHT): for x in range(WIDTH): if AREAS[y][x] == area_label: - area_type_cells.append(sc.shape_type_grid[y][x]) - area_instance_cells.append(sc.shape_instance_grid[y][x]) + p = Point(y, x) + area_type_cells.append(sc.shape_type_grid[p]) + area_instance_cells.append(sc.shape_instance_grid[p]) area_type = Int(f"at-{area_label}") sc.solver.add(area_type >= 0) @@ -71,20 +74,21 @@ def add_nurikabe_constraints(sym, sg, rc): sg.solver.add(sea_id < HEIGHT * WIDTH) for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) sg.solver.add(Implies( - Not(sg.cell_is(y, x, sym.W)), - rc.region_id_grid[y][x] == sea_id + Not(sg.cell_is(p, sym.W)), + rc.region_id_grid[p] == sea_id )) sg.solver.add(Implies( - sg.cell_is(y, x, sym.W), - rc.region_id_grid[y][x] != sea_id + sg.cell_is(p, sym.W), + rc.region_id_grid[p] != sea_id )) # The sea is not allowed to contain 2x2 areas of black cells. for sy in range(HEIGHT - 1): for sx in range(WIDTH - 1): pool_cells = [ - sg.grid[y][x] for y in range(sy, sy + 2) for x in range(sx, sx + 2) + sg.grid[Point(y, x)] for y in range(sy, sy + 2) for x in range(sx, sx + 2) ] sg.solver.add(Not(And(*[Not(cell == sym.W) for cell in pool_cells]))) @@ -93,13 +97,14 @@ def add_adjacent_tetronimo_constraints(sc): """Ensure that no two matching tetrominoes are orthogonally adjacent.""" for y in range(HEIGHT): for x in range(WIDTH): - shape_type = sc.shape_type_grid[y][x] - shape_id = sc.shape_instance_grid[y][x] + p = Point(y, x) + shape_type = sc.shape_type_grid[p] + shape_id = sc.shape_instance_grid[p] adjacent_types = [ - n.symbol for n in grilops.adjacent_cells(sc.shape_type_grid, y, x) + n.symbol for n in grilops.adjacent_cells(sc.shape_type_grid, p) ] adjacent_ids = [ - n.symbol for n in grilops.adjacent_cells(sc.shape_instance_grid, y, x) + n.symbol for n in grilops.adjacent_cells(sc.shape_instance_grid, p) ] for adjacent_type, adjacent_id in zip(adjacent_types, adjacent_ids): sc.solver.add( @@ -117,16 +122,16 @@ def add_adjacent_tetronimo_constraints(sc): def main(): """LITS solver example.""" sym = grilops.SymbolSet(["L", "I", "T", "S", ("W", " ")]) - sg = grilops.SymbolGrid(HEIGHT, WIDTH, sym) - rc = grilops.regions.RegionConstrainer(HEIGHT, WIDTH, solver=sg.solver) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, sym) + rc = grilops.regions.RegionConstrainer(locations, solver=sg.solver) sc = grilops.shapes.ShapeConstrainer( - HEIGHT, - WIDTH, + locations, [ - [(0, 0), (1, 0), (2, 0), (2, 1)], # L - [(0, 0), (1, 0), (2, 0), (3, 0)], # I - [(0, 0), (0, 1), (0, 2), (1, 1)], # T - [(0, 0), (1, 0), (1, 1), (2, 1)], # S + [Vector(0, 0), Vector(1, 0), Vector(2, 0), Vector(2, 1)], # L + [Vector(0, 0), Vector(1, 0), Vector(2, 0), Vector(3, 0)], # I + [Vector(0, 0), Vector(0, 1), Vector(0, 2), Vector(1, 1)], # T + [Vector(0, 0), Vector(1, 0), Vector(1, 1), Vector(2, 1)], # S ], solver=sg.solver, allow_rotations=True, diff --git a/examples/masyu.py b/examples/masyu.py index 47fc12f..d46b754 100644 --- a/examples/masyu.py +++ b/examples/masyu.py @@ -8,6 +8,7 @@ import grilops import grilops.loops +from grilops import Point def main(): @@ -33,7 +34,8 @@ def main(): sym = grilops.loops.LoopSymbolSet() sym.append("EMPTY", " ") - sg = grilops.SymbolGrid(10, 10, sym) + locations = grilops.get_rectangle_locations(len(givens), len(givens[0])) + sg = grilops.SymbolGrid(locations, sym) grilops.loops.LoopConstrainer(sg, single_loop=True) straights = [sym.NS, sym.EW] @@ -41,51 +43,52 @@ def main(): for y in range(len(givens)): for x in range(len(givens[0])): + p = Point(y, x) if givens[y][x] == b: # The loop must turn at a black circle. - sg.solver.add(sg.cell_is_one_of(y, x, turns)) + sg.solver.add(sg.cell_is_one_of(p, turns)) # All connected adjacent cells must contain straight loop segments. if y > 0: sg.solver.add(Implies( - sg.cell_is_one_of(y, x, [sym.NE, sym.NW]), - sg.cell_is(y - 1, x, sym.NS) + sg.cell_is_one_of(p, [sym.NE, sym.NW]), + sg.cell_is(Point(y - 1, x), sym.NS) )) - if y < len(sg.grid) - 1: + if y < len(givens) - 1: sg.solver.add(Implies( - sg.cell_is_one_of(y, x, [sym.SE, sym.SW]), - sg.cell_is(y + 1, x, sym.NS) + sg.cell_is_one_of(p, [sym.SE, sym.SW]), + sg.cell_is(Point(y + 1, x), sym.NS) )) if x > 0: sg.solver.add(Implies( - sg.cell_is_one_of(y, x, [sym.SW, sym.NW]), - sg.cell_is(y, x - 1, sym.EW) + sg.cell_is_one_of(p, [sym.SW, sym.NW]), + sg.cell_is(Point(y, x - 1), sym.EW) )) - if x < len(sg.grid[0]) - 1: + if x < len(givens[0]) - 1: sg.solver.add(Implies( - sg.cell_is_one_of(y, x, [sym.NE, sym.SE]), - sg.cell_is(y, x + 1, sym.EW) + sg.cell_is_one_of(p, [sym.NE, sym.SE]), + sg.cell_is(Point(y, x + 1), sym.EW) )) elif givens[y][x] == w: # The loop must go straight through a white circle. - sg.solver.add(sg.cell_is_one_of(y, x, straights)) + sg.solver.add(sg.cell_is_one_of(p, straights)) # At least one connected adjacent cell must turn. - if 0 < y < len(sg.grid) - 1: + if 0 < y < len(givens) - 1: sg.solver.add(Implies( - sg.cell_is(y, x, sym.NS), + sg.cell_is(p, sym.NS), Or( - sg.cell_is_one_of(y - 1, x, turns), - sg.cell_is_one_of(y + 1, x, turns) + sg.cell_is_one_of(Point(y - 1, x), turns), + sg.cell_is_one_of(Point(y + 1, x), turns) ) )) - if 0 < x < len(sg.grid[0]) - 1: + if 0 < x < len(givens[0]) - 1: sg.solver.add(Implies( - sg.cell_is(y, x, sym.EW), + sg.cell_is(p, sym.EW), Or( - sg.cell_is_one_of(y, x - 1, turns), - sg.cell_is_one_of(y, x + 1, turns) + sg.cell_is_one_of(Point(y, x - 1), turns), + sg.cell_is_one_of(Point(y, x + 1), turns) ) )) diff --git a/examples/nanro.py b/examples/nanro.py index 3bb7bae..b613e05 100644 --- a/examples/nanro.py +++ b/examples/nanro.py @@ -9,6 +9,7 @@ import grilops import grilops.regions +from grilops import Point HEIGHT, WIDTH = 8, 8 @@ -38,24 +39,26 @@ def main(): """Nanro solver example.""" - sg = grilops.SymbolGrid(HEIGHT, WIDTH, SYM) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, SYM) rc = grilops.regions.RegionConstrainer( - HEIGHT, WIDTH, solver=sg.solver, complete=False) + locations, solver=sg.solver, complete=False) # Constrain the symbol grid to contain the given labels. for (y, x), l in GIVEN_LABELS.items(): - sg.solver.add(sg.cell_is(y, x, l)) + sg.solver.add(sg.cell_is(Point(y, x), l)) # Use the RegionConstrainer to require a single connected group made up of # only labeled cells. label_region_id = rc.location_to_region_id(min(GIVEN_LABELS.keys())) for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) sg.solver.add( If( - sg.cell_is(y, x, SYM.EMPTY), - rc.region_id_grid[y][x] == -1, - rc.region_id_grid[y][x] == label_region_id + sg.cell_is(p, SYM.EMPTY), + rc.region_id_grid[p] == -1, + rc.region_id_grid[p] == label_region_id ) ) @@ -63,14 +66,14 @@ def main(): for sy in range(HEIGHT - 1): for sx in range(WIDTH - 1): pool_cells = [ - sg.grid[y][x] for y in range(sy, sy + 2) for x in range(sx, sx + 2) + sg.grid[Point(y, x)] for y in range(sy, sy + 2) for x in range(sx, sx + 2) ] sg.solver.add(Or(*[c == SYM.EMPTY for c in pool_cells])) region_cells = defaultdict(list) for y in range(HEIGHT): for x in range(WIDTH): - region_cells[REGIONS[y][x]].append(sg.grid[y][x]) + region_cells[REGIONS[y][x]].append(sg.grid[Point(y, x)]) # Each bold region must contain at least one labeled cell. for cells in region_cells.values(): @@ -87,13 +90,14 @@ def main(): # numbers must be different. for y in range(HEIGHT): for x in range(WIDTH): - for n in sg.adjacent_cells(y, x): - ny, nx = n.location - if REGIONS[y][x] != REGIONS[ny][nx]: + p = Point(y, x) + for n in sg.adjacent_cells(p): + np = n.location + if REGIONS[y][x] != REGIONS[np.y][np.x]: sg.solver.add( Implies( - And(sg.grid[y][x] != SYM.EMPTY, sg.grid[ny][nx] != SYM.EMPTY), - sg.grid[y][x] != sg.grid[ny][nx] + And(sg.grid[p] != SYM.EMPTY, sg.grid[np] != SYM.EMPTY), + sg.grid[p] != sg.grid[np] ) ) diff --git a/examples/numberlink.py b/examples/numberlink.py index 98c5465..74bdc5e 100644 --- a/examples/numberlink.py +++ b/examples/numberlink.py @@ -8,6 +8,7 @@ import grilops import grilops.loops import grilops.regions +from grilops import Point HEIGHT, WIDTH = 7, 7 @@ -34,8 +35,9 @@ def main(): """Numberlink solver example.""" - sg = grilops.SymbolGrid(HEIGHT, WIDTH, SYM) - rc = grilops.regions.RegionConstrainer(HEIGHT, WIDTH, sg.solver) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, SYM) + rc = grilops.regions.RegionConstrainer(locations, sg.solver) numbers = sorted(list(set(GIVENS.values()))) number_regions = {n: Int(f"nr-{n}") for n in numbers} @@ -43,37 +45,38 @@ def main(): def append_or_term(sym, a, a_syms, b, b_syms): or_terms.append(And( - sg.cell_is(y, x, sym), - sg.cell_is_one_of(a[0], a[1], a_syms), - sg.cell_is_one_of(b[0], b[1], b_syms), - rc.region_id_grid[y][x] == rc.region_id_grid[a[0]][a[1]], - rc.region_id_grid[y][x] == rc.region_id_grid[b[0]][b[1]], + sg.cell_is(p, sym), + sg.cell_is_one_of(a, a_syms), + sg.cell_is_one_of(b, b_syms), + rc.region_id_grid[p] == rc.region_id_grid[a], + rc.region_id_grid[p] == rc.region_id_grid[b], )) for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) if (y, x) in GIVENS: n = GIVENS[(y, x)] - sg.solver.add(sg.cell_is(y, x, SYM.TERMINAL)) - sg.solver.add(rc.region_id_grid[y][x] == number_regions[n]) + sg.solver.add(sg.cell_is(p, SYM.TERMINAL)) + sg.solver.add(rc.region_id_grid[p] == number_regions[n]) continue or_terms = [] if 0 < y < HEIGHT - 1: - append_or_term(SYM.NS, (y - 1, x), S_SYMS, (y + 1, x), N_SYMS) + append_or_term(SYM.NS, Point(y - 1, x), S_SYMS, Point(y + 1, x), N_SYMS) if 0 < x < WIDTH - 1: - append_or_term(SYM.EW, (y, x - 1), E_SYMS, (y, x + 1), W_SYMS) + append_or_term(SYM.EW, Point(y, x - 1), E_SYMS, Point(y, x + 1), W_SYMS) if y > 0 and x < WIDTH - 1: - append_or_term(SYM.NE, (y - 1, x), S_SYMS, (y, x + 1), W_SYMS) + append_or_term(SYM.NE, Point(y - 1, x), S_SYMS, Point(y, x + 1), W_SYMS) if y < HEIGHT - 1 and x < WIDTH - 1: - append_or_term(SYM.SE, (y + 1, x), N_SYMS, (y, x + 1), W_SYMS) + append_or_term(SYM.SE, Point(y + 1, x), N_SYMS, Point(y, x + 1), W_SYMS) if y < HEIGHT - 1 and x > 0: - append_or_term(SYM.SW, (y + 1, x), N_SYMS, (y, x - 1), E_SYMS) + append_or_term(SYM.SW, Point(y + 1, x), N_SYMS, Point(y, x - 1), E_SYMS) if y > 0 and x > 0: - append_or_term(SYM.NW, (y - 1, x), S_SYMS, (y, x - 1), E_SYMS) + append_or_term(SYM.NW, Point(y - 1, x), S_SYMS, Point(y, x - 1), E_SYMS) sg.solver.add(Or(*or_terms)) def print_grid(): - sg.print(lambda y, x, _: str(GIVENS[(y, x)]) if (y, x) in GIVENS else None) + sg.print(lambda p, _: str(GIVENS[(p.y, p.x)]) if (p.y, p.x) in GIVENS else None) if sg.solve(): print_grid() diff --git a/examples/nurikabe.py b/examples/nurikabe.py index 1abe1dd..b49eb13 100644 --- a/examples/nurikabe.py +++ b/examples/nurikabe.py @@ -7,7 +7,7 @@ import grilops import grilops.regions - +from grilops import Point HEIGHT, WIDTH = 9, 10 GIVENS = { @@ -36,23 +36,24 @@ def constrain_sea(sym, sg, rc): sg.solver.add(sea_id >= 0) sg.solver.add(sea_id < HEIGHT * WIDTH) for p in GIVENS: - sg.solver.add(sea_id != rc.location_to_region_id(p)) + sg.solver.add(sea_id != rc.location_to_region_id(Point(p[0], p[1]))) for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) sg.solver.add(Implies( - sg.cell_is(y, x, sym.B), - rc.region_id_grid[y][x] == sea_id + sg.cell_is(p, sym.B), + rc.region_id_grid[p] == sea_id )) sg.solver.add(Implies( - sg.cell_is(y, x, sym.W), - rc.region_id_grid[y][x] != sea_id + sg.cell_is(p, sym.W), + rc.region_id_grid[p] != sea_id )) # The sea is not allowed to contain 2x2 areas of black cells. for sy in range(HEIGHT - 1): for sx in range(WIDTH - 1): pool_cells = [ - sg.grid[y][x] for y in range(sy, sy + 2) for x in range(sx, sx + 2) + sg.grid[Point(y, x)] for y in range(sy, sy + 2) for x in range(sx, sx + 2) ] sg.solver.add(Not(And(*[cell == sym.B for cell in pool_cells]))) @@ -63,25 +64,26 @@ def constrain_islands(sym, sg, rc): # cells in that island. Each island must contain exactly one numbered cell. for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) if (y, x) in GIVENS: - sg.solver.add(sg.cell_is(y, x, sym.W)) + sg.solver.add(sg.cell_is(p, sym.W)) # Might as well force the given cell to be the root of the region's tree, # to reduce the number of possibilities. - sg.solver.add(rc.parent_grid[y][x] == grilops.regions.R) - sg.solver.add(rc.region_size_grid[y][x] == GIVENS[(y, x)]) + sg.solver.add(rc.parent_grid[p] == grilops.regions.R) + sg.solver.add(rc.region_size_grid[p] == GIVENS[(y, x)]) else: # Ensure that cells that are part of island regions are colored white. for gp in GIVENS: - island_id = rc.location_to_region_id(gp) + island_id = rc.location_to_region_id(Point(gp[0], gp[1])) sg.solver.add(Implies( - rc.region_id_grid[y][x] == island_id, - sg.cell_is(y, x, sym.W) + rc.region_id_grid[p] == island_id, + sg.cell_is(p, sym.W) )) # Force a non-given white cell to not be the root of the region's tree, # to reduce the number of possibilities. sg.solver.add(Implies( - sg.cell_is(y, x, sym.W), - rc.parent_grid[y][x] != grilops.regions.R + sg.cell_is(p, sym.W), + rc.parent_grid[p] != grilops.regions.R )) @@ -89,15 +91,16 @@ def constrain_adjacent_cells(sg, rc): """Different regions of the same color may not be orthogonally adjacent.""" for y in range(HEIGHT): for x in range(WIDTH): - adjacent_cells = [n.symbol for n in sg.adjacent_cells(y, x)] + p = Point(y, x) + adjacent_cells = [n.symbol for n in sg.adjacent_cells(p)] adjacent_region_ids = [ - n.symbol for n in grilops.adjacent_cells(rc.region_id_grid, y, x) + n.symbol for n in grilops.adjacent_cells(rc.region_id_grid, p) ] for cell, region_id in zip(adjacent_cells, adjacent_region_ids): sg.solver.add( Implies( - sg.grid[y][x] == cell, - rc.region_id_grid[y][x] == region_id + sg.grid[p] == cell, + rc.region_id_grid[p] == region_id ) ) @@ -105,15 +108,16 @@ def constrain_adjacent_cells(sg, rc): def main(): """Nurikabe solver example.""" sym = grilops.SymbolSet([("B", chr(0x2588)), ("W", " ")]) - sg = grilops.SymbolGrid(HEIGHT, WIDTH, sym) - rc = grilops.regions.RegionConstrainer(HEIGHT, WIDTH, solver=sg.solver) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, sym) + rc = grilops.regions.RegionConstrainer(locations, solver=sg.solver) constrain_sea(sym, sg, rc) constrain_islands(sym, sg, rc) constrain_adjacent_cells(sg, rc) def print_grid(): - sg.print(lambda y, x, _: str(GIVENS[(y, x)]) if (y, x) in GIVENS else None) + sg.print(lambda p, _: str(GIVENS[(p.y, p.x)]) if (p.y, p.x) in GIVENS else None) if sg.solve(): print_grid() diff --git a/examples/shape.py b/examples/shape.py new file mode 100644 index 0000000..e58faad --- /dev/null +++ b/examples/shape.py @@ -0,0 +1,72 @@ +"""Shape solver example. + +Example puzzle can be found at +https://www.gmpuzzles.com/blog/category/regiondivision/otherregdiv/ +in the instructions for the SSS (Sundoku Snake Shape) puzzle +""" + +from z3 import And, Implies + +import grilops +import grilops.shapes +from grilops import Point, Vector + +GRID = [ + "OOOO", + "OO", + "OOXO", + "OOOOO", + "OOOO" +] + +def main(): + """Shape solver example.""" + locations = [] + for y, row in enumerate(GRID): + for x, c in enumerate(row): + if c == "O": + locations.append(Point(y, x)) + + shapes = [ + [Vector(0, 0), Vector(1, 0), Vector(2, 0), Vector(3, 0)], # I + [Vector(0, 0), Vector(1, 0), Vector(2, 0), Vector(2, 1)], # L + [Vector(0, 1), Vector(0, 2), Vector(1, 0), Vector(1, 1)], # S + ] + + sym = grilops.SymbolSet([("B", chr(0x2588) * 2), ("W", " ")]) + sg = grilops.SymbolGrid(locations, sym) + sc = grilops.shapes.ShapeConstrainer( + locations, shapes, sg.solver, + complete=False, + allow_rotations=True, + allow_reflections=True, + allow_copies=False + ) + for p in locations: + sg.solver.add(sg.cell_is(p, sym.W) == (sc.shape_type_grid[p] == -1)) + for n in sg.touching_cells(p): + np = n.location + sg.solver.add( + Implies( + And(sc.shape_type_grid[p] != -1, sc.shape_type_grid[np] != -1), + sc.shape_type_grid[p] == sc.shape_type_grid[np] + ) + ) + + + if sg.solve(): + sg.print() + print() + sc.print_shape_types() + print() + if sg.is_unique(): + print("Unique solution") + else: + print("Alternate solution") + sg.print() + else: + print("No solution") + + +if __name__ == "__main__": + main() diff --git a/examples/skyscraper.py b/examples/skyscraper.py index 003366e..e15e0e0 100644 --- a/examples/skyscraper.py +++ b/examples/skyscraper.py @@ -7,6 +7,7 @@ import grilops import grilops.sightlines +from grilops import Point, Vector SIZE = 5 @@ -19,13 +20,14 @@ def main(): """Skyscraper solver example.""" - sg = grilops.SymbolGrid(SIZE, SIZE, SYM) + locations = grilops.get_square_locations(SIZE) + sg = grilops.SymbolGrid(locations, SYM) # Each row and each column contains each building height exactly once. for y in range(SIZE): - sg.solver.add(Distinct(*sg.grid[y])) + sg.solver.add(Distinct(*[sg.grid[Point(y, x)] for x in range(SIZE)])) for x in range(SIZE): - sg.solver.add(Distinct(*[sg.grid[y][x] for y in range(SIZE)])) + sg.solver.add(Distinct(*[sg.grid[Point(y, x)] for y in range(SIZE)])) # We'll use the sightlines accumulator to keep track of a tuple storing: # the tallest building we've seen so far @@ -41,16 +43,16 @@ def accumulate(a, height): for x, c in enumerate(GIVEN_TOP): sg.solver.add(c == Acc.num_visible(grilops.sightlines.reduce_cells( - sg, (0, x), (1, 0), Acc.acc(0, 0), accumulate))) + sg, Point(0, x), Vector(1, 0), Acc.acc(0, 0), accumulate))) for y, c in enumerate(GIVEN_LEFT): sg.solver.add(c == Acc.num_visible(grilops.sightlines.reduce_cells( - sg, (y, 0), (0, 1), Acc.acc(0, 0), accumulate))) + sg, Point(y, 0), Vector(0, 1), Acc.acc(0, 0), accumulate))) for y, c in enumerate(GIVEN_RIGHT): sg.solver.add(c == Acc.num_visible(grilops.sightlines.reduce_cells( - sg, (y, SIZE - 1), (0, -1), Acc.acc(0, 0), accumulate))) + sg, Point(y, SIZE - 1), Vector(0, -1), Acc.acc(0, 0), accumulate))) for x, c in enumerate(GIVEN_BOTTOM): sg.solver.add(c == Acc.num_visible(grilops.sightlines.reduce_cells( - sg, (SIZE - 1, x), (-1, 0), Acc.acc(0, 0), accumulate))) + sg, Point(SIZE - 1, x), Vector(-1, 0), Acc.acc(0, 0), accumulate))) if sg.solve(): sg.print() diff --git a/examples/slitherlink.py b/examples/slitherlink.py index c32d26d..2da4146 100644 --- a/examples/slitherlink.py +++ b/examples/slitherlink.py @@ -8,6 +8,7 @@ import grilops import grilops.loops import grilops.regions +from grilops import Point HEIGHT, WIDTH = 6, 6 @@ -35,7 +36,8 @@ def loop_solve(): # We'll place symbols at the intersections of the grid lines, rather than in # the spaces between the grid lines where the givens are written. This # requires increasing each dimension by one. - sg = grilops.SymbolGrid(HEIGHT + 1, WIDTH + 1, sym) + locations = grilops.get_rectangle_locations(HEIGHT + 1, WIDTH + 1) + sg = grilops.SymbolGrid(locations, sym) grilops.loops.LoopConstrainer(sg, single_loop=True) for (y, x), c in GIVENS.items(): @@ -44,16 +46,16 @@ def loop_solve(): # symbols in the north-west and south-east corners of this given location. terms = [ # Check for east edge of north-west corner (given's north edge). - sg.cell_is_one_of(y, x, [sym.EW, sym.NE, sym.SE]), + sg.cell_is_one_of(Point(y, x), [sym.EW, sym.NE, sym.SE]), # Check for north edge of south-east corner (given's east edge). - sg.cell_is_one_of(y + 1, x + 1, [sym.NS, sym.NE, sym.NW]), + sg.cell_is_one_of(Point(y + 1, x + 1), [sym.NS, sym.NE, sym.NW]), # Check for west edge of south-east corner (given's south edge). - sg.cell_is_one_of(y + 1, x + 1, [sym.EW, sym.SW, sym.NW]), + sg.cell_is_one_of(Point(y + 1, x + 1), [sym.EW, sym.SW, sym.NW]), # Check for south edge of north-west corner (given's west edge). - sg.cell_is_one_of(y, x, [sym.NS, sym.SE, sym.SW]), + sg.cell_is_one_of(Point(y, x), [sym.NS, sym.SE, sym.SW]), ] sg.solver.add(PbEq([(term, 1) for term in terms], c)) @@ -72,39 +74,41 @@ def loop_solve(): def region_solve(): """Slitherlink solver example using regions.""" sym = grilops.SymbolSet([("I", chr(0x2588)), ("O", " ")]) - sg = grilops.SymbolGrid(HEIGHT, WIDTH, sym) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, sym) rc = grilops.regions.RegionConstrainer( - HEIGHT, WIDTH, solver=sg.solver, complete=False) + locations, solver=sg.solver, complete=False) region_id = Int("region_id") for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) # Each cell must be either "inside" (part of a single region) or # "outside" (not part of any region). sg.solver.add( Or( - rc.region_id_grid[y][x] == region_id, - rc.region_id_grid[y][x] == -1 + rc.region_id_grid[p] == region_id, + rc.region_id_grid[p] == -1 ) ) sg.solver.add( - (sg.grid[y][x] == sym.I) == (rc.region_id_grid[y][x] == region_id)) + (sg.grid[p] == sym.I) == (rc.region_id_grid[p] == region_id)) if (y, x) not in GIVENS: continue given = GIVENS[(y, x)] - neighbors = sg.adjacent_cells(y, x) + neighbors = sg.adjacent_cells(p) # The number of grid edge border segments adjacent to this cell. num_grid_borders = 4 - len(neighbors) # The number of adjacent cells on the opposite side of the loop line. num_different_neighbors_terms = [ - (n.symbol != sg.grid[y][x], 1) for n in neighbors + (n.symbol != sg.grid[p], 1) for n in neighbors ] # If this is an "inside" cell, we should count grid edge borders as loop # segments, but if this is an "outside" cell, we should not. sg.solver.add( If( - sg.grid[y][x] == sym.I, + sg.grid[p] == sym.I, PbEq(num_different_neighbors_terms, given - num_grid_borders), PbEq(num_different_neighbors_terms, given) ) @@ -114,10 +118,10 @@ def region_solve(): # an adjacent cell. for y in range(HEIGHT - 1): for x in range(WIDTH - 1): - nw = sg.grid[y][x] - ne = sg.grid[y][x + 1] - sw = sg.grid[y + 1][x] - se = sg.grid[y + 1][x + 1] + nw = sg.grid[Point(y, x)] + ne = sg.grid[Point(y, x + 1)] + sw = sg.grid[Point(y + 1, x)] + se = sg.grid[Point(y + 1, x + 1)] sg.solver.add( Implies( And(nw == sym.I, se == sym.I), diff --git a/examples/spiral_galaxies.py b/examples/spiral_galaxies.py index 5524311..893b055 100644 --- a/examples/spiral_galaxies.py +++ b/examples/spiral_galaxies.py @@ -9,6 +9,7 @@ import grilops import grilops.regions +from grilops import Point HEIGHT, WIDTH = 7, 7 @@ -31,19 +32,19 @@ def main(): """Spiral Galaxies solver example.""" # The grid symbols will be the region IDs from the region constrainer. sym = grilops.make_number_range_symbol_set(0, HEIGHT * WIDTH - 1) - sg = grilops.SymbolGrid(HEIGHT, WIDTH, sym) - rc = grilops.regions.RegionConstrainer(HEIGHT, WIDTH, sg.solver) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, sym) + rc = grilops.regions.RegionConstrainer(locations, sg.solver) - for y in range(HEIGHT): - for x in range(WIDTH): - sg.solver.add(sg.cell_is(y, x, rc.region_id_grid[y][x])) + for p in sg.grid: + sg.solver.add(sg.cell_is(p, rc.region_id_grid[p])) # Make the upper-left-most cell covered by a circle the root of its region. roots = {(int(math.floor(y)), int(math.floor(x))) for (y, x) in GIVENS} for y in range(HEIGHT): for x in range(WIDTH): sg.solver.add( - (rc.parent_grid[y][x] == grilops.regions.R) == ((y, x) in roots)) + (rc.parent_grid[Point(y, x)] == grilops.regions.R) == ((y, x) in roots)) # Ensure that each cell has a "partner" within the same region that is # rotationally symmetric with respect to that region's circle. @@ -59,16 +60,16 @@ def main(): continue or_terms.append( And( - rc.region_id_grid[y][x] == region_id, - rc.region_id_grid[py][px] == region_id, + rc.region_id_grid[Point(y, x)] == region_id, + rc.region_id_grid[Point(py, px)] == region_id, ) ) sg.solver.add(Or(*or_terms)) - def show_cell(unused_y, unused_x, region_id): - ry, rx = rc.region_id_to_location(region_id) + def show_cell(unused_p, region_id): + rp = rc.region_id_to_location(region_id) for i, (gy, gx) in enumerate(GIVENS): - if int(math.floor(gy)) == ry and int(math.floor(gx)) == rx: + if int(math.floor(gy)) == rp.y and int(math.floor(gx)) == rp.x: return chr(65 + i) raise Exception("unexpected region id") diff --git a/examples/star_battle.py b/examples/star_battle.py index 1266511..2ee4f2f 100644 --- a/examples/star_battle.py +++ b/examples/star_battle.py @@ -8,6 +8,7 @@ from z3 import And, If, Implies, Sum # type: ignore import grilops +from grilops import Point HEIGHT, WIDTH = 10, 10 @@ -28,34 +29,36 @@ def main(): """Star Battle solver example.""" sym = grilops.SymbolSet([("EMPTY", " "), ("STAR", "*")]) - sg = grilops.SymbolGrid(HEIGHT, WIDTH, sym) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, sym) # There must be exactly two stars per column. for y in range(HEIGHT): sg.solver.add(Sum( - *[If(sg.cell_is(y, x, sym.STAR), 1, 0) for x in range(WIDTH)] + *[If(sg.cell_is(Point(y, x), sym.STAR), 1, 0) for x in range(WIDTH)] ) == 2) # There must be exactly two stars per row. for x in range(WIDTH): sg.solver.add(Sum( - *[If(sg.cell_is(y, x, sym.STAR), 1, 0) for y in range(HEIGHT)] + *[If(sg.cell_is(Point(y, x), sym.STAR), 1, 0) for y in range(HEIGHT)] ) == 2) # There must be exactly two stars per area. area_cells = defaultdict(list) for y in range(HEIGHT): for x in range(WIDTH): - area_cells[AREAS[y][x]].append(sg.grid[y][x]) + area_cells[AREAS[y][x]].append(sg.grid[Point(y, x)]) for cells in area_cells.values(): sg.solver.add(Sum(*[If(c == sym.STAR, 1, 0) for c in cells]) == 2) # Stars may not touch each other, not even diagonally. for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) sg.solver.add(Implies( - sg.cell_is(y, x, sym.STAR), - And(*[n.symbol == sym.EMPTY for n in sg.touching_cells(y, x)]) + sg.cell_is(p, sym.STAR), + And(*[n.symbol == sym.EMPTY for n in sg.touching_cells(p)]) )) if sg.solve(): diff --git a/examples/statue_park_loop.py b/examples/statue_park_loop.py new file mode 100644 index 0000000..9b75e2d --- /dev/null +++ b/examples/statue_park_loop.py @@ -0,0 +1,106 @@ +"""Statue Park (Loop) solver example. + +Example puzzle can be found at https://www.gmpuzzles.com/blog/category/loop/loop2/ +""" + +import sys +from z3 import And, Implies + +import grilops +import grilops.loops +import grilops.shapes +from grilops import Point, Vector + + +E, W, B, X = " ", chr(0x25e6), chr(0x2022), "X" +GIVENS = [ + [E, B, E, E, E, W, E, E], + [E, W, E, E, E, E, B, E], + [W, E, E, E, E, E, E, B], + [E, E, E, E, E, E, E, E], + [E, E, E, E, E, E, E, E], + [B, E, E, E, E, E, E, B], + [E, E, E, E, E, E, W, E], + [X, E, B, E, E, E, W, E], +] + +SHAPES = [ + [(0, 0), (1, 0), (2, 0), (3, 0), (3, 1)], # L + [(0, 1), (0, 2), (1, 0), (1, 1), (2, 0)], # W + [(0, 1), (1, 0), (1, 1), (1, 2), (2, 1)], # X + [(0, 0), (0, 1), (1, 0), (1, 1), (1, 2)], # P + [(0, 2), (1, 2), (2, 0), (2, 1), (2, 2)], # V +] + + +def main(): + """Masyu solver example.""" + for row in GIVENS: + for cell in row: + sys.stdout.write(cell) + print() + + sym = grilops.loops.LoopSymbolSet() + sym.append("EMPTY", " ") + + locations = [] + for y, row in enumerate(GIVENS): + for x, c in enumerate(row): + if c != X: + locations.append(Point(y, x)) + + sg = grilops.SymbolGrid(locations, sym) + lc = grilops.loops.LoopConstrainer(sg, single_loop=True) + sc = grilops.shapes.ShapeConstrainer( + locations, + [[Vector(y, x) for y, x in shape] for shape in SHAPES], + solver=sg.solver, + allow_rotations=True, + allow_reflections=True, + allow_copies=False + ) + + for p in locations: + if GIVENS[p.y][p.x] == W: + # White circles must be part of the loop + sg.solver.add(lc.inside_outside_grid[p] == grilops.loops.L) + elif GIVENS[p.y][p.x] == B: + # Black circles must be part of a shape + sg.solver.add(sc.shape_type_grid[p] != -1) + + # A cell is part of the loop if and only if it is not part of + # any shape + sg.solver.add( + (lc.inside_outside_grid[p] == grilops.loops.L) == + (sc.shape_type_grid[p] == -1) + ) + + # Orthogonally-adjacent cells can't be part of the same shape. + for n in sg.adjacent_cells(p): + np = n.location + sg.solver.add( + Implies( + And( + sc.shape_type_grid[p] != -1, + sc.shape_type_grid[np] != -1 + ), + sc.shape_type_grid[p] == sc.shape_type_grid[np] + ) + ) + + if sg.solve(): + sg.print() + print() + sc.print_shape_types() + print() + if sg.is_unique(): + print("Unique solution") + else: + print("Alternate solution") + sg.print() + else: + print("No solution") + + +if __name__ == "__main__": + main() diff --git a/examples/sudoku.py b/examples/sudoku.py index 18a23f8..80bb0d3 100644 --- a/examples/sudoku.py +++ b/examples/sudoku.py @@ -6,7 +6,7 @@ from z3 import Distinct import grilops - +from grilops import Point def main(): """Sudoku solver example.""" @@ -23,23 +23,23 @@ def main(): ] sym = grilops.make_number_range_symbol_set(1, 9) - sg = grilops.SymbolGrid(9, 9, sym) + sg = grilops.SymbolGrid(grilops.get_square_locations(9), sym) - for given_row, grid_row in zip(givens, sg.grid): - for given, grid_cell in zip(given_row, grid_row): + for y, given_row in enumerate(givens): + for x, given in enumerate(given_row): if given != 0: - sg.solver.add(grid_cell == sym[given]) + sg.solver.add(sg.cell_is(Point(y, x), sym[given])) for y in range(9): - sg.solver.add(Distinct(*sg.grid[y])) + sg.solver.add(Distinct(*[sg.grid[Point(y, x)] for x in range(9)])) for x in range(9): - sg.solver.add(Distinct(*[r[x] for r in sg.grid])) + sg.solver.add(Distinct(*[sg.grid[Point(y, x)] for y in range(9)])) for z in range(9): top = (z // 3) * 3 left = (z % 3) * 3 - cells = [r[x] for r in sg.grid[top:top + 3] for x in range(left, left + 3)] + cells = [sg.grid[Point(y, x)] for y in range(top, top + 3) for x in range(left, left + 3)] sg.solver.add(Distinct(*cells)) if sg.solve(): diff --git a/examples/tapa.py b/examples/tapa.py index 8697770..a2c2695 100644 --- a/examples/tapa.py +++ b/examples/tapa.py @@ -8,6 +8,7 @@ import grilops import grilops.regions +from grilops import Point HEIGHT, WIDTH = 10, 10 GIVENS = { @@ -116,16 +117,17 @@ def add_neighbor_constraints(sg, y, x): for pattern in neighbor_patterns: and_terms = [] for (ny, nx), symbol in zip(neighbor_locations, pattern): - and_terms.append(sg.cell_is(ny, nx, symbol)) + and_terms.append(sg.cell_is(Point(ny, nx), symbol)) or_terms.append(And(*and_terms)) sg.solver.add(Or(*or_terms)) def main(): """Tapa solver example.""" - sg = grilops.SymbolGrid(HEIGHT, WIDTH, SYM) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, SYM) rc = grilops.regions.RegionConstrainer( - HEIGHT, WIDTH, solver=sg.solver, complete=False) + locations, solver=sg.solver, complete=False) # Ensure the wall consists of a single region and is made up of shaded # symbols. @@ -134,17 +136,18 @@ def main(): sg.solver.add(wall_id < HEIGHT * WIDTH) for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) sg.solver.add( - sg.cell_is(y, x, SYM.B) == (rc.region_id_grid[y][x] == wall_id)) + sg.cell_is(p, SYM.B) == (rc.region_id_grid[p] == wall_id)) # Ensure that given clue cells are not part of the wall. if (y, x) in GIVENS: - sg.solver.add(sg.cell_is(y, x, SYM.W)) + sg.solver.add(sg.cell_is(p, SYM.W)) # Shaded cells may not form a 2x2 square anywhere in the grid. for sy in range(HEIGHT - 1): for sx in range(WIDTH - 1): pool_cells = [ - sg.grid[y][x] for y in range(sy, sy + 2) for x in range(sx, sx + 2) + sg.grid[Point(y, x)] for y in range(sy, sy + 2) for x in range(sx, sx + 2) ] sg.solver.add(Not(And(*[cell == SYM.B for cell in pool_cells]))) @@ -152,8 +155,8 @@ def main(): for y, x in GIVENS.keys(): add_neighbor_constraints(sg, y, x) - def show_cell(y, x, _): - given = GIVENS.get((y, x)) + def show_cell(p, _): + given = GIVENS.get((p.y, p.x)) if given is None: return None if len(given) > 1: diff --git a/examples/tutorial.ipynb b/examples/tutorial.ipynb index 26ead4f..f44395e 100644 --- a/examples/tutorial.ipynb +++ b/examples/tutorial.ipynb @@ -100,6 +100,7 @@ }, "source": [ "import grilops\n", + "from grilopos import Point\n", "from z3 import *" ], "execution_count": 0, @@ -171,7 +172,8 @@ }, "source": [ "sym = grilops.make_number_range_symbol_set(1, 9)\n", - "sg = grilops.SymbolGrid(9, 9, sym)" + "locations = grilops.get_square_locations(9)\n", + "sg = grilops.SymbolGrid(locations, sym)" ], "execution_count": 0, "outputs": [] @@ -198,7 +200,7 @@ " for x in range(9):\n", " given = givens[y][x]\n", " if given != 0:\n", - " sg.solver.add(sg.cell_is(y, x, given))" + " sg.solver.add(sg.cell_is(Point(y, x), given))" ], "execution_count": 0, "outputs": [] @@ -229,14 +231,14 @@ "for row in rows:\n", " sg.solver.add(Distinct(*row))\n", "\n", - "columns = [[sg.grid[y][x] for y in range(9)] for x in range(9)]\n", + "columns = [[sg.grid[Point(y, x)] for y in range(9)] for x in range(9)]\n", "for column in columns:\n", " sg.solver.add(Distinct(*column))\n", "\n", "for subgrid_index in range(9):\n", " top = (subgrid_index // 3) * 3\n", " left = (subgrid_index % 3) * 3\n", - " cells = [sg.grid[y][x] for y in range(top, top + 3) for x in range(left, left + 3)]\n", + " cells = [sg.grid[Point(y, x)] for y in range(top, top + 3) for x in range(left, left + 3)]\n", " sg.solver.add(Distinct(*cells))" ], "execution_count": 0, @@ -433,7 +435,8 @@ }, "source": [ "sym = grilops.make_number_range_symbol_set(1, 10)\n", - "sg = grilops.SymbolGrid(9, 9, sym)" + "locations = grilops.get_square_locations(9)\n", + "sg = grilops.SymbolGrid(locations, sym)" ], "execution_count": 0, "outputs": [] @@ -459,7 +462,7 @@ }, "source": [ "import grilops.regions\n", - "rc = grilops.regions.RegionConstrainer(9, 9, solver=sg.solver)" + "rc = grilops.regions.RegionConstrainer(locations, solver=sg.solver)" ], "execution_count": 0, "outputs": [] @@ -486,7 +489,7 @@ "source": [ "for y in range(9):\n", " for x in range(9):\n", - " sg.solver.add(sg.grid[y][x] == rc.region_size_grid[y][x])" + " sg.solver.add(sg.grid[Point(y, x)] == rc.region_size_grid[Point(y, x)])" ], "execution_count": 0, "outputs": [] @@ -513,7 +516,7 @@ " for x in range(9):\n", " given = givens[y][x]\n", " if given != 0:\n", - " sg.solver.add(rc.region_size_grid[y][x] == given)" + " sg.solver.add(rc.region_size_grid[Point(y, x)] == given)" ], "execution_count": 0, "outputs": [] @@ -538,13 +541,14 @@ "source": [ "for y in range(9):\n", " for x in range(9):\n", - " adjacent_sizes = grilops.adjacent_cells(rc.region_size_grid, y, x)\n", - " adjacent_ids = grilops.adjacent_cells(rc.region_id_grid, y, x)\n", + " p = Point(y, x)\n", + " adjacent_sizes = grilops.adjacent_cells(rc.region_size_grid, p)\n", + " adjacent_ids = grilops.adjacent_cells(rc.region_id_grid, p)\n", " for adjacent_size, adjacent_id in zip(adjacent_sizes, adjacent_ids):\n", " sg.solver.add(\n", " Implies(\n", - " rc.region_size_grid[y][x] == adjacent_size.symbol,\n", - " rc.region_id_grid[y][x] == adjacent_id.symbol\n", + " rc.region_size_grid[p] == adjacent_size.symbol,\n", + " rc.region_id_grid[p] == adjacent_id.symbol\n", " )\n", " )" ], @@ -730,7 +734,8 @@ " (\"EMPTY\", \" \"),\n", " (\"LIGHT\", \"*\"),\n", "])\n", - "sg = grilops.SymbolGrid(height, width, sym)" + "locations = grilops.get_rectangle_locations(height, width)\n", + "sg = grilops.SymbolGrid(locations, sym)" ], "execution_count": 0, "outputs": [] @@ -755,16 +760,17 @@ "source": [ "for y in range(height):\n", " for x in range(width):\n", + " p = Point(y, x)\n", " if (y, x) in givens:\n", - " sg.solver.add(sg.cell_is(y, x, sym.BLACK))\n", + " sg.solver.add(sg.cell_is(p, sym.BLACK))\n", " light_bulb_count = givens[(y, x)]\n", " if light_bulb_count is not None:\n", " sg.solver.add(light_bulb_count == sum(\n", - " If(n.symbol == sym.LIGHT, 1, 0) for n in sg.adjacent_cells(y, x)\n", + " If(n.symbol == sym.LIGHT, 1, 0) for n in sg.adjacent_cells(p)\n", " ))\n", " else:\n", " # All black cells are given; don't allow this cell to be black.\n", - " sg.solver.add(Not(sg.cell_is(y, x, sym.BLACK)))" + " sg.solver.add(Not(sg.cell_is(p, sym.BLACK)))" ], "execution_count": 0, "outputs": [] @@ -811,7 +817,7 @@ " visible_light_bulb_count = sum(\n", " grilops.sightlines.count_cells(\n", " sg, n.location, n.direction, stop=is_black, count=count_light\n", - " ) for n in sg.adjacent_cells(y, x)\n", + " ) for n in sg.adjacent_cells(Point(y, x))\n", " )\n", " \n", " # If this cell contains a light bulb, then ensure that it cannot see any\n", @@ -820,7 +826,7 @@ " # least one light bulb.\n", " sg.solver.add(\n", " If(\n", - " sg.cell_is(y, x, sym.LIGHT),\n", + " sg.cell_is(Point(y, x), sym.LIGHT),\n", " visible_light_bulb_count == 0,\n", " visible_light_bulb_count > 0\n", " )\n", @@ -946,4 +952,4 @@ ] } ] -} \ No newline at end of file +} diff --git a/examples/yajilin.py b/examples/yajilin.py index d574ad1..76ae641 100644 --- a/examples/yajilin.py +++ b/examples/yajilin.py @@ -9,6 +9,7 @@ import grilops import grilops.loops +from grilops import Point U, R, D, L = chr(0x25B4), chr(0x25B8), chr(0x25BE), chr(0x25C2) @@ -57,40 +58,42 @@ def main(): sym.append("BLACK", chr(0x25AE)) sym.append("GRAY", chr(0x25AF)) sym.append("INDICATIVE", " ") - sg = grilops.SymbolGrid(HEIGHT, WIDTH, sym) + locations = grilops.get_rectangle_locations(HEIGHT, WIDTH) + sg = grilops.SymbolGrid(locations, sym) grilops.loops.LoopConstrainer(sg, single_loop=True) for y in range(HEIGHT): for x in range(WIDTH): + p = Point(y, x) if (y, x) in GIVENS: - sg.solver.add(sg.cell_is(y, x, sym.INDICATIVE)) + sg.solver.add(sg.cell_is(p, sym.INDICATIVE)) elif (y, x) in GRAYS: - sg.solver.add(sg.cell_is(y, x, sym.GRAY)) + sg.solver.add(sg.cell_is(p, sym.GRAY)) else: - sg.solver.add(Not(sg.cell_is_one_of(y, x, [sym.INDICATIVE, sym.GRAY]))) + sg.solver.add(Not(sg.cell_is_one_of(p, [sym.INDICATIVE, sym.GRAY]))) sg.solver.add(Implies( - sg.cell_is(y, x, sym.BLACK), - And(*[n.symbol != sym.BLACK for n in sg.adjacent_cells(y, x)]) + sg.cell_is(p, sym.BLACK), + And(*[n.symbol != sym.BLACK for n in sg.adjacent_cells(p)]) )) for (sy, sx), (direction, count) in GIVENS.items(): if direction == U: cells = [(y, sx) for y in range(sy)] elif direction == R: - cells = [(sy, x) for x in range(sx + 1, len(sg.grid[0]))] + cells = [(sy, x) for x in range(sx + 1, WIDTH)] elif direction == D: - cells = [(y, sx) for y in range(sy + 1, len(sg.grid))] + cells = [(y, sx) for y in range(sy + 1, HEIGHT)] elif direction == L: cells = [(sy, x) for x in range(sx)] sg.solver.add( PbEq( - [(sg.cell_is(y, x, sym.BLACK), 1) for (y, x) in cells], + [(sg.cell_is(Point(y, x), sym.BLACK), 1) for (y, x) in cells], count ) ) def print_grid(): - sg.print(lambda y, x, _: GIVENS[(y, x)][0] if (y, x) in GIVENS else None) + sg.print(lambda p, _: GIVENS[(p.y, p.x)][0] if (p.y, p.x) in GIVENS else None) if sg.solve(): print_grid() diff --git a/grilops/grids.py b/grilops/grids.py index d117e1c..fde0ecf 100644 --- a/grilops/grids.py +++ b/grilops/grids.py @@ -1,79 +1,143 @@ """This module supports constructing and working with grids of cells.""" import sys -from typing import List, NamedTuple, Tuple +from typing import Dict, List, NamedTuple from z3 import ArithRef, BoolRef, Int, Or, Solver, sat, unsat # type: ignore from .symbols import SymbolSet +class Vector(NamedTuple): + """Properties of a vector representing an offset in two dimensions + + # Attributes + dy (int): The relative distance in the y dimension + dx (int): The relative distance in the x dimension + """ + dy: int + dx: int + + +class Point(NamedTuple): + """Properties of a point, generally corresponding to the center of a grid cell. + + # Attributes + y (int): The location in the y dimension + x (int): The location in the x dimension + """ + y: int + x: int + + def translate(self, d: Vector) -> "Point": + """Translates this point in the given direction.""" + return Point(self.y + d.dy, self.x + d.dx) + + class Neighbor(NamedTuple): """Properties of a cell that is a neighbor of another. # Attributes - location (Tuple[int, int]): The (y, x) coordinate of the location of the cell. - direction (Tuple[int, int]): The (+y, +x) distance from the original cell. + location (Point): The (y, x) coordinate of the location of the cell. + direction (Vector): The direction from the original cell. symbol (z3.ArithRef): The symbol constant of the cell. """ - location: Tuple[int, int] - direction: Tuple[int, int] + location: Point + direction: Vector symbol: ArithRef +def get_adjacency_offsets() -> List[Vector]: + """Returns a list of offsets corresponding to adjacent cells.""" + return [ + Vector(-1, 0), # N + Vector(1, 0), # S + Vector(0, 1), # E + Vector(0, -1), # W + ] + + +def get_touching_offsets() -> List[Vector]: + """Returns a list of offsets corresponding to touching cells.""" + return [ + Vector(-1, 0), # N + Vector(1, 0), # S + Vector(0, 1), # E + Vector(0, -1), # W + Vector(-1, 1), # NE + Vector(-1, -1), # NW + Vector(1, 1), # SE + Vector(1, -1), # SW + ] + + def adjacent_cells( - grid: List[List[ArithRef]], y: int, x: int) -> List[Neighbor]: + grid: Dict[Point, ArithRef], p: Point) -> List[Neighbor]: """Returns a list of cells orthogonally adjacent to the given cell. # Arguments - grid (List[List[z3.ArithRef]]): A grid of z3 constants. - y (int): y-coordinate of the given cell. - x (int): x-coordinate of the given cell. + grid (Dict[Point, ArithRef]): A dictionary of z3 constants. + p (Point): Location of the given cell. # Returns (List[Neighbor]): The cells orthogonally adjacent to the given cell. """ cells = [] - if y > 0: - cells.append(Neighbor((y - 1, x), (-1, 0), grid[y - 1][x])) - if x < len(grid[0]) - 1: - cells.append(Neighbor((y, x + 1), (0, 1), grid[y][x + 1])) - if y < len(grid) - 1: - cells.append(Neighbor((y + 1, x), (1, 0), grid[y + 1][x])) - if x > 0: - cells.append(Neighbor((y, x - 1), (0, -1), grid[y][x - 1])) + for d in get_adjacency_offsets(): + translated_p = p.translate(d) + if translated_p in grid: + cells.append(Neighbor(translated_p, d, grid[translated_p])) return cells def touching_cells( - grid: List[List[ArithRef]], y: int, x: int) -> List[Neighbor]: + grid: Dict[Point, ArithRef], p: Point) -> List[Neighbor]: """Returns the cells touching the given cell (orthogonally and diagonally). # Arguments - grid (List[List[z3.ArithRef]]): A grid of z3 constants. - y (int): y-coordinate of the given cell. - x (int): x-coordinate of the given cell. + grid (Dict[Point, ArithRef]): A dictionary of z3 constants. + p (Point): Location of the given cell. # Returns (List[Neighbor]): The cells touching the given cell. """ - cells = adjacent_cells(grid, y, x) - if y > 0 and x > 0: - cells.append(Neighbor((y - 1, x - 1), (-1, -1), grid[y - 1][x - 1])) - if y > 0 and x < len(grid[0]) - 1: - cells.append(Neighbor((y - 1, x + 1), (-1, 1), grid[y - 1][x + 1])) - if x > 0 and y < len(grid) - 1: - cells.append(Neighbor((y + 1, x - 1), (1, -1), grid[y + 1][x - 1])) - if y < len(grid) - 1 and x < len(grid[0]) - 1: - cells.append(Neighbor((y + 1, x + 1), (1, 1), grid[y + 1][x + 1])) + cells = [] + for d in get_touching_offsets(): + translated_p = p.translate(d) + if translated_p in grid: + cells.append(Neighbor(translated_p, d, grid[translated_p])) return cells +def get_rectangle_locations(height: int, width: int) -> List[Point]: + """Returns a list of locations corresponding to a rectangular grid. + + # Arguments + height (int): Height of the grid + width (int): Width of the grid + + # Returns + (List[Point]): The list of cell locations. + """ + return [Point(y, x) for x in range(width) for y in range(height)] + + +def get_square_locations(height: int) -> List[Point]: + """Returns a list of locations corresponding to a square grid. + + # Arguments + height (int): Height of the grid + + # Returns + (List[Point]): The list of cell locations. + """ + return get_rectangle_locations(height, height) + + class SymbolGrid: """A grid of cells that can be solved to contain specific symbols. # Arguments - height (int): The height of the grid. - width (int): The width of the grid. + locations (List[Point]): The locations of grid cells. symbol_set (SymbolSet): The set of symbols to be filled into the grid. solver (z3.Solver, None): A #Solver object. If None, a #Solver will be constructed. @@ -82,8 +146,7 @@ class SymbolGrid: def __init__( self, - height: int, - width: int, + locations: List[Point], symbol_set: SymbolSet, solver: Solver = None ): @@ -93,15 +156,12 @@ def __init__( else: self.__solver = Solver() self.__symbol_set = symbol_set - self.__grid: List[List[ArithRef]] = [] - for y in range(height): - row = [] - for x in range(width): - v = Int(f"sg-{SymbolGrid._instance_index}-{y}-{x}") - self.__solver.add(v >= symbol_set.min_index()) - self.__solver.add(v <= symbol_set.max_index()) - row.append(v) - self.__grid.append(row) + self.__grid: Dict[Point, ArithRef] = {} + for p in locations: + v = Int(f"sg-{SymbolGrid._instance_index}-{p.y}-{p.x}") + self.__solver.add(v >= symbol_set.min_index()) + self.__solver.add(v <= symbol_set.max_index()) + self.__grid[p] = v @property def solver(self) -> Solver: @@ -114,61 +174,57 @@ def symbol_set(self) -> SymbolSet: return self.__symbol_set @property - def grid(self) -> List[List[ArithRef]]: - """(List[List[z3.ArithRef]]): The grid of cells.""" + def grid(self) -> Dict[Point, ArithRef]: + """(Dict[Point, ArithRef]): The grid of cells.""" return self.__grid - def adjacent_cells(self, y: int, x: int) -> List[Neighbor]: + def adjacent_cells(self, p: Point) -> List[Neighbor]: """Returns a list of cells orthogonally adjacent to the given cell. # Arguments - y (int): y-coordinate of the given cell. - x (int): x-coordinate of the given cell. + p: Location of the given cell. # Returns (List[Neighbor]): The cells orthogonally adjacent to the given cell. """ - return adjacent_cells(self.__grid, y, x) + return adjacent_cells(self.__grid, p) - def touching_cells(self, y: int, x: int) -> List[Neighbor]: + def touching_cells(self, p: Point) -> List[Neighbor]: """Returns the cells touching the given cell (orthogonally and diagonally). # Arguments - y (int): y-coordinate of the given cell. - x (int): x-coordinate of the given cell. + p: Location of the given cell. # Returns (List[Neighbor]): The cells touching the given cell. """ - return touching_cells(self.__grid, y, x) + return touching_cells(self.__grid, p) - def cell_is(self, y: int, x: int, value: int) -> BoolRef: + def cell_is(self, p: Point, value: int) -> BoolRef: """Returns an expression for whether this cell contains this value. # Arguments - y (int): The y-coordinate in the grid. - x (int): The x-coordinate in the grid. + p: The location of the given cell in the grid. value (int): The value to satisfy the expression. # Returns - (z3.BoolRef): an expression that's true if and only if the cell at (y, x) + (z3.BoolRef): an expression that's true if and only if the cell at p contains this value. """ - return self.__grid[y][x] == value + return self.__grid[p] == value - def cell_is_one_of(self, y: int, x: int, values: List[int]) -> BoolRef: + def cell_is_one_of(self, p: Point, values: List[int]) -> BoolRef: """Returns an expression for whether this cell contains one of these values. # Arguments - y (int): The y-coordinate in the grid. - x (int): The x-coordinate in the grid. + p: The location of the given cell in the grid. values (list(int)): The list of values to satisfy the expression. # Returns - (z3.BoolRef): an expression that's true if and only if the cell at (y, x) + (z3.BoolRef): an expression that's true if and only if the cell at p contains one of the values. """ - cell = self.__grid[y][x] + cell = self.__grid[p] return Or(*[cell == value for value in values]) def solve(self) -> bool: @@ -184,27 +240,20 @@ def is_unique(self) -> bool: """ model = self.__solver.model() or_terms = [] - for row in self.__grid: - for cell in row: - or_terms.append(cell != model.eval(cell).as_long()) + for cell in self.__grid.values(): + or_terms.append(cell != model.eval(cell).as_long()) self.__solver.add(Or(*or_terms)) result = self.__solver.check() return result == unsat - def solved_grid(self) -> List[List[int]]: + def solved_grid(self) -> Dict[Point, int]: """Returns the solved symbol grid. Should be called only after #SymbolGrid.solve() has already completed successfully. """ model = self.__solver.model() - solved = [] - for row in self.__grid: - solved_row = [] - for cell in row: - solved_row.append(model.eval(cell).as_long()) - solved.append(solved_row) - return solved + return dict((p, model.eval(self.__grid[p]).as_long()) for p in self.__grid) def print(self, hook_function=None): """Prints the solved grid using symbol labels. @@ -215,18 +264,27 @@ def print(self, hook_function=None): # Arguments hook_function (function, None): A function implementing custom symbol display behavior, or None. If this function is provided, it - will be called for each cell in the grid, with the arguments y (int), - x (int), and the symbol index for that cell (int). It may return a + will be called for each cell in the grid, with the arguments + c (Point) and the symbol index for that cell (int). It may return a string to print for that cell, or None to keep the default behavior. """ model = self.__solver.model() label_width = max(len(s.label) for s in self.__symbol_set.symbols.values()) - for y, row in enumerate(self.__grid): - for x, cell in enumerate(row): + min_y = min(p.y for p in self.__grid) + min_x = min(p.x for p in self.__grid) + max_y = max(p.y for p in self.__grid) + max_x = max(p.x for p in self.__grid) + for y in range(min_y, max_y + 1): + for x in range(min_x, max_x + 1): + p = Point(y, x) + if p not in self.__grid: + sys.stdout.write(" " * label_width) + continue + cell = self.__grid[p] i = model.eval(cell).as_long() label = None if hook_function: - label = hook_function(y, x, i) + label = hook_function(p, i) if label is None: label = f"{self.__symbol_set.symbols[i].label:{label_width}}" sys.stdout.write(label) diff --git a/grilops/loops.py b/grilops/loops.py index d3dd606..cac4454 100644 --- a/grilops/loops.py +++ b/grilops/loops.py @@ -10,12 +10,12 @@ """ import sys -from typing import Any, List +from typing import Any, Dict from z3 import ( # type: ignore And, ArithRef, BoolRef, Distinct, If, Implies, Int, Or, Xor ) -from .grids import SymbolGrid +from .grids import Point, SymbolGrid, Vector from .symbols import SymbolSet from .sightlines import reduce_cells @@ -78,8 +78,8 @@ def __init__( LoopConstrainer._instance_index += 1 self.__symbol_grid = symbol_grid - self.__inside_outside_grid: List[List[ArithRef]] = [] - self.__loop_order_grid: List[List[ArithRef]] = [] + self.__inside_outside_grid: Dict[Point, ArithRef] = {} + self.__loop_order_grid: Dict[Point, ArithRef] = {} self.__add_loop_edge_constraints() self.__make_inside_outside_grid() @@ -91,134 +91,134 @@ def __add_loop_edge_constraints(self): solver = self.__symbol_grid.solver sym: Any = self.__symbol_grid.symbol_set - for y in range(len(grid)): - for x in range(len(grid[0])): - cell = grid[y][x] - - if y > 0: - n = grid[y - 1][x] - solver.add(Implies( - Or(cell == sym.NS, cell == sym.NE, cell == sym.NW), - Or(n == sym.NS, n == sym.SE, n == sym.SW) - )) - else: - solver.add(cell != sym.NS) - solver.add(cell != sym.NE) - solver.add(cell != sym.NW) - - if y < len(grid) - 1: - s = grid[y + 1][x] - solver.add(Implies( - Or(cell == sym.NS, cell == sym.SE, cell == sym.SW), - Or(s == sym.NS, s == sym.NE, s == sym.NW) - )) - else: - solver.add(cell != sym.NS) - solver.add(cell != sym.SE) - solver.add(cell != sym.SW) - - if x > 0: - w = grid[y][x - 1] - solver.add(Implies( - Or(cell == sym.EW, cell == sym.SW, cell == sym.NW), - Or(w == sym.EW, w == sym.NE, w == sym.SE) - )) - else: - solver.add(cell != sym.EW) - solver.add(cell != sym.SW) - solver.add(cell != sym.NW) - - if x < len(grid[0]) - 1: - e = grid[y][x + 1] - solver.add(Implies( - Or(cell == sym.EW, cell == sym.NE, cell == sym.SE), - Or(e == sym.EW, e == sym.SW, e == sym.NW) - )) - else: - solver.add(cell != sym.EW) - solver.add(cell != sym.NE) - solver.add(cell != sym.SE) + for p in grid: + cell = grid[p] + + n = p.translate(Vector(-1, 0)) + if n in grid: + solver.add(Implies( + Or(cell == sym.NS, cell == sym.NE, cell == sym.NW), + Or(grid[n] == sym.NS, grid[n] == sym.SE, grid[n] == sym.SW) + )) + else: + solver.add(cell != sym.NS) + solver.add(cell != sym.NE) + solver.add(cell != sym.NW) + + s = p.translate(Vector(1, 0)) + if s in grid: + solver.add(Implies( + Or(cell == sym.NS, cell == sym.SE, cell == sym.SW), + Or(grid[s] == sym.NS, grid[s] == sym.NE, grid[s] == sym.NW) + )) + else: + solver.add(cell != sym.NS) + solver.add(cell != sym.SE) + solver.add(cell != sym.SW) + + w = p.translate(Vector(0, -1)) + if w in grid: + solver.add(Implies( + Or(cell == sym.EW, cell == sym.SW, cell == sym.NW), + Or(grid[w] == sym.EW, grid[w] == sym.NE, grid[w] == sym.SE) + )) + else: + solver.add(cell != sym.EW) + solver.add(cell != sym.SW) + solver.add(cell != sym.NW) + + e = p.translate(Vector(0, 1)) + if e in grid: + solver.add(Implies( + Or(cell == sym.EW, cell == sym.NE, cell == sym.SE), + Or(grid[e] == sym.EW, grid[e] == sym.SW, grid[e] == sym.NW) + )) + else: + solver.add(cell != sym.EW) + solver.add(cell != sym.NE) + solver.add(cell != sym.SE) def __add_single_loop_constraints(self): grid = self.__symbol_grid.grid solver = self.__symbol_grid.solver sym: Any = self.__symbol_grid.symbol_set - cell_count = len(grid) * len(grid[0]) + cell_count = len(grid.keys()) loop_order_grid = self.__loop_order_grid - for y in range(len(grid)): - row: List[ArithRef] = [] - for x in range(len(grid[0])): - v = Int(f"log-{LoopConstrainer._instance_index}-{y}-{x}") - solver.add(v >= -cell_count) - solver.add(v < cell_count) - row.append(v) - loop_order_grid.append(row) - - solver.add(Distinct(*[v for row in loop_order_grid for v in row])) - - for y in range(len(grid)): - for x in range(len(grid[0])): - cell = grid[y][x] - li = loop_order_grid[y][x] - - solver.add(If(sym.is_loop(cell), li >= 0, li < 0)) - - if 0 < y < len(grid) - 1: - solver.add(Implies( - And(cell == sym.NS, li > 0), - Or( - loop_order_grid[y - 1][x] == li - 1, - loop_order_grid[y + 1][x] == li - 1 - ) - )) - - if 0 < x < len(grid[0]) - 1: - solver.add(Implies( - And(cell == sym.EW, li > 0), - Or( - loop_order_grid[y][x - 1] == li - 1, - loop_order_grid[y][x + 1] == li - 1 - ) - )) - - if y > 0 and x < len(grid[0]) - 1: - solver.add(Implies( - And(cell == sym.NE, li > 0), - Or( - loop_order_grid[y - 1][x] == li - 1, - loop_order_grid[y][x + 1] == li - 1 - ) - )) - - if y < len(grid) - 1 and x < len(grid[0]) - 1: - solver.add(Implies( - And(cell == sym.SE, li > 0), - Or( - loop_order_grid[y + 1][x] == li - 1, - loop_order_grid[y][x + 1] == li - 1 - ) - )) - - if y < len(grid) - 1 and x > 0: - solver.add(Implies( - And(cell == sym.SW, li > 0), - Or( - loop_order_grid[y + 1][x] == li - 1, - loop_order_grid[y][x - 1] == li - 1 - ) - )) - - if y > 0 and x > 0: - solver.add(Implies( - And(cell == sym.NW, li > 0), - Or( - loop_order_grid[y - 1][x] == li - 1, - loop_order_grid[y][x - 1] == li - 1 - ) - )) + for p in grid: + v = Int(f"log-{LoopConstrainer._instance_index}-{p.y}-{p.x}") + solver.add(v >= -cell_count) + solver.add(v < cell_count) + loop_order_grid[p] = v + + solver.add(Distinct(*loop_order_grid.values())) + + for p in grid: + cell = grid[p] + li = loop_order_grid[p] + + solver.add(If(sym.is_loop(cell), li >= 0, li < 0)) + + n = p.translate(Vector(-1, 0)) + s = p.translate(Vector(1, 0)) + w = p.translate(Vector(0, -1)) + e = p.translate(Vector(0, 1)) + + if n in grid and s in grid: + solver.add(Implies( + And(cell == sym.NS, li > 0), + Or( + loop_order_grid[n] == li - 1, + loop_order_grid[s] == li - 1 + ) + )) + + if e in grid and w in grid: + solver.add(Implies( + And(cell == sym.EW, li > 0), + Or( + loop_order_grid[e] == li - 1, + loop_order_grid[w] == li - 1 + ) + )) + + if n in grid and e in grid: + solver.add(Implies( + And(cell == sym.NE, li > 0), + Or( + loop_order_grid[n] == li - 1, + loop_order_grid[e] == li - 1 + ) + )) + + if s in grid and e in grid: + solver.add(Implies( + And(cell == sym.SE, li > 0), + Or( + loop_order_grid[s] == li - 1, + loop_order_grid[e] == li - 1 + ) + )) + + if s in grid and w in grid: + solver.add(Implies( + And(cell == sym.SW, li > 0), + Or( + loop_order_grid[s] == li - 1, + loop_order_grid[w] == li - 1 + ) + )) + + if n in grid and w in grid: + solver.add(Implies( + And(cell == sym.NW, li > 0), + Or( + loop_order_grid[n] == li - 1, + loop_order_grid[w] == li - 1 + ) + )) def __make_inside_outside_grid(self): grid = self.__symbol_grid.grid @@ -227,33 +227,24 @@ def __make_inside_outside_grid(self): def accumulate(a, c): return Xor(a, Or(c == sym.EW, c == sym.NW, c == sym.SW)) - for y in range(len(grid)): - row: List[ArithRef] = [] - for x in range(len(grid[0])): - a = reduce_cells( - self.__symbol_grid, (y, x), (-1, 0), - False, accumulate - ) - row.append( - If( - sym.is_loop(grid[y][x]), - L, - If(a, I, O) - ) - ) - self.__inside_outside_grid.append(row) + for p in grid: + a = reduce_cells( + self.__symbol_grid, p, Vector(-1, 0), + False, accumulate + ) + self.__inside_outside_grid[p] = If(sym.is_loop(grid[p]), L, If(a, I, O)) @property - def loop_order_grid(self) -> List[List[ArithRef]]: - """(List[List[ArithRef]]): A grid of constants of a loop traversal order. + def loop_order_grid(self) -> Dict[Point, ArithRef]: + """(Dict[Point, ArithRef]): A dictionary of constants of a loop traversal order. Only populated if single_loop was true. """ return self.__loop_order_grid @property - def inside_outside_grid(self) -> List[List[ArithRef]]: - """(List[List[ArithRef]]): A grid of which cells are contained by loops.""" + def inside_outside_grid(self) -> Dict[Point, ArithRef]: + """(Dict[Point, ArithRef]): A dictionary of which cells are contained by loops.""" return self.__inside_outside_grid def print_inside_outside_grid(self): @@ -264,7 +255,16 @@ def print_inside_outside_grid(self): O: "O", } model = self.__symbol_grid.solver.model() - for row in self.__inside_outside_grid: - for v in row: - sys.stdout.write(labels[model.eval(v).as_long()]) + min_y = min(p.y for p in self.__inside_outside_grid) + min_x = min(p.x for p in self.__inside_outside_grid) + max_y = max(p.y for p in self.__inside_outside_grid) + max_x = max(p.x for p in self.__inside_outside_grid) + for y in range(min_y, max_y + 1): + for x in range(min_x, max_x + 1): + p = Point(y, x) + if p in self.__inside_outside_grid: + v = self.__inside_outside_grid[p] + sys.stdout.write(labels[model.eval(v).as_long()]) + else: + sys.stdout.write(" ") print() diff --git a/grilops/regions.py b/grilops/regions.py index afbe8e9..cb327d4 100644 --- a/grilops/regions.py +++ b/grilops/regions.py @@ -20,9 +20,10 @@ """ import sys -from typing import List, Optional, Tuple +from typing import Dict, List, Optional from z3 import And, ArithRef, If, Implies, Int, Or, Solver, Sum # type: ignore +from .grids import Vector, Point X, R, N, E, S, W = range(6) @@ -31,8 +32,7 @@ class RegionConstrainer: # pylint: disable=R0902 """Creates constraints for grouping cells into contiguous regions. # Arguments - height (int): The height of the grid. - width (int): The width of the grid. + locations (List[Point]): List of locations in the grid. solver (z3.Solver, None): A #Solver object. If None, a #Solver will be constructed. complete (bool): If true, every cell must be part of a region. Defaults to @@ -44,14 +44,15 @@ class RegionConstrainer: # pylint: disable=R0902 def __init__( # pylint: disable=R0913 self, - height: int, - width: int, + locations: List[Point], solver: Solver = None, complete: bool = True, min_region_size: Optional[int] = None, max_region_size: Optional[int] = None ): RegionConstrainer._instance_index += 1 + self.__locations = sorted(locations) + self.__location_to_region_id = dict((c, i) for i, c in enumerate(self.__locations)) if solver: self.__solver = solver else: @@ -64,146 +65,132 @@ def __init__( # pylint: disable=R0913 if max_region_size is not None: self.__max_region_size = max_region_size else: - self.__max_region_size = height * width - self.__width = width - self.__create_grids(height, width) + self.__max_region_size = len(self.__locations) + self.__create_grids(locations) self.__add_constraints() - def __create_grids(self, height: int, width: int): + def __create_grids(self, locations: List[Point]): """Create the grids used to model region constraints.""" - self.__parent_grid: List[List[ArithRef]] = [] - for y in range(height): - row = [] - for x in range(width): - v = Int(f"rcp-{RegionConstrainer._instance_index}-{y}-{x}") - if self.__complete: - self.__solver.add(v >= R) - else: - self.__solver.add(v >= X) - self.__solver.add(v <= W) - row.append(v) - self.__parent_grid.append(row) - - self.__subtree_size_grid: List[List[ArithRef]] = [] - for y in range(height): - row = [] - for x in range(width): - v = Int(f"rcss-{RegionConstrainer._instance_index}-{y}-{x}") - if self.__complete: - self.__solver.add(v >= 1) - else: - self.__solver.add(v >= 0) - self.__solver.add(v <= self.__max_region_size) - row.append(v) - self.__subtree_size_grid.append(row) - - self.__region_id_grid: List[List[ArithRef]] = [] - for y in range(height): - row = [] - for x in range(width): - v = Int(f"rcid-{RegionConstrainer._instance_index}-{y}-{x}") - if self.__complete: - self.__solver.add(v >= 0) - else: - self.__solver.add(v >= -1) - self.__solver.add(v < height * width) - parent = self.__parent_grid[y][x] - self.__solver.add(Implies(parent == X, v == -1)) - self.__solver.add(Implies( - parent == R, v == self.location_to_region_id((y, x)))) - row.append(v) - self.__region_id_grid.append(row) - - self.__region_size_grid: List[List[ArithRef]] = [] - for y in range(height): - row = [] - for x in range(width): - v = Int(f"rcrs-{RegionConstrainer._instance_index}-{y}-{x}") - if self.__complete: - self.__solver.add(v >= self.__min_region_size) - else: - self.__solver.add(Or(v >= self.__min_region_size, v == -1)) - self.__solver.add(v <= self.__max_region_size) - parent = self.__parent_grid[y][x] - subtree_size = self.__subtree_size_grid[y][x] - self.__solver.add(Implies(parent == X, v == -1)) - self.__solver.add(Implies(parent == R, v == subtree_size)) - row.append(v) - self.__region_size_grid.append(row) + self.__parent_grid: Dict[Point, ArithRef] = {} + for p in locations: + v = Int(f"rcp-{RegionConstrainer._instance_index}-{p.y}-{p.x}") + if self.__complete: + self.__solver.add(v >= R) + else: + self.__solver.add(v >= X) + self.__solver.add(v <= W) + self.__parent_grid[p] = v + + self.__subtree_size_grid: Dict[Point, ArithRef] = {} + for p in locations: + v = Int(f"rcss-{RegionConstrainer._instance_index}-{p.y}-{p.x}") + if self.__complete: + self.__solver.add(v >= 1) + else: + self.__solver.add(v >= 0) + self.__solver.add(v <= self.__max_region_size) + self.__subtree_size_grid[p] = v + + self.__region_id_grid: Dict[Point, ArithRef] = {} + for p in locations: + v = Int(f"rcid-{RegionConstrainer._instance_index}-{p.y}-{p.x}") + if self.__complete: + self.__solver.add(v >= 0) + else: + self.__solver.add(v >= -1) + self.__solver.add(v < len(locations)) + parent = self.__parent_grid[p] + self.__solver.add(Implies(parent == X, v == -1)) + self.__solver.add(Implies( + parent == R, v == self.location_to_region_id(p))) + self.__region_id_grid[p] = v + + self.__region_size_grid: Dict[Point, ArithRef] = {} + for p in locations: + v = Int(f"rcrs-{RegionConstrainer._instance_index}-{p.y}-{p.x}") + if self.__complete: + self.__solver.add(v >= self.__min_region_size) + else: + self.__solver.add(Or(v >= self.__min_region_size, v == -1)) + self.__solver.add(v <= self.__max_region_size) + parent = self.__parent_grid[p] + subtree_size = self.__subtree_size_grid[p] + self.__solver.add(Implies(parent == X, v == -1)) + self.__solver.add(Implies(parent == R, v == subtree_size)) + self.__region_size_grid[p] = v def __add_constraints(self): """Add constraints to the region modeling grids.""" - def constrain_side(yx, sysx, sd): - y, x = yx - sy, sx = sysx + def constrain_side(p, sp, sd): self.__solver.add(Implies( - self.__parent_grid[y][x] == X, - self.__parent_grid[sy][sx] != sd + self.__parent_grid[p] == X, + self.__parent_grid[sp] != sd )) self.__solver.add(Implies( - self.__parent_grid[sy][sx] == sd, + self.__parent_grid[sp] == sd, And( - self.__region_id_grid[y][x] == self.__region_id_grid[sy][sx], - self.__region_size_grid[y][x] == self.__region_size_grid[sy][sx], + self.__region_id_grid[p] == self.__region_id_grid[sp], + self.__region_size_grid[p] == self.__region_size_grid[sp], ) )) - def subtree_size_term(sysx, sd): - sy, sx = sysx + def subtree_size_term(sp, sd): return If( - self.__parent_grid[sy][sx] == sd, - self.__subtree_size_grid[sy][sx], + self.__parent_grid[sp] == sd, + self.__subtree_size_grid[sp], 0 ) - for y in range(len(self.__parent_grid)): - for x in range(len(self.__parent_grid[0])): - parent = self.__parent_grid[y][x] - subtree_size_terms = [ - If(parent != X, 1, 0) - ] - - if y > 0: - constrain_side((y, x), (y - 1, x), S) - subtree_size_terms.append(subtree_size_term((y - 1, x), S)) - else: - self.__solver.add(parent != N) - - if y < len(self.__parent_grid) - 1: - constrain_side((y, x), (y + 1, x), N) - subtree_size_terms.append(subtree_size_term((y + 1, x), N)) - else: - self.__solver.add(parent != S) - - if x > 0: - constrain_side((y, x), (y, x - 1), E) - subtree_size_terms.append(subtree_size_term((y, x - 1), E)) - else: - self.__solver.add(parent != W) - - if x < len(self.__parent_grid[0]) - 1: - constrain_side((y, x), (y, x + 1), W) - subtree_size_terms.append(subtree_size_term((y, x + 1), W)) - else: - self.__solver.add(parent != E) - - self.__solver.add( - self.__subtree_size_grid[y][x] == Sum(*subtree_size_terms) - ) + for p in self.__locations: + parent = self.__parent_grid[p] + subtree_size_terms = [ + If(parent != X, 1, 0) + ] + + sp = p.translate(Vector(-1, 0)) + if sp in self.__parent_grid: + constrain_side(p, sp, S) + subtree_size_terms.append(subtree_size_term(sp, S)) + else: + self.__solver.add(parent != N) + + sp = p.translate(Vector(1, 0)) + if sp in self.__parent_grid: + constrain_side(p, sp, N) + subtree_size_terms.append(subtree_size_term(sp, N)) + else: + self.__solver.add(parent != S) + + sp = p.translate(Vector(0, -1)) + if sp in self.__parent_grid: + constrain_side(p, sp, E) + subtree_size_terms.append(subtree_size_term(sp, E)) + else: + self.__solver.add(parent != W) + + sp = p.translate(Vector(0, 1)) + if sp in self.__parent_grid: + constrain_side(p, sp, W) + subtree_size_terms.append(subtree_size_term(sp, W)) + else: + self.__solver.add(parent != E) + + self.__solver.add( + self.__subtree_size_grid[p] == Sum(*subtree_size_terms) + ) - def location_to_region_id(self, location: Tuple[int, int]) -> int: + def location_to_region_id(self, location: Point) -> int: """Returns the region root ID for a grid location. # Arguments - location (Tuple[int, int]): The (y, x) grid location. + location (Tuple[int, int]): The grid location. # Returns (int): The region ID. """ - y, x = location - return y * self.__width + x + return self.__location_to_region_id[location] - def region_id_to_location(self, region_id: int) -> Tuple[int, int]: + def region_id_to_location(self, region_id: int) -> Point: """Returns the grid location for a region root ID. # Arguments @@ -212,7 +199,7 @@ def region_id_to_location(self, region_id: int) -> Tuple[int, int]: # Returns (Tuple[int, int]): The (y, x) grid location. """ - return divmod(region_id, self.__width) + return self.__locations[region_id] @property def solver(self) -> Solver: @@ -220,8 +207,8 @@ def solver(self) -> Solver: return self.__solver @property - def region_id_grid(self) -> List[List[ArithRef]]: - """(List[List[ArithRef]]): A grid of numbers identifying regions. + def region_id_grid(self) -> Dict[Point, ArithRef]: + """(Dict[Point, ArithRef]): A dictionary of numbers identifying regions. A region's identifier is the position in the grid (going in order from left to right, top to bottom) of the root of that region's subtree. @@ -229,13 +216,13 @@ def region_id_grid(self) -> List[List[ArithRef]]: return self.__region_id_grid @property - def region_size_grid(self) -> List[List[ArithRef]]: - """(List[List[ArithRef]]): A grid of region sizes.""" + def region_size_grid(self) -> Dict[Point, ArithRef]: + """(Dict[Point, ArithRef]): A dictionary of region sizes.""" return self.__region_size_grid @property - def parent_grid(self) -> List[List[ArithRef]]: - """(List[List[ArithRef]]): A grid of region subtree parent pointers. + def parent_grid(self) -> Dict[Point, ArithRef]: + """(Dict[Point, ArithRef]): A dictionary of region subtree parent pointers. The values that may be present in this grid are the module attributes #X, #R, #N, #E, #S, and #W. @@ -243,8 +230,8 @@ def parent_grid(self) -> List[List[ArithRef]]: return self.__parent_grid @property - def subtree_size_grid(self) -> List[List[ArithRef]]: - """(List[List[ArithRef]]): A grid of cell subtree sizes. + def subtree_size_grid(self) -> Dict[Point, ArithRef]: + """(Dict[Point, ArithRef]): A dictionary of cell subtree sizes. A cell's subtree size is one plus the number of cells that are descendents of the cell in its region's subtree. @@ -265,9 +252,18 @@ def print_trees(self): W: chr(0x25C2), } model = self.__solver.model() - for row in self.__parent_grid: - for v in row: - sys.stdout.write(labels[model.eval(v).as_long()]) + min_y = min(p.y for p in self.__parent_grid) + min_x = min(p.x for p in self.__parent_grid) + max_y = max(p.y for p in self.__parent_grid) + max_x = max(p.x for p in self.__parent_grid) + for y in range(min_y, max_y + 1): + for x in range(min_x, max_x + 1): + p = Point(y, x) + if p not in self.__parent_grid: + sys.stdout.write(" ") + else: + v = self.__parent_grid[p] + sys.stdout.write(labels[model.eval(v).as_long()]) print() def print_subtree_sizes(self): @@ -276,9 +272,18 @@ def print_subtree_sizes(self): Should be called only after the solver has been checked. """ model = self.__solver.model() - for row in self.__subtree_size_grid: - for v in row: - sys.stdout.write(f"{model.eval(v).as_long():3}") + min_y = min(p.y for p in self.__subtree_size_grid) + min_x = min(p.x for p in self.__subtree_size_grid) + max_y = max(p.y for p in self.__subtree_size_grid) + max_x = max(p.x for p in self.__subtree_size_grid) + for y in range(min_y, max_y + 1): + for x in range(min_x, max_x + 1): + p = Point(y, x) + if p not in self.__subtree_size_grid: + sys.stdout.write(" ") + else: + v = self.__subtree_size_grid[p] + sys.stdout.write(f"{model.eval(v).as_long():3}") print() def print_region_ids(self): @@ -287,9 +292,18 @@ def print_region_ids(self): Should be called only after the solver has been checked. """ model = self.__solver.model() - for row in self.__region_id_grid: - for v in row: - sys.stdout.write(f"{model.eval(v).as_long():3}") + min_y = min(p.y for p in self.__region_id_grid) + min_x = min(p.x for p in self.__region_id_grid) + max_y = max(p.y for p in self.__region_id_grid) + max_x = max(p.x for p in self.__region_id_grid) + for y in range(min_y, max_y + 1): + for x in range(min_x, max_x + 1): + p = Point(y, x) + if p not in self.__region_id_grid: + sys.stdout.write(" ") + else: + v = self.__region_id_grid[p] + sys.stdout.write(f"{model.eval(v).as_long():3}") print() def print_region_sizes(self): @@ -298,7 +312,16 @@ def print_region_sizes(self): Should be called only after the solver has been checked. """ model = self.__solver.model() - for row in self.__region_size_grid: - for v in row: - sys.stdout.write(f"{model.eval(v).as_long():3}") + min_y = min(p.y for p in self.__region_id_grid) + min_x = min(p.x for p in self.__region_id_grid) + max_y = max(p.y for p in self.__region_id_grid) + max_x = max(p.x for p in self.__region_id_grid) + for y in range(min_y, max_y + 1): + for x in range(min_x, max_x + 1): + p = Point(y, x) + if p not in self.__region_size_grid: + sys.stdout.write(" ") + else: + v = self.__region_size_grid[p] + sys.stdout.write(f"{model.eval(v).as_long():3}") print() diff --git a/grilops/shapes.py b/grilops/shapes.py index 4b5da0f..2cbbfac 100644 --- a/grilops/shapes.py +++ b/grilops/shapes.py @@ -1,77 +1,76 @@ """This module supports puzzles that place fixed shape regions into the grid.""" import sys -from typing import List, Tuple +from typing import Dict, List from z3 import And, ArithRef, If, Int, Or, Solver, Sum, PbEq # type: ignore +from .grids import Point, Vector -def rotate_shape_clockwise(shape): - """Returns a new shape coordinate list rotated 90 degrees clockwise. + +def rotate_shape_clockwise(shape: List[Vector]) -> List[Vector]: + """Returns a new shape offset list rotated 90 degrees clockwise. # Arguments: - shape (List[Tuple[int, int]]): A list of (y, x) coordinates defining a shape. + shape (List[Vector]): A list of offsets defining a shape. # Returns: - (List[Tuple[int, int]]): A list of (y, x) coordinates defining the 90-degree + (List[Vector]): A list of offsets defining the 90-degree clockwise rotation of the input shape. """ - return [(x, -y) for y, x in shape] + return [Vector(v.dx, -v.dy) for v in shape] -def reflect_shape_y(shape): - """Returns a new shape coordinate list reflected vertically. +def reflect_shape_y(shape: List[Vector]) -> List[Vector]: + """Returns a new shape offset list reflected vertically. # Arguments: - shape (List[Tuple[int, int]]): A list of (y, x) coordinates defining a shape. + shape (List[Vector]): A list of offsets defining a shape. # Returns: - (List[Tuple[int, int]]): A list of (y, x) coordinates defining the vertical + (List[Vector]): A list of offsets defining the vertical reflection of the input shape. """ - return [(-y, x) for y, x in shape] + return [Vector(-v.dy, v.dx) for v in shape] -def reflect_shape_x(shape): +def reflect_shape_x(shape: List[Vector]) -> List[Vector]: """Returns a new shape coordinate list reflected horizontally. # Arguments: - shape (List[Tuple[int, int]]): A list of (y, x) coordinates defining a shape. + shape (List[Vector]): A list of offsets defining a shape. # Returns: - (List[Tuple[int, int]]): A list of (y, x) coordinates defining the horizontal + (List[Vector]): A list of offsets defining the horizontal reflection of the input shape. """ - return [(y, -x) for y, x in shape] - + return [Vector(v.dy, -v.dx) for v in shape] -def canonicalize_shape(shape): - """Returns a new shape that's canonicalized. - A canonicalized shape is in sorted order and its first point is (0, 0). This - helps with deduplication, since equivalent shapes will be canonicalized - identically. +def canonicalize_shape(shape: List[Vector]) -> List[Vector]: + """Returns a new shape that's canonicalized, i.e., it's in sorted order + and its first offset is Vector(0, 0). This helps with deduplication, + since equivalent shapes will be canonicalized identically. # Arguments: - shape (List[Tuple[int, int]]): A list of (y, x) coordinates defining a shape. + shape (List[Vector]): A list of offsets defining a shape. # Returns: - (List[Tuple[int, int]]): A list of (y, x) coordinates defining the - canonicalized version of the shape, i.e., in sorted order and - with first point (0, 0). + (List[Vector]): A list of offsets defining the canonicalized version + of the shape, i.e., in sorted order and with first offset equal + to Vector(0, 0). """ shape = sorted(shape) - uly, ulx = shape[0] - return [(py - uly, px - ulx) for py, px in shape] + ulv = shape[0] + return [Vector(v.dy - ulv.dy, v.dx - ulv.dx) for v in shape] class ShapeConstrainer: """Creates constraints for placing fixed shape regions into the grid. # Arguments - height (int): The height of the grid. - width (int): The width of the grid. - shapes (List[List[Tuple[int, int]]]): A list of region shape definitions. - Each region shape definition should be a list of (y, x) tuples. + locations (List[Point]): The locations in the grid. + shapes (List[List[Vector]]): A list of region shape definitions. + Each region shape definition should be a list of offsets. The same region shape definition may be included multiple times to indicate the number of times that shape may appear (if allow_copies is false). @@ -90,9 +89,8 @@ class ShapeConstrainer: def __init__( # pylint: disable=R0913 self, - height: int, - width: int, - shapes: List[List[Tuple[int, int]]], + locations: List[Point], + shapes: List[List[Vector]], solver: Solver = None, complete: bool = False, allow_rotations: bool = False, @@ -105,13 +103,15 @@ def __init__( # pylint: disable=R0913 else: self.__solver = Solver() + self.__locations = sorted(locations) + self.__location_to_instance_id = dict((c, i) for i, c in enumerate(self.__locations)) self.__complete = complete self.__allow_copies = allow_copies self.__shapes = shapes self.__variants = self.__make_variants(allow_rotations, allow_reflections) - self.__create_grids(height, width) + self.__create_grids(locations) self.__add_constraints() def __make_variants(self, allow_rotations, allow_reflections): @@ -135,33 +135,27 @@ def __make_variants(self, allow_rotations, allow_reflections): all_variants.append(variants) return all_variants - def __create_grids(self, height: int, width: int): + def __create_grids(self, locations: List[Point]): """Create the grids used to model shape region constraints.""" - self.__shape_type_grid: List[List[ArithRef]] = [] - for y in range(height): - row = [] - for x in range(width): - v = Int(f"scst-{ShapeConstrainer._instance_index}-{y}-{x}") - if self.__complete: - self.__solver.add(v >= 0) - else: - self.__solver.add(v >= -1) - self.__solver.add(v < len(self.__shapes)) - row.append(v) - self.__shape_type_grid.append(row) - - self.__shape_instance_grid: List[List[ArithRef]] = [] - for y in range(height): - row = [] - for x in range(width): - v = Int(f"scsi-{ShapeConstrainer._instance_index}-{y}-{x}") - if self.__complete: - self.__solver.add(v >= 0) - else: - self.__solver.add(v >= -1) - self.__solver.add(v < height * width) - row.append(v) - self.__shape_instance_grid.append(row) + self.__shape_type_grid: Dict[Point, ArithRef] = {} + for p in locations: + v = Int(f"scst-{ShapeConstrainer._instance_index}-{p.y}-{p.x}") + if self.__complete: + self.__solver.add(v >= 0) + else: + self.__solver.add(v >= -1) + self.__solver.add(v < len(self.__shapes)) + self.__shape_type_grid[p] = v + + self.__shape_instance_grid: Dict[Point, ArithRef] = {} + for p in locations: + v = Int(f"scsi-{ShapeConstrainer._instance_index}-{p.y}-{p.x}") + if self.__complete: + self.__solver.add(v >= 0) + else: + self.__solver.add(v >= -1) + self.__solver.add(v < len(locations)) + self.__shape_instance_grid[p] = v def __add_constraints(self): self.__add_grid_agreement_constraints() @@ -171,79 +165,76 @@ def __add_constraints(self): self.__add_single_copy_constraints(shape_index, shape) def __add_grid_agreement_constraints(self): - for y in range(len(self.__shape_type_grid)): - for x in range(len(self.__shape_type_grid[0])): - self.__solver.add( - Or( - And( - self.__shape_type_grid[y][x] == -1, - self.__shape_instance_grid[y][x] == -1 - ), - And( - self.__shape_type_grid[y][x] != -1, - self.__shape_instance_grid[y][x] != -1 - ) - ) - ) + for p in self.__shape_type_grid: + self.__solver.add( + Or( + And( + self.__shape_type_grid[p] == -1, + self.__shape_instance_grid[p] == -1 + ), + And( + self.__shape_type_grid[p] != -1, + self.__shape_instance_grid[p] != -1 + ) + ) + ) def __add_shape_instance_constraints(self): - for gy in range(len(self.__shape_instance_grid)): - for gx in range(len(self.__shape_instance_grid[0])): - instance_id = gy * len(self.__shape_instance_grid[0]) + gx - instance_size = Sum(*[ - If(c == instance_id, 1, 0) - for row in self.__shape_instance_grid - for c in row - ]) - - or_terms = [self.__shape_instance_grid[gy][gx] == -1] - for shape_index, variants in enumerate(self.__variants): - for variant in variants: - or_terms.extend(self.__make_instance_constraints_for_variant( - gy, gx, shape_index, variant, instance_size)) - self.__solver.add(Or(*or_terms)) + for gp in self.__shape_instance_grid: + instance_id = self.__location_to_instance_id[gp] + instance_size = Sum(*[ + If(v == instance_id, 1, 0) + for v in self.__shape_instance_grid.values() + ]) + + or_terms = [self.__shape_instance_grid[gp] == -1] + for shape_index, variants in enumerate(self.__variants): + for variant in variants: + or_terms.extend(self.__make_instance_constraints_for_variant( + gp, shape_index, variant, instance_size)) + self.__solver.add(Or(*or_terms)) # pylint: disable=R0913,R0914 def __make_instance_constraints_for_variant( - self, gy, gx, shape_index, variant, instance_size): + self, gp, shape_index, variant, instance_size): or_terms = [] - # Identify an instance by its first defined coordinate. - sidy, sidx = variant[0] - for (sry, srx) in variant: - # Find the id coordinate when (sry, srx) is at (gy, gx). - gidy, gidx = gy - (sry - sidy), gx - (srx - sidx) - instance_id = gidy * len(self.__shape_instance_grid[0]) + gidx + for srv in variant: + # Find the instance ID when srv offsets to gp. Since + # the instance ID is the ID of the point corresponding + # to that first-defined offset, and the variant's + # first-defined offset is always Vector(0, 0), + # we can compute the point as gp - srv. + gidp = Point(gp.y - srv.dy, gp.x - srv.dx) + if gidp not in self.__location_to_instance_id: + continue + instance_id = self.__location_to_instance_id[gidp] constraint = self.__make_instance_constraint_for_variant_coordinate( - gy, gx, sry, srx, shape_index, variant, instance_id) - if gy == gidy and gx == gidx: + gp, srv, shape_index, variant, instance_id) + if gp == gidp: constraint = And(constraint, instance_size == len(variant)) or_terms.append(constraint) return or_terms # pylint: disable=R0913 def __make_instance_constraint_for_variant_coordinate( - self, gy, gx, sry, srx, shape_index, variant, instance_id): + self, gp, srv, shape_index, variant, instance_id): and_terms = [] - for (spy, spx) in variant: - gpy, gpx = gy - (sry - spy), gx - (srx - spx) - if gpy < 0 or gpy >= len(self.__shape_instance_grid): - return False - if gpx < 0 or gpx >= len(self.__shape_instance_grid[0]): + for spv in variant: + p = Point(gp.y - (srv.dy - spv.dy), gp.x - (srv.dx - spv.dx)) + if p not in self.__shape_instance_grid: return False and_terms.append( And( - self.__shape_instance_grid[gpy][gpx] == instance_id, - self.__shape_type_grid[gpy][gpx] == shape_index + self.__shape_instance_grid[p] == instance_id, + self.__shape_type_grid[p] == shape_index ) ) return And(*and_terms) def __add_single_copy_constraints(self, shape_index, shape): sum_terms = [] - for y in range(len(self.__shape_type_grid)): - for x in range(len(self.__shape_type_grid[0])): - sum_terms.append( - (self.__shape_type_grid[y][x] == shape_index, 1)) + for p in self.__shape_type_grid: + sum_terms.append((self.__shape_type_grid[p] == shape_index, 1)) self.__solver.add(PbEq(sum_terms, len(shape))) @property @@ -252,8 +243,8 @@ def solver(self) -> Solver: return self.__solver @property - def shape_type_grid(self) -> List[List[ArithRef]]: - """(List[List[ArithRef]]): A grid of z3 constants of shape types. + def shape_type_grid(self) -> Dict[Point, ArithRef]: + """(Dict[Point, ArithRef]): A dictionary of z3 constants of shape types. Each cell contains the index of the shape type placed in that cell (as indexed by the shapes list passed in to the #ShapeConstrainer constructor), @@ -262,8 +253,8 @@ def shape_type_grid(self) -> List[List[ArithRef]]: return self.__shape_type_grid @property - def shape_instance_grid(self) -> List[List[ArithRef]]: - """(List[List[ArithRef]]): A grid of z3 constants of shape instance IDs. + def shape_instance_grid(self) -> Dict[Point, ArithRef]: + """(Dict[Point, ArithRef]): A dictionary of z3 constants of shape instance IDs. Each cell contains a number shared among all cells containing the same instance of the shape, or -1 if no shape is placed within that cell. @@ -276,9 +267,17 @@ def print_shape_types(self): Should be called only after the solver has been checked. """ model = self.__solver.model() - for row in self.__shape_type_grid: - for v in row: - shape_index = model.eval(v).as_long() + min_y = min(p.y for p in self.__shape_type_grid) + min_x = min(p.x for p in self.__shape_type_grid) + max_y = max(p.y for p in self.__shape_type_grid) + max_x = max(p.x for p in self.__shape_type_grid) + for y in range(min_y, max_y + 1): + for x in range(min_x, max_x + 1): + p = Point(y, x) + shape_index = -1 + if p in self.__shape_type_grid: + v = self.__shape_type_grid[p] + shape_index = model.eval(v).as_long() if shape_index >= 0: sys.stdout.write(f"{shape_index:3}") else: @@ -291,11 +290,19 @@ def print_shape_instances(self): Should be called only after the solver has been checked. """ model = self.__solver.model() - for row in self.__shape_instance_grid: - for v in row: - shape_index = model.eval(v).as_long() - if shape_index >= 0: - sys.stdout.write(f"{shape_index:3}") + min_y = min(p.y for p in self.__shape_instance_grid) + min_x = min(p.x for p in self.__shape_instance_grid) + max_y = max(p.y for p in self.__shape_instance_grid) + max_x = max(p.x for p in self.__shape_instance_grid) + for y in range(min_y, max_y + 1): + for x in range(min_x, max_x + 1): + p = Point(y, x) + shape_instance = -1 + if p in self.__shape_instance_grid: + v = self.__shape_instance_grid[p] + shape_instance = model.eval(v).as_long() + if shape_instance >= 0: + sys.stdout.write(f"{shape_instance:3}") else: sys.stdout.write(" ") print() diff --git a/grilops/sightlines.py b/grilops/sightlines.py index 349eea2..ed1fb1a 100644 --- a/grilops/sightlines.py +++ b/grilops/sightlines.py @@ -6,16 +6,16 @@ also have a custom counting or accumulation function. """ -from typing import Callable, Tuple, TypeVar +from typing import Callable, TypeVar from z3 import ArithRef, BoolRef, If # type: ignore -from .grids import SymbolGrid +from .grids import Point, SymbolGrid, Vector def count_cells( symbol_grid: SymbolGrid, - start: Tuple[int, int], - direction: Tuple[int, int], + start: Point, + direction: Vector, count: Callable[[int], ArithRef] = lambda c: 1, stop: Callable[[int], BoolRef] = lambda c: False ): @@ -23,10 +23,10 @@ def count_cells( # Arguments symbol_grid (SymbolGrid): The SymbolGrid to check against. - start (Tuple[int, int]): The (y, x) coordinate of the cell where the sightline - should begin. This is the first cell checked. - direction (Tuple[int, int]): The (delta-y, delta-x) distance to advance to - reach the next cell in the sightline. + start (Point): The location of the cell where the sightline should begin. + This is the first cell checked. + direction (Vector): The direction to advance to reach the next cell in the + sightline. count (Callable[[int], ArithRef]): A function that accepts a symbol as an argument and returns the integer value to add to the count when this symbol is encountered. By default, each symbol will count with a value of @@ -51,8 +51,8 @@ def count_cells( def reduce_cells( # pylint: disable=R0913 symbol_grid: SymbolGrid, - start: Tuple[int, int], - direction: Tuple[int, int], + start: Point, + direction: Vector, initializer: Accumulator, accumulate: Callable[[Accumulator, int], Accumulator], stop: Callable[[Accumulator, int], BoolRef] = lambda a, c: False, @@ -61,10 +61,10 @@ def reduce_cells( # pylint: disable=R0913 # Arguments symbol_grid (SymbolGrid): The SymbolGrid to check against. - start (Tuple[int, int]): The (y, x) coordinate of the cell where the sightline - should begin. This is the first cell checked. - direction (Tuple[int, int]): The (delta-y, delta-x) distance to advance to - reach the next cell in the sightline. + start (Point): The location of the cell where the sightline should begin. + This is the first cell checked. + direction (Vector): The direction to advance to reach the next cell in the + sightline. initializer (Accumulator): The initial value for the accumulator. accumulate (Callable[[Accumulator, int], Accumulator]): A function that accepts an accumulated value and a symbol as arguments, and returns a new @@ -79,16 +79,13 @@ def reduce_cells( # pylint: disable=R0913 """ stop_terms = [] acc_terms = [initializer] - y, x = start - while ( - 0 <= y < len(symbol_grid.grid) and 0 <= x < len(symbol_grid.grid[0]) - ): - cell = symbol_grid.grid[y][x] + p = start + while p in symbol_grid.grid: + cell = symbol_grid.grid[p] acc_term = accumulate(acc_terms[-1], cell) acc_terms.append(acc_term) stop_terms.append(stop(acc_term, cell)) - y += direction[0] - x += direction[1] + p = p.translate(direction) expr = acc_terms.pop() for stop_term, acc_term in zip(reversed(stop_terms), reversed(acc_terms)): expr = If(stop_term, acc_term, expr) diff --git a/test/golden/shape.py.txt b/test/golden/shape.py.txt new file mode 100644 index 0000000..0c49926 --- /dev/null +++ b/test/golden/shape.py.txt @@ -0,0 +1,13 @@ +████████ + +████ +██ ████ +██ ████ + + 0 0 0 0 + + 1 1 + 1 2 2 + 1 2 2 + +Unique solution diff --git a/test/golden/statue_park_loop.py.txt b/test/golden/statue_park_loop.py.txt new file mode 100644 index 0000000..5cd98e3 --- /dev/null +++ b/test/golden/statue_park_loop.py.txt @@ -0,0 +1,27 @@ + • ◦ + ◦ • +◦ • + + +• • + ◦ +X • ◦ + ┌┐ + ┌─┐││ +┌┘ └┘└┐ +│ ┌┐└┐ +└┐ ┌┘└─┘ + └┐└┐ + └┐└─┐ + └──┘ + + 0 0 0 0 3 3 + 0 3 3 + 2 3 + 2 2 2 + 2 + 1 4 4 4 + 1 1 4 + 1 1 4 + +Unique solution