You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
160 lines
4.4 KiB
160 lines
4.4 KiB
# coding: utf-8
|
|
import os, sys
|
|
from z3 import *
|
|
|
|
from itertools import combinations
|
|
|
|
pretty_print = True
|
|
|
|
# get the playground information
|
|
if len(sys.argv) != 2:
|
|
print("Usage: python3 seating-arrangement.py <wedding-file>")
|
|
sys.exit(0)
|
|
|
|
def faulty_line(line, num):
|
|
print("Faulty input at line " + str(num) + ". Ignoring '" + line + "'")
|
|
|
|
# data structures prepared for you
|
|
guests = set()
|
|
friends = []
|
|
foes = []
|
|
longest_name_len = 0
|
|
|
|
def add_to_guest_list(a,b=None):
|
|
guests.add(a)
|
|
if b != None:
|
|
guests.add(b)
|
|
|
|
def longest_name(a,b=None):
|
|
global longest_name_len
|
|
if len(a) > longest_name_len: longest_name_len = len(a)
|
|
if b != None and len(b) > longest_name_len : longest_name_len = len(b)
|
|
|
|
solver = Solver()
|
|
|
|
################################### Parse Guests and Constraints ####################################
|
|
|
|
Guest = DeclareSort("Guest")
|
|
|
|
with open(sys.argv[1]) as f:
|
|
wedding = f.read()
|
|
wedding = wedding.strip().split("\n")
|
|
linenum = 0
|
|
for line in wedding:
|
|
linenum += 1
|
|
if line[0] == '#':
|
|
continue
|
|
if line.rstrip():
|
|
info = line.split(" ")
|
|
|
|
if len(info) == 1:
|
|
guest = Const(info[0], Guest)
|
|
add_to_guest_list(guest)
|
|
longest_name(info[0])
|
|
continue
|
|
|
|
if len(info) != 3:
|
|
faulty_line(line, linenum)
|
|
continue
|
|
|
|
longest_name(info[0], info[2])
|
|
if info[1] == "dislikes":
|
|
first_guest = Const(info[0], Guest)
|
|
second_guest = Const(info[2], Guest)
|
|
add_to_guest_list(first_guest, second_guest)
|
|
# todo add the pair of guests as foes
|
|
elif info[1] == "likes":
|
|
first_guest = Const(info[0], Guest)
|
|
second_guest = Const(info[2], Guest)
|
|
add_to_guest_list(first_guest, second_guest)
|
|
# todo add pair of guests as friends
|
|
else:
|
|
faulty_line(line, linenum)
|
|
continue
|
|
|
|
################################### Wedding Guests ####################################
|
|
|
|
# todo create an uninterpreted function from the Guest sort to an IntSort()
|
|
|
|
# todo create a function which returns whether two guests are sitting next to each other
|
|
def neigbours(a, b):
|
|
pass
|
|
|
|
# todo all guests must be seated at the big table
|
|
# check the indices here
|
|
for guest in guests:
|
|
pass
|
|
|
|
# todo no two guests should sit on the same position
|
|
for combination in combinations(guests,2): #todo
|
|
pass
|
|
|
|
#todo friends should be neigbours
|
|
for (a,b) in friends: #todo
|
|
pass
|
|
|
|
#todo foes should not be neigbours
|
|
for (a,b) in foes: # todo
|
|
pass
|
|
|
|
# check satisfiability
|
|
res = solver.check()
|
|
if res != sat:
|
|
print("unsat")
|
|
sys.exit(1)
|
|
m = solver.model()
|
|
|
|
################################################################################
|
|
|
|
|
|
arrangement = ["" for guest in range(len(guests))]
|
|
for guest in guests:
|
|
arrangement[m.evaluate(position(guest),model_completion=True).as_long()] = guest.decl().name()
|
|
|
|
def print_table():
|
|
side_length = round(len(guests)/4)
|
|
top = arrangement[0:side_length]
|
|
right = arrangement[side_length:2*side_length]
|
|
bottom = arrangement[2*side_length:3*side_length]
|
|
left = arrangement[3*side_length:]
|
|
while len(left) < len(right):
|
|
left.append("")
|
|
while len(right) < len(left):
|
|
right.append("")
|
|
table_line_length = longest_name_len + 1
|
|
|
|
print("\n")
|
|
|
|
top_row = ""
|
|
top_row += (longest_name_len + 1) * " "
|
|
for top_guest in top:
|
|
top_row += top_guest + " "
|
|
table_line_length += len(top_guest) + 1
|
|
print(top_row)
|
|
print((longest_name_len + 1) * " " + table_line_length * "-")
|
|
|
|
first_element = True
|
|
for left_guest, right_guest in zip(reversed(left), right):
|
|
row = ""
|
|
if not first_element:
|
|
row += longest_name_len * " "
|
|
row += "|" + ">"* (table_line_length) + "|"
|
|
print(row)
|
|
row = ""
|
|
else:
|
|
first_element = False
|
|
row += left_guest.rjust(longest_name_len) + "|" + "<"* (table_line_length) + "|" + right_guest
|
|
print(row)
|
|
|
|
print((longest_name_len + 1) * " " + table_line_length * "-")
|
|
bottom_row = ""
|
|
bottom_row += (longest_name_len + 1) * " "
|
|
for bottom_guest in reversed(bottom):
|
|
bottom_row += bottom_guest + " "
|
|
print(bottom_row)
|
|
print("\n")
|
|
|
|
if(pretty_print):
|
|
print_table()
|
|
print("Seating plan:")
|
|
print(arrangement)
|