From a38e6b1866e189775fc5f933ea7ed52e9d6d6da6 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Tue, 26 Nov 2024 10:33:01 +0100
Subject: [PATCH] added empty scripts for lecture 2

---
 Lecture2/example-colours.py           | 32 +++++++++++
 Lecture2/example-maestria-in-class.py | 77 +++++++++++++++++++++++++++
 Lecture2/example_xkcd_287.py          | 15 ++++++
 3 files changed, 124 insertions(+)
 create mode 100644 Lecture2/example-colours.py
 create mode 100644 Lecture2/example-maestria-in-class.py
 create mode 100644 Lecture2/example_xkcd_287.py

diff --git a/Lecture2/example-colours.py b/Lecture2/example-colours.py
new file mode 100644
index 0000000..79011e7
--- /dev/null
+++ b/Lecture2/example-colours.py
@@ -0,0 +1,32 @@
+from itertools import combinations
+from z3 import *
+
+solver = Solver()
+
+Colours = Datatype("Colours")
+Colours.declare("RED")
+Colours.declare("BLUE")
+Colours.declare("GREEN")
+Colours.declare("YELLOW")
+
+Colour = Colours.create()
+f    = Function('f', IntSort(), Colour)
+
+variables = list()
+for i in range(0,5):
+    variables.append(Int(i))
+    solver.add(0 <= variables[-1])
+    solver.add(variables[-1] <= 5)
+
+solver.add(Distinct(variables))
+
+"""
+|cell 1|cell 2|cell 3|cell 4|cell 5|
+
+"""
+
+# neighbouring cells needs to be coloured differently
+
+result = solver.check()
+if result == sat:
+    print(solver.model())
diff --git a/Lecture2/example-maestria-in-class.py b/Lecture2/example-maestria-in-class.py
new file mode 100644
index 0000000..d56a341
--- /dev/null
+++ b/Lecture2/example-maestria-in-class.py
@@ -0,0 +1,77 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+import string
+# get the playground information
+directory = os.path.dirname(os.path.realpath(__file__))
+fname = directory + "/" + "level0.txt"
+
+if len(sys.argv) == 2:
+    fname = sys.argv[1]
+
+with open(fname) as f:
+    playground = f.read()
+playground = [[c for c in row] for row in 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)
+for row in playground:
+    assert(len(row) == size_x)
+
+bells = {}
+for i in range(size_y):
+    for j in range(size_x):
+        c = playground[i][j]
+        if ord(c) in range(ord("1"), ord("9") + 1):
+            assert(int(c) not in bells.keys())
+            bells[int(c)] = (j, i)
+
+################################### Maestria ###################################
+
+
+print(f"Playground size : {size_x} x {size_y}")
+print("Playground:")
+print("\n".join(["".join(i) for i in playground]))
+print("Bell positions:")
+print(bells)
+print("\n")
+
+# create the solver
+solver = Solver()
+
+fudge_x, fudge_y = Ints("fudge_x fudge_y")
+
+
+# call the solver and check satisfiability
+while solver.check() == sat:
+    m = solver.model()
+    if fudge_x is not None and fudge_y is not None:
+        pos_x = m[fudge_x].as_long()
+        pos_y = m[fudge_y].as_long()
+        playground[pos_y][pos_x] = "F"
+        solver.add(Or(fudge_x != pos_x, fudge_y != pos_y))
+
+################################################################################
+
+from colorama import Fore, Back, Style
+
+cols = [Fore.BLUE, Fore.GREEN, Fore.RED, Fore.YELLOW, Fore.MAGENTA, Fore.CYAN]
+tones = [Style.BRIGHT, Style.DIM]
+cols = sum([[c + t for c in cols] for t in tones], [])
+
+if sys.stdout.isatty():
+    for bell in sorted(list(bells.keys())):
+        x, y = bells[bell]
+        playground[y][x] = Back.BLACK + cols[bell - 1] + playground[y][x] + Style.RESET_ALL
+    for y in range(size_y):
+        for x in range(size_x):
+            c = playground[y][x]
+            if c == "_": playground[y][x] = Fore.BLACK + Back.WHITE + c + Style.RESET_ALL
+            if c == "X": playground[y][x] = Fore.WHITE + Back.BLACK + c + Style.RESET_ALL
+            if c == "F": playground[y][x] = Fore.BLACK + Back.WHITE + c + Style.RESET_ALL
+
+text = "\n".join(["".join([c for c in row]) for row in playground])
+print(text)
diff --git a/Lecture2/example_xkcd_287.py b/Lecture2/example_xkcd_287.py
new file mode 100644
index 0000000..fdaf6f9
--- /dev/null
+++ b/Lecture2/example_xkcd_287.py
@@ -0,0 +1,15 @@
+#!/usr/bin/python3
+
+from z3 import *
+
+# Prices: 215, 275, 335, 355, 420, 580
+# Sum: 1505
+
+s = Solver()
+
+a,b,c,d,e,f = Ints("a b c d e f")
+
+
+if s.check() == sat:
+    m = s.model()
+    print(m)