From 368c506bc365162cd22f4001ab729ee3df110b79 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Fri, 29 Nov 2024 22:31:49 +0100 Subject: Minor optimization of day 14 part 2. The previous code kept using the Part2Memory even after a cycle had been found. While this didn't break anything, it's a waste of CPU time. --- Day14.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'Day14.lean') diff --git a/Day14.lean b/Day14.lean index d0acf6b..ad87e68 100644 --- a/Day14.lean +++ b/Day14.lean @@ -230,6 +230,14 @@ structure Part2Memory where recordedPanels : Std.HashMap ControlPanel Nat deriving Inhabited +/-- Helper for runCycles. No point in keeping a memory once we have found a cycle. -/ +private def runCycles_bruteForce (cycleCount : Nat) (controlPanel : ControlPanel) : ControlPanel := + match cycleCount with + | 0 => controlPanel + | p+1 => + let r := cycle controlPanel + runCycles_bruteForce p r + private def runCycles (cycleCount : Nat) (controlPanel : ControlPanel) : StateM (Part2Memory) ControlPanel := match cycleCount with | 0 => pure controlPanel @@ -245,15 +253,11 @@ private def runCycles (cycleCount : Nat) (controlPanel : ControlPanel) : StateM if let some previousCount := maybePreviousCount then let period := previousCount - p let remaining := p % period - runCycles remaining r + pure $ runCycles_bruteForce remaining r else runCycles p r else runCycles p r -termination_by cycleCount -decreasing_by - exact Nat.lt_succ_of_le $ Nat.mod_le _ _ - exact Nat.le_refl _ def part2 (input : ControlPanel) : Nat := let r := StateT.run' (runCycles 1000000000 input) Inhabited.default -- cgit v1.2.3