Lösungen für Tag 24, Teil 2 (mit Z3 als Solver :/ ...)

4 files changed, 46 insertions, 33 deletions

diff --git a/compile_flags.txt b/compile_flags.txt
index 966e06b..0000d86 100644
--- a/compile_flags.txt
+++ b/compile_flags.txt
@@ -5,3 +5,4 @@
 -Wdouble-promotion
 -pedantic
 -std=c++20
+-I/usr/local/include
diff --git a/makefile b/makefile
index 07e42b8..1c4a023 100644
--- a/makefile
+++ b/makefile
@@ -31,6 +31,9 @@ bin:
 bin/%: src/%.cpp | bin
         c++ $(CPPFLAGS) $^ -o $@
 
+bin/day24: src/day24.cpp | bin
+        c++ $(CPPFLAGS) -Wno-sign-conversion -I/usr/local/include $^ -L/usr/local/lib -lz3 -o $@
+
 clean:
         rm -rf bin
 
diff --git a/src/day24.cpp b/src/day24.cpp
index 296d38a..76f459b 100644
--- a/src/day24.cpp
+++ b/src/day24.cpp
@@ -2,9 +2,12 @@
 #include <fstream>
 #include <iostream>
 #include <limits>
+#include <map>
 #include <string>
 #include <tuple>
 #include <vector>
+#include <z3++.h>
+
 using namespace std;
 
 using line_type   = tuple<double, double, double, double, double, double>;
@@ -122,10 +125,49 @@ part1(const puzzle_type& input)
         cout << sum << endl;
 }
 
+void
+part2(const puzzle_type& input)
+{
+        auto config  = z3::config();
+        auto context = z3::context(config);
+        auto solver  = z3::solver(context);
+
+        const auto px = context.int_const("px");
+        const auto py = context.int_const("py");
+        const auto pz = context.int_const("pz");
+        const auto vx = context.int_const("vx");
+        const auto vy = context.int_const("vy");
+        const auto vz = context.int_const("vz");
+
+        for ( size_t i = 0; i != input.size(); ++i ) {
+                const auto& stone = input[i];
+
+                const auto pxn = context.int_val(int64_t(get<0>(stone)));
+                const auto pyn = context.int_val(int64_t(get<1>(stone)));
+                const auto pzn = context.int_val(int64_t(get<2>(stone)));
+                const auto vxn = context.int_val(int64_t(get<3>(stone)));
+                const auto vyn = context.int_val(int64_t(get<4>(stone)));
+                const auto vzn = context.int_val(int64_t(get<5>(stone)));
+                const auto tn  = context.int_const(to_string(i+1).c_str());
+
+                solver.add(tn >= 0);
+                solver.add(pxn + vxn * tn == px + vx * tn);
+                solver.add(pyn + vyn * tn == py + vy * tn);
+                solver.add(pzn + vzn * tn == pz + vz * tn);
+        }
+
+        solver.check();
+
+        auto model = solver.get_model();
+
+        cout << model.eval(px).as_int64() + model.eval(py).as_int64() + model.eval(pz).as_int64() << endl;
+}
+
 int
 main()
 {
         const auto input = read_file("data/day24.txt");
 
         part1(input);
+        part2(input);
 }
diff --git a/src/day24.py b/src/day24.py
deleted file mode 100644
index 809f2d0..0000000
--- a/src/day24.py
+++ /dev/null
@@ -1,33 +0,0 @@
-class Hailstone:
-    def __init__(self, sx, sy, sz, vx, vy, vz):
-        self.sx = sx
-        self.sy = sy
-        self.sz = sz
-        self.vx = vx
-        self.vy = vy
-        self.vz = vz
-        
-        self.a = vy
-        self.b = -vx
-        self.c = vy * sx - vx * sy
-    
-    def __repr__(self):
-        return "Hailstone{" + f"a={self.a}, b={self.b}, c={self.c}" + "}"
-
-hailstones = [Hailstone(*map(int, line.replace("@", ",").split(","))) for line in open("data/day24.txt")]
-
-total = 0
-
-for i, hs1 in enumerate(hailstones):
-    for hs2 in hailstones[:i]:
-        a1, b1, c1 = hs1.a, hs1.b, hs1.c
-        a2, b2, c2 = hs2.a, hs2.b, hs2.c
-        if a1 * b2 == b1 * a2:
-            continue
-        x = (c1 * b2 - c2 * b1) / (a1 * b2 - a2 * b1)
-        y = (c2 * a1 - c1 * a2) / (a1 * b2 - a2 * b1)
-        if 200000000000000 <= x <= 400000000000000 and 200000000000000 <= y <= 400000000000000:
-            if all((x - hs.sx) * hs.vx >= 0 and (y - hs.sy) * hs.vy >= 0 for hs in (hs1, hs2)):
-                total += 1
-
-print(total)