1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
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);
}
|
