From 7492bdaeb74a7e7daba312f69e1e923c643b21f1 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Wed, 8 Mar 2023 22:09:31 +0100
Subject: [PATCH] added exercises for assignment one

---
 Assignment1/branchless_min.py | 21 +++++++++++
 Assignment1/square.py         | 70 +++++++++++++++++++++++++++++++++++
 Assignment1/test0.txt         |  3 ++
 Assignment1/transposition.py  | 20 ++++++++++
 4 files changed, 114 insertions(+)
 create mode 100644 Assignment1/branchless_min.py
 create mode 100644 Assignment1/square.py
 create mode 100644 Assignment1/test0.txt
 create mode 100644 Assignment1/transposition.py

diff --git a/Assignment1/branchless_min.py b/Assignment1/branchless_min.py
new file mode 100644
index 0000000..b0b77bc
--- /dev/null
+++ b/Assignment1/branchless_min.py
@@ -0,0 +1,21 @@
+# coding: utf-8
+from z3 import *
+
+# Create an instance of a z3 solver
+
+solver = Solver()
+
+min_ite = BitVec("min", 32)
+x = BitVec("x", 32)
+y = BitVec("y", 32)
+# Declare additional z3 variables
+
+solver.add(min_ite == If(x < y, x, y))
+
+# solver.add(...)
+
+# Check and print the result.
+result = solver.check()
+print(result)
+if result == sat:
+    print(solver.model())
diff --git a/Assignment1/square.py b/Assignment1/square.py
new file mode 100644
index 0000000..de352b7
--- /dev/null
+++ b/Assignment1/square.py
@@ -0,0 +1,70 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+
+# get the playground information
+if len(sys.argv) != 2:
+    print("Usage: python3 square.py <test-file>")
+    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: enfoce that each column sums up to the declared variable
+for j in range(size_x):
+    pass # ... replace this with your code ...
+
+# todo: enfoce that each row sums up to the declared variable
+for i in range(size_y):
+    pass # ... replace this with your code ...
+
+# todo: enfoce that both diagonals sum up to the declared variable
+# ... your code goes here ...
+diag1 = [numbers[i][i] for i in range(size_y)]
+diag2 = [numbers[i][size_y - i - 1] for i in range(size_y)]
+
+# 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/Assignment1/test0.txt b/Assignment1/test0.txt
new file mode 100644
index 0000000..515a0e0
--- /dev/null
+++ b/Assignment1/test0.txt
@@ -0,0 +1,3 @@
+_ _ 28
+_ 35 21
+_ 7 _
diff --git a/Assignment1/transposition.py b/Assignment1/transposition.py
new file mode 100644
index 0000000..5dda50b
--- /dev/null
+++ b/Assignment1/transposition.py
@@ -0,0 +1,20 @@
+# coding: utf-8
+from z3 import *
+
+# Create an instance of a z3 solver
+
+solver = None
+
+# Declare needed z3 variables
+
+# Add the needed constraints to check equivalence of the two formulae.
+
+# solver.add(...)
+
+
+# Check and print the result.
+
+result = solver.check()
+print(result)
+if result == sat:
+    print(solver.model())