Language: Python

Github

Catching up missed days.

Python

Questions and feedback welcome!

import collections
import re

from .solver import Solver

class Day04(Solver):
  def __init__(self):
    super().__init__(4)
    self.cards = []

  def presolve(self, input: str):
    lines = input.rstrip().split('\n')
    self.cards = []
    for line in lines:
      left, right = re.split(r' +\| +', re.split(': +', line)[1])
      left, right = map(int, re.split(' +', left)), map(int, re.split(' +', right))
      self.cards.append((list(left), list(right)))

  def solve_first_star(self):
    points = 0
    for winning, having in self.cards:
      matches = len(set(winning) & set(having))
      if not matches:
        continue
      points += 1 << (matches - 1)
    return points

  def solve_second_star(self):
    factors = collections.defaultdict(lambda: 1)
    count = 0
    for i, (winning, having) in enumerate(self.cards):
      count += factors[i]
      matches = len(set(winning) & set(having))
      if not matches:
        continue
      for j in range(i + 1, i + 1 + matches):
        factors[j] = factors[j] + factors[i]
    return count

Crystal

late because I had to skip two days of aoc. Fairly easy

input =  File.read("input.txt").lines

sum = 0
winnings = Array.new(input.size) {[1, 0]}
input.each_with_index do |line, i|
	card, values = line.split(":")
	nums = values.split("|").map(&.split.map(&.to_i))

	points = 0
	nums[1].each do |num|
		if nums[0].includes?(num)
			points = points == 0 ? 1 : points * 2
			winnings[i][1] += 1
	end    end
	sum += points
end
puts sum

winnings.each_with_index do |card, i|
	next if card[1] == 0
	(1..card[1]).each do |n|
		winnings[i+n][0] += card[0]
end    end
puts winnings.sum(&.[0])

My solution in C for part 1: https://git.sr.ht/~aidenisik/aoc23/tree/master/item/day4

I’ve been running a day behind the whole time since I forgot about it on day 1, I should really catch up.

EDIT: Part 2 is also uploaded.

[Language: Lean4]

I’ll only post the actual parsing and solution. I have written some helpers which are in other files, as is the main function. For the full code, please see my github repo.

I’m pretty sure that implementing part 2 in a naive way would cause Lean to demand a proof of termination, what might not be that easy to supply in this case… Luckily there’s a way more elegant and way faster solution than the naive one, that can use structural recursion and therefore doesn’t need an extra proof of termination.

structure Card where
  id : Nat
  winningNumbers : List Nat
  haveNumbers : List Nat
  deriving Repr

private def Card.matches (c : Card) : Nat :=
  flip c.haveNumbers.foldl 0 λo n ↦
    if c.winningNumbers.contains n then o + 1 else o

private def Card.score : Card → Nat :=
  (· / 2) ∘ (2^·) ∘ Card.matches

abbrev Deck := List Card

private def Deck.score : Deck → Nat :=
  List.foldl (· + ·.score) 0

def parse (input : String) : Option Deck := do
  let mut cards : Deck := []
  for line in input.splitOn "\n" do
    if line.isEmpty then
      continue
    let cs := line.splitOn ":"
    if p : cs.length = 2 then
      let f := String.trim $ cs[0]'(by simp[p])
      let g := String.trim $ cs[1]'(by simp[p])
      if not $ f.startsWith "Card " then
        failure
      let f := f.drop 5 |> String.trim
      let f ← f.toNat?
      let g := g.splitOn "|"
      if q : g.length = 2 then
        let winners := String.trim $ g[0]'(by simp[q])
        let draws := String.trim $ g[1]'(by simp[q])
        let toNumbers := λ(s : String) ↦
          s.split (·.isWhitespace)
          |> List.filter (not ∘ String.isEmpty)
          |> List.mapM String.toNat?
        let winners ← toNumbers winners
        let draws ← toNumbers draws
        cards := {id := f, winningNumbers := winners, haveNumbers := draws : Card} :: cards
      else
        failure
    else
      failure
  return cards -- cards is **reversed**, that's intentional. It doesn't affect part 1, but makes part 2 easier.

def part1 : Deck → Nat := Deck.score

def part2 (input : Deck) : Nat :=
  -- Okay, doing this brute-force is dumb.
  -- Instead let's compute how many cards each original card is worth, and sum that up.
  -- This relies on parse outputting the cards in **reverse** order.
  let multipliers := input.map Card.matches
  let sumNextN : Nat → List Nat → Nat := λn l ↦ (l.take n).foldl (· + ·) 0
  let rec helper : List Nat → List Nat → List Nat := λ input output ↦ match input with
    | [] => output
    | a :: as => helper as $ (1 + (sumNextN a output)) :: output
  let worths := helper multipliers []
  worths.foldl (· + ·) 0