[SMT-LIB] Standardizing extraction of arrays

[Alberto Griggio]

Hi all,

> 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.

I agree, there should be a way to extract the information. Calling
get-value repeatedly is not enough, if you don't know which indices are
relevant.

>
> 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.

[...]

> MathSat:
> ( (array_0 @0) )

[...]

> (My MathSat version dates back to 2013, so it might've changed in the
> mean time.)

FWIW, yes, it has. Now MathSAT (since version 5.3.0) will print
something like:

   ( (array_0 (store ((as const (Array (_ BitVec 8) (_ BitVec 8))) (_ 
bv0 8)) (_ bv64 8) (_ bv128 8))) )

I.e., the model is represented as a sequence of writes over a base
constant array.


Alberto