init programming assignment repo

README.md

@@ -0,0 +1,4 @@
+Student 1: Name Surname Matriculation Number
+
+
+Student 2: Name Surname Matriculation Number

branchless_min.py

@@ -0,0 +1,14 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+
+# Create an instance of a z3 solver
+solver = Solver()
+# Declare z3 variables for the needed BitVectors
+
+
+# Check and print the result.
+result = solver.check()
+print(result)
+if result == sat:
+    print(solver.model())

burglars.py

@@ -0,0 +1,31 @@
+# coding: utf-8
+from z3 import *
+
+################################# Burglars ##################################
+# create the solver
+solver = Solver()
+
+#############################################################################
+# (1) Ed: "Fred did it, and Ted is innocent".
+# (2) Fred: "If Ed is guilty , then so is Ted".
+# (3) Ted: "Im innocent, but at least one of the others is guilty".
+#############################################################################
+
+# TODO Create boolean variables for each of the culprits
+# TODO Add constraints to the solver representing the statements from above
+
+# Hint: The statement of a culprit should be true if and only if he is not guilty!
+
+
+
+res = solver.check()
+if res != sat:
+    print("unsat")
+    sys.exit(1)
+
+print(solver)
+m = solver.model()
+for d in m.decls():
+    print("%s -> %s" % (d, m[d]))
+
+print("\n" + str(m))

forest0.txt

@@ -0,0 +1,3 @@
+.10
+0T?
+1??

forest1.txt

@@ -0,0 +1,4 @@
+.1011
+1T???
+1???T
+1???T

forest2.txt

@@ -0,0 +1,7 @@
+.301111
+1T?????
+1??TT??
+2???T??
+1?T????
+1??????
+1?T???T

forest3.txt

@@ -0,0 +1,7 @@
+.021211
+2?T?T??
+0???T??
+2T?????
+0?????T
+3??????
+0?T?T??

rpssl.py

@@ -0,0 +1,123 @@
+# coding: utf-8
+import os, sys, subprocess
+import time
+from z3 import *
+
+CHOICES = ["Rock", "Paper", "Scissors", "Spock", "Lizard"]
+
+def next_random_number(s_i):
+    return ((11 * s_i) + 12345) & 0x7fff
+
+class RPSSLComputer:
+    def __init__(self, s0):
+        self.previous_random_number = s0
+
+    def compute_choice(self):
+        random_number = next_random_number(self.previous_random_number)
+        self.previous_random_number = random_number
+        return random_number % 5, CHOICES[random_number % 5]
+
+
+# cf. https://bigbangtheory.fandom.com/wiki/Rock,_Paper,_Scissors,_Lizard,_Spock
+def winning_mapping(i):
+    if i == 0: return 1#"Paper"
+    if i == 1: return 2#"Scissors"
+    if i == 2: return 0#"Rock"
+    if i == 3: return 4#"Lizard"
+    if i == 4: return 0#"Rock"
+    return "Did you forget to compute the remainder modulo 5?"
+
+def compute_winner(computer, player):
+    if computer == player:
+        return "\tTie.", False
+    is_player_bigger = True if player > computer else False
+    absolute_difference = abs(computer - player)
+    if absolute_difference % 2 == 1:
+        if is_player_bigger:
+            return "\tPlayer wins.", True
+        else:
+            return "\tComputer wins.", False
+    else:
+        if is_player_bigger:
+            return "\tComputer wins.", False
+        else:
+            return "\tPlayer wins.", True
+
+solver = Solver()
+states = list()
+
+# We are adding the first state s_0 to the list of states
+states.append(BitVec("state0", 16))
+
+s0 = int(sys.argv[1])
+computer = RPSSLComputer(s0)
+
+preprocess_count = 5
+
+def add_constraint(solver, index, computers_choice):
+    # TODO create a BitVec and append it to the list of states
+    # You might want to call it state{index}
+
+    # TODO Enforce that the newly added BitVec-variable must evaluate to the result of the LCG computation using the previous result
+
+    # TODO Enforce that the unsigned remainder of the newly added BitVec-varialbe and 5 evaluates to the choice of the computer
+
+    pass
+
+def store_backtracking_point(solver):
+    solver.push()
+
+def restore_backtracking_point(solver):
+    solver.pop()
+
+def add_next_state_constraint(solver):
+    s_i_plus_1 = BitVec("s_i_plus_1", 16)
+    # TODO Enforce that the next state value is computed via the same computation as above
+
+    return s_i_plus_1
+
+def get_players_choice(solver, s_i_plus_1):
+    # TODO Get the value of next_state from the model and return it modulo 5
+    # Hint: winning_mapping(...) returns a good answer for the computer's choice
+    # Hint: use solver.model() like a python dict.
+    # Hint: use `.as_long()` to convert a z3 variable to a python integer value
+    return 0
+
+
+# Main loop:
+
+# We read preprocess_count many choices from the computer before we start to ask z3 for a solution
+# Note that for these preprocessing rounds we do not need to make a good guess and compute the winner
+# We are only interested in what the computer picks for the first few rounds
+for index in range(1,preprocess_count):
+    computer_choice, _ = computer.compute_choice()
+    player_choice = 0 # We always choose Rock since we cannot make good guesses in the beginning
+
+    add_constraint(solver,index,computer_choice)
+    output, won = compute_winner(computer_choice, player_choice)
+    print(output)
+    if won: print("Congratulations!")
+    else:   print("Try again.")
+
+
+# Now we start by adding a 'special' variable s_i_plus_1 and try to win
+index = preprocess_count
+while True:
+    store_backtracking_point(solver)
+    s_i_plus_1 = add_next_state_constraint(solver)
+    solver.check()
+
+    player_choice = get_players_choice(solver, s_i_plus_1)
+    computer_choice, _ = computer.compute_choice()
+    output, won = compute_winner(computer_choice, player_choice)
+
+    print(output)
+    if won: print("Congratulations!")
+    else:   print("Try again.")
+
+    restore_backtracking_point(solver)
+    add_constraint(solver, index, computer_choice)
+    # input("")
+    index += 1
+    if index >= 100:
+        break

square.py

@@ -0,0 +1,53 @@
+# 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()
+
+numbers = [[None for _j in range(size_x)] for _j in range(size_y)]
+
+# TODO: create an integer variable for each playground cell
+# hint: use something like the coordinates as part of the variable name
+# TODO: assign each known number the corresponding value from playground
+# TODO: declare a variable for the sum of all columns, rows and diagonals
+# TODO: enforce that each column sums up to the declared variable
+# TODO: enforce that each row sums up to the declared variable
+# 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))
+
+################################################################################

square0.txt

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

trees_and_tents.py

@@ -0,0 +1,62 @@
+# create the solver
+cells = [[None for j in range(size_x)] for i in range(size_y)]
+solver = Solver()
+
+def get_possible_tents_in_col(col):
+    possible_tent_positions = []
+    for row in range(size_y):
+        if playground[row][col] != "T":
+           possible_tent_positions.append(cells[row][col])
+    return possible_tent_positions
+
+def get_possible_tents_in_row(row):
+    possible_tent_positions = []
+    for col in range(size_x):
+        if playground[row][col] != "T":
+           possible_tent_positions.append(cells[row][col])
+    return possible_tent_positions
+
+def get_neighbours(i, j):
+    cs = []
+    for p in range(max(i-1, 0), min(i+2, size_y)):
+        for q in range(max(j-1, 0), min(j+2, size_x)):
+            if p == i and q == j: continue
+            cs.append(cells[p][q])
+    return cs
+
+def get_tree_neighbours(i, j):
+    tree_pos = []
+    for p in [max(i-1, 0), min(i+1, size_y - 1)]:
+        if p == i: continue
+        tree_pos.append(cells[p][j])
+    for q in [max(j-1, 0), min(j+1, size_x - 1)]:
+        if q == j: continue
+        tree_pos.append(cells[i][q])
+    return tree_pos
+
+
+# TODO Cell entries need to be represented by a Z3 variable
+# TODO Bound/restrict the values of the cells according to the input
+
+# TODO The sums of tents per row/column must match the amounts given in the input
+
+for i in range(size_y):
+    for j in range(size_x):
+        if playground[i][j] == "T":
+            # TODO A tent needs to be next to a tree
+            # Incrementally build up the tree_constraint ...
+            tree_constraint = False
+            for possible_tent in get_tree_neighbours(i, j):
+                pass
+        else:
+            neighbours = get_neighbours(i, j)
+            # TODO A tent must not be next to another tent
+
+res = solver.check()
+if res == unsat:
+    print("UNSAT")
+    print_forest()
+else:
+    m = solver.model()
+    print(m)
+    print_result(m)