added exercises for assignment one

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

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

Assignment1/test0.txt

@@ -0,0 +1,3 @@
+_ _ 28
+_ 35 21
+_ 7 _

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