Advent Of Code 2015: Day 7

Challenge

--- Day 7: Some Assembly Required ---
This year, Santa brought little Bobby Tables a set of wires and bitwise logic gates! Unfortunately, little Bobby is a little under the recommended age range, and he needs help assembling the circuit.

Each wire has an identifier (some lowercase letters) and can carry a 16-bit signal (a number from 0 to 65535). A signal is provided to each wire by a gate, another wire, or some specific value. Each wire can only get a signal from one source, but can provide its signal to multiple destinations. A gate provides no signal until all of its inputs have a signal.

The included instructions booklet describes how to connect the parts together: x AND y -> z means to connect wires x and y to an AND gate, and then connect its output to wire z.

For example:

123 -> x means that the signal 123 is provided to wire x.
x AND y -> z means that the bitwise AND of wire x and wire y is provided to wire z.
p LSHIFT 2 -> q means that the value from wire p is left-shifted by 2 and then provided to wire q.
NOT e -> f means that the bitwise complement of the value from wire e is provided to wire f.
Other possible gates include OR (bitwise OR) and RSHIFT (right-shift). If, for some reason, you'd like to emulate the circuit instead, almost all programming languages (for example, C, JavaScript, or Python) provide operators for these gates.

For example, here is a simple circuit:

123 -> x
456 -> y
x AND y -> d
x OR y -> e
x LSHIFT 2 -> f
y RSHIFT 2 -> g
NOT x -> h
NOT y -> i
After it is run, these are the signals on the wires:

d: 72
e: 507
f: 492
g: 114
h: 65412
i: 65079
x: 123
y: 456
In little Bobby's kit's instructions booklet (provided as your puzzle input), what signal is ultimately provided to wire a?

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.

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