LAC-Practical-Assignments-WS2024/rpssl.py

# 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