aoc 2024, day 13, lösung mit z3

1 files changed, 110 insertions, 0 deletions

diff --git a/2024/src/day13-z3.cpp b/2024/src/day13-z3.cpp
new file mode 100644
index 0000000..4f2755a
--- /dev/null
+++ b/2024/src/day13-z3.cpp
@@ -0,0 +1,110 @@
+#include <array>
+#include <fstream>
+#include <iostream>
+#include <iterator>
+#include <numeric>
+#include <regex>
+#include <vector>
+#include <z3++.h>
+using namespace std;
+
+vector<string>
+split(string_view line, string_view delimiter)
+{
+        string::size_type pos_start = 0;
+        string::size_type pos_end   = 0;
+
+        vector<string> res;
+        while ( (pos_end = line.find(delimiter, pos_start)) != string::npos ) {
+                res.emplace_back(line.substr(pos_start, pos_end - pos_start));
+
+                pos_start = pos_end + delimiter.length();
+        }
+        if ( pos_start != line.size() ) {
+                res.emplace_back(line.substr(pos_start));
+        }
+        return res;
+}
+
+vector<array<long, 6>>
+read_file(string_view filename)
+{
+        static const regex pattern{ R"((\d+).*\+(\d+).*\+(\d+).*\+(\d+).*=(\d+).*=(\d+))" };
+
+        fstream input{ filename };
+        string  content{ istreambuf_iterator<char>{ input }, {} };
+
+        auto parts = split(content, "\n\n");
+
+        vector<array<long, 6>> data;
+        for ( auto part: parts ) {
+                part.erase(std::remove(part.begin(), part.end(), '\n'), part.cend());
+
+                smatch matches;
+                if ( regex_search(part, matches, pattern) ) {
+                        data.push_back({ stoi(matches[1]),
+                                         stoi(matches[2]),
+                                         stoi(matches[3]),
+                                         stoi(matches[4]),
+                                         stoi(matches[5]),
+                                         stoi(matches[6]) });
+                }
+        }
+
+        return data;
+}
+
+long
+test_z3(const array<long, 6>& machine, long offset)
+{
+        auto config  = z3::config();
+        auto context = z3::context(config);
+        auto solver  = z3::solver(context);
+
+        const auto i = context.int_const("i");
+        const auto j = context.int_const("j");
+
+        solver.add(i > 0);
+        solver.add(j > 0);
+
+        const auto button_a_x = context.int_val(machine[0]);
+        const auto button_a_y = context.int_val(machine[1]);
+        const auto button_b_x = context.int_val(machine[2]);
+        const auto button_b_y = context.int_val(machine[3]);
+        const auto price_x    = context.int_val(machine[4] + offset);
+        const auto price_y    = context.int_val(machine[5] + offset);
+
+        solver.add(i * button_a_x + j * button_b_x == price_x);
+        solver.add(i * button_a_y + j * button_b_y == price_y);
+
+        if ( solver.check() == z3::sat ) {
+                auto model = solver.get_model();
+                return model.eval(i).as_int64() * 3 + model.eval(j).as_int64();
+        }
+
+        return 0;
+}
+
+void
+part1(const vector<array<long, 6>>& machines)
+{
+        cout << accumulate(machines.begin(), machines.end(), 0L, [](auto init, const auto& machine) {
+                return init + test_z3(machine, 0);
+        }) << endl;
+}
+
+void
+part2(const vector<array<long, 6>>& machines)
+{
+        cout << accumulate(machines.begin(), machines.end(), 0L, [](auto init, const auto& machine) {
+                return init + test_z3(machine, 10000000000000);
+        }) << endl;
+}
+
+int
+main()
+{
+        auto data = read_file("data/day13.txt");
+        part1(data);
+        part2(data);
+}