Part 2 requires some mathematics, or at least that’s what got me to solve it quite quickly I did one other thing, too.
It’s probably not necessary, but I clipped the viewing area every now and then. That is, once the cavern grew too large, I removed the bottom n rows, where n was determined by checking the maximum “height” in each column.
The number of jets is prime, or at least mine was. That’s the trick to solving it. Every time the program cycled through the list of jets, I looked at the number of figures completed, along with the height of the tower, and it becomes very obvious very quickly that these sequences of numbers follow a very regular pattern. From there is was… well, not as straightforward to complete as it should have been. I really should have slept first.
Using both 1 and 2, I printed the cavern every time the jets cycled (or rather the top of the cavern) and indeed, it was the same every time, confirming my hopes.
The solution I uploaded for part 2 will probably not work on the example program, because the example’s sequences aren’t quite as well-behaved as the actual puzzle, which made the problem a little harder. But the same technique really does work!
It took me way longer than it should have because I didn’t try enough possibilities of something, but I did finally get part B solved and am now working to get gnatprove happy. I knew as I was writing it that I would have to "pay the piper’ eventually with regard to overflow checks. I ended up having to use --level=2 to get it to prove one long integer multiply.
For part b:
First, definitely reduce the board occasionally. The example data doesn’t actually ever produce a row where all the cells are filled, but if you just look for a chain of filled cells where adjacent cells only differ by one in the Y direction, you can then reduce the board up to the bottom of that chain.
Now, think of the number of jets times the number of shapes as a cycle. Then, is there a point at the beginning of a cycle where the board has been in that position before? Specifically, if you start at the highest point and measure the distance to the topmost filled cell in each column, has that occurred before? If so, the gap between the two occurrences is will continually repeat, so you can calculate how many repetitions you need to do to get close to the number of rocks, and then run through a little more to get to the exact number of rocks. My problem was that I was only checking 100 cycles for a repeat, when the actual cycle length was well over 300. It would eventually find a cycle because just because 100 and the actual number were relatively prime, but then I could never get the exact answer.