|
|
@ -1,3 +1,55 @@ |
|
|
|
# coding: utf-8 |
|
|
|
import os, sys |
|
|
|
from z3 import * |
|
|
|
|
|
|
|
# get the playground information |
|
|
|
if len(sys.argv) != 2: |
|
|
|
print("Usage: python3 trees_and_tents.py <forest-file>") |
|
|
|
|
|
|
|
EMPTY = "?" |
|
|
|
TREE = 2 |
|
|
|
|
|
|
|
if len(sys.argv) == 2: |
|
|
|
fname = sys.argv[1] |
|
|
|
|
|
|
|
with open(fname) as f: |
|
|
|
playground = f.read() |
|
|
|
cols = [col for col in playground.strip().split("\n")[0][1:]] |
|
|
|
rows = [row[0] for row in playground.strip().split("\n")[1:]] |
|
|
|
playground = [[EMPTY if x == EMPTY else x for x in row[1:]] |
|
|
|
for row in playground.strip().split("\n")[1:]] |
|
|
|
|
|
|
|
# get the playground size |
|
|
|
size_y = len(rows) |
|
|
|
assert(size_y != 0) |
|
|
|
size_x = len(cols) |
|
|
|
assert(size_x != 0) |
|
|
|
|
|
|
|
def print_result(model): |
|
|
|
print(" " + ''.join(cols) + " "*5 + ''.join(cols)) |
|
|
|
for i in range(size_y): |
|
|
|
print(rows[i] + " " + ''.join(playground[i]) + " >>> ", end='') |
|
|
|
for j in range(size_x): |
|
|
|
cell = model[cells[i][j]].as_long() |
|
|
|
if cell != TREE: |
|
|
|
print(cell, end='') |
|
|
|
elif cell == TREE: |
|
|
|
print("T", end='') |
|
|
|
print() |
|
|
|
|
|
|
|
def print_forest(): |
|
|
|
print(" " + ''.join(cols)) |
|
|
|
for i in range(size_y): |
|
|
|
print(rows[i] + " ", end='') |
|
|
|
for j in range(size_x): |
|
|
|
cell = playground[i][j] |
|
|
|
if cell != TREE: |
|
|
|
print(cell, end='') |
|
|
|
elif cell == TREE: |
|
|
|
print("T", end='') |
|
|
|
print() |
|
|
|
|
|
|
|
################################# Trees and Tents ################################## |
|
|
|
# create the solver |
|
|
|
cells = [[None for j in range(size_x)] for i in range(size_y)] |
|
|
|
solver = Solver() |
|
|
|