From e7884b66007d6b3a95aff5815bafa3a312044998 Mon Sep 17 00:00:00 2001
From: Tomasz Kramkowski <tomasz@kramkow.ski>
Date: Sun, 24 Dec 2023 14:28:37 +0100
Subject: day 24 cheese

---
 24.py | 84 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)
 create mode 100644 24.py

diff --git a/24.py b/24.py
new file mode 100644
index 0000000..47b4ba0
--- /dev/null
+++ b/24.py
@@ -0,0 +1,84 @@
+from dataclasses import dataclass
+from functools import cache
+from itertools import combinations
+from sys import stdin
+
+from z3 import z3
+
+
+@dataclass(frozen=True, slots=True)
+class Vec:
+    x: float
+    y: float
+    z: float
+
+    def __str__(self) -> str:
+        return f"{self.x}, {self.y}, {self.z}"
+
+
+@dataclass(frozen=True, slots=True)
+class Hailstone:
+    pos: Vec
+    vel: Vec
+
+    @property
+    @cache
+    def m(self) -> float:
+        return self.vel.y / self.vel.x
+
+    @property
+    @cache
+    def c(self) -> float:
+        return self.pos.y - self.pos.x / self.vel.x * self.vel.y
+
+    def __str__(self) -> str:
+        return f"{self.pos} @ {self.vel}"
+
+
+inp: list[Hailstone] = list()
+for line in stdin:
+    pos, vel = line.rstrip("\n").split(" @ ")
+    pos = Vec(*map(float, pos.split(", ")))
+    vel = Vec(*map(float, vel.split(", ")))
+    inp.append(Hailstone(pos, vel))
+
+
+def intersection(a: Hailstone, b: Hailstone) -> tuple[float, float] | None:
+    numer = b.c - a.c
+    denom = a.m - b.m
+    if denom == 0:
+        return None
+    xi = numer / denom
+    return xi, xi * a.m + a.c
+
+
+lbound = 200000000000000
+ubound = 400000000000000
+
+p1 = 0
+for a, b in combinations(inp, 2):
+    inter = intersection(a, b)
+    if inter is None:
+        continue
+    ix, iy = inter
+    a_dist = (ix - a.pos.x) / a.vel.x
+    b_dist = (ix - b.pos.x) / b.vel.x
+    if (
+        a_dist >= 0
+        and b_dist >= 0
+        and lbound <= ix <= ubound
+        and lbound <= iy <= ubound
+    ):
+        p1 += 1
+print(p1)
+
+a, b, c, x, y, z = (z3.Int(c) for c in "abcxyz")
+s = z3.Solver()
+for i, m in enumerate("tuvw"):
+    m = z3.Int(m)
+    h = inp[i]
+    s.add(h.pos.x + h.vel.x * m == x + a * m)
+    s.add(h.pos.y + h.vel.y * m == y + b * m)
+    s.add(h.pos.z + h.vel.z * m == z + c * m)
+s.check()
+print(s.model().eval(x + y + z))
-- 
cgit v1.2.3-54-g00ecf