Gracefully print counterexamples involving SMT arrays defined as function mappings

[RyanGlScott]

Generally speaking, SMT solvers produce models of SMT arrays in one of two ways when producing counterexamples:

1. A constant array where all indices map to a particular value, but with elements at particular indices updated to other values.
2. An array defined as a total function from index values to element values.

SAW is capable of printing SMT arrays of type (1) (e.g., [<default> := False]), but it is not capable of printing SMT arrays of type (2). Nor is the purpose of this issue to propose that SAW be able to print type-(2) arrays. Rather, the issue is that SAW's behavior when printing type-(2) arrays is currently rather poor. At present, attempting to do so will cause SAW to fail outright with a full-blown error message. This can be seen in the following example:

// test.saw
import "Array.cry";

prove_print w4
  {{ \(a : Array Integer Bool) (n : Integer) ->
     arrayLookup a n /\ ~(arrayLookup a (n + 1)) }};

With a recent SAW nightly, this will fail thusly:

[16:34:35.255] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[16:34:35.338] Stack trace:
"prove_print" (/home/ryanscott/Documents/Hacking/SAW/test.saw:4:1-4:12)
"w4" (/home/ryanscott/Documents/Hacking/SAW/test.saw:4:13-4:15)
Unsupported FOV Array (values only available by lookup)

(The "Unsupported FOV Array (values only available by lookup)" part of the error message is a very dense way of saying that it encountered a type-(2) SMT array.)

Really, we ought to gracefully handle these situations by printing these arrays as something opaque. This is more or less than SAW 1.2 and earlier do:

[16:34:46.127] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[16:34:46.222] Stack trace:
"prove_print" (/home/ryanscott/Documents/Hacking/SAW/test.saw:4:1-4:12)
prove: 1 unsolved subgoal(s)
Invalid: [a = FOTArray FOTInt FOTBit, n = 0]

The output "FOTArray FOTInt FOTBit" is rather obtuse, so we should consider something a bit prettier to print here, e.g., <array Integer Bit>. While we can't print out the full contents of a type-(2) array, we should at least print it out opaquely in the counterexample without causing the rest of SAW to fall over.

[sauclovian-g]

I broke it, I'll fix it