# 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()
                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)