It was nice to get an easy one after the past two days. The only hard thing was that gnatprove was either hanging or crashing, and I guessed that it didn’t like all the nested-nested-nested loops. I rewrote it so I generated an array of all coordinates and looped through that instead of the nested loops and I was able to get gnatprove to finish.
In case anyone needs help with part B:
I created a cube of booleans indicating whether an empty cube was connected to the outside, initialized the outer faces of the cube to true if they were empty, and then kept looping over the empty cubes that weren’t outside changing them to outside if they were adjacent to an empty one that was outside. The loop quits if it gets through all the coordinates and nothing changed.
Yeah, this is my third Advent of Code, and it’s pretty common to get a couple of murderous puzzles, followed by one that seems easier than even the first few!
I enjoyed this one. I thought about doing it in SPARK, but it didn’t like my use of Ada.Containers.Unbounded_Synchronized_Queues, so I gave up on that.
My approach to part 2 seems to have been different from yours. I performed a breadth-first search from a known exterior point (namely, (-1,-1,-1)) to determine which points are on the exterior, and that allows me to determine which points are on the interior.
I think that’s not that different from my approach …
… since what I described is basically a breadth-first search, starting from the outside faces of a cube and moving in one layer at a time. I found that three-dimensional arrays of booleans were mostly all I needed data-structure wise, except that to make gnatprove happy I also had to make 1-dimensional array containing all the possible x-y-z triplets.
I think this is my third time doing AoC where I have stuck with it past the first few. Two years ago I did it in Common Lisp, and last year in a language I had created that was basically like ML with a Scheme-like syntax. That one was interpreted, so some of the really complex problems would take a long time to run.
Something that may happen with loops is that GNATprove unrolls them when you don’t provide a loop invariant and the number of iterations is bounded by a small number (20 currently). That may cause memory exhaustion on nested loops, as the unrolled program becomes huge. You can try --no-loop-unrolling to prevent unrolling completely. Otherwise, feel free to open an issue on SPARK GitHub repo!