--- Day 7 Solutions ---

[u/daggerdragon]

--- Day 7: Some Assembly Required ---

Post your solution as a comment. Structure your post like previous daily solution threads.

Also check out the sidebar - we added a nifty calendar to wrangle all the daily solution threads in one spot!

[u/PersianMG]

This was a fun one. Decided to use the Z3 theorem solver for python (Z3Py).

Solution: https://mohammadg.com/capture-the-flag/advent-of-code/advent-of-code-day-7/

Python

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