From 00000420f10f068d18fedc7e40583b35d1e1acba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matej=20Jane=C5=BEi=C4=8D?= <janezic.mj@gmail.com>
Date: Mon, 25 Dec 2023 05:59:42 +0100
Subject: [PATCH] solution: day 24

---
 Cargo.lock           | 197 +++++++++++++++++++++++++++++++++++++++++--
 Cargo.toml           |   2 +
 data/examples/24.txt |   5 ++
 src/bin/24.rs        |  94 +++++++++++++++++++++
 4 files changed, 291 insertions(+), 7 deletions(-)
 create mode 100644 data/examples/24.txt
 create mode 100644 src/bin/24.rs

diff --git a/Cargo.lock b/Cargo.lock
index 70eb21f..4ea0bc0 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -17,9 +17,21 @@ version = "1.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe"
 
+[[package]]
+name = "aho-corasick"
+version = "1.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b2969dcb958b36655471fc61f7e416fa76033bdd4bfed0678d8fee1e2d07a1f0"
+dependencies = [
+ "memchr",
+]
+
 [[package]]
 name = "aoc"
 version = "46.0.0"
+dependencies = [
+ "z3",
+]
 
 [[package]]
 name = "autocfg"
@@ -48,12 +60,38 @@ version = "0.21.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "35636a1494ede3b646cc98f74f8e62c773a38a659ebc777a2cf26b9b74171df9"
 
+[[package]]
+name = "bindgen"
+version = "0.66.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f2b84e06fc203107bfbad243f4aba2af864eb7db3b1cf46ea0a023b0b433d2a7"
+dependencies = [
+ "bitflags 2.4.1",
+ "cexpr",
+ "clang-sys",
+ "lazy_static",
+ "lazycell",
+ "peeking_take_while",
+ "proc-macro2",
+ "quote",
+ "regex",
+ "rustc-hash",
+ "shlex",
+ "syn 2.0.42",
+]
+
 [[package]]
 name = "bitflags"
 version = "1.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
+[[package]]
+name = "bitflags"
+version = "2.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "327762f6e5a765692301e5bb513e0d9fef63be86bbc14528052b1cd3e6f03e07"
+
 [[package]]
 name = "bumpalo"
 version = "3.11.1"
@@ -72,12 +110,41 @@ version = "1.0.78"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a20104e2335ce8a659d6dd92a51a767a0c062599c73b343fd152cb401e828c3d"
 
+[[package]]
+name = "cexpr"
+version = "0.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6fac387a98bb7c37292057cffc56d62ecb629900026402633ae9160df93a8766"
+dependencies = [
+ "nom",
+]
+
 [[package]]
 name = "cfg-if"
 version = "1.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
+[[package]]
+name = "clang-sys"
+version = "1.6.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c688fc74432808e3eb684cae8830a86be1d66a2bd58e1f248ed0960a590baf6f"
+dependencies = [
+ "glob",
+ "libc",
+ "libloading",
+]
+
+[[package]]
+name = "cmake"
+version = "0.1.50"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a31c789563b815f77f4250caee12365734369f942439b7defd71e18a48197130"
+dependencies = [
+ "cc",
+]
+
 [[package]]
 name = "core-foundation"
 version = "0.9.3"
@@ -211,6 +278,12 @@ version = "0.28.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6fb8d784f27acf97159b40fc4db5ecd8aa23b9ad5ef69cdd136d3bc80665f0c0"
 
+[[package]]
+name = "glob"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b"
+
 [[package]]
 name = "h2"
 version = "0.3.15"
@@ -372,12 +445,28 @@ version = "1.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
 
+[[package]]
+name = "lazycell"
+version = "1.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "830d08ce1d1d941e6b30645f1a0eb5643013d835ce3779a5fc208261dbe10f55"
+
 [[package]]
 name = "libc"
 version = "0.2.150"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "89d92a4743f9a61002fae18374ed11e7973f530cb3a3255fb354818118b2203c"
 
+[[package]]
+name = "libloading"
+version = "0.7.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b67380fd3b2fbe7527a606e18729d21c6f3951633d0500574c4dc22d2d638b9f"
+dependencies = [
+ "cfg-if",
+ "winapi",
+]
+
 [[package]]
 name = "log"
 version = "0.4.17"
@@ -399,6 +488,12 @@ version = "0.3.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "2a60c7ce501c71e03a9c9c0d35b861413ae925bd979cc7a4e30d060069aaac8d"
 
+[[package]]
+name = "minimal-lexical"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
+
 [[package]]
 name = "miniz_oxide"
 version = "0.7.1"
@@ -437,6 +532,16 @@ dependencies = [
  "tempfile",
 ]
 
+[[package]]
+name = "nom"
+version = "7.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a"
+dependencies = [
+ "memchr",
+ "minimal-lexical",
+]
+
 [[package]]
 name = "num_cpus"
 version = "1.15.0"
@@ -468,7 +573,7 @@ version = "0.10.45"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b102428fd03bc5edf97f62620f7298614c45cedf287c271e7ed450bbaf83f2e1"
 dependencies = [
- "bitflags",
+ "bitflags 1.3.2",
  "cfg-if",
  "foreign-types",
  "libc",
@@ -485,7 +590,7 @@ checksum = "b501e44f11665960c7e7fcf062c7d96a14ade4aa98116c004b2e37b5be7d736c"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.107",
 ]
 
 [[package]]
@@ -507,6 +612,12 @@ dependencies = [
  "vcpkg",
 ]
 
+[[package]]
+name = "peeking_take_while"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "19b17cddbe7ec3f8bc800887bab5e717348c95ea2ca0b1bf0837fb964dc67099"
+
 [[package]]
 name = "percent-encoding"
 version = "2.2.0"
@@ -561,9 +672,38 @@ version = "0.2.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "fb5a58c1855b4b6819d59012155603f0b22ad30cad752600aadfcb695265519a"
 dependencies = [
- "bitflags",
+ "bitflags 1.3.2",
 ]
 
+[[package]]
+name = "regex"
+version = "1.10.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "380b951a9c5e80ddfd6136919eef32310721aa4aacd4889a8d39124b026ab343"
+dependencies = [
+ "aho-corasick",
+ "memchr",
+ "regex-automata",
+ "regex-syntax",
+]
+
+[[package]]
+name = "regex-automata"
+version = "0.4.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5f804c7828047e88b2d32e2d7fe5a105da8ee3264f01902f796c8e067dc2483f"
+dependencies = [
+ "aho-corasick",
+ "memchr",
+ "regex-syntax",
+]
+
+[[package]]
+name = "regex-syntax"
+version = "0.8.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c08c74e62047bb2de4ff487b251e4a92e24f48745648451635cec7d591162d9f"
+
 [[package]]
 name = "remove_dir_all"
 version = "0.5.3"
@@ -617,6 +757,12 @@ version = "0.1.23"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76"
 
+[[package]]
+name = "rustc-hash"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2"
+
 [[package]]
 name = "ryu"
 version = "1.0.12"
@@ -648,7 +794,7 @@ version = "2.7.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "2bc1bb97804af6631813c55739f771071e0f2ed33ee20b68c86ec505d906356c"
 dependencies = [
- "bitflags",
+ "bitflags 1.3.2",
  "core-foundation",
  "core-foundation-sys",
  "libc",
@@ -694,6 +840,12 @@ dependencies = [
  "serde",
 ]
 
+[[package]]
+name = "shlex"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a7cee0529a6d40f580e7a5e6c495c8fbfe21b7b52795ed4bb5e62cdf92bc6380"
+
 [[package]]
 name = "slab"
 version = "0.4.7"
@@ -734,13 +886,24 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "syn"
+version = "2.0.42"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5b7d0a2c048d661a1a59fcd7355baa232f7ed34e0ee4df2eef3c1c1c0d3852d8"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "system-configuration"
 version = "0.5.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ba3a3adc5c275d719af8cb4272ea1c4a6d668a777f37e115f6d11ddbc1c8e0e7"
 dependencies = [
- "bitflags",
+ "bitflags 1.3.2",
  "core-foundation",
  "system-configuration-sys",
 ]
@@ -931,7 +1094,7 @@ dependencies = [
  "once_cell",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.107",
  "wasm-bindgen-shared",
 ]
 
@@ -965,7 +1128,7 @@ checksum = "07bc0c051dc5f23e307b13285f9d75df86bfdf816c5721e573dec1f9b8aa193c"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.107",
  "wasm-bindgen-backend",
  "wasm-bindgen-shared",
 ]
@@ -1126,3 +1289,23 @@ dependencies = [
  "cfg-if",
  "windows-sys 0.48.0",
 ]
+
+[[package]]
+name = "z3"
+version = "0.12.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4a7ff5718c079e7b813378d67a5bed32ccc2086f151d6185074a7e24f4a565e8"
+dependencies = [
+ "log",
+ "z3-sys",
+]
+
+[[package]]
+name = "z3-sys"
+version = "0.8.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d7cf70fdbc0de3f42b404f49b0d4686a82562254ea29ff0a155eef2f5430f4b0"
+dependencies = [
+ "bindgen",
+ "cmake",
+]
diff --git a/Cargo.toml b/Cargo.toml
index 310f228..1766195 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -21,4 +21,6 @@ authors.workspace = true
 repository.workspace = true
 
 [dependencies]
+# so much for no dependencies this year, but I really cba so here it is
+z3 = { version = "0.12.1", features = [ "static-link-z3" ] }
 
diff --git a/data/examples/24.txt b/data/examples/24.txt
new file mode 100644
index 000000000..d2f1359
--- /dev/null
+++ b/data/examples/24.txt
@@ -0,0 +1,5 @@
+19, 13, 30 @ -2, 1, -2
+18, 19, 22 @ -1, -1, -2
+20, 25, 34 @ -2, -2, -4
+12, 31, 28 @ -1, -2, -1
+20, 19, 15 @ 1, -5, -3
diff --git a/src/bin/24.rs b/src/bin/24.rs
new file mode 100644
index 000000000..0c7f56d
--- /dev/null
+++ b/src/bin/24.rs
@@ -0,0 +1,94 @@
+use z3::ast::{Ast, Int};
+
+type Vector3 = (f64, f64, f64);
+
+fn parse_input(input: &str) -> Vec<(Vector3, Vector3)> {
+    input
+        .lines()
+        .filter_map(|x| x.split_once(" @ "))
+        .map(|(a, b)| {
+            let av: Vec<_> = a.splitn(3, ", ").filter_map(|x| x.parse().ok()).collect();
+            let bv: Vec<_> = b.splitn(3, ", ").filter_map(|x| x.parse().ok()).collect();
+            ((av[0], av[1], av[2]), (bv[0], bv[1], bv[2]))
+        })
+        .collect()
+}
+
+fn part_one_with_area(input: &str, min: f64, max: f64) -> u32 {
+    let points = parse_input(input);
+
+    let mut c = 0;
+
+    let test_area = |x: f64, y: f64| x <= max && x >= min && y <= max && y >= min;
+
+    for (i, ((x1, y1, _), (dx1, dy1, _))) in points.iter().copied().enumerate() {
+        for ((x2, y2, _), (dx2, dy2, _)) in points.iter().skip(i + 1).copied() {
+            let n2 = (x2 - x1 + (y1 - y2) * dx1 / dy1) / (dy2 * dx1 / dy1 - dx2);
+            let n1 = (x1 - x2 + (y2 - y1) * dx2 / dy2) / (dy1 * dx2 / dy2 - dx1);
+
+            if n1 <= 0.0 || n2 <= 0.0 {
+                continue;
+            }
+
+            let x = x1 + n1 * dx1;
+            let y = y1 + n1 * dy1;
+
+            if test_area(x, y) {
+                c += 1;
+            }
+        }
+    }
+
+    c
+}
+pub fn part_one(input: &str) -> Option<u32> {
+    let min = 200000000000000.0;
+    let max = 400000000000000.0;
+    Some(part_one_with_area(input, min, max))
+}
+
+pub fn part_two(input: &str) -> Option<u64> {
+    let points = parse_input(input);
+
+    let ctx = z3::Context::new(&z3::Config::new());
+    let solver = z3::Solver::new(&ctx);
+
+    let zero = Int::from_u64(&ctx, 0);
+    let [a, b, c, da, db, dc] = ["a", "b", "c", "da", "db", "dc"].map(|x| Int::new_const(&ctx, x));
+
+    for (i, ((x, y, z), (dx, dy, dz))) in points.iter().enumerate().take(3) {
+        let [x, y, z, dx, dy, dz] = [x, y, z, dx, dy, dz].map(|w| Int::from_i64(&ctx, *w as i64));
+        let t = Int::new_const(&ctx, format!("t_{i}").as_str());
+        solver.assert(&t.ge(&zero));
+        solver.assert(&((&x + &dx * &t)._eq(&(&a + &da * &t))));
+        solver.assert(&((&y + &dy * &t)._eq(&(&b + &db * &t))));
+        solver.assert(&((&z + &dz * &t)._eq(&(&c + &dc * &t))));
+    }
+
+    solver.check();
+    let model = solver.get_model().unwrap();
+    let res = model.eval(&(&a + &b + &c), true).unwrap();
+
+    res.as_u64()
+}
+
+aoc::solution!(24);
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    #[test]
+    fn test_part_one() {
+        let input = aoc::template::read_file("examples", 24);
+        let min = 7.0;
+        let max = 27.0;
+        assert_eq!(part_one_with_area(&input, min, max), 2);
+    }
+    #[test]
+    fn test_part_two() {
+        assert_eq!(
+            part_two(&aoc::template::read_file("examples", 24)),
+            Some(47)
+        );
+    }
+}