diff --git a/ex2/practical_assignment2.pdf b/ex2/practical_assignment2.pdf new file mode 100644 index 0000000..941e502 Binary files /dev/null and b/ex2/practical_assignment2.pdf differ diff --git a/ex2/square.py b/ex2/square.py new file mode 100644 index 0000000..8930575 --- /dev/null +++ b/ex2/square.py @@ -0,0 +1,67 @@ +# coding: utf-8 +import os, sys +from z3 import * + +# get the playground information +if len(sys.argv) != 2: + print("Usage: python3 square.py ") + sys.exit(0) + +with open(sys.argv[1]) as f: + playground = f.read() +rows = playground.strip().split("\n") +playground = [[None if x == "_" else int(x) for x in r.split()] for r in rows] + +# get the playground size +size_y = len(playground) +assert(size_y != 0) +size_x = len(playground[0]) +assert(size_x != 0) +assert(size_x == size_y) + +#################################### Square #################################### + +# create the solver +solver = Solver() + +# todo: create an integer variable for each playground cell +# hint: use something like the coordinates as part of the variable name +numbers = [[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): + pass # ... replace this with your code ... + +# todo: assign each known number the corresponding value from playground +for i in range(size_y): + for j in range(size_x): + pass # ... replace this with your code ... + +# todo: declare a variable for the sum of all columns, rows and diagonals +# ... your code goes here ... + +# todo: enforce that each column sums up to the declared variable +for j in range(size_x): + pass # ... replace this with your code ... + +# todo: enforce that each row sums up to the declared variable +for i in range(size_y): + pass # ... replace this with your code ... + +# todo: enforce that both diagonals sum up to the declared variable + +# call the solver and check satisfiability +res = solver.check() +if res != sat: + print("unsat") + sys.exit(1) + +# print the model +m = solver.model() +for i in range(size_y): + results = [] + for j in range(size_x): + num = numbers[i][j] + results.append("_" if num is None else m[num].as_long()) + print(("%4s" * len(results)) % tuple(results)) + +################################################################################ diff --git a/ex2/test0.txt b/ex2/test0.txt new file mode 100644 index 0000000..515a0e0 --- /dev/null +++ b/ex2/test0.txt @@ -0,0 +1,3 @@ +_ _ 28 +_ 35 21 +_ 7 _ diff --git a/ex2/test1.txt b/ex2/test1.txt new file mode 100644 index 0000000..b046a32 --- /dev/null +++ b/ex2/test1.txt @@ -0,0 +1,4 @@ +_ _ 28 _ +_ 35 21 _ +_ 7 _ _ +_ _ _ _