[SMT-LIB] Standardizing extraction of arrays

[Tinelli, Cesare]

Hi Levent,

You raise a good point. We, the SMT-LIB coordinators, are aware of this problem and have been discussing possible solutions. The issue is fairly tricky to address well and might require the definition of a new theory of arrays. I'll send a more detailed reply once we are done with the second (and hopefully finally draft) of Version 2.5 of SMT-LIB standard. That is almost ready and I expect we will circulate it in the next few days.


Cesare


On 9 Mar 2015, at 00:45, Levent Erkok <erkokl at gmail.com> wrote:

> 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.
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib