-
Notifications
You must be signed in to change notification settings - Fork 5
/
hexalgemy.py
119 lines (100 loc) · 3.28 KB
/
hexalgemy.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
from z3 import *
from hexgrid import HexGrid, coord_add
from hex_display import draw_grid
from invalidobj import Invalid, IAnd, IOr
from functools import reduce
givens = [
' ',
' ',
' Y N ',
' 0 ',
' ',
' NO ',
' '
]
height, width, west_row, east_row = 7, 7, 3, 3
composite_allowed = False
# givens = [
# '0 ',
# ' B ',
# ' B'
# ]
# height, width, west_row, east_row = 3, 3, 1, 1
# composite_allowed = False
ColorSort, ColorVal, (R, Y, B) = TupleSort('Color', [BoolSort(), BoolSort(), BoolSort()])
def Color(name):
return Const(name, ColorSort)
given_values = {
'0': (False, False, False),
'B': (False, False, True),
'Y': (False, True, False),
'G': (False, True, True),
'R': (True, False, False),
'V': (True, False, True),
'O': (True, True, False),
'N': (True, True, True)
}
def combine_colors(left, right):
return ColorVal(Or(R(left), R(right)), Or(Y(left), Y(right)), Or(B(left), B(right)))
def combine_all_colors(list):
return reduce(combine_colors, list, ColorVal(False, False, False))
g = HexGrid(height, width, west_row, east_row, cellgen=Color)
s = Solver()
dirs = [
(1,-1,0),
(1,0,-1),
(-1,1,0),
(-1,0,1),
(0,1,-1),
(0,-1,1)
]
def seen_from(cell):
yield cell
for dir in dirs:
here = g.cell(*coord_add(cell.coords, dir))
while not isinstance(here, Invalid) and here.given == ' ':
yield here
here = g.cell(*coord_add(here.coords, dir))
for (givenrow, cellrow) in zip(givens, g.rows):
for (given, cell) in zip(givenrow, cellrow):
cell.given = given
for cell in g.cells:
if cell.given != ' ':
# no lights in givens
s.add(cell.var == ColorVal(False, False, False))
# given must see correct color
s.add(combine_all_colors([other.var for other in seen_from(cell)]) == ColorVal(*given_values[cell.given]))
else:
# only allow proper colors
if composite_allowed:
s.add(AtMost(R(cell.var), Y(cell.var), B(cell.var), 2))
else:
s.add(AtMost(R(cell.var), Y(cell.var), B(cell.var), 1))
# all cells must see a light of some kind
if cell.given != '0':
s.add(IOr([other.var != ColorVal(False, False, False) for other in seen_from(cell)]))
# no two lights can see each other
s.add(IOr([cell.var == ColorVal(False, False, False), IAnd([other.var == ColorVal(False, False, False) for other in seen_from(cell) if other != cell])]))
s.check()
print(s.model())
def draw_edge(ctx):
ctx.draw()
colors = {
(False, False, False): (0.8, 0.8, 0.8, 0.8),
(False, False, True): (0, 0, 1, 1),
(False, True, False): (1, 1, 0, 1),
(False, True, True): (0, 1, 0, 1),
(True, False, False): (1, 0, 0, 1),
(True, False, True): (1, 0, 1, 1),
(True, True, False): (1, 0.5, 0, 1),
(True, True, True): (0.5, 0.2, 0, 1)
}
def draw_cell(ctx):
if ctx.cell.given != ' ':
color = colors[given_values[ctx.cell.given]]
ctx.fill(*color)
else:
color = ctx.model[ctx.cell.var]
realcolor = colors[(bool(ctx.model.eval(R(color))), bool(ctx.model.eval(Y(color))), bool(ctx.model.eval(B(color))))]
ctx.circle(color=realcolor, fill=True)
draw_grid(g, s.model(), 30, cell_fn=draw_cell, edge_fn=draw_edge)