From 3ad6fb6f1d34b698237a3bc74601131b641cceb5 Mon Sep 17 00:00:00 2001 From: sp Date: Fri, 17 Mar 2023 13:56:48 +0100 Subject: [PATCH] added exercise for second assignment sheet --- Assignment2/colours.py | 114 ++++++++++++++++++++ Assignment2/seating-arrangement.py | 160 +++++++++++++++++++++++++++++ 2 files changed, 274 insertions(+) create mode 100644 Assignment2/colours.py create mode 100644 Assignment2/seating-arrangement.py diff --git a/Assignment2/colours.py b/Assignment2/colours.py new file mode 100644 index 0000000..00a10d2 --- /dev/null +++ b/Assignment2/colours.py @@ -0,0 +1,114 @@ +# coding: utf-8 import os, sys +from z3 import * + +# get the playground information +if len(sys.argv) != 2: + print("Usage: python3 colours.py ") + sys.exit(0) + +with open(sys.argv[1]) as f: + playground = f.read() +playground = playground.strip().split("\n") + +# get the playground size +size_y = len(playground) +assert(size_y != 0) +size_x = len(playground[0]) +assert(size_x != 0) +assert(all([len(p) == size_x for p in playground])) +# get the number of regions +regions = set("".join(playground)) + +################################### Colours #################################### + +# create the solver +solver = Solver() + +# todo: create a datatype Colour +# ... +# todo: declare four valid colours +# ... +# hint: don't forget to call "create" for the datatype to get a Sort +# ... + +# todo: create a colour variable for each playground cell +# hint: you can do this with Const("var_name", YourSort) +# hint: use something like the coordinates as part of the variable name +p_colours = [[None for _j in range(size_x)] for _j in range(size_y)] +for i in range(size_y): + for j in range(size_x): + # p_colours[i][j] = ... replace this with your code + pass + +print("All regions found in this map: '{}'.".format(",".join(regions))) +for r in regions: + # todo: find all cells that belong to the same region + region_vars = [] + for i in range(size_y): + for j in range(size_x): + pass # ... add the variable to region_vars here + + # todo: make all colours in the same region identical + # hint: use the transitivitiy of equality x1 = x2 & x2 = x3 -> x1 = x3 + for c in range(len(region_vars) - 1): + pass # ... replace this with your code ... + + +def get_neighbours(i, j): + regions = [] + colours = [] + if i > 0: + colours.append( p_colours[i-1][j]) + regions.append(playground[i-1][j]) + if i < size_y - 1: + colours.append( p_colours[i+1][j]) + regions.append(playground[i+1][j]) + if j > 0: + colours.append( p_colours[i][j-1]) + regions.append(playground[i][j-1]) + if j < size_x - 1: + colours.append( p_colours[i][j+1]) + regions.append(playground[i][j+1]) + return zip(regions, colours) + + +# todo: if two neighboring cells are from different regions +# then they must have different colours +for i in range(size_y): + for j in range(size_x): + cell_r = playground[i][j] + cell_c = p_colours[i][j] + for r, c in get_neighbours(i, j): + pass # ... replace this with your code ... + +# call the solver and check satisfiability +res = solver.check() +if res != sat: + print("unsat") + sys.exit(1) + +# todo make a translation to strings "1", "2", "3", "4" +def translate(s): + # hint: do something analogouns to the following line here + # if s.sexpr() == "C1": return "1" + # ... + return "0" + +################################################################################ + +from colorama import Fore, Back, Style +cols = [Back.BLACK, Back.RED, Back.GREEN, Back.BLUE, Back.MAGENTA] +cols = [Style.BRIGHT + Fore.WHITE + c for c in cols] + +# print the model as translated numbers +m = solver.model() +names = [x.name() for x in m.decls()] +for i in range(size_y): + row = "" + for j in range(size_x): + pc = p_colours[i][j] + invalid = (pc is None or pc.decl() not in m.decls()) + t = "0" if invalid else translate(m[pc]) + if sys.stdout.isatty(): t = cols[int(t)] + t + Style.RESET_ALL + row += t + print(row) diff --git a/Assignment2/seating-arrangement.py b/Assignment2/seating-arrangement.py new file mode 100644 index 0000000..a508768 --- /dev/null +++ b/Assignment2/seating-arrangement.py @@ -0,0 +1,160 @@ +# 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 ") + 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)