1 files changed, 173 insertions, 0 deletions

diff --git a/src/day24.cpp b/src/day24.cpp
new file mode 100644
index 0000000..76f459b
--- /dev/null
+++ b/src/day24.cpp
@@ -0,0 +1,173 @@
+#include <cstdlib>
+#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>;
+using point_type  = tuple<double, double>;
+using puzzle_type = vector<line_type>;
+
+template<typename T>
+int
+sgn(T val)
+{
+        return (T(0) < val) - (val < T(0));
+}
+
+puzzle_type
+read_file(string_view filename)
+{
+        fstream     input{ filename };
+        puzzle_type result;
+
+        for ( string line; getline(input, line); ) {
+                const auto NFIELDS = 6;
+
+                double x, y, z, dx, dy, dz; // NOLINT
+
+                if ( sscanf(line.data(), "%lf, %lf, %lf @ %lf, %lf, %lf", &x, &y, &z, &dx, &dy, &dz) != NFIELDS ) {
+                        continue;
+                }
+
+                result.emplace_back(make_tuple(x, y, z, dx, dy, dz));
+        }
+
+        return result;
+}
+
+point_type
+get_direction(line_type line)
+{
+        const auto [x, y, z, dx, dy, dz] = line;
+
+        return make_tuple(sgn(dx), sgn(dy));
+}
+
+point_type
+get_direction(line_type from, point_type to)
+{
+        const auto [x, y, z, dx, dy, dz] = from;
+        const auto [to_x, to_y]          = to;
+
+        return make_tuple(sgn(to_x - x), sgn(to_y - y));
+}
+
+bool
+lint(line_type stone_a, line_type stone_b, point_type& cross_point)
+{
+        const auto p_1 = make_tuple(get<0>(stone_a), get<1>(stone_a));
+        const auto p_2 = make_tuple(get<0>(stone_a) + get<3>(stone_a), get<1>(stone_a) + get<4>(stone_a));
+
+        const auto p_3 = make_tuple(get<0>(stone_b), get<1>(stone_b));
+        const auto p_4 = make_tuple(get<0>(stone_b) + get<3>(stone_b), get<1>(stone_b) + get<4>(stone_b));
+
+        const auto a_1 = get<1>(p_2) - get<1>(p_1);
+        const auto b_1 = get<0>(p_1) - get<0>(p_2);
+        const auto c_1 = a_1 * (get<0>(p_1)) + b_1 * (get<1>(p_1));
+
+        const auto a_2 = get<1>(p_4) - get<1>(p_3);
+        const auto b_2 = get<0>(p_3) - get<0>(p_4);
+        const auto c_2 = a_2 * (get<0>(p_3)) + b_2 * (get<1>(p_3));
+
+        const auto determinant = a_1 * b_2 - a_2 * b_1;
+
+        if ( determinant == 0 ) {
+                return false;
+        }
+
+        auto p_x = (b_2 * c_1 - b_1 * c_2) / determinant;
+        auto p_y = (a_1 * c_2 - a_2 * c_1) / determinant;
+
+        cross_point = make_tuple(p_x, p_y);
+
+        return true;
+}
+
+void
+part1(const puzzle_type& input)
+{
+        const auto in_range = [](point_type point) -> bool {
+                static const auto lower_limit = 200000000000000.0;
+                static const auto upper_limit = 400000000000000.0;
+
+                const auto [x, y] = point;
+
+                return x > lower_limit && x < upper_limit && y > lower_limit && y < upper_limit;
+        };
+
+        const auto in_future = [](line_type stone, point_type point) -> bool {
+                const auto sgn_stone = get_direction(stone);
+                const auto sgn_point = get_direction(stone, point);
+
+                return sgn_stone == sgn_point;
+        };
+
+        long sum = 0;
+        for ( size_t idx = 0; idx != input.size(); ++idx ) {
+                const auto& stone_a = input[idx];
+
+                for ( size_t idx2 = idx + 1; idx2 < input.size(); ++idx2 ) {
+                        const auto& stone_b = input[idx2];
+
+                        point_type cross_point;
+                        if ( lint(stone_a, stone_b, cross_point) && in_range(cross_point) && in_future(stone_a, cross_point) && in_future(stone_b, cross_point) ) {
+                                ++sum;
+                        }
+                }
+        }
+        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);
+}