You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 

123 lines
3.9 KiB

# 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