[SMT-LIB] Standardizing extraction of arrays

[Levent Erkok]

Dear SMT-Lib community:

A common question that comes up in interfacing with SMT-Solvers is that of
extracting values of arrays. As far as I know, SMTLib2 has not specified
any means of bulk-extraction of array values; though one can use get-value
to extract individual elements. Unfortunately the latter is not very useful
when building tools on top of these solvers as the driving program usually
doesn't know which elements are relevant for the model at hand.

Needless to say, almost all solvers do support bulk array models, and they
print the models in somewhat similar yet in their own idiosyncratic ways.
To test, I created a simple benchmark and fed it to different solvers, to
get various responses. (The benchmark itself is not particularly
interesting, so I'm skipping that.) In each case the call was "(get-value
(array_0))"

CVC4:
((array_0 (__array_store_all__ (Array (_ BitVec 8) (_ BitVec 8)) (_ bv0
8))))

MathSat:
( (array_0 @0) )

Z3:
((array_0 ((as const (Array (_ BitVec 8) (_ BitVec 8))) #xfc)))

Yices:
(function array_0
(type (-> (bitvector 8) (bitvector 8)))
(= (array_0 0b00000011) 0b00000000)
(default 0b00000011))

Boolector:
((((array_0 #b00000011) #b10000010)))

If one squints sufficiently enough, the tools are all giving the necessary
information in a nice format of their own choosing to an extent; except for
MathSat which seems to refer to an internal node. (My MathSat version dates
back to 2013, so it might've changed in the mean time.)

I personally like the way Yices-1 series printed the array values, as it
showed the minimum set with a default for everything else. Perhaps a
variant of that can be standardized.

I think it'd be beneficial for the community to standardize on the
bulk-array model printing. There're several questions of interest, for
instance how does one avoid printing voluminous output if the index happens
to be a 64-bit integer and all the entries are relevant for the model. But
we can start simple and fill in as specific needs arise.

I'd be happy to participate in discussions if there's enough interest;
though such work should probably be led by our friends in the academia and
of course the authors of the solvers themselves.

-Levent.