Challenge
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 |
# Day 7 - Part 1 and Part 2 # # To find Part 1 answer: python day7.py | grep ' a = ' # To find Part 2 answer: Edit value of b in input.txt to result from part 1 and rerun script import re from z3 import * def z3VarsAddIfMissing(wire): if wire not in z3Vars: z3Vars[wire] = BitVec(wire, 32) #32 bit integers z3Vars = {} s = Solver() with open('input.txt') as f: lines = f.readlines() for line in lines: # Get command -> store variables res = re.search(r'(.*)\s*->\s*(.*)', line) command, store_var = res.group(1).strip(), res.group(2) # Store var z3VarsAddIfMissing(store_var) # Add logical constraints to solver # Store other variables in commands if they don't exit on the way # Bitwise AND res = re.search(r'(.*?)\s*AND\s*(.*)', command) if res and res.group(1) != '' and res.group(2) != '': z3VarsAddIfMissing(res.group(2)) # If first component is an integer if res.group(1).isdigit(): s.add(z3Vars[store_var] == int(res.group(1)) & z3Vars[res.group(2)]) else: z3VarsAddIfMissing(res.group(1)) s.add(z3Vars[store_var] == z3Vars[res.group(1)] & z3Vars[res.group(2)]) continue # Bitwise OR res = re.search(r'(.*?)\s*OR\s*(.*)', command) if res and res.group(1) != '' and res.group(2) != '': z3VarsAddIfMissing(res.group(1)) z3VarsAddIfMissing(res.group(2)) s.add(z3Vars[store_var] == z3Vars[res.group(1)] | z3Vars[res.group(2)]) continue # Bit LSHIFT res = re.search(r'(.*?)\s*LSHIFT\s*(\d*)', command) if res and res.group(1) != '' and res.group(2) != '': z3VarsAddIfMissing(res.group(1)) s.add(z3Vars[store_var] == z3Vars[res.group(1)] << int(res.group(2))) continue # Bit RSHIFT res = re.search(r'(.*?)\s*RSHIFT\s*(\d*)', command) if res and res.group(1) != '' and res.group(2) != '': z3VarsAddIfMissing(res.group(1)) s.add(z3Vars[store_var] == z3Vars[res.group(1)] >> int(res.group(2))) continue # Bitwise NOT res = re.search(r'NOT\s*(.*)', command) if res and res.group(1) != '': z3VarsAddIfMissing(res.group(1)) s.add(z3Vars[store_var] == (~z3Vars[res.group(1)]) & 0xFFFF ) # 0xFFFF bitwise and to constrain value to [0, 2^16) continue # Assign operation (variable or integer) == res = re.search(r'^(.*)$', command) if res and res.group(1) != '': if res.group(1).isdigit(): s.add(z3Vars[store_var] == res.group(1)) else: z3VarsAddIfMissing(res.group(1)) s.add(z3Vars[store_var] == z3Vars[res.group(1)]) continue # Print answers set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000) print(s.check()) print(s.model()) |
Solution
Wow this one was fun! I decided to use Z3Py, a theorem prover module for python. My solution essentially parses each command using regexp and adds the various boolean rules to a solver object. Finally, the theorem solver checks all possible values and prints out the results of every ‘wire’. Determining the answer is then very simple. To solve part 2 I simply changed the value of b in my input.txt to the answer from part a and reran the script.
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 |
# Day 7 - Part 1 and Part 2 # # To find Part 1 answer: python day7.py | grep ' a = ' # To find Part 2 answer: Edit value of b in input.txt to result from part 1 and rerun script import re from z3 import * z3Vars = {} s = Solver() with open('input.txt') as f: lines = f.readlines() for line in lines: # Get command -> store variables res = re.search(r'(.*)\s*->\s*(.*)', line) command, store_var = res.group(1).strip(), res.group(2) # Store var if store_var not in z3Vars: z3Vars[store_var] = BitVec(store_var, 32) #32 bit integers # Add logical constraints to solver # Store other variables in commands if they don't exit on the way # Assign operation (integer) == res = re.search(r'^(\d*?)$', command) if res and res.group(1) != '': s.add(z3Vars[store_var] == res.group(1)) continue # Bitwise AND (with integer) res = re.search(r'(\d*)\s*AND\s*(.*)', command) if res and res.group(1) != '' and res.group(2) != '': if res.group(2) not in z3Vars: z3Vars[res.group(2)] = BitVec(res.group(2), 32) s.add(z3Vars[store_var] == int(res.group(1)) & z3Vars[res.group(2)]) continue # Bitwise AND res = re.search(r'(.*?)\s*AND\s*(.*)', command) if res and res.group(1) != '' and res.group(2) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) if res.group(2) not in z3Vars: z3Vars[res.group(2)] = BitVec(res.group(2), 32) s.add(z3Vars[store_var] == z3Vars[res.group(1)] & z3Vars[res.group(2)]) continue # Bitwise OR res = re.search(r'(.*?)\s*OR\s*(.*)', command) if res and res.group(1) != '' and res.group(2) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) if res.group(2) not in z3Vars: z3Vars[res.group(2)] = BitVec(res.group(2), 32) s.add(z3Vars[store_var] == z3Vars[res.group(1)] | z3Vars[res.group(2)]) continue # Bit LSHIFT res = re.search(r'(.*?)\s*LSHIFT\s*(\d*)', command) if res and res.group(1) != '' and res.group(2) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) s.add(z3Vars[store_var] == z3Vars[res.group(1)] << int(res.group(2))) continue # Bit RSHIFT res = re.search(r'(.*?)\s*RSHIFT\s*(\d*)', command) if res and res.group(1) != '' and res.group(2) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) s.add(z3Vars[store_var] == z3Vars[res.group(1)] >> int(res.group(2))) continue # Bitwise NOT res = re.search(r'NOT\s*(.*)', command) if res and res.group(1) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) s.add(z3Vars[store_var] == (~z3Vars[res.group(1)]) & 0xFFFF ) # 0xFFFF logical and to contrain value to [0, 2^16) continue # Assign operation (variable) == res = re.search(r'(.*)', command) if res and res.group(1) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) s.add(z3Vars[store_var] == z3Vars[res.group(1)]) continue # Print answers set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000) print(s.check()) print(s.model()) |
