[2024][ruby][13.x] refactored
diff --git a/2024/ruby/day_13.rb b/2024/ruby/day_13.rb
index 85a795f..1784773 100644
--- a/2024/ruby/day_13.rb
+++ b/2024/ruby/day_13.rb
@@ -5,59 +5,33 @@ gemfile do
gem "z3"
end
+require "z3"
+
input = DATA.read
machines = input.split("\n\n")
- .map {|machine| machine.scan(/\d+/).map(&:to_i) }
-
-wins = ->(machine) {
- ax, ay = machine[0,2]
- bx, by = machine[2,2]
- cx, cy = machine[4,2]
-
- (0..cx/ax).filter_map {|a|
- b = (cx - a * ax) / bx.to_f
- if a * ax + b.to_i * bx == cx && a * ay + b.to_i * by == cy
- [a, b.to_i]
- else
- nil
- end
- }.sort_by {|a,b| a + b }
-}
-
-pp machines.map { wins[_1].first }.compact.sum { 3 * _1 + _2 }
-
-require "z3"
-
-machines.each do |machine|
- machine[4,2] = machine[4,2].map { _1 + 10_000_000_000_000 }
-end
+ .map {|machine| machine.scan(/\d+/).map(&:to_i).each_slice(2).to_a }
def wins(machine)
- return enum_for(__method__, machine) unless block_given?
-
- ax, ay = machine[0,2]
- bx, by = machine[2,2]
- cx, cy = machine[4,2]
-
- solutions = []
- loop do
- a = Z3.Int("a")
- b = Z3.Int("b")
- solver = Z3::Solver.new
- solver.assert cx == a*ax + b*bx
- solver.assert cy == a*ay + b*by
- solutions.each do |a_s, b_s|
- solver.assert a != a_s
- end
- return unless solver.satisfiable?
+ a = Z3.Int("a")
+ b = Z3.Int("b")
+ solver = Z3::Solver.new
+ machine.transpose.each do |a_, b_, c|
+ solver.assert a*a_ + b*b_ == c
+ end
+ if solver.satisfiable?
model = solver.model
- solutions << [model[a].to_i, model[b].to_i]
- yield solutions.last
+ [a, b].map { model[_1].to_i }
+ else
+ nil
end
end
-pp machines.flat_map {|m| wins(m).sort_by { _1 + _2 } }.reject(&:empty?).sum { 3 * _1 + _2 }
+pp machines.map { wins(_1) }.compact.sum { 3 * _1 + _2 }
+
+pp machines
+ .map {|a,b,c| [a,b,c.map { _1 + 10_000_000_000_000 }] }
+ .map { wins(_1) }.compact.sum { 3 * _1 + _2 }
__END__