added exercise for second assignment sheet

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 <map-file>")
+    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)

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