From df89ce46eebb355acf353600b148de52641f060c Mon Sep 17 00:00:00 2001
From: Thomas Schmucker <ts@its1.de>
Date: Sat, 14 Dec 2024 14:28:00 +0100
Subject: aoc 2024, day 13, lösung mit z3
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 2024/src/day13-z3.cpp | 110 ++++++++++++++++++++++++++++++++++++++++++++++++++
 makefile              |   3 ++
 2 files changed, 113 insertions(+)
 create mode 100644 2024/src/day13-z3.cpp

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);
+}
diff --git a/makefile b/makefile
index 8d9d8bc..928c1bb 100644
--- a/makefile
+++ b/makefile
@@ -35,6 +35,9 @@ all: $(patsubst 2015/src/%.cpp,2015/bin/%,$(wildcard 2015/src/*.cpp)) \
 2024/bin/%: 2024/src/%.cpp | 2024/bin
 	c++ $(CPPFLAGS) $^ -o $@
 
+2024/bin/day13-z3: 2024/src/day13-z3.cpp | 2024/bin
+	c++ $(CPPFLAGS) $^ -L/usr/local/lib -lz3 -o $@
+
 clean:
 	rm -rf 2015/bin 2020/bin 2022/bin 2023/bin 2024/bin
 
-- 
cgit v1.3